Paper 2022/1732

TreeSync: Authenticated Group Management for Messaging Layer Security

Théophile Wallez, Inria Paris
Jonathan Protzenko, Microsoft Research
Benjamin Beurdouche, Mozilla
Karthikeyan Bhargavan, Inria Paris

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.

Available format(s)
Cryptographic protocols
Publication info
Contact author(s)
theophile wallez @ inria fr
protz @ microsoft com
beurdouche @ mozilla com
karthikeyan bhargavan @ inria fr
2023-03-01: revised
2022-12-16: received
See all versions
Short URL
Creative Commons Attribution-NonCommercial-NoDerivs


      author = {Théophile Wallez and Jonathan Protzenko and Benjamin Beurdouche and Karthikeyan Bhargavan},
      title = {TreeSync: Authenticated Group Management for Messaging Layer Security},
      howpublished = {Cryptology ePrint Archive, Paper 2022/1732},
      year = {2022},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.