Searching for just a few words should be enough to get started. If you need to make more complex queries, use the tips below to guide you.
Issue title: Selected Papers From ESORICS 2020
Guest editors: Kaitai Liang, Liqun Chen, Ninghui Li and Steve Schneider
Article type: Research Article
Authors: Cortier, Véroniquea | Delaune, Stéphanieb | Dreier, Jannika; * | Klein, Elisea
Affiliations: [a] Université de Lorraine, CNRS, Inria, LORIA, F-54000 Nancy, France | [b] Université Rennes, CNRS, IRISA, France
Correspondence: [*] Corresponding author. E-mail: jannik.dreier@loria.fr.
Note: [1] This is an extended version of “Automatic Generation of Sources Lemmas in TAMARIN: Towards Automatic Proofs of Security Protocols” that originally appeared in Computer Security – ESORICS 2020, Springer, pp. 3–22, 2020.
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. Following the intuition of manually written sources lemmas, our lemmas try to keep track of the origin of a term by looking into emitted messages or facts. 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.
Keywords: Formal verification, Tamarin prover
DOI: 10.3233/JCS-210053
Journal: Journal of Computer Security, vol. 30, no. 4, pp. 573-598, 2022
IOS Press, Inc.
6751 Tepper Drive
Clifton, VA 20124
USA
Tel: +1 703 830 6300
Fax: +1 703 830 2300
sales@iospress.com
For editorial issues, like the status of your submitted paper or proposals, write to editorial@iospress.nl
IOS Press
Nieuwe Hemweg 6B
1013 BG Amsterdam
The Netherlands
Tel: +31 20 688 3355
Fax: +31 20 687 0091
info@iospress.nl
For editorial issues, permissions, book requests, submissions and proceedings, contact the Amsterdam office info@iospress.nl
Inspirees International (China Office)
Ciyunsi Beili 207(CapitaLand), Bld 1, 7-901
100025, Beijing
China
Free service line: 400 661 8717
Fax: +86 10 8446 7947
china@iospress.cn
For editorial issues, like the status of your submitted paper or proposals, write to editorial@iospress.nl
如果您在出版方面需要帮助或有任何建, 件至: editorial@iospress.nl