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



Job offers: a post-doc position (for 1 year) and a PhD position (3 years) are available on this project.
If you are interested, please send me (Stéphanie Delaune) a CV and recommandation letters.

Research themes

Members

Permanent members Temporary members/Visitors
Stéphanie Delaune, CR1 CNRS at LSV
Steve Kremer, CR1 INRIA at LORIA
Graham Steel, CR1 INRIA at LSV
Vincent Cheval, PhD student at LSV
Rémy Chrétien, Master student LSV/LORIA (1er april-30 sept. 2012)
Myrto Arapinis, Visitor (1 week/April 2012)

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

Meetings

Publications

— 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 Bauder, Véronique Cortier and Stéphanie Delaune. YAPA: A generic tool for computing intruder knowledge. ACM Transactions on Computational Logic, To appear.



Page maintained by Stéphanie Delaune.
Last modified: 17 April 2012.
Valid HTML 4.01! Valid CSS!