Centres
CISPA Helmholtz Center for Information SecurityContributing organisations
ETH Zurich , Université de Lorraine , University of OxfordKeywords
Formal Verification Cryptographic ProtocolsResearch field
InformationScientific community
Computer Aided Verification, Computer Security, Communication Security, Privacy, Logic and Computation, Formal methodsFunding
Programming Languages
Haskell, JavascriptLicense
GPL-3.0-onlyCosts
freeCite
10.1007/978-3-642-39799-8_48Contact
cremers@cispa.deResources
Tamarin prover in a nutshell
The Tamarin prover is a tool for the symbolic modelling and analysis of security protocols. It takes as input a security protocol model, specifying the actions taken by agents running the protocol in different roles (e.g., the protocol initiator, the responder, and the trusted key server), a specification of the adversary, and a specification of the protocol’s desired properties. Tamarin can then be used to automatically construct a proof that, even when arbitrarily many instances of the protocol’s roles are interleaved in parallel, together with the actions of the adversary, the protocol fulfils its specified properties; or produce a counterexample that represents an attack on the property.

In practice, the Tamarin tool has proven to be highly successful. It features support for trace and observational equivalence properties, automatic and interactive modes. Tamarin has built-in support for fine-grained models of cryptographic primitives through so-called equational theories, such as the one modelling Diffie-Hellman key exchanges. Tamarin has been applied to numerous protocols from different domains including:
- Advanced key agreement protocols based on Diffie-Hellman exponentiation, such as verifying Naxos with respect to the eCK (extended Canetti Krawczyk) model; see (Schmidt et al. 2012).
- The Attack Resilient Public Key Infrastructure (ARPKI) (Basin et al. 2014).
- Transport Layer Security (TLS) (Cremers et al. 2016)
- and many others
Back to Software Spotlights Overview