Projet ANR-11-JS02-0006 – VIP : Vérification de propriétés d'indistinguabilité
Programme : JCJC - SIMI 2 - Science informatique et applications (JCJC SIMI 2)
Année de financement : 2011
Coordinateur du projet : Madame Stéphanie DELAUNE (CNRS - DELEGATION REGIONALE ILE-DE-FRANCE SECTEUR EST)
Partenaires : Laboratoire Spécification et Vérification
Montant : 200408.0 euros
Date de début : 2012
Durée : 48 mois
Résumé : Vérification de propriétés d'indistinguabilité1. Modélisation de protocoles et des propriétés du type «respect de la vie privée«.2. Algorithmes pour vérifier les propriétés d'équivalence.3. Modularité.
Analyser des propriétés du type «respect de la vie privée«Internet est un espace commun accessible à tous. Il est important de s'assurer du bon fonctionnement des applications que nous utilisons. Parce que les protocoles de sécurité sont difficiles à concevoir et à analyser, les techniques de vérification formelles jouent un rôle important. Cependant, la plupart des études menées 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.
Vérification formelleLe but de ce projet est d'analyser des applications modernes pour lesquelles le respect de la vie privée joue un rôle important. De nombreuses applications sont concernées, comme par exemple, le vote électronique, les application de sécurité dans les réseaux de voitures, protocoles de routage, étiquettes RFID qui sont maintenant embarquées dans de nombreux objets de la vie courante.
Résumé de la soumission : 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, lestechniques 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 étudesmené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.1. 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.2. 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.3. 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.
Résultats : Une étude récente a révélée l'existence d'une attaque sur l'implémentation du protocole d'établissement de clef dans le passeport français. Cela permet de tracer physiquement une personne en possession d'un tel passeport.
Perspectives : Nous prévoyons développer de nouvelles techniques pour  permettre l'étude de protocoles utilisés dans les téléphones mobiles.
Publications et brevets : Les publications scientifiques liées au projet sont disponibles sur le site web du projet.