en
Vérification de Propriétés d'Indistinguabilité ANR    
Programme Jeunes Chercheuses Jeunes Chercheurs (JCJC)
(Janvier 2012 - Juin 2016)
VIP ANR-11-JS02-006




Highlights:

Thématiques de recherche

Participants

Membres permanents Membres temporaires Ancien membres
David Baelde, MdC ENS Cachan (depuis sept. 2012)
Stéphanie Delaune, CR1 CNRS au LSV
Steve Kremer, DR2 INRIA au LORIA
Graham Steel, CR1 INRIA au LSV (jusqu'en août 2012)
Lucca Hirschi, Doctorant au LSV (depuis sept. 2013)
Antoine Dallon, Doctorant au LSV (depuis nov. 2015)
Ivan Gazeau, Post doc at LSV (depuis juin 2015)
Vincent Cheval, Doctorant au LSV (jusqu'au 31 décembre 2012)
Malika Izabachène, ATER au LSV (jusqu'au 31 août 2012)
Rémy Chrétien, Étudiant M2 & Doctorant LSV/LORIA (2012-2015)
Apoorvaa Deshpande, Étudiante M2 LSV/LORIA (juil.-déc. 2012)
Lucca Hirschi, Étudiant M2 LSV (fev.-juin. 2013)
Antoine Dallon, Étudiant M2 LSV/LORIA (avril-oct. 2015)

Description du projet

Internet est un espace commun accessible à tous. Comme dans tout espace commun, chacun doit prendre ses dispositions pour se protéger contre d'éventuelles personnes et/ou applications malhonnêtes. Pour cela, il est important de s'assurer du bon fonctionnement des applications que nous utilisons pour sécuriser nos données et nos transactions. Parce que les protocoles de sécurité sont difficiles à concevoir et à analyser, les techniques de vérification formelles jouent un rôle important. La vérification formelle de protocoles de sécurité a connu un succés important pendant les 20 dernières années. Les techniques sont devenues matures et plusieurs outils de vérification ont vu le jour. Cependant, la plupart des études menées concernent les propriétés dites de traces (secret, authentification, ...), et ne permettent pas d'analyser les propriétés du type "respect de la vie privée" qui jouent pourtant un rôle important dans de nombreuses applications.

Modélisation de protocoles et des propriétés du type "respect de la vie privée". Nous avons commencé l'étude de ce type de propriétés il y a quelques années à travers l'application du vote électronique. Même pour cette application particulière, ce concept de respect de la vie privée représente formellement plusieurs propriétés de sécurité bien distinctes. En fait, la notion de respect de la vie privée est un concept général qui a également été étudié dans le cadre des protocoles RFID conduisant à plusieurs définitions formelles (différentes de celles obtenues dans le cadre du vote électronique). Pour bien d'autres applications comme les protocoles de routage sécurisés ou les services proposées dans les réseaux de voitures (e.g. péage électronique, service d'assurance à la demande, ...), aucune définition formelle n'a été proposée à ce jour.

Algorithmes pour vérifier les propriétés d'équivalence. Alors que des algorithmes et des outils existent pour vérifier les propriétés dites de trace, peu de résultats permettent à l'heure actuelle d'analyser les propriétés d'équivalence. Les procédures existantes sont assez limitées. De plus, les applications visées ont des spécificités qui ne permettent pas de les modéliser dans les modèles existants. Enfin, il sera sans doute plus pertinent d'analyser ces protocoles avec un nouveau modèle d'attaquant et de considérer différentes notions d'équivalence. À notre connaissance, le seul outil de vérification capable de vérifier des propriétés d'équivalence est l'outil ProVerif. Cependant, nous avons déjà observé que les approximations utilisées par cet outil ne sont pas appropriées pour les propriétés d'équivalence que nous souhaitons étudier. De plus, ProVerif n'est pas adapté pour analyser les propriétés d'équivalence de trace. Cette notion semble cependant être la notion la plus adaptée pour modéliser bon nombre de propriété d'équivalence. D'autres techniques pour décider les propriétés d'équivalence ont été proposées, mais elles ne sont pas effectives et elles ne permettent pas de traiter des protocoles (même relativement simples) en un temps raisonnable. De plus, il est nécessaire d'étendre ces techniques pour traiter une classe plus large de protocoles et permettre l'étude de nouveaux types de protocoles.

Modularité. Une des tâches de ce projet est dédiée à la modularité. Nous proposons deux directions principales. Tout d'abord, nous souhaitons pouvoir combiner les procédures que nous allons obtenir pour traiter différentes primitives cryptographiques. Un deuxième aspect est le problème de la composition de protocoles. Ce type de résultats permettra d'effectuer l'analyse d'un protocole complexe d'une façon modulaire, mais aussi d'établir une propriété d'équivalence en propriété d'équivalence en présence de deux votants ou deux étiquettes RFID, et de garantir la sécurité dans un contexte plus général, i.e. plusieurs votants ou plusieurs tags.

Une présentation plus détaillée est donnée dans le texte complet du projet.

Rapports

Outils

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

Réunions

La plupart de nos réunions sont là pour permettre les échanges entre les membres du projet (les autres membres de l'équipe SecSI sont également bienvenus) et la présentation de nos travaux. Parfois, nous invitons des extérieurs afin de bénéficier de leur expertise.

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 maintenue par Stéphanie Delaune.
Dernières modifications : 11 juillet 2016.
Valid HTML 4.01! Valid CSS!