We have developed several tools for the symbolic analysis of security protocols.

The below table provides a high-level overview of their differentiating features.

The executive summary is: for standard analysis with respect to various adversary models, or learning about security protocols, use Scyther. If you want machine-checked proofs, use scyther-proof. For advanced analysis and cutting-edge features, use Tamarin.

Scyther scyther-proof Tamarin
Main reference CCS'08, CAV'08 CSF 2010 CSF 2012 (extended version), CAV 2013, S&P 2014
Example applications Compromising adversaries, protocol security hierarchies, IKE, ISO/IEC 9798 (authentication), ISO/IEC 11770 (key establishment) ISO/IEC 9798 Naxos, UM, Signed Diffie-Hellman, group protocols, APIs/protocols with global state, ARPKI, TLS 1.3
Unbounded verification Yes Yes Yes
Attack finding and visualisation Yes Yes
Classical properties
(secrecy, agreement, aliveness, synchronisation) 		Yes Yes Yes
Complete characterization Yes Yes
Property specification using a
guarded fragment of first-order logic 		Yes
Protocol specification Linear role scripts Linear role scripts Multiset Rewriting (branching, loops)
Support for APIs/protocols with global state Yes
Cryptographic message model Free term algebra Free term algebra Diffie-Hellman; bilinear pairing; AC operators; user-defined subterm-convergent rewrite theory; beyond subtem-convergent for e.g., blind signatures
Dynamic corruption Yes Yes Yes
Compromising adversaries Yes Yes
User-specified adversaries Yes (e.g., eCK, eCK-PFS)
Generating machine-checked proofs Yes (via Isabelle/HOL)
Generating protocol security hierarchies Yes
Support for use in teaching Book and exercises Manual and tutorial materials
Proof visualisation Yes Yes
Interactive proof construction and exploration Yes
Source files Available on Github Available on Github Available on Github
visit website
download, report issues or contribute 		visit website visit website
report issues or contribute