User-Guided Verification of Security Protocols via Sound Animation
Kangfeng Ye, Roberto Metere, Poonam Yadav

TL;DR
This paper introduces a user-guided, sound animation tool for security protocol verification that integrates symbolic analysis into the design process, making security evaluation more accessible to protocol designers.
Contribution
It presents a novel approach that compiles security protocols into executable animators using a formal, mechanized method in Isabelle/HOL, bridging the gap between complex verification tools and informal design.
Findings
Successfully implemented symbolic analysis with CSP and ITrees
Demonstrated the tool on Diffie-Hellman and Needham-Schroeder protocols
Revealed attack mechanics and verified protocol corrections
Abstract
Current formal verification of security protocols relies on specialized researchers and complex tools, inaccessible to protocol designers who informally evaluate their work with emulators. This paper addresses this gap by embedding symbolic analysis into the design process. Our approach implements the Dolev-Yao attack model using a variant of CSP based on Interaction Trees (ITrees) to compile protocols into animators -- executable programs that designers can use for debugging and inspection. To guarantee the soundness of our compilation, we mechanised our approach in the theorem prover Isabelle/HOL. As traditionally done with symbolic tools, we refer to the Diffie-Hellman key exchange and the Needham-Schroeder public-key protocol (and Lowe's patched variant). We demonstrate how our animator can easily reveal the mechanics of attacks and verify corrections. This work facilitates security…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsUser Authentication and Security Systems
