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 combined with a user-defined subterm-convergent rewriting theory.

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, Ralf Sasse

Documentation

The Tamarin user manual is availabe here.
We also have a GitHub repository for other teaching materials, such as tutorials.

Research Papers and Theses

Papers on Tamarin and its theory

Tamarin Extensions

Papers using Tamarin

Screenshots

Tamarin introduction page

Introduction page

Tamarin introduction page

Overview

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

Installation instructions are in the manual.