Tamarin

The Tamarin prover is a state-of-the-art automated symbolic cryptographic protocol verification tool. It supports both verification and falsification (attack-finding) of security protocols. The tool has helped improve standards and other proposed protocols before deployment by finding attacks, and then proving absence of those attacks after fixes are applied. The case studies it has been used for include the TLS v1.3 standard, the Attack-Resilient Public Key Infrastructure (ARPKI), NAXOS, YubiKey, group Joux, group Diffie-Hellman (GDH), and identity-based protocols.

More precisely, Tamarin prover analyzes security protocols specified as multiset rewriting systems and supports unbounded verification and falsification with respect to (temporal) first-order properties as well as observational equivalence properties. It uses a message theory that models Diffie-Hellman exponentiation and bilinear pairing, which can be combined with a user-defined convergent rewriting theory with the finite variant property. See http://tamarin-prover.github.io/ for links to documentation, source code, and installation instructions.

Software

The Tamarin prover is open-source software. Its code and issue tracker are available at GitHub. Its low-volume mailing list for announcements and discussion can be found here. We provide an extensive manual for Tamarin.

Publications

David Basin, Sasa Radomirovic, Lara Schmid
Modeling Human Errors in Security Protocols
In Proceedings of the 29th IEEE Computer Security Foundations Symposium (CSF), 2016.

David Basin, Jannik Dreier, Ralf Sasse
Automated Symbolic Proofs of Observational Equivalence
In Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security (CCS), 2015.

David Basin, Cas Cremers, Tiffany Hyun-Jin Kim, Adrian Perrig, Ralf Sasse, and Pawel Szalachowski
ARPKI: Attack Resilient Public-Key Infrastructure
In Proceedings of the ACM SIGSAC Conference on Computer and Communications Security (CCS), 2014.

Benedikt Schmidt, Ralf Sasse, Cas Cremers, David Basin
Automated Verification of Group Key Agreement Protocols
In Proceedings of the 35th IEEE Symposium on Security and Privacy (S&P), 2014

Simon Meier, Benedikt Schmidt, Cas Cremers, David Basin
The TAMARIN Prover for the Symbolic Analysis of Security Protocols (Tool Paper)
In Proceedings of the 25th International Conference on Computer Aided Verification (CAV), 2013.

Benedikt Schmidt, Simon Meier, Cas Cremers, and David Basin
Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties
In Proceedings of the 25th IEEE Computer Security Foundations Symposium (CSF), 2012.