Vérification formelle appliquée : étude d'un cas concret et amélioration du support des opérateurs AC dans Tamarin
Formal Verification in Practice: Real-World Case Study and Enhanced Support for AC Operators in Tamarin
Jury
Directeur de these_KREMER_Steve_Centre Inria de l'Université de Lorraine
Rapporteur_CHEVALIER_Yannick_Université de Toulouse
Rapporteur_FILA_Barbara_INSA de Rennes
CoDirecteur de these_DREIER_Jannik_Université de Lorraine
Président_BAELDE_David_ENS Rennes
Examinateur_IGNAT_Claudia_Centre Inria de l'Université de Lorraine
Examinateur_BOUREANU_Ioana_University of Surrey
école doctorale
IAEM - INFORMATIQUE - AUTOMATIQUE - ELECTRONIQUE - ELECTROTECHNIQUE - MATHEMATIQUES
Laboratoire
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Mention de diplôme
Informatique
A008
Bâtiment Ada Lovelace, 615 Rue du Jardin-Botanique, 54600, Villers-lès-Nancy
Mots clés
Cybersécurité,Vérification,Logique,Protocole cryptographique,Sécurité,
Résumé de la thèse
Nous présentons dans cette thèse deux contributions principales :
- Analyse formelle approfondie du protocole EDHOC : EDHOC (Ephemeral Diffie-Hellman Over COSE) est un protocole d'échange de clés proposé par le groupe de travail LAKE (Lightweight Authenticated Key Exchange) de l'IETF. Il a été conçu pour minimiser la taille des messages, afin de s'adapter aux technologies de communication contraignantes utilisées dans l'Internet des objets (IoT).
Keywords
Cybersecurity,Verification,Logic,Cryptographic protocol,Security,
Abstract
We present in this thesis two main contributions:
- Comprehensive formal analysis of the EDHOC protocol: EDHOC (Ephemeral Diffie Hellman Over COSE) is a key exchange proposed by IETF's Lightweight Authenticated Key Exchange (LAKE) working group. Its design focuses on small message sizes to be suitable for constrained IoT communication technologies. We provide an in-depth formal analysis of EDHOC-draft version 12 (published in October 2021), taking into account the different proposed authentication methods and various options.
