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.

  • iso9798-original-scyther-models_20110513.tar.gz
  • scyther-proof_and_iso-9798-repaired-model-proofs_20110513.tar.gz


Simon Meier, Cas Cremers, and David Basin


See our homepage for additional information and downloads.

Page URL:
© 2015 Eidgenössische Technische Hochschule Zürich