Tamarin Prover

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

Documentation

The Tamarin user manual is availabe here.

Research Papers and Theses

  • 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].

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.

Installation

Installation instructions are in the manual.