Tamarin Prover

The Tamarin prover is a security protocol verification tool that supports both falsification (attack finding) and unbounded verification (proving) in the symbolic model. Security protocols are specified as multiset rewriting systems and analyzed with respect to temporal first-order properties.

Tamarin has been successfully used to analyze and support the development of modern security protocols [1,2], including TLS 1.3 [3,4], 5G‑AKA [5,6], Noise [7], EMV (Chip-and-pin) [8], and Apple iMessage [9].

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 available here.
We also have a GitHub repository for other teaching materials, such as tutorials.
For general information, also see the Wikipedia article.


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. Note that the issue tracker is only intended for tool issues, i.e., reporting potential bugs, and not for asking questions.

Tamarin's low-volume mailing list/forum for announcements, asking questions, and discussion is https://groups.google.com/group/tamarin-prover. The mailing list can be used if you have questions related to the theory, modeling, or using the tool.

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.

Research Papers and Theses

Overview Papers on Tamarin

Papers on Tamarin and its theory

Tamarin Extensions

Papers using Tamarin