Tamarin Prover

Main content

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

See the new project webpage for up-to-date details at:




The manual is available now as PDF or HTML!


 Research papers and theses on Tamarin up to 2016, see above link for newer results





The Tamarin prover is open-source software. Its code and issue tracker are available at



Installation instructions are in the Manual.



Page URL: http://www.infsec.ethz.ch/research/software/tamarin.html
© 2017 Eidgenössische Technische Hochschule Zürich