Institute of Information Security

The scyther-proof security protocol verification tool

Zurich Information Security Center

We are affiliated with the Zurich Information Security Center (ZISC)

Events & News

  • Best paper award

    Paper: Formal Analysis of Electronic Exams
    Conference: SECRYPT'14 in Vienna
    Authors: Jannik Dreier, Rosario Guistolisi, Ali Kassem, Pascal Lafourcade, Gabriele Lenzini, and Peter Y. A. Ryan

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.


Wichtiger Hinweis:
Diese Website wird in älteren Versionen von Netscape ohne graphische Elemente dargestellt. Die Funktionalität der Website ist aber trotzdem gewährleistet. Wenn Sie diese Website regelmässig benutzen, empfehlen wir Ihnen, auf Ihrem Computer einen aktuellen Browser zu installieren. Weitere Informationen finden Sie auf
folgender Seite.

Important Note:
The content in this site is accessible to any browser or Internet device, however, some graphics will display correctly only in the newer versions of Netscape. To get the most out of our site we suggest you upgrade to a newer browser.
More information

© 2014 ETH Zurich | Imprint | Disclaimer | 14 July 2012