ANR/FNR Project Sequoia
Security properties, process equivalences and automated verification
Kick-off meetingThe kick-off meeting of the ANR SEQUOIA project will be held on March 9 2015 at Nancy.
VenueThe meeting will be held in room B013 of the Inria Nancy center. Directions are available here.
- 10:30 Welcome coffee
- 10:45 Steve Kremer: Short presentation of SEQUOIA
- 11:00 Lucca Hirschi: Partial order reduction techniques for the verification of security protocols
- 11:35 Rémy Chrétien: Decidability of trace equivalence with nonces
- 12:10 Lunch
- 13:45 Peter Ryan: On Secrecy and Symmetry
- 14:20 Jean Lancrenon: On relations between computational PAKE security models (ongoing work)
- 14:55 Eric Le Morvan: Secure composition of cryptographic protocols
- 15:30 Coffee break
- 16:00 Ludovic Robin: Automated verification of protocols using weak secrets - work in progress
- 16:35 - 17:00 Administrative questions
Security protocols are concurrent processes that communicate using cryptography with the aim of achieving various security properties. Recent work on their formal verification has brought procedures and tools for deciding trace equivalence properties (e.g. anonymity, unlinkability, vote secrecy) for a bounded number of sessions. However, these procedures are based on a naive symbolic exploration of all traces of the considered processes which, unsurprisingly, greatly limits the scalability and practical impact of the verification tools. We overcome this difficulty by developing partial order reduction techniques for the verification of security protocols. We provide reduced transition systems that optimally eliminate redundant traces, and which are adequate for model-checking trace equivalence properties of protocols by means of symbolic execution. We have implemented our reductions in the tool Apte, and demonstrated that it achieves the expected speedup on various protocols.
Privacy properties such as anonymity, unlinkability, or vote secrecy are typically expressed as equivalence properties. In this paper, we provide the first decidability result for trace equivalence of security protocols, for an unbounded number of sessions and unlimited fresh nonces. Our class encompasses most symmetric key protocols of the literature, in their tagged variant.
Some musings on how confidentiality properties have been defined in terms of symmetries in both the symbolic and crypto/computational approaches. Some speculations on approaches to a "Grand Unified Theory of Secrecy".
Password-Authenticated Key Exchange (PAKE) has been widely studied in the last twenty years. In particular, computational models to assess PAKE schemes' provable security have been developed. However, quite a few models exist and it is not clear how they relate to one another, making the interpretation of security theorems difficult. This work is about trying to formally compare some of these models. While variants of them have been proven equivalent in the "public-key infrastructure" setting, the "password setting" is not so clear.
Protocols are not isolated from other protocols that are used at the same time. This may be due to the fact that several versions of a single protocols may be used concurrently with the same keys and data, or to the fact that protocols can be used as subroutines of other protocols. It is difficult to verify a composition of protocols due to combinatorial explosion. The goal of my work is to find syntactic conditions under which there are no interference between protocols.
We design a model of security protocols that accounts for low-entropy secrets. Such weak secrets may occur in multi-factor authentication protocols when small, human copyable confirmation codes are sent over out-of-band channels. In our model an attacker may guess such secrets, in case the attacker has a possibility to check the validity of this guess offline. We automate the verification of this model in the AKISS tool.