Véronique Cortier, Stéphanie Delaune, and Jannik Dreier. Automatic generation of sources lemmas in Tamarin: towards automatic proofs of security protocols. In Proceedings of the 25th European Symposium on Research in Computer Security (ESORICS'20), Lecture Notes in Computer Science, Springer, Virtual conference, 2020.
Tamarin is a popular tool dedicated to the formal analysis of security protocols. One major strength of the tool is that itoffers an interactive mode, allowing to go beyond what push-buttontools can typically handle. Tamarin is for example able to verifycomplex protocols such as TLS, 5G, or RFID protocols.However, one of its drawback is its lack of automation.For many simple protocols, the useroften needs to help Tamarin by writing specific lemmas, called“sources lemmas”, which requires some knowledge of the internalbehaviour of the tool.In this paper, we propose a technique to automaticallygenerate sources lemmas in Tamarin. We prove formally that our lemmasindeed hold, for arbitrary protocols that make use of cryptographicprimitives that can be modelled with a subterm convergentequational theory (modulo associativity and commutativity).We have implemented our approach within Tamarin. Our experimentsshow that, in most examples of the literature, we are now able togenerate suitable sources lemmas automatically, in replacement of thehand-written lemmas. As a direct application, many simple protocols can now be analysed fully automatically, while theypreviously required user interaction.
@inproceedings{CDD-esorics20,
address = {Virtual conference},
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 push-button
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
hand-written lemmas. As a direct application,
many simple protocols can now be analysed fully automatically, while they
previously required user interaction.
},
author = {V{\'{e}}ronique Cortier and
St{\'{e}}phanie Delaune and
Jannik Dreier},
title = {Automatic generation of sources lemmas in Tamarin: towards
automatic proofs of security protocols},
booktitle = {{P}roceedings of the 25th {E}uropean {S}ymposium on {R}esearch in {C}omputer {S}ecurity (ESORICS'20)},
year = {2020},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
acronym = {{ESORICS}'20},
}