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
Example applications Compromising adversaries, IKE, protocol security hierarchies ISO/IEC 9798 Naxos, UM, Signed Diffie-Hellman
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)
Cryptographic message model Free term algebra Free term algebra Diffie-Hellman & user-defined subterm-convergent rewrite theory
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
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