![](https://csdnimg.cn/release/download_crawler_static/77942515/bg1.jpg)
The TAMARIN Prover for the
Symbolic Analysis of Security Protocols
Simon Meier
?
, Benedikt Schmidt
†
, Cas Cremers
?
, and David Basin
?
?
Institute of Information Security, ETH Zurich, Switzerland
†
IMDEA Software Institute, Madrid, Spain
Abstract.
The Tamarin prover supports the automated, unbounded,
symbolic analysis of security protocols. It features expressive languages
for specifying protocols, adversary models, and properties, and support
for efficient deduction and equational reasoning. We provide an overview
of the tool and its applications.
1 Introduction
During the last two decades, there has been considerable research devoted to the
symbolic analysis of security protocols and existing tools have had considerable
success both in detecting attacks on protocols and showing their absence. Never-
theless, there is still a large discrepancy between the symbolic models that one
specifies on paper and the models that can be effectively analyzed by tools.
In this paper, we present the Tamarin prover for the symbolic analysis of
security protocols. Tamarin generalizes the backwards search used by the Scyther
tool [4] to enable: protocol specification by multiset rewriting rules; property
specification in a guarded fragment of first-order logic, which allows quantification
over messages and timepoints; and reasoning modulo equational theories. As
practical examples, these generalizations respectively enable the tool to handle:
protocols with non-monotonic mutable global state and complex control flow such
as loops; complex security properties such as the eCK model [9] for key exchange
protocols; and equational theories such as Diffie-Hellman, bilinear pairings, and
user-specified subterm-convergent theories.
Tamarin provides two ways of constructing proofs: an efficient, fully auto-
mated mode that uses heuristics to guide proof search, and an interactive mode. If
the tool’s automated proof search terminates, it returns either a proof of correct-
ness (for an unbounded number of threads and fresh values) or a counterexample
(e. g., an attack). Due to the undecidable nature of most properties in our setting,
the tool may not terminate. The interactive mode enables the user to explore
the proof states, inspect attack graphs, and seamlessly combine manual proof
guidance with automated proof search.
The theory for Diffie-Hellman exponentiation and the application to Diffie-
Hellman-based two-party key exchange protocols have been published in [13]. In
the theses of Meier [10] and Schmidt [14], the approach is extended with trace
induction and with support for bilinear pairings and AC operators.