Automatic generation of sources lemmas in Tamarin: towards automatic proofs of security protocols

Automatic generation of sources lemmas in Tamarin: towards automatic proofs of security protocols. Véronique Cortier, Stéphanie Delaune, and Jannik Dreier. In 25th European Symposium on Research in Computer Security (ESORICS 2020), Guilford / virtual, United Kingdom, September 2020. Esorics best paper award.

Download

[PDF] [HTML]

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 / virtual, United Kingdom},
  YEAR = {2020},
  MONTH = {September},
  note = {{\bf Esorics best paper award}},
  doi = {10.1007/978-3-030-59013-0_1},
  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. },
}