Chaque jour, nous effectuons des actions en apparence bénignes : envoyer un message à un proche ou payer ses courses avec sa carte bancaire. Pourtant, ces applications mettent en jeu des données sensibles. Dans le cas des messageries ce sont notre identité et celle de nos correspondants, ainsi que le contenu de nos conversations. Dans le cas d’un paiement, ce sont notre identité et des informations sur notre compte en banque. Des attaques sur de tels services pourraient avoir de implications catastrophiques pour les victimes : usurpation d’identité, violation de la vie privée, vol… Les conséquences peuvent être encore plus étendues si la cible de l’attaque est par exemple un protocole de vote utilisé lors d’une élection nationale. Pour garantir des propriétés de sécurité telles que la confidentialité ou l’authentification des données qu’ils manipulent, ces services utilisent des protocoles cryptographiques. Ces protocoles sont généralement basés sur des primitives cryptographiques et décrivent comment les participants doivent communiquer (comment sont formatés les messages qu’ils échangent). Malheureusement, l’utilisation de primitives cryptographiques ne suffit pas à garantir la sécurité d’un protocole.

Dans le cadre de ma thèse, je me suis intéressée à la vérification formelle de protocole, un domaine qui s’attache à prouver des propriétés de sécurité sur les protocoles. D’une part, j’ai participé à l’analyse de protocoles déployés. Ces analyses ont permis de découvrir des attaques compromettant la sécurité de ses protocoles, mais également de proposer des solutions et de prouver que les versions corrigées de ses protocoles sont sécurisées. D’autre part, je me suis intéressée à Tamarin, un outil utilisé pour automatiser les preuves de sécurité. Comme les problèmes que Tamarin essaie de résoudre sont indécidables (il n’existe pas algorithme qui puisse toujours répondre à la question en un nombre fini d’étape); il arrive que certaines preuves ne puissent pas parvenir à une conclusion. Pour augmenter le nombre de preuves que Tamarin parvient à terminer, j’ai proposé de nouveaux algorithmes adaptatifs d’exploration des preuves permettant à l’outil de reconnaître une mauvaise situation et d’essayer d’en sortir. Trois de ces algorithmes parviennent à des meilleurs résultats que la version actuelle.