The scyther-proof security protocol verification tool

external pagescyther-proofcall_made 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 pageIsabelle/HOLcall_made. 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 pagetool supportcall_made was presented at external pageCSF 2010call_made. 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 pagescyther-proofcall_made 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.