Analyse de protocoles - unir les outils existants – TECAP

L'essor d'Internet et l'omniprésence des appareils électroniques ont changé notre mode de vie. De nos jours, presque tous les services ont un homologue numérique (e.g. vote électronique, messagerie, commerce électronique). Malheureusement, cette digitalisation du monde s’accompagne de nouveaux risques pour notre sécurité et notre vie privée. Ces risques sont d’autant plus importants sur les systèmes numériques puisqu’une faille de sécurité peut engendrer des fraudes à grande échelle même avec des ressources limitées. Pour sécuriser ces applications, de nombreux protocoles cryptographiques ont été déployés (e.g. TLS, Verified-by-Visa, le protocole de messagerie sécurisé Signal). Néanmoins, ces protocoles contiennent parfois des défauts de sécurité qui peuvent être exploités et qui ont d’importantes conséquences socio-économiques (e.g., passeport français traçable, failles dans TLS). La conception et l’analyse des protocoles de sécurité sont connues pour être difficiles puisqu’elles demandent de considérer toutes les actions malicieuses d’un attaquant sur le protocole. Les méthodes formelles ont été utilisées avec succès pour prouver la sécurité de protocoles et pour découvrir de nouvelles failles de sécurité. Par exemple, en formalisant le protocole de vote Helios dans un modèle symbolique, Cortier et Smith ont identifié une faille dans le protocole qui permettait de compromettre la confidentialité du vote. Pourtant, prouver à la main la sécurité des protocoles cryptographiques est difficile et souvent source d’erreurs. C’est pourquoi une grande variété d’outils de vérification automatiques a été développée afin de prouver ou découvrir des attaques sur les protocoles, bien que la portée de ces outils, leur degré d’automatisation et leur modèle d’attaquant diffèrent grandement.

Malgré ce grand nombre d’outils, de nombreux protocoles cryptographiques représentent toujours un vrai défi et révèlent les limitations des outils. C’est en particulier le cas pour les protocoles à états, i.e. les protocoles qui demandent aux participants de se souvenir d’informations à travers plusieurs sessions, et pour les protocoles qui dépendent de primitives cryptographiques ayant des propriétés algébriques complexes (e.g. signature aveugle, ou exclusif). Pour faire face à ces limites, chaque outil se concentre sur des classes différentes de protocoles qui dépendent des primitives cryptographiques, des propriétés de sécurité, etc. De plus, les outils ne peuvent pas interagir entre eux puisqu’ils évoluent au sein de modèles différents avec des hypothèses spécifiques. Ainsi, bien qu’il soit déjà difficile de choisir l’outil le plus adapté pour un protocole donné parmi la pléthore d’outils existants, il est également impossible de prouver un protocole en utilisant plusieurs outils de vérification quand bien même des parties différentes de ce protocole pourraient être traitées par différents outils.

Le but de ce projet est d’obtenir le meilleur de ces outils. Dans un premier temps, nous améliorerons la théorie et l’implémentation de chaque outil individuellement en nous inspirant les forces des autres outils. Dans un second temps, nous construirons des ponts permettant la coopération des techniques employées et outils. Nous nous concentrerons dans ce projet sur les outils CryptoVerif, EasyCrypt, Scary, ProVerif, Tamarin, AKiSs et APTE (étant donné que la France est l’un des pays les plus avancés dans le développement de ce type d’outils, la plupart de ces outils sont français mais certains sont internationaux : EasyCrypt et Tamarin). Afin de valider les résultats obtenus dans ce projet, nous les utiliserons sur plusieurs études de cas telles que le protocole "Authentication and Key Agreement" issu des réseaux de télécommunication, les protocoles de vote électronique Scytl et Helios, ainsi que le protocole d’authentification à secrets faibles 3D-Secure. Ces protocoles ont été choisis car ils couvrent les nombreuses limites des outils actuels.