A Decidable Class of Security Protocols for Both Reachability and Equivalence Properties
- PDF / 747,264 Bytes
- 42 Pages / 439.37 x 666.142 pts Page_size
- 72 Downloads / 179 Views
A Decidable Class of Security Protocols for Both Reachability and Equivalence Properties Véronique Cortier1 · Stéphanie Delaune2 · Vaishnavi Sundararajan2 Received: 22 January 2020 / Accepted: 9 October 2020 © Springer Nature B.V. 2020
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 “simple”, meaning that an attacker can precisely identify from which participant and which session a message originates from. We also consider protocols with no else branches (only positive test). (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 a dependency graph, which, given a protocol, characterises how actions depend on the other ones (both sequential dependencies and data dependencies are taken into account). Whenever 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. Keywords Security protocols · Verification · Privacy properties
1 Introduction Security protocols are notoriously difficult to design and analyse. In this context, formal methods have proved their interest to help to detect automatically flaws and provide better security guarantees. For example, they have been used during the standardisation process to detect and correct flaws in the Transport Layer Security (TLS) 1.3 protocol [1]. In the context of voting, the production of symbolic proofs is now a legal requirement in Switzerland [2]. Symbolic models for security protocols abstract away how cryptographic primitives are implemented. They instead focus on the analysis of the flow of the protocols. Thanks to this level of abstraction, security analysis is amenable to automation. Several tools can now,
B
Véronique Cortier [email protected] Stéphanie Delaune [email protected]
1
LORIA, CNRS & Univ Lorraine & Inria Grand Est, Vandœuvre-lès-Nancy, France
2
IRISA, CNRS & Univ Rennes, Rennes, France
123
V. Cortier et al.
given the abstract specification of a protocol, automatically find flaws or prove security. Examples of popular tools are ProVerif [3], Tamarin [4], Avispa [5], Maude-NPA [6], or Scyther [7]. However, even simple security properties like confidentiality are undecidable in general [8]. To retrieve decidability, one standard assumption is to bound the number of sessions, which corresponds to analysing the protocol when it is run a finite number of times. In that case, reachability properties like confidentiality and authentication properties are (co)NP-complete [9]. Privacy properties like anonymity, vote secrecy or unlinkability are rather expressed as equivalence propert
Data Loading...
