Élise Klein (Pesto), défendra sa thèse intitulée

Formal Verification in Practice:
Real-World Case Study and Enhanced Support for AC Operators in Tamarin .

La soutenance aura lieu en public le jeudi 11 décembre à 9h30, au LORIA, en salle A008. Elle sera suivie d’un pot.

Jury :

•  Yannick Chevalier (rapporteur — MCF HDR à l’Université de Toulouse)
•  Barbara Fila (rapportrice — MCF HDR à l’INSA de Rennes)
•  David Baelde (examinateur — Prof ENS Rennes)
•  Claudia Ignat (examinatrice — DR INRIA au Centre Inria de l’Université de Lorraine et LORIA)
•  Ioana Boureanu (examinatrice — Prof University of Surrey, UK)
•  Steve Kremer (Directeur de thèse — DR INRIA au Centre Inria de l’Université de Lorraine et LORIA)
•  Jannik Dreier (Directeur de thèse — MCF Université de Lorraine)

Abstract:

« During my PhD, I studied the Tamarin-prover, a cryptographic protocol verification tool, initially focusing on modeling and later on improving its internal mechanisms. I first used the Sapic+ platform, integrated into Tamarin, to model the draft 12 of the LAKE-EDHOC protocol, designed for deployment on IoT devices. Sapic+ enables the translation of a single model into three different tools (Tamarin, ProVerif, and DeepSec), allowing us to leverage the strengths of each. This approach led to the discovery of several vulnerabilities, and our proposed fixes were integrated into subsequent versions of the protocol. Later, I extended Tamarin to support user-defined associative and commutative symbols. To achieve this, I designed an algorithm along with new reduction rules to handle infinite chains of constructors/destructors, which often arise from such symbols. This extension enabled the modeling of new cryptographic primitives, such as re-encryption. »

Résumé :

 » Durant ma thèse, j’ai étudié le prouveur Tamarin, un outil de vérification de protocoles cryptographiques, en me concentrant d’abord sur la modélisation puis sur l’amélioration de ses mécanismes internes. J’ai d’abord utilisé la plateforme Sapic+, intégrée à Tamarin, pour modéliser la version 12 du protocole LAKE-EDHOC, conçu pour être déployé sur des objets connectés. Sapic+ permet de traduire un même modèle vers trois outils différents (Tamarin, ProVerif et DeepSec), ce qui nous permet de tirer parti des forces de chacun. Cette approche a conduit à la découverte de plusieurs vulnérabilités, et les correctifs que nous avons proposés ont été intégrés dans les versions ultérieures du protocole. Par la suite, j’ai intégré à Tamarin la prise en charge des symboles associatifs et commutatifs définis par l’utilisateur. Pour ce faire, j’ai conçu un algorithme ainsi que de nouvelles règles de réduction pour gérer les chaînes infinies de constructeurs/destructeurs, qui apparaissent souvent avec de tels symboles. Cette extension a permis la modélisation de nouvelles primitives cryptographiques, telles que le rechiffrement. «