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.
Simon Meier, Cas Cremers, and David Basin
See our homepage for additional information and downloads.