Automatic generation of sources lemmas in Tamarin: towards automatic proofs of security protocols
Véronique Cortier, Stéphanie Delaune, and Jannik Dreier. Automatic generation of sources lemmas in Tamarin: towards automatic proofs of security protocols. In 25th European Symposium on Research in Computer Security (ESORICS 2020), pp. 3–22, Lecture Notes in Computer Science 12309, Guilford, United Kingdom, September 2020. Best paper award.
doi:10.1007/978-3-030-59013-0_1
Download
Abstract
Tamarin is a popular tool dedicated to the formal analysis of security protocols. One major strength of the tool is that it offers an interactive mode, allowing to go beyond what pushbutton tools can typically handle. Tamarin is for example able to verify complex protocols such as TLS, 5G, or RFID protocols. However, one of its drawback is its lack of automation. For many simple protocols, the user often needs to help Tamarin by writing specific lemmas, called "sources lemmas", which requires some knowledge of the internal behaviour of the tool.
In this paper, we propose a technique to automatically generate sources lemmas in Tamarin. We prove formally that our lemmas indeed hold, for arbitrary protocols that make use of cryptographic primitives that can be modelled with a subterm convergent equational theory (modulo associativity and commutativity). We have implemented our approach within Tamarin. Our experiments show that, in most examples of the literature, we are now able to generate suitable sources lemmas automatically , in replacement of the handwritten lemmas. As a direct application , many simple protocols can now be analysed fully automatically, while they previously required user interaction.
BibTeX
@inproceedings{Tamarin-Esorics20,
TITLE = {{Automatic generation of sources lemmas in Tamarin:
towards automatic proofs of security protocols}},
AUTHOR = {Cortier, V{\'e}ronique and Delaune, St{\'e}phanie
and Dreier, Jannik},
URL = {https://hal.archives-ouvertes.fr/hal-02903620},
BOOKTITLE = {{25th European Symposium on Research in Computer
Security (ESORICS 2020)}},
ADDRESS = {Guilford, United Kingdom},
YEAR = 2020,
MONTH = {September},
pages = {3--22},
series = {Lecture Notes in Computer Science},
volume = 12309,
note = {{\bf Esorics best paper award}},
abstract = {Tamarin is a popular tool dedicated to the formal
analysis of security protocols. One major strength
of the tool is that it offers an interactive mode,
allowing to go beyond what pushbutton tools can
typically handle. Tamarin is for example able to
verify complex protocols such as TLS, 5G, or RFID
protocols. However, one of its drawback is its lack
of automation. For many simple protocols, the user
often needs to help Tamarin by writing specific
lemmas, called "sources lemmas", which requires some
knowledge of the internal behaviour of the tool.
\par In this paper, we propose a technique to
automatically generate sources lemmas in Tamarin. We
prove formally that our lemmas indeed hold, for
arbitrary protocols that make use of cryptographic
primitives that can be modelled with a subterm
convergent equational theory (modulo associativity
and commutativity). We have implemented our approach
within Tamarin. Our experiments show that, in most
examples of the literature, we are now able to
generate suitable sources lemmas automatically , in
replacement of the handwritten lemmas. As a direct
application , many simple protocols can now be
analysed fully automatically, while they previously
required user interaction. },
note = {\textbf{Best paper award}},
={https://hal.archives-ouvertes.fr/hal-02903620/file/main.pdf},
doi = {10.1007/978-3-030-59013-0_1},
}