Topology-Driven Symbolic Verification of Post-Quantum Migration Paths Using Tamarin Prover
Muhammed Sihan Haroon
The transition from classical public-key cryptography to post-quantum
cryptography introduces protocol-level risks that are not fully addressed
by configuration review, performance benchmarking, or endpoint reachability
testing. Under the current abstraction, deployments may appear operationally
correct while still permitting secrecy, authentication, or forward-secrecy
violations at the protocol level. This paper presents a topology-driven
symbolic verification workflow that translates distribut