Doctorant en modélisation formelle des cérémonies de sécurité. (h/f)

Description du Poste Sujet De Thèse Au cours des trois dernières décennies, de nombreux modèles et outils ont été développés et se sont avérés très efficaces pour détecter des failles de sécurité dans les protocoles de communication [[1](#), [2](#), [3](#), [4](#), [5](#)]. Cependant, lors de l’analyse des interactions au sein d’un système distribué, il est insuffisant de se concentrer uniquement sur la couche technique des protocoles. Les systèmes actuels impliquent non seulement des entités informatiques (ordinateurs, serveurs), mais aussi des objets physiques (appareils IoT, smartphones, puces) et des humains (utilisateurs, clients), dont les faiblesses et l’impact doivent être pris en compte dans l’analyse de la sécurité du système.Pour relever ce défi, Ellison a introduit la notion de **cérémonies de sécurité**, qui étendent les protocoles de communication classiques en intégrant des aspects que ces derniers considéraient comme externes [[6](#)]. Une cérémonie rassemble les composants techniques, physiques et humains du système, ainsi que l’environnement dans lequel il est déployé. En 2024, Fila et Radomirovic ont proposé un cadre formel générique pour la spécification et la vérification des cérémonies de sécurité [[7](#)]. Ce cadre permet de modéliser différents types d’agents (machines, humains, objets physiques, droits juridiques) et prend en charge le raisonnement sur les interactions synchrones entre un nombre fini quelconque d’agents.L’objectif de ce projet doctoral est de poursuivre la ligne de recherche initiée dans [[7](#)] et de développer une méthodologie scientifique complète pour l’analyse pratique des cérémonies de sécurité. Cela inclut des recherches fondamentales sur la modélisation et l’analyse des cérémonies et des propriétés de sécurité sous-jacentes, l’automatisation de la vérification des cérémonies, ainsi que la validation des outils théoriques et informatiques proposés sur des études de cas réels. En particulier, le doctorant abordera les défis de recherche suivants :---1.Les approches existantes pour la vérification des cérémonies reposent sur des propriétés de sécurité conçues pour les protocoles, comme la confidentialité, l’authentification ou l’anonymat. Cependant, ces propriétés ne tiennent pas compte des particularités spécifiques aux agents humains ni des caractéristiques des objets physiques. Une étude des exigences de sécurité et fonctionnelles pour les cérémonies sera menée afin d’identifier et de définir formellement des propriétés pertinentes dans ce contexte élargi. L’objectif est de concevoir de nouvelles propriétés intégrant des notions telles que le **consentement**, l’**intention** et l’**origine**, nécessaires pour garantir le niveau de sécurité attendu dans un système distribué, du point de vue humain.---2.De nombreuses tentatives de recherche ont montré qu’il était possible, mais peu pratique et inefficace, d’utiliser des outils conçus pour la vérification de protocoles afin d’analyser des cérémonies [[7](#), [8](#)]. La modélisation du comportement non déterministe des humains dans ces outils est complexe, et l’utilisation de règles d’inférence non monotones (nécessaires pour modéliser des actions comme l’oubli, la perte ou la récupération) pose un défi majeur pour les algorithmes classiques de résolution de contraintes. Nowar et al. ont récemment développé un prototype d’outil pour la vérification des cérémonies [[8](#)]. Cet outil utilise une approche de recherche directe (*forward search*), et son moteur de vérification s’inspire de la réécriture de graphes. Les tests préliminaires ont montré des résultats prometteurs en termes de fonctionnalité et d’efficacité. Le doctorant contribuera au développement futur de cet outil. L’objectif principal sera d’étendre ses capacités à gérer divers types de propriétés (formules LTL, CTL, logiques du premier ordre et d’ordre supérieur) et d’améliorer les algorithmes sur lesquels il repose pour optimiser davantage l’efficacité de la vérification.---3.Le cadre de modélisation issu de [[7](#)] et l’outil associé seront validés sur des cérémonies réelles, comme le vote électronique. L’objectif est d’identifier des **stratégies** et des **heuristiques** pour guider le modélisateur dans une utilisation pratique du cadre, une piste de recherche déjà initiée dans [[9](#)]. Des motifs de modélisation pour les interactions typiques avec des appareils physiques, critiques pour la sécurité et connectés en réseau seront développés, et une collection de cérémonies contextuelles utiles sera constituée.------**Références**[1] R. Gil-Pons, R. Horne, S. Mauw, F. Stutz, S. Yurkov, *Security Protocols and Threat Models -- Security and Privacy via The Applied π-Calculus*, Information Security and Cryptography, Springer 2026, ISBN 978-3-032-08248-0, pp. 3-216.[2] V. Cortier, S. Kremer, *Formal Models and Techniques for Analyzing Security Protocols*, Cryptology and Information Security Series 5, IOS Press 2011, ISBN 978-1-60750-713-0.[3] D. A. Basin, C. Cremers, J. Dreier, R. Sasse, *Modeling and Analyzing Security Protocols with Tamarin - A Comprehensive Guide*, Information Security and Cryptography, Springer 2026, ISBN 978-3-031-90935-1, pp. 3-276.[4] D. A. Basin, C. Cremers, J. Dreier, S. Meier, R. Sasse, et B. Schmidt, *Tamarin Prover*, [https://tamarin-prover.github.io/](https://tamarin-prover.github.io/).[5] B. Blanchet et V. Cheval, *ProVerif: Cryptographic protocol verifier in the formal model*, [https://bblanche.gitlabpages.inria.fr/proverif/](https://bblanche.gitlabpages.inria.fr/proverif/).[6] C. M. Ellison, *Ceremony design and analysis*, IACR Cryptol. 2007.[7] B. Fila, S. Radomirovic, *Nothing is out-of-band: formal modeling of ceremonies*, CSF 2024 : 464-478.[8] B. Fila, N. Kazem, S. Radomirovic, *Automating the verification of security ceremonies* (en cours de soumission), 2026.[9] B. Fila, E. Hoxha, *Pragmatic Guidelines for Formal Modeling of Security Ceremonies*, STM 2025 : 43-62. Votre Environnement de Travail A propos du laboratoire=============www.irisa.frL'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-cnrsPrésentation de l'IRISA comme laboratoire d'affectation : https://www.irisa.fr/umr-6074Le 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 Référence de l’offre UMR6074-BENJOS-003 Section(s) CN / Domaine de recherche Sciences informatiques : fondements de l'informatique, calculs, algorithmes, représentations, exploitations À 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