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

Vos missions en quelques mots 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érificati Voir plus sur le site emploi.cnrs.fr Profil recherché Contraintes et risques : Niveau d'études minimum requis Niveau Niveau 8 Doctorat/diplômes équivalents Spécialisation Formations générales Langues Français Seuil