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
Current maintainers: Cas Cremers, Jannik Dreier, Ralf Sasse
The Tamarin user manual is availabe here.
Research Papers and Theses
- CSF 2016 paper [PDF] : the paper presented at CSF.
- 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
For other inquiries (not bug reports!) you can reach the current maintainers of the Tamarin Prover via mail at
Installation instructions are in the manual.