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

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.

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 35^e é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.

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.