Verification of Indistinguishability Properties |
![]() |
Programme Jeunes Chercheuses Jeunes Chercheurs (JCJC) (January 2012 - June 2016) | VIP ANR-11-JS02-006 |
Highlights:
- Nous avons organisés avec le soutien du pole de compétitivité system@tic (via l'ANR VIP) un colloque de 2 jours en l'honneur de Martin Abadi . Plus d'informations ici.
- La soutenance de Rémy Chrétien a eu lieu à Cachan le 11 Janvier 2016. Il est maintenant expert technique au Ministère de la Défense.
- Prix EASST du meilleur article à ETAPS 2016 : Véronique Cortier, Antoine Dallon et Stéphanie Delaune ont reçu le prix EASST du meilleur article à ETAPS 2016 pour leur article intitulé Bounding the number of agents, for equivalence too et présenté à POST 2016.
Research themes
- Formal verification
- Security protocols
- Anonymity, Privacy
- Applications: e-voting, RFID protocols, e-auction, routing protocols,...
Members
Permanent members | Temporary members | Former members | |||||||||||||
|
|
|
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
- Web site. January 2012.
- D2.1: Formal definitions of some privacy-type properties. March 2013.
- D6.1: Description of some case studies. September 2013.
- D3.1: Decision procedures for equivalence based properties. December 2013.
- D3.1: Decision procedures for equivalence based properties (part II). September 2015.
- D4.1: Composition results for equivalence-based properties. September 2015.
- D4.2: Composition issues. June 2016.
- D2.2: Results on the case studies. June 2016.
- Poster - Rencontres du Numérique 2016. June 2016.
Tools
The tools that have been developed or improved by members of the VIP project are listed below:- AKiSs Active Knowledge In Security protocolS
- APTE Algorithm for Proving Trace Equivalence and its extension regarding POR
- ProVerif Cryptographic protocol verifier in the formal model
- cpp2dpa is a tool to convert cryptographic protocols into deterministic pushdown automata, enabling proofs of equivalence and discovery of attacks
- UKano is a tool that automatically checks unlinkability and anonymity for a large class of 2-agents protocols for an unbounded number of sessions.
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.- 25 Février 2015: Groupe de Travail (Cachan)
Rémy Chrétien : Decidability of trace equivalence for protocols with nonces - 11 Mars 2015: Groupe de Travail (Cachan)
Stéphanie Delaune : Leakiness is decidable for well-founded protocols - 1 Avril 2015: Groupe de Travail (Cachan)
Ivan Gazeau : Providing transparent accountability for electronic currencies - 3 Juin 2015: Groupe de Travail (Cachan)
Rémy Chrétien : Checking trace equivalence: How to get rid of nonces? - 17 Juin 2015: Groupe de Travail (Cachan)
Lucca Hirschi : Sound Approach to Check Privacy Protection for an Unbounded Number of Sessions - 8 Juillet 2015: Groupe de Travail (Cachan)
Antoine Dallon : Reducing the number of agents in equivalence properties - 10 Décembre 2015: Groupe de Travail (Cachan)
Stéphanie Delaune & Lucca Hirschi: Présentation de Tamarin - 10 Mars 2016: Groupe de Travail (Cachan)
Ivan Gazeau : Verification of privacy-type properties for security protocols with XOR - 14 Avril 2016: Groupe de Travail (Cachan)
Ioana Boureanu : Automatic Verification of Security Protocols using Temporal-Epistemic Logics - 12 Mai 2016: Groupe de Travail (Cachan)
Antoine Dallon : Verifying protocols using SAT solvers - 29 Janvier 2015: Réunion de travail à Nancy dans le cadre de la thèse de Rémy Chrétien
Participants: Rémy Chrétien, Véronique Cortier, et Stéphanie Delaune. - 18 Mars 2015: Réunion de travail à Cachan dans le cadre de la thèse de Rémy Chrétien
Participants: Rémy Chrétien, Véronique Cortier, et Stéphanie Delaune. - 28 Mai 2015: Réunion de travail à Cachan dans le cadre de la thèse de Rémy Chrétien et du stage de M2 d'Antoine Dallon.
Participants: Rémy Chrétien, Véronique Cortier, Antoine Dallon, et Stéphanie Delaune. - 18 Novembre 2015: Réunion de travail à Nancy.
Participants: Ivan Gazeau et Steve Kremer. - 14 Janvier 2016: Réunion de travail à Nancy dans le cadre de la thèse d'Antoine Dallon.
Participants: Véronique Cortier, Antoine Dallon, et Stéphanie Delaune. - 11 Février 2016: Réunion de travail à Cachan dans le cadre de la thèse de Rémy Chrétien et Antoine Dallon
Participants: Rémy Chrétien, Véronique Cortier, Antoine Dallon, et Stéphanie Delaune. - 18 Mars 2016: Réunion de travail à Nancy dans le cadre de la thèse d'Antoine Dallon.
Participants: Véronique Cortier, Antoine Dallon, et Stéphanie Delaune. - 14 Avril 2016: Visite de Ioana Boureanu à Cachan.
Participants: Ioana Boureanu, et Stéphanie Delaune. - 11 Mai 2016: Réunion de travail à Cachan dans le cadre de la thèse d'Antoine Dallon.
Participants: Véronique Cortier, Antoine Dallon, et Stéphanie Delaune. - 5 Juillet 2016: Réunion de travail à Nancy dans le cadre de la thèse d'Antoine Dallon.
Participants: Véronique Cortier, Antoine Dallon, et Stéphanie Delaune.
Groupes de travail 2015/2016
Réunions et Visites 2015/2016
Réunions et groupes de travail pour l'année 2012
Réunions et groupes de travail pour l'année 2013
Réunions et groupes de travail pour l'année 2014
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.