The Tamarin Prover

Tamarin has been successfully used to analyze and support the development of modern security protocols [PDF, PDF], including TLS 1.3 [PDF, PDF], 5G‑AKA [PDF, PDF], Noise [PDF], EMV (Chip-and-pin) [PDF], and Apple iMessage [Apple blog].

Extensive graphical user interface

Automatically find attacks or proofs. Attack graphs show exactly how a property can be violated.

Interactive proof construction or attack finding

Construct partial proofs, or guide proof/attack search manually. For complex protocols, users can inspect partial proofs and write auxiliary lemmas.

Command-line interface

Perform protocol analysis in batch mode using the commandline.

Model protocol state machines

Tamarin's core modeling mechanism uses multiset rewrite rules. Alternatively, specify protocols using a process calculus, which are automatically translated into rewrite rules.

Specify security properties

Security properties can be specified using a first-order logic with quantification over timepoints.

Want to learn more? Consult Tamarin's extensive documentation.