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
Abstract

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.

Metadata
Available format(s)
PDF
Category
Cryptographic protocols
Publication info
Preprint.
Keywords
mls messaging f* fstar dy* dystar symbolic dolev-yao
Contact author(s)
theophile wallez @ inria fr
protz @ microsoft com
beurdouche @ mozilla com
karthikeyan bhargavan @ inria fr
History
2022-12-19: approved
2022-12-16: received
See all versions
Short URL
https://ia.cr/2022/1732
License
Creative Commons Attribution-NonCommercial-NoDerivs
CC BY-NC-ND

BibTeX

@misc{cryptoeprint:2022/1732,
      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{https://eprint.iacr.org/2022/1732}},
      url = {https://eprint.iacr.org/2022/1732}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.