The scyther-proof security protocol verification tool

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 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 tool support was presented at 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 scyther-proof tool to provide machine-checked proofs of repaired versions of the authentication protocols from the ISO/IEC 9798 standard. The following two files provide the original protocol models to be used with the Scyther security protocol analysis tool and the scyther-proof tool together with the repaired and provenly correct protocol models.

Authors

Simon Meier, Cas Cremers, and David Basin

Homepage

See our homepage for additional information and downloads.

 
Page URL: http://www.infsec.ethz.ch/research/software/scyther-proof.html
28.08.2015
© 2015 Eidgenössische Technische Hochschule Zürich