The scyther-proof security protocol verification tool

external page scyther-proof implements a proof-generating version of the algorithm underlying the Scyther security protocol verification tool. The resulting proofs can be visualized and machine-checked using our security protocol verification theory formalized in external page Isabelle/HOL. Note that this theory is of independent interest, as it allows for both the efficient interactive construction as well as the automatic generation of machine-checked protocol security proofs. The paper "Strong Invariants for the Efficient Construction of Protocol Security Proofs" documenting this theory and its external page tool support was presented at external page CSF 2010. A journal version of this paper will appear in the Journal of Computer Security.

Verification of our fixes to the ISO/IEC 9798 standard

We also used the corresponding external page scyther-proof tool to provide machine-checked proofs of repaired versions of the authentication protocols from the ISO/IEC 9798 standard.  

Authors

Simon Meier, Cas Cremers, and David Basin

Homepage

See our homepage for additional information and downloads.