Tamarin Prover

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.
For general information, also see the Wikipedia article.

Research Papers and Theses

Papers on Tamarin and its theory

• CSF 2018 paper [PDF]: the paper presented at CSF, about adding support for Exclusive-Or: "Automated Unbounded Verification of Stateful Cryptographic Protocols with Exclusive OR", by Jannik Dreier, Lucca Hirschi, Saša Radomirović, Ralf Sasse.
• SIGLOG Newsletter 2017 paper [PDF]: the paper published in the SIGLOG Newsletter October 2017, presenting an overview of Tamarin and its features: "Symbolically Analyzing Security Protocols using TAMARIN", by David Basin, Cas Cremers, Jannik Dreier, Ralf Sasse.
• POST 2017 paper [PDF]: the paper presented at POST, about allowing user-defined equational theories to be non-subterm-convergent: "Beyond Subterm-Convergent Equational Theories in Automated Verification of Stateful Protocols", by Jannik Dreier, Charles Duménil, Steve Kremer, Ralf Sasse.
• CCS 2015 paper [PDF]: the paper presented at CCS, also available as Extended Version with proofs; about observational equivalence for Tamarin: "Automated Symbolic Proofs of Observational Equivalence", by David Basin, Jannik Dreier, Ralf Sasse.
• S&P 2014 paper [PDF]: the paper presented at S&P, about group protocols and bilinear pairing extensions: "Automated Verification of Group Key Agreement Protocols", by Benedikt Schmidt, Ralf Sasse, Cas Cremers, David Basin.
• CAV 2013 paper [PDF]: the paper presented at CAV, presenting the tool in more detail: "The TAMARIN Prover for the Symbolic Analysis of Security Protocols", by Simon Meier, Benedikt Schmidt, Cas Cremers, David Basin.
• CSF 2012 paper [PDF]: the paper presented at CSF, also available as extended version [PDF]: extended version that contains the full proofs and additional examples; original paper introducing Tamarin Prover: "Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties", by Benedikt Schmidt, Simon Meier, Cas Cremers, David Basin.
• 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.

Tamarin Extensions

• "Distance-Bounding Protocols: Verification without Time and Location" [PDF], by Sjouke Mauw, Zach Smith, Jorge Toro-Pozo, Rolando Trujillo-Rasua, presented at S&P 2018.
• "A Novel Approach for Reasoning about Liveness in Cryptographic Protocols and its Application to Fair Exchange" [PDF], by Michael Backes, Jannik Dreier, Steve Kremer, Robert Künnemann, presented at EuroS&P 2017.
• "Modeling Human Errors in Security Protocols" [PDF], by David Basin, Saša Radomirović, Lara Schmid, presented at CSF 2016.
• "Alice and Bob Meet Equational Theories" [PDF], by David Basin, Michel Keller, Saša Radomirović, Ralf Sasse, paper presented at Logic, Rewriting, and Concurrency 2015 - Festschrift Symposium in Honor of José Meseguer.
• "Automated analysis of security protocols with global state" [PDF], by Steve Kremer, Robert Künnemann, paper presented at S&P 2014, also avaible extended journal version at Journal of Computer Security: [PDF].
• Andrina Denzler's bachelor Thesis [PDF]: on how to automate the analysis of communications protocols with human errors.
• Dorela Kozmai's bachelor Thesis [PDF]: on how to translate Tamarin specifications into Alice&Bob protocol notation, with implementation available [zip].
• Lara Schmid's master Thesis [PDF]: on how one can model human errors in secure communication protocols.
• Michel Keller's bachelor thesis [PDF]: about translating Alice&Bob protocol notation into Tamarin's input language, with implementation available [tar.gz].

Papers using Tamarin

• "Alethea: A Provably Secure Random Sample Voting Protocol" [PDF], by David Basin, Saša Radomirović, Lara Schmid, presented at CSF 2018.
• "A Comprehensive Symbolic Analysis of TLS 1.3" [PDF], by Cas Cremers, Marko Horvat, Jonathan Hoyland, Sam Scott, Thyla van der Merwe, presented at CCS 2017.
• "Formal Analysis of Combinations of Secure Protocols" [PDF], by Elliott Blot, Jannik Dreier, Pascal Lafourcade, presented at FPS 2017.
• "Towards a Mechanized Proof of Selene Receipt-Freeness and Vote-Privacy" [PDF], by Alessandro Bruni, Eva Drewsen, Carsten Schürmann, presented at E-Vote-ID 2017.
• "Secure Authentication in the Grid: A formal analysis of DNP3: SAv5" [PDF], by Cas Cremers, Martin Dehnel-Wild, Kevin Milner, presented at ESORICS 2017.
• "Formal Analysis of V2X Revocation Protocols" [PDF] [Source], by Jorden Whitefield, Liqun Chen, Frank Kargl, Andrew Paverd, Steve Schneider, Helen Treharne, Stephan Wesemeyer, presented at STM 2017.
• "Formally Verifying Flow Integrity Properties in Industrial Systems" [PDF], by Jannik Dreier, Maxime Puys, Marie-Laure Potet, Pascal Lafourcade, Jean-Louis Roch, presented at SECRYPT 2017.
• "Designing and proving an EMV-compliant payment protocol for mobile devices" [PDF], by Véronique Cortier, Alicia Filipiak, Saïd Gharout, Jacques Traoré, presented at EuroS&P 2017.
• "Automated Analysis and Verification of TLS 1.3: 0-RTT, Resumption and Delayed Authentication" [PDF], by Cas Cremers, Marko Horvat, Sam Scott, Thyla van der Merwe, presented at S&P 2016.
• "Automated Backward Analysis of PKCS#11 v2.20" [PDF], by Robert Künnemann, presented at POST 2105.
• "ARPKI: Attack Resilient Public-Key Infrastructure" [PDF], by David Basin, Cas Cremers, Tiffany Hyun-Jin Kim, Adrian Perrig, Ralf Sasse, Pawel Szalachowski, presented at CCS 2014, also available extended journal version at Transactions on Dependable and Secure Computing: [PDF].
• David Lanzenberger's bachelor thesis [PDF]: 5G protocols analysis and model for Tamarin [zip].
• Vincent Stettler's bachelor thesis [PDF]: TLS1.3,v13 analysis and model for Tamarin [zip].

Screenshots

Introduction page

Overview

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.