Lien visio : http://newyork.iut-clermont.uca.fr/b/leo-ygg-wnr-sxi

La Sécurité Après-Compromission (PCS pour Post-Compromise Security) est une propriété de sécurité concernant les schémas
d'établissement de canal sécurisé. Elle vise à limiter les failles de sécurité que pourrait introduire un attaquant en compromettant un
utilisateur. Le phénomène de guérison, qui est le résultat de la PCS, permet d'éjecter l'attaquant ce qui rend le canal à nouveau
sécurisé. Cette propriété intéressante, surtout depuis les révélations d'Edward Snowden concernant la surveillance de masse, se retrouve dans
la plupart des protocoles de messageries populaires, notamment Signal.

Dans cette thèse, nous présentons dans un premier temps deux variantes de Signal ; ces deux protocoles (MARSHAL et SAMURAI) sont construits
pour améliorer la propriété de PCS. En faisant l'observation que la PCS n'est pas une propriété binaire mais plutôt un spectre de
possibilités, nous proposons dans un second chapitre un modèle pour quantifier et comparer la PCS en fonction du type d'adversaire
considéré. Nous détaillerons d'ailleurs tous les adversaires possibles pour notre contexte. La généralité et flexibilité de notre approche
nous permet de modéliser une vaste diversité de protocoles, en particulier Signal mais aussi une nos variante décrite dans le premier
chapitre, ainsi qu'une autre variante (SAID) de Signal mais basé sur l'identité. Un dernier cas est analysé, montrant l'expressivité de
notre modèle, celui d'une série de procédure pour le réseau 5G nommée protocoles relais. L'étude de ce dernier cas nous amène à proposer une
amélioration concernant la PCS pour un protocole de relais.

La dernière partie de cette thèse se concentre sur un problème lié à la sécurité, l'attestation dans le contexte de
virtualisation. L'attestation en profondeur, un type d'attestation, permet de vérifier l'intégrité d'une plateforme à l'aide d'un serveur
de vérification à distance. Nous nous concentrons sur l'attestation d'hyperviseurs et de machines virtuelles. Il existe deux solutions
standardisées, la première permet d'attester l'hyperviseur et la machine virtuelle en même temps alors que la deuxième permet
d'attester indépendamment ces deux composants. Nous proposons une solution qui regroupe les avantages de ces deux alternatives (sécurisé
et efficace) dans un modèle inédit. Le but est de formaliser un modèle de sécurité visant à prouver la sécurité de notre approche.

Jury :

• Pascal LAFOURCADE, LIMOS Université Clermont Auvergne (directeur de thèse);
• Cristina ONETE, XLIM Université de Limoges (directrice de thèse);
• Benjamin NGUYEN, LIFO INSA Centre Val de Loire (Rapporteur);
• Melek ÖNEN, EURECOM Sophia-Antipolis (Rapporteure);
• Karthikeyan BHARGAVAN, INRIA de Paris (Examinateur);
• Jean-Guillaume DUMAS, LJK Université Grenoble Alpes (Examinateur);
• David POINTCHEVAL, INRIA, PSL, ENS Paris (Examinateur);
• Olivier SANDERS, Orange Labs Cesson-Sevigne (Examinateur);

Toutes les informations mises à jour sont sur mon site personnel : https://perso.limos.fr/~leorober/