This work presents a formal specification and security proof for an important component of the new Messaging Layer Security Protocol (MLS) standard and represents several years of collaboration with the IETF MLS working group.
Théophile Wallez is a PhD student in the Prosecco team at Inria Paris. His work is funded by PR[AI]RIE and focuses on the formal security and privacy analysis of large-scale multi-party cryptographic protocols.
Karthikeyan Bhargavan is Directeur de Recherche at Inria Prosecco and a Prairie Chaire. He is currently on a leave of absence to work on Cryspen, a Prairie Startup and associated partner that builds high-assurance security software for use in multiple domains, including privacy-preserving machine learning.
You can read the paper here.