fr
Verification of Indistinguishability Properties ANR    
Programme Jeunes Chercheuses Jeunes Chercheurs (JCJC) (January 2012 - June 2016) VIP ANR-11-JS02-006




Highlights:

Research themes

Members

Permanent members Temporary members Former members
David Baelde, MdC ENS Cachan (since sept. 2012)
Stéphanie Delaune, CR1 CNRS at LSV
Steve Kremer, DR2 INRIA at LORIA
Graham Steel, CR1 INRIA at LSV (until August 2012)
Lucca Hirschi, PhD student at LSV (since sept. 2013)
Antoine Dallon, PhD student at LSV (since nov. 2015)
Ivan Gazeau, Post doc at LSV (since june 2015)
Vincent Cheval, PhD student at LSV (until December 2012)
Malika Izabachène, ATER au LSV (until August 2012)
Rémy Chrétien, Master & PhD student LSV/LORIA (2012-2015)
Apoorvaa Deshpande, Master student (july-dec. 2012)
Lucca Hirschi, Master student (feb-june. 2013)
Antoine Dallon, Master student LSV/LORIA (avril-oct. 2015)

Project description

The Internet is a large common space, accessible to everyone around the world. As in any public space, people should take appropriate precautions to protect themselves against fraudulent people and processes. It is therefore essential to obtain as much confidence as possible in the correctness of the applications that we use.
Because security protocols are notoriously difficult to design and analyse, formal verification techniques are extremely important. Formal verification of security protocols has known significant success during the two last decades. The techniques have become mature and several tools for protocol verification are nowadays available. However, nearly all studies focus on trace-based security properties, and thus do not allow one to analyse privacy-type properties that play an important role in many modern applications.

Modelling protocols and their privacy properties. We came to the study of privacy-type properties a few years ago through the electronic voting application. Even for this particular application the concept of privacy represents formally several security properties. Actually, privacy is a general requirement that has also been recently studied in the context of RFID protocols leading again to several definitions (different from those obtained in electronic voting). For many applications such as routing protocols or location-based services for vehicular ad hoc networks (e.g. e-toll collection, ``pay-as-you-go'' insurance, ...), formal definitions of privacy are still missing.

Algorithms for verifying equivalence-based properties. While algorithms and efficient tools already exist for trace-based security properties, there are still few results to analyse privacy-type properties. The existing procedures are actually quite limited. Moreover, our target applications have some specificities that can not be expressed in current models. Lastly, we may want to consider a different intruder model or express our privacy definitions relying on different notions of equivalence (e.g. trace equivalence, observational equivalence).
To the best of our knowledge, the only verification tool that is able to check equivalence is the ProVerif tool. However, we have already observed that the approximations used in ProVerif are not suited for the privacy properties we wish to verify. Moreover, ProVerif is not well-suited to analyse trace equivalence that seems however to be the right notion in some applications. Other techniques to decide equivalence-based properties have been proposed, but either they are not effective or the implementation does not scale up well to deal with even rather small processes. Moreover, in order to deal with our target applications, it seems necessary to enlarge the scope of the method to a larger class of processes.

Modularity issues.One of the tasks of the project is focused at proposing modular techniques in two main directions. First, we would like to combine the decision procedures that we will obtain for various cryptographic primitives.
Secondly, regarding protocol composition, it is well-known that composition works when the protocols do not share secrets. However, there is no result allowing us to derive some interesting results when the processes rely on some shared secrets such as long term keys. This kind of composition results will be very useful. For instance, this could allow us to establish privacy in presence of two honest voters or untraceability in presence of two different tags, and to obtain guarantees in a setting that involves an arbitrary number of voters or tags.

More details are available in the full text of the proposal.

Reports

Tools

The tools that have been developed or improved by members of the VIP project are listed below:

Meetings

Most of our meetings are focused on interactions between members (other members of the SecSI team will also be welcome) and internal presentations of advances. Sometimes, we also invite external guests to obtain external feedback on our work.

Publications

— 2016 —

[Chretien-PhD16] Rémy Chrétien. Analyse automatique de propriétés d'équivalence pour les protocoles cryptographiques. PhD thesis, 2016.
[CCCK16] Rohit Chadha, Vincent Cheval, Stefan Ciobaca and Steve Kremer. Automated verification of equivalence properties of cryptographic protocols. In TOCL'16, To appear.
[HBD16] Lucca Hirschi, David Baelde, and Stéphanie Delaune. A method for verifying privacy-type properties: the unbounded case. In S&P'16, 2016.
[CDD16] Véronique Cortier, Antoine Dallon and Stéphanie Delaune. Bounding the number of agents, for equivalence too. In POST'16, 2016.

— 2015 —

[CCD15c] Rémy Chrétien, Véronique Cortier, and Stéphanie Delaune. From security protocols to pushdown automata. In TOCL'15, 2015.
[BDH15] David Baelde, Stéphanie Delaune and Lucca Hirschi. Partial Order Reduction for Security Protocols. In CONCUR'15, 2015.
[CCD15a] Rémy Chrétien, Véronique Cortier and Stéphanie Delaune. Decidability of trace equivalence for protocols with nonces. In CSF'15, 2015.
[CCD15b] Rémy Chrétien, Véronique Cortier and Stéphanie Delaune. Checking trace equivalence: How to get rid of nonces?. In ESORICS'15, 2015.
[ACD15] Myrto Arapinis, Vincent Cheval and Stéphanie Delaune. Composing security protocols: from confidentiality to privacy. In POST'15, 2015.

— 2014 —

[BCD14] Sergiu Bursuc, Hubert Comon-Lundh, and Stéphanie Delaune. Deducibility constraints and blind signatures. In Information and Computation, 2014.
[ACD14] Mathilde Arnaud, Véronique Cortier, and Stéphanie Delaune. Modeling and Verifying Ad Hoc Routing Protocols. In Information and Computation, 2014.
[ADK14] Myrto Arapinis, Stéphanie Delaune and Steve Kremer. Dynamic Tags for Security Protocols. In Logical Methods in Computer Science, 2014.
[CDKR14] Céline Chevalier, Stéphanie Delaune, Steve Kremer and Mark Ryan. Composition of Password-based Protocols. In Formal Methods in System Design, 2014.
[BDH14] David Baelde, Stéphanie Delaune and Lucca Hirschi. A reduced semantics for deciding trace equivalence using constraint systems. In POST'14, 2014.
[CCD14] Rémy Chrétien, Véronique Cortier and Stéphanie Delaune. Typing messages for free in security protocols: the case of equivalence properties. In CONCUR'14, 2014.
[CDR14] Vincent Cheval, Stéphanie Delaune and Mark Ryan. Tests for establishing security properties. In TGC'14, 2014.
[CD14] Rémy Chrétien, and Stéphanie Delaune. Le bitcoin, une monnaie 100% numérique. Interstices, 2014.

— 2013 —

[CK13] Véronique Cortier, and Steve Kremer. Vote par Internet. Interstices, 2013.
[CCP13] Vincent Cheval, Véronique Cortier, and Antoine Plet. Lengths may break privacy -- or how to check for equivalences with length. In CAV'13, 2013.
[CCD13a] Vincent Cheval, Véronique Cortier, and Stéphanie Delaune. Deciding equivalence-based properties using constraint solving. In TCS'13, 2013.
[CCD13b] Rémy Chrétien, Véronique Cortier, and Stéphanie Delaune. From security protocols to pushdown automata. In ICALP'13, 2013.
[CD13] Rémy Chrétien and Stéphanie Delaune. Formal analysis of privacy for routing protocols in mobile ad hoc networks. In POST'13, 2013.
[ACKR13] Myrto Arapinis, Véronique Cortier, Steve Kremer, and Mark Ryan. Practical everlasting privacy. In POST'13, 2013.
[CB13] Vincent Cheval and Bruno Blanchet. Proving more observational equivalences with ProVerif. In POST'13, 2013.

— 2012 —

[Chretien12] Rémy Chrétien. Trace equivalence of protocols for an unbounded number of sessions. Master report, 2012.
[Deshpande12] Apoorvaa Deshpande. Automated verification of equivalence properties in cryptographic protocols modulo AC. Master report, 2012.
[CCK12] Rohit Chadha, Stefan Ciobaca and Steve Kremer. Automated verification of equivalence properties of cryptographic protocols. In ESOP'12, 2012.
[CDD12] Véronique Cortier, Jan Degrieck and Stéphanie Delaune. Analysing routing protocols: four nodes topologies are sufficient. In POST'12, 2012.
[DKP12] Stéphanie Delaune, Steve Kremer and Daniel Pasaila. Security protocols, constraint systems, and group theories. In IJCAR'12, 2012.
[ACD12] Myrto Arapinis, Vincent Cheval and Stéphanie Delaune. Verifying privacy-type properties in a modular way. In CSF'12, 2012.
[BCD12] Mathieu Baudet, Véronique Cortier and Stéphanie Delaune. YAPA: A generic tool for computing intruder knowledge. ACM Transactions on Computational Logic, 2012.




Page maintained by Stéphanie Delaune.
Last modified: 11 July 2016.
Valid HTML 4.01! Valid CSS!