Une équipe de scientifiques passe à la loupe les protocoles cryptographiques

Distinctions Informatique

Plutôt que de réparer incessamment des failles de sécurité une fois qu’elles ont été exploitées par un attaquant, il est possible de réduire ces risques en aidant les cryptographes à les détecter en amont grâce à des outils de vérification de protocoles. C’est l’objet des recherches en cybersécurité d'une équipe de scientifiques dont les travaux ont été récompensés par un Distinguished Paper Award lors de la conférence CSF 2022.

Payer en ligne, voter électroniquement, transmettre ses données de santé à la pharmacie. Si ces actions sont protégées, c’est grâce à des protocoles cryptographiques. Ces petits programmes informatiques sécurisent les échanges d’informations. Ils reposent pour cela sur des combinaisons d’algorithmes de base tels que le chiffrement et les signatures. Il existe une multitude de protocoles qui évoluent en permanence selon les applications et les ressources des technologies utilisées. Par exemple, un téléphone portable n’offre pas les mêmes capacités qu’une carte à puce. Mais bien qu’ils soient omniprésents dans notre quotidien, sont-ils pour autant infaillibles ? En réalité, des attaques exploitent fréquemment des failles décelées au sein de ces programmes. Elles sont corrigées, mais d’autres attaques exploitent à leurs tours différentes failles, et ainsi de suite dans un cycle infernal.

Il n’existe pas un seul protocole de vote, de chiffrement, ou d’authentification, mais une multitude. Nos travaux visent à améliorer l’analyse de tous ces protocoles pour les rendre plus sûrs et sans failles.
,

Pour répondre à cette problématique et anticiper plutôt que réagir, David Baelde, professeur à l'ENS Rennes, Stéphanie Delaune, directrice de recherche CNRS, membres l'équipe Spicy de l'Institut de recherche en informatique et systèmes aléatoires (IRISA - CNRS/Université de Rennes 1), Adrien Koutsos, chargé de recherche Inria Paris et Solène Moreau, ancienne doctorante à l'IRISA et maintenant ingénieure de recherche Inria Saclay, développent des programmes de vérification de protocoles cryptographiques. « Notre objectif est de déceler des failles dans des protocoles existants à l’aide de méthodes formelles. Pour cela, nous modélisons mathématiquement chaque protocole et nous le vérifions à l’aide d’outils divers, plus ou moins automatiques, dont Squirrel », explique Stéphanie Delaune. Ce logiciel, en partie développé au sein de l’équipe Spicy, est un assistant de preuve qui accompagne le développeur pas à pas. Celui-ci renseigne son protocole, décrit sa méthode et les propriétés qu’il veut démontrer. Squirrel vérifie chaque étape de la preuve, détecte les erreurs de raisonnement, et, in fine, permet de proposer des recommandations afin d’améliorer la fiabilité du protocole face à des attaques.

Les premiers résultats sont probants, en témoigne la distinction des travaux de l'équipe de scientifiques de l'IRISA et d'Inria lors de la 35e édition de la conférence CSF 2022 - IEEE Computer Security Foundations Symposium en août dernier. « Différentes techniques de vérification existent, mais nous avons démontré que Squirrel permet en particulier de traiter les protocoles à états – des protocoles qui s’appuient sur des données stockées de session en session », détaille la chercheuse.

Désormais, l’équipe souhaite automatiser plusieurs tâches au sein de Squirrel. Le but : permettre au programme de déduire certaines étapes sans avoir à lui préciser et faciliter ainsi sa prise en main. En résultera des preuves plus courtes mais tout aussi efficaces.

Avec l’arrivée de l’ordinateur quantique, nous devons adapter nos méthodes de vérification pour prendre en compte cette menace, et aussi développer l’analyse de protocoles dit hybrides actuellement en cours de normalisation.
,

Par ailleurs, l’arrivée des ordinateurs quantiques va apporter une puissance supplémentaire à des attaquants. Le protocole de chiffrement RSA, par exemple, utilisé par le commerce en ligne et basé sur la factorisation, deviendra obsolète. Le besoin de développer de nouveaux protocoles cryptographiques est donc prégnant. Et c’est tout autant de programmes à vérifier pour l’équipe de Stéphanie Delaune. « Une des questions qui anime nos recherches actuelles est d’adapter Squirrel à la preuve de protocoles classiques en présence d’un attaquant quantique. Des premiers résultats prometteurs ont d’ores-et-déjà été obtenus, mais les tests doivent se poursuivre », explique la chercheuse.

Analyse de protocoles cryptographique afin d’assurer leur sécurité et la protection de la vie privée / © Christian MOREL / IRISA / CNRS Photothèque

Publication

David Baelde, Stéphanie Delaune, Adrien Koutsos, Solène Moreau. Cracking the Stateful Nut: Computational Proofs of Stateful Security Protocols using the Squirrel Proof AssistantCSF 2022 - 35th IEEE Computer Security Foundations Symposium, Aug 2022, Haifa, Israel.

Contact

Stéphanie Delaune
Directrice de recherche CNRS à l'IRISA