ANR/FNR Project Sequoia
Security properties, process equivalences and automated verification
3nd Sequoia meetingThe meeting of the ANR/FNR SEQUOIA project will be held on March 6, 2017 at ENS Cachan.
VenueThe meeting will be held at ENS Cachan, amphithéatre Chemla (IDA building). Directions to ENS Cachan. Plan of the campus showing the IDA building.
- 11:00-11:30 Welcome coffee
- 11:30-12:15 Adrien Koutsos (LSV): TBA (on RFID protocols and the computationally sound symbolic attacker)
- 12:15-13:00 Antoine Dallon (LSV, LORIA, IRISA): SAT-Equiv: an efficient tool for equivalence properties
- 13:00-14:00 Lunch buffet
- 14:00-14:40 Lucca Hirschi (LSV): New AKA Privacy Attacks in 4G Networks
- 14:40-15:20 Peter Browne Roenne (SnT): Improving verifiability in JCJ
- 15:20-16:00 Formal verification of protocols based on short authenticated strings Ludovic Robin (LORIA, IRISA)
- 16:00-16:20 Coffee break
- 16:20-17:00 On communication models when verifying equivalence properties Vincent Cheval (LORIA)
The fourth generation (4G), also known as Long Term Evolution, is a high speed cellular network system worldwide. It is used in 49 countries as of now and considered to be more secure than the previous generations. Every 4G network supported device deployed worldwide executes an extended third generation (3G) authentication protocol between the Universal Subscriber Identity Module (USIM) smart card and the network, referred as Authentication and Key Agreement (AKA). This AKA protocol provides security measures to establish mutual authentication and encryption to notably protect mobile subscriber's privacy. In this paper, we carefully investigate this protocol and its deployments in some European 4G networks. We reveal a new logical flaw in the AKA protocol specification: a lack of randomness in a message yields important leaks when replaying authentication challenges. Since those challenges can be requested without being authenticated, we show that this flaw constitutes a new attack vector exposing the AKA protocol to traceability and user activity monitoring attacks. We explore the protocol design and implementation mistakes by the cellular network operators that enabled those attacks: shortcomings of AKA protocol specifications, of AKA implementations in USIM and authentication centers, of interface to access unused and unlimited authentication challenges from the network. We demonstrate the feasibility of our attack using low cost implementation methods. Finally we conduct a security analysis and discuss countermeasures to remedy those new privacy issues.
In their seminal paper Juels, Catalano and Jakobsson constructed the first coercion-resistant remote e-voting protocol. However, the strong privacy guarantees came at the expense of trusting the authorities for verifiability. We will show how to remove this trust resulting in better verifiability and dispute resolution properties. Further, we demonstrate how the Selene mechanism can be used to allow the voters to check their vote directly while still being able to mitigate coercion.
Modern security protocols may involve humans, in order to compare or copy short strings between different devices. Multi-factor authentication protocols, such as Google 2-factor or 3D-secure are typical examples of such protocols. However, such short strings may be subject to brute force attacks. We propose a symbolic model which includes attacker capabilities for guessing short strings, and producing collisions when short strings are produced by weak hash functions. We propose a new decision procedure for analysing (a bounded number of sessions of) protocols that rely on short strings. The procedure has been integrated in the AKiSs tool and tested on protocols from the ISO/IEC 9798-6:2010 standard.
Symbolic models for security protocol verification, following the seminal ideas of Dolev and Yao, come in many flavors, even though they share the same ideas. A common assumption is that the attacker has complete control over the network: he can therefore intercept any message. Depending on the precise model this may be reflected either by the fact that any protocol output is directly routed to the adversary, or communications may be among any two participants, including the attacker - the scheduling between which exact parties the communication happens is left to the attacker. These two models may seem equivalent at first glance and, depending on the verification tools, either one or the other semantics is implemented. We show that, unsurprisingly, they indeed coincide for reachability properties. However, when we consider indistinguishability properties, we prove that these two semantics are incomparable. We also introduce a new semantics, where internal communications are allowed but messages are always eavesdropped by the attacker. We show that this new semantics yields strictly stronger equivalence relations. We also identify two subclasses of protocols for which the three semantics coincide. Finally, we implemented verification of trace equivalence for each of these semantics in the APTE tool and compare their performances on several classical examples.