International Association for Cryptologic Research

International Association
for Cryptologic Research

CryptoDB

Formally analyzing a cryptographic protocol standard (or: how MLS kept this PhD student busy for three years)

Authors:
Théophile Wallez
Download:
Search ePrint
Search Google
Presentation: Slides
Abstract: In this talk, we report on our experience in producing machine-checked security proofs for cryptographic protocol standards in all their gory detail, and more specifically for Messaging Layer Security (MLS). We outline the methodology we used to tackle this beast of a protocol, talk about the formal verification tools we developed along the way, and give some insights on protocol design, analysis, and standardization that we learned during this journey.
Video: https://youtu.be/doBiylWUBC0
BibTeX
@misc{rwc-2025-35848,
  title={Formally analyzing a cryptographic protocol standard (or: how MLS kept this PhD student busy for three years)},
  note={Video at \url{https://youtu.be/doBiylWUBC0}},
  howpublished={Talk given at RWC 2025},
  author={Théophile Wallez},
  year=2025
}