Doctorant en Vérification de protocoles avec opérateurs AC à l'aide de PROVERIF. (H/F)

Description du Poste

Sujet De Thèse

La vérification formelle repose sur des techniques de raisonnement mathématique pour établir des propriétés de systèmes distribués complexes. Dans les cadres de vérification symbolique, les comportements du système et les manipulations de données sont représentés sous forme de termes algébriques et analysés à l’aide de procédures de déduction automatisées. Une difficulté centrale dans ce contexte réside dans le traitement des structures algébriques satisfaisant des propriétés équationnelles non triviales, en particulier l’associativité et la commutativité. La prise en charge de telles théories augmente considérablement la complexité des procédures de raisonnement automatisé et soulève des questions fondamentales concernant la correction, la complétude et la terminaison.
ProVerif est un outil de raisonnement automatisé largement utilisé, basé sur une traduction des problèmes de vérification en clauses de Horn [5], ainsi que sur une procédure de résolution dont la correction est prouvée [1, 2]. Bien que la correction soit garantie, la terminaison n’est pas assurée en général, bien qu’elle soit souvent observée en pratique.
Plusieurs extensions ont été étudiées afin d’intégrer les théories associatives-commutatives (AC) dans ce cadre, y compris les théories liées au XOR, aux groupes abéliens et à l’exponentiation de Diffie-Hellman, principalement par le biais de techniques de prétraitement [4]. Cependant, ces approches présentent des limites importantes et n’ont pas été intégrées dans l’outil principal. Récemment, nous avons étendu ProVerif pour prendre en charge le XOR dans l’analyse des propriétés d’accessibilité [3]. En nous appuyant sur ce travail, l’objectif de ce projet de thèse est de développer de nouvelles techniques de résolution capables de gérer des classes plus riches de théories équationnelles associatives-commutatives dans le même cadre de raisonnement automatisé.

Objectifs du projet de thèse
Le premier objectif du projet de thèse sera d’acquérir une compréhension approfondie du moteur de résolution de ProVerif et de ses fondements théoriques.
L’objectif scientifique principal consistera ensuite à étendre cette procédure de résolution pour prendre en charge des théories équationnelles associatives-commutatives supplémentaires, telles que les groupes abéliens (AG), l’exponentiation de Diffie-Hellman ou les appariements bilinéaires. L’accent sera d’abord mis sur les propriétés d’accessibilité.
Plus précisément, le projet de thèse comportera les tâches suivantes :

Concevoir une nouvelle procédure de résolution en adaptant le cadre existant pour prendre en charge des théories associatives-commutatives plus riches ;
Établir les propriétés de correction et, dans la mesure du possible, de complétude de la procédure proposée ;
Implémenter la nouvelle procédure dans le code source de ProVerif et évaluer son comportement pratique, en prêtant une attention particulière aux questions d’évolutivité et de terminaison.
Ces trois axes de recherche sont étroitement interconnectés. En particulier, si la procédure proposée présente un comportement de terminaison médiocre en pratique, le cadre théorique devra être affiné en conséquence.
Une fois qu’une première extension aura été développée avec succès, plusieurs pistes de recherche pourront être explorées, notamment :

l’analyse des propriétés d’équivalence ;
la prise en charge d’opérateurs associatifs-commutatifs définis par l’utilisateur.

Références
[1] Bruno Blanchet. An efficient cryptographic protocol verifier based on prolog rules. Dans 14th IEEE Computer Security Foundations Workshop (CSFW-14 2001), 11-13 juin 2001, Cape Breton, Nouvelle-Écosse, Canada, pages 82–96. IEEE Computer Society, 2001.
[2] Bruno Blanchet, Vincent Cheval, et Véronique Cortier. Proverif with lemmas, induction, fast subsumption, and much more. Dans Proceedings of the 42nd IEEE Symposium on Security and Privacy (S&P’22). IEEE Computer Society Press, 2022.
[3] Vincent Cheval et Stéphanie Delaune. Symbolic protocol verification modulo xor in proverif. Dans Proceedings of the 33rd ACM Conference on Computer and Communications Security (CCS’26). ACM Press, novembre 2026.
[4] Ralf Küsters et Tomasz Truderung. Reducing protocol analysis with XOR to the xor-free case in the horn theory based approach. J. Autom. Reason., 46(3-4) : 325–352, 2011.
[5] ProVerif. https://bblanche.gitlabpages.inria.fr/proverif/, 2001.

La thèse est financée par le projet SVP (PEPR Cybersécurité).
https://pepr-cyber-svp.cnrs.fr/

Mots-clés
Protocoles, vérification formelle, modèle symbolique, opérateurs AC, ProVerif

Nom et adresse e-mail de la directrice de thèse
Stéphanie Delaune, Stephanie.Delaune@irisa.fr

Votre Environnement de Travail

A propos du laboratoire
=============
www.irisa.fr
L'IRISA est aujourd'hui l'un des plus grands laboratoires de recherche français (plus de 850 personnes) dans le domaine de l'informatique et des technologies de l'information. Structuré en sept départements scientifiques, l'IRISA est un laboratoire d'excellence dont les priorités scientifiques sont la bioinformatique, la sécurité des systèmes, les nouvelles architectures logicielles, la réalité virtuelle, l'analyse des big data et l'intelligence artificielle. Tourné vers l'avenir de l'informatique et nécessairement tourné vers l'international, l'IRISA est au cœur même de la transition numérique de la société et de l'innovation au service de la cybersécurité, de la santé, de l'environnement et de l'écologie, des transports, de la robotique, de l'énergie, de la culture et de l'intelligence artificielle.

Présentation du CNRS en tant qu'employeur : https://www.cnrs.fr/fr/le-cnrs
Présentation de l'IRISA comme laboratoire d'affectation : https://www.irisa.fr/umr-6074

Le poste se situe dans un secteur relevant de la protection du potentiel scientifique et technique (PPST), et nécessite donc, conformément à la réglementation, que votre arrivée soit autorisée par l'autorité compétente du MESR.

Le poste se situe dans un secteur relevant de la protection du potentiel scientifique et technique (PPST), et nécessite donc, conformément à la réglementation, que votre arrivée soit autorisée par l'autorité compétente du MESR.

Rémunération et avantages

Rémunération

La rémunération est d'un minimum de 2300,00 € mensuel

Congés et RTT annuels

44 jours

Pratique et Indemnisation du TT

Pratique et indemnisation du TT

Transport

Prise en charge à 75% du coût et forfait mobilité durable jusqu’à 300€

À propos de l’offre

À propos du CNRS

Le CNRS est un acteur majeur de la recherche fondamentale à une échelle mondiale. Le CNRS est le seul organisme français actif dans tous les domaines scientifiques. Sa position unique de multi-spécialiste lui permet d’associer les différentes disciplines pour affronter les défis les plus importants du monde contemporain, en lien avec les acteurs du changement.

Le CNRS

Les métiers de la recherche