Tamarin Prover

The Tamarin prover is a security protocol verification tool that supports both falsification and unbounded verification in the symbolic model. Security protocols are specified as multiset rewriting systems and analysed with respect to (temporal) first-order properties and a message theory that models Diffie-Hellman exponentiation and exclusive-or (XOR), combined with a user-defined rewriting theory that has the Finite Variant Property, which includes subterm-convergent theories.

Get the docs Install Tamarin

About / Core team:

David Basin, Cas Cremers, Jannik Dreier, Simon Meier, Ralf Sasse, Benedikt Schmidt
Tamarin is a collaborative effort: see the manual for a more extensive overview of its development and additional contributors.
Current maintainers: Cas Cremers, Jannik Dreier, Robert Künnemann, Ralf Sasse


The Tamarin user manual is availabe here.
We also have a GitHub repository for other teaching materials, such as tutorials.
For general information, also see the Wikipedia article.

Research Papers and Theses

Papers on Tamarin and its theory

Tamarin Extensions

Papers using Tamarin


Tamarin introduction page

Introduction page

Tamarin introduction page


Tamarin introduction page

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 https://groups.google.com/group/tamarin-prover. For other inquiries (not bug reports!) you can reach the current maintainers of the Tamarin Prover via mail at tamarin-prover-maintainers@googlegroups.com.


Installation instructions are in the manual.