Security protocol analysis tools
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 |