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
Research papers and theses on Tamarin
- CCS 2015 paper [PDF] (PDF, 373 KB) : the paper presented at CCS, also available as Extended Version with proofs [PDF].
- S&P 2014 paper [PDF] (PDF, 939 KB) : the paper presented at S&P
- CSF 2012 paper [PDF] (PDF, 1009 KB) : the paper presented at CSF
- Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties (Extended Version 1, April 24th, 2012 [PDF] (PDF, 1.3 MB)): extended version of the above paper that contains the full proofs and additional examples.
- Meier's PhD thesis : provides a detailed explanation of the theory and implementation of Tamarin including inductive invariants and type assertions.
- Schmidt's PhD thesis: provides a detailed explanation of the theory and application of Tamarin including the reasoning about Diffie-Hellman exponentiation and bilinear pairing.
- Staub's bachelor's thesis [PDF]: about the implementation of the original version of Tamarin's GUI.
- Work on Alice&Bob input language for Tamarin.
- Stettler's bachelor's thesis [PDF] (PDF, 1.9 MB): TLS1.3,v13 analysis and model for Tamarin [zip] (ZIP, 6.3 MB).