SoSySec seminar Software and Systems Security
Inria - Rennes
Friday January 12, 11:00
Remotely via BBB: https://bbb.inria.fr/all-t0p-qjq-9em
Access code: 192737
-------------------------------------------------------
Théophile Wallez (Inria)
TreeSync: Authenticated Group Management for Messaging Layer Security
Messaging Layer Security (MLS), currently undergoing standardization at the IETF, is an asynchronous group messaging protocol that aims to be efficient for large dynamic groups, while providing strong guarantees like forward secrecy (FS) and post-compromise security (PCS). While prior work on MLS has extensively studied its group key establishment component (called TreeKEM), many flaws in early designs of MLS have stemmed from its group integrity and authentication mechanisms that are not as well-understood. In this work, we identify and formalize TreeSync: a sub-protocol of MLS that specifies the shared group state, defines group management operations, and ensures consistency, integrity, and authentication for the group state across all members. We present a precise, executable, machine-checked formal specification of TreeSync, and show how it can be composed with other components to implement the full MLS protocol. Our specification is written in F* and serves as a reference implementation of MLS; it passes the RFC test vectors and is interoperable with other MLS implementations. Using the DY* symbolic protocol analysis framework, we formalize and prove the integrity and authentication guarantees of TreeSync, under minimal security assumptions on the rest of MLS. Our analysis identifies a new attack and we propose several changes that have been incorporated in the latest MLS draft. Ours is the first testable, machine-checked, formal specification for MLS, and should be of interest to both developers and researchers interested in this upcoming standard.
To follow the presentation remotely, please connect to the followingURL with a modern web browser:
- URL: https://bbb.inria.fr/all-t0p-qjq-9em
Access code: 192737
- Alternative audio access by phone will be possible but the parameters will be announced only a few minutes before the presentation.
Seminar taking place in person with mandatory registration at least 48h beforehand for *all* in-person participants by email to Nadia Derouault < nadia [*] derouault
inria [*] fr >. Participants non-affiliated with Inria or IRISA will be asked to present an ID at the reception desk of the IRISA building.
To receive the SoSySec announcements, please subscribe to the SoSySec mailing list:
https://sympa.inria.fr/sympa/subscribe/sosysec
All past and future SoSySec talks are listed at
https://seminaires-dga.inria.fr/en/seances-a-venir/
----------------------------------------------------------------------
Séminaire en présentiel ouvert à tous et toutes mais avec inscription obligatoire au moins 48h à l'avance pour *tous* les participants en présentiel auprès de Nadia Derouault <nadia [*] derouaultinria [*] fr>.
Les participants externes devront se présenter à l'accueil avec une pièce d'identité.
Vous pouvez vous abonner à nos annonces de séminaires :
https://sympa.inria.fr/sympa/subscribe/sosysec
et consulter la liste des exposés passés et à venir :
https://seminaires-dga.inria.fr/seances-a-venir/