L’Ecole doctorale : Ecole Doctorale de l’Institut Polytechnique de Paris

et le Laboratoire de recherche SAMOVAR – Services répartis, Architectures, Modélisation, Validation, Administration des Réseaux

présentent

l’AVIS DE SOUTENANCE de Monsieur Arthur TRAN VAN

Autorisé à présenter ses travaux en vue de l’obtention du Doctorat de l’Institut Polytechnique de Paris, préparé à Télécom SudParis en :

Informatique

« Amélioration de l’implémentation des protocoles cryptographiques grâce à l’inférence grammaticale »

le MARDI 25 NOVEMBRE 2025 à 14h00

à

Amphithéâtre 3
19 Place Marguerite Perey, 91120 Palaiseau

https://webconf.imt.fr/frontend/rooms/4oc-jdn-ghh-dhb/join

Membres du jury :

M. Thomas CLAUSEN, Professeur, Ecole Polytechnique, FRANCE – Examinateur
M. Luca HIRSCHI, Chargé de recherche, Loria, FRANCE – Examinateur
M. Vincent NICOMETTE, Professeur, INSA Toulouse, FRANCE – Examinateur

M. Erik POLL, Full professor, Radboud University, PAYS-BAS – Rapporteur
Mme Valérie VIET TRIEM TONG, Professeure, Centrale Supélec, FRANCE – Rapporteur

M. Hervé DEBAR, Professeur, Télécom SudParis, FRANCE – Directeur de thèse
M. Olivier LEVILLAIN, Maître de conférences, Télécom SudParis, FRANCE – Co-encadrant de thèse

« Amélioration de l’implémentation des protocoles cryptographiques grâce à l’inférence grammaticale »

présenté par Monsieur Arthur TRAN VAN

Résumé :

Les protocoles réseaux cryptographiques, tels que SSH et OPC UA, sont essentiels dans la sécurisation des communications. Cependant, leurs spécifications sont souvent longues, ambiguës et incomplètes, entraînant des erreurs d’implémentation et des vulnérabilités exploitables. Sans accès au code source, la vérification de la conformité d’une implémentation à sa spécification devient particulièrement complexe et se limite à l’analyse des échanges avec l’implémentation. L’apprentissage actif d’automates (Active Automata Learning, AAL) permet de construire un automate pour la vérification formelle, via des interrogations dynamiques de l’implémentation. Toutefois, le coût élevé de cette méthode limite son adoption pratique. Cette thèse propose plusieurs contributions visant à améliorer l’efficacité et l’applicabilité de l’analyse de protocoles basée sur les automates. Tout d’abord, elle introduit un cadre unifié pour l’apprentissage actif adaptatif, permettant d’exploiter des spécifications partielles ou des modèles issus de versions antérieures afin de guider le processus d’apprentissage. Ce cadre généralise les stratégies adaptatives existantes et facilite l’intégration de nouvelles, aboutissant à un nouvel algorithme adaptatif, ALλ, qui réalise à la fois des gains de performance et permet d’étudier les limites de l’apprentissage actif adaptatif. Ensuite, elle s’attaque aux limites de la phase de vérification en présentant le Mealy Verifier, un outil spécialisé capable de fournir rapidement des ensembles exhaustifs de contre-exemples pour des propriétés spécifiques aux protocoles. Cet outil réduit le besoin d’itération d’extraction de modèle et de vérification. La méthode proposée est validée au travers d’études de cas sur OPC UA et SSH, permettant la découverte de vulnérabilités inédites. Enfin, dans un projet de recherche distinct mené durant la thèse, un protocole de stockage multi-cloud sécurisé est conçu et implémenté sous forme de preuve de concept, offrant des garanties renforcées en matière de confidentialité, d’intégrité et de récupérabilité des fichiers. Dans l’ensemble, ces travaux contribuent à rendre les méthodes formelles plus pratiques et plus évolutives pour la vérification des protocoles dans des environnements réels.

Abstract :

Cryptographic network protocols, such as SSH and OPC UA, are critical to secure communications. However, their specifications are often lengthy, ambiguous, and incomplete, leading to implementation inconsistencies and security vulnerabilities. Without access to the source code, verifying that an implementation complies with its specification becomes particularly complex and is limited to analyzing its interactions. Active automata learning (AAL) builds an automaton for verification by actively interrogating the protocol implementation. However, the high learning costs limit the adoption of this method in practice. This thesis introduces several contributions to improve the efficiency and applicability of automata-based protocol analysis. First, it presents a unified framework for adaptive AAL, allowing learners to leverage partial specifications or legacy models to guide the learning process. The framework generalizes existing adaptive strategies and supports the development of new ones, culminating in the novel adaptive learning algorithm ALλ, which both achieves performance gains and facilitates analysis of adaptive AAL’s limits. Second, the thesis addresses limitations in verification by introducing the Mealy Verifier, a specialized tool that rapidly identifies exhaustive sets of counterexamples for protocol-specific properties, reducing the number of costly model extraction and verification iterations. This method is validated through case studies on OPC UA and SSH, uncovering previously unknown vulnerabilities. Finally, although independent from the main line of contributions, the thesis presents the design and proof-of-concept implementation of a secure multi-cloud storage protocol, offering enhanced guarantees for privacy, integrity, and file retrievability. Overall, this thesis contributes to the broader objective of making formal methods more practical and scalable for real-world protocol verification.