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.

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

  • POST 2017 paper [PDF] : the paper presented at POST.
  • CSF 2016 paper [PDF] : the paper presented at CSF.
  • 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].
  • Stettler's bachelor thesis [PDF]: TLS1.3,v13 analysis and model for Tamarin [zip].
  • Denzler's bachelor Thesis [PDF]: on how to automate the analysis of communications protocols with human errors.
  • Lanzenberger's bachelor thesis [PDF]: 5G protocols analysis and model for Tamarin [zip].

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.