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.

Visual representation of an attack found on the current protocol model.

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