English below

Lucca Hirschi (équipe Pesto) soutiendra son Habilitation à Diriger des Recherches le lundi 2 novembre 2026 à 14h00 en salle C005. La présentation se fera en anglais.

Titre :

“Formal Methods and Real-World Cryptographic Protocols: Advancing the Verification and Testing Frontiers for Specifications and Implementations”

Résumé :

 » Les protocoles cryptographiques sont les garants de nos échanges numériques sécurisés, piliers technologiques de notre société de l’information. L’histoire répétée d’attaques exploitant les erreurs de conception et d’implémentation de ces protocoles n’a de cesse de démontrer leur fragilité. Ce manuscrit aborde un défi central de la sécurité informatique : comment obtenir de meilleures garanties pour les protocoles cryptographiques ?

Premièrement, nous présentons des avancées fondamentales en méthodes formelles, introduisant de nouvelles techniques de modélisation, des algorithmes de vérification et des méthodologies de preuve dans le modèle Dolev-Yao visant à garantir formellement la sécurité des protocoles cryptographiques face à leur modèle d’attaquant. Deuxièmement, nous les mettons en application à grande échelle dans des analyses de sécurité de protocoles largement déployés. Nous détaillons notamment la découverte de vulnérabilités critiques et leur correction dans des protocoles majeurs tels que les standards industriels de la téléphonie mobile (4G et 5G) et des systèmes de contrôle industriels (OPC UA), ainsi que le système de vote électronique français (FLEP) déployé pour les élections législatives. Enfin, nous ciblons l’écart entre la vérification formelle des spécifications de protocoles et la sécurité de leurs implémentations en introduisant une nouvelle approche de test par fuzzing guidée par le modèle formel de Dolev-Yao. Ce nouveau paradigme de test logiciel permet la découverte automatique d’attaques logiques causées par des bugs dans des implémentations de protocoles cryptographiques complexes. Nous démontrons son efficacité, notamment par la détection de plusieurs nouvelles vulnérabilités et de dizaines de bugs dans des implémentations de protocoles parmi les plus testés (TLS et SSH).  »

La soutenance sera suivie d’un pot en salle club du Loria.

Informations pratiques

Toutes les informations pratiques sont regroupées sur la page dédiée : https://members.loria.fr/LHirschi/hdr/

Le manuscrit (version provisoire) y est déjà disponible et les transparents y seront mis en ligne. Pour celles et ceux qui souhaitent suivre la soutenance à distance, un lien de visioconférence sera publié sur cette page la veille.

Jury

Rapporteurs :

• Gilles Barthe, Directeur scientifique, Max Planck Institute for Security and Privacy (MPI-SP), Allemagne & IMDEA Software Institute, Espagne
• Karthik Bhargavan, Chief Research Scientist, Cryspen, France
• Ralf Küsters, Professeur, Université de Stuttgart, Allemagne

Examinateurs et examinatrices :

• David Basin, Professeur, ETH Zurich, Suisse
• Anne Canteaut, Directrice de recherche, Inria Paris, France
• Jean-Yves Marion, Professeur, Université de Lorraine, LORIA, France
• Catuscia Palamidessi, Directrice de recherche, Inria Saclay, LIX, France
• Olivier Pereira, Professeur, UCLouvain, Belgique

Invités :

• Thorsten Holz, Directeur scientifique, Max Planck Institute for Security and Privacy (MPI-SP), Allemagne
• Steve Kremer, Directeur de recherche, Inria Nancy – Grand Est, LORIA, France

Lucca Hirschi (Pesto team) will defend his HDR on Monday, November 2 at 2:00 pm in room C005. The presentation will be held in English.

Title:

“Formal Methods and Real-World Cryptographic Protocols: Advancing the Verification and Testing Frontiers for Specifications and Implementations”

Abstract:

« Cryptographic protocols are the backbone of secure digital communication and a key technological pillar of our information society. Yet a long history of attacks exploiting both design flaws and implementation bugs has repeatedly exposed their fragility. This manuscript addresses a central challenge in computer security: how can we achieve higher assurance for cryptographic protocols?

First, we present foundational advances in formal methods, introducing new modeling techniques, verification algorithms, and proof methodologies within the Dolev-Yao model that aim to provide formal security guarantees for cryptographic protocols against a powerful network attacker. Second, we put these methods into practice through large-scale security analyses of widely deployed protocols. In particular, we detail the discovery and remediation of critical vulnerabilities—since fixed—in major protocols, including mobile telephony standards (4G and 5G), industrial control system standards (OPC UA), and the French electronic voting system (FLEP) deployed for national elections. Finally, we address the gap between the formal verification of protocol specifications and the security of their real-world implementations by introducing a novel Dolev-Yao model-guided fuzzing approach. This new software testing paradigm enables the automatic discovery of logical attacks caused by implementation bugs in complex cryptographic protocols. We demonstrate its effectiveness through the detection of several previously unknown vulnerabilities and dozens of bugs in implementations of TLS and SSH—some of the most extensively tested protocols. »

The defense will be followed by drinks starting at around 4:00–5:00 PM in the « Salle Club » at LORIA, to which you are warmly invited.

Practical information

All practical details are gathered on the dedicated webpage: https://members.loria.fr/LHirschi/hdr/
A draft of the manuscript is already available there, and the slides will be uploaded later. For remote attendees, the video conference link will be posted on that same page the day before the defense.

Committee

Reviewers:

• Gilles Barthe, Scientific Director, Max Planck Institute for Security and Privacy (MPI-SP), Germany & IMDEA Software Institute, Spain
• Karthik Bhargavan, Chief Research Scientist, Cryspen, France
• Ralf Küsters, Professor, University of Stuttgart, Germany

Examiners:

• David Basin, Professor, ETH Zurich, Switzerland
• Anne Canteaut, Research Director, Inria Paris, France
• Jean-Yves Marion, Professor, Université de Lorraine, LORIA, France
• Catuscia Palamidessi, Research Director, Inria Saclay, LIX, France
• Olivier Pereira, Professor, UCLouvain, Belgium

Guests:

• Thorsten Holz, Scientific Director, Max Planck Institute for Security and Privacy (MPI-SP), Germany
• Steve Kremer, Research Director, Inria Nancy – Grand Est, LORIA, France

The defense will be followed by drinks in the « Salle Club » at Loria.