A Decidable Class of Security Protocols for Both Reachability and Equivalence Properties

A Decidable Class of Security Protocols for Both Reachability and Equivalence Properties. Véronique Cortier, Stéphanie Delaune, and Vaishnavi Sundararajan . Journal of Automated Reasoning, 65:479–520, April 2021.

Download

[PDF] [long version] [HTML]

Abstract

We identify a new decidable class of security protocols, both for reachability and equivalence properties. Our result holds for an unbounded number of sessions and for protocols with nonces. It covers all standard cryptographic primitives. Our class sets up three main assumptions. (i) Protocols need to be without else branch and "simple", meaning that an attacker can precisely identify from which participant and which session a message originates from. (ii) Protocols should be type-compliant which is intuitively guaranteed as soon as two encrypted messages of the protocol cannot be confused. (iii) Finally, we define the notion of dependency graph, which given a protocol, characterises how actions depend from the other ones. As soon as the graph is acyclic then the protocol falls into our class. We show that many protocols of the literature belong to our decidable class, including for example some of the protocols embedded in the biometric passport.

BibTeX

@Article{JAR2020,
  author = 	 {V\'eronique Cortier and St\'ephanie Delaune and Vaishnavi Sundararajan },
  title = 	 {A Decidable Class of Security Protocols for Both Reachability and Equivalence Properties},
  journal = 	 {Journal of Automated Reasoning},
  year = 	 {2021},
  abstract = {We identify a new decidable class of security protocols, both for reachability and equivalence properties. Our result holds for an unbounded number of sessions and for protocols with nonces. It covers all standard cryptographic primitives. Our class sets up three main assumptions. (i) Protocols need to be without else branch and "simple", meaning that an attacker can precisely identify from which participant and which session a message originates from. (ii) Protocols should be type-compliant which is intuitively guaranteed as soon as two encrypted messages of the protocol cannot be confused. (iii) Finally, we define the notion of dependency graph, which given a protocol, characterises how actions depend from the other ones. As soon as the graph is acyclic then the protocol falls into our class. We show that many protocols of the literature belong to our decidable class, including for example some of the protocols embedded in the biometric passport.},
  OPTkey = 	 {},
  volume = 	 {65},
  OPTnumber = 	 {},
  pages = 	 {479--520},
  month = 	 {April},
  doi = {10.1007/s10817-020-09582-9},
}