Vérification symbolique de protocoles cryptographiques en F*: application au sous-protocole TreeSync de MLS - Trente-Quatrièmes Journées Francophones des Langages Applicatifs Accéder directement au contenu
Communication Dans Un Congrès Année : 2023

Vérification symbolique de protocoles cryptographiques en F*: application au sous-protocole TreeSync de MLS

Résumé

TreeSync est un sous-protocole d'authentification pour MLS, un protocole de messagerie de groupe sécurisé en cours de standardisation à l'IETF. Nous formalisons MLS en F* , et présentons un théorème de sécurité pour TreeSync à l'aide du cadriciel de cryptographie symbolique DY*. Afin de comprendre les hypothèses clés qui permettent d'exprimer un tel théorème, nous présentons en détail le fonctionnement interne de DY*. Au cours de notre analyse, nous avons proposé plusieurs changements à TreeSync qui ont été intégrés à MLS, et avons développé de nouvelles méthodes de preuves pour passer à l'échelle avec DY* afin de pouvoir s'attaquer à un gros protocole comme MLS, par exemple, un mécanisme permettant à la fois l'exécution concrète et symbolique du protocole, la génération automatique de parseurs et sérialiseurs binaires vérifiés, ou encore la génération d'invariants globaux du protocole à partir d'invariants locaux.
Fichier principal
Vignette du fichier
jfla23_paper_4053.pdf (478.61 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-03936726 , version 1 (12-01-2023)

Identifiants

  • HAL Id : hal-03936726 , version 1

Citer

Théophile Wallez. Vérification symbolique de protocoles cryptographiques en F*: application au sous-protocole TreeSync de MLS. JFLA 2023 - 34èmes Journées Francophones des Langages Applicatifs, Jan 2023, Praz-sur-Arly, France. pp.243-263. ⟨hal-03936726⟩
58 Consultations
116 Téléchargements

Partager

Gmail Facebook X LinkedIn More