The Tamarin prover is a security protocol verification tool that
supports both falsification and unbounded verification of security
protocols specified as multiset rewriting systems with respect to
(temporal) first-order properties and a message theory that models
Diffie-Hellman exponentiation combined with a user-defined
subterm-convergent rewriting theory.
Authors: Simon Meier, Benedikt Schmidt
Contributors: Cas Cremers, Cedric Staub
Observational equivalence authors: Jannik Dreier, Ralf Sasse
The Tamarin user manual is availabe here.
Research Papers and Theses
- CCS 2015 paper [PDF] : the paper presented at CCS, also available as Extended Version with proofs.
- S&P 2014 paper [PDF] : the paper presented at S&P.
- CSF 2012 paper [PDF] : the paper presented at CSF.
- Extended version [PDF] : extended version of the above paper that contains the full proofs and additional examples.
- Meier's PhD thesis [PDF]: provides a detailed explanation of the theory and implementation of Tamarin including inductive invariants and type assertions.
- Schmidt's PhD thesis [PDF]: provides a detailed explanation of the theory and application of Tamarin including the reasoning about Diffie-Hellman exponentiation and bilinear pairing.
- Staub's bachelor thesis [PDF]: about the implementation of the original version of Tamarin's GUI.
- Keller's bachelor thesis [PDF]: about translating Alice&Bob protocol notation into Tamarin's input language, with implementation available [tar.gz].
Tamarin Attack Display
Sourcecode and Mailing List
The Tamarin prover is open-source software. Its code and issue tracker
are available at https://github.com/tamarin-prover/tamarin-prover. Its
low-volume mailing list for announcements and discussion is
Installation instructions are in the manual.