Paper 2025/410
TreeKEM: A Modular Machine-Checked Symbolic Security Analysis of Group Key Agreement in Messaging Layer Security
, Inria Paris, Microsoft Azure Research, CryspenAbstract
The Messaging Layer Security (MLS) protocol standard proposes a novel tree-based protocol that enables efficient end-to-end encrypted messaging over large groups with thousands of members. Its functionality can be divided into three components: TreeSync for authenticating and synchronizing group state, TreeKEM for the core group key agreement, and TreeDEM for group message encryption. While previous works have analyzed the security of abstract models of TreeKEM, they do not account for the precise low-level details of the protocol standard. This work presents the first machine-checked security proof for TreeKEM. Our proof is in the symbolic Dolev-Yao model and applies to a bit-level precise, executable, interoperable specification of the protocol. Furthermore, our security theorem for TreeKEM composes naturally with a previous result for TreeSync to provide a strong modular security guarantee for the published MLS standard.
Metadata
- Available format(s)
-
PDF
- Category
- Cryptographic protocols
- Publication info
- Preprint.
- Keywords
- mlsmessagingf*fstardy*dystarsymbolicdolev-yao
- Contact author(s)
-
theophile wallez @ inria fr
protz @ microsoft com
karthik @ cryspen com - History
- 2025-03-04: approved
- 2025-03-04: received
- See all versions
- Short URL
- https://ia.cr/2025/410
- License
-
CC BY-NC-ND
BibTeX
@misc{cryptoeprint:2025/410,
author = {Théophile Wallez and Jonathan Protzenko and Karthikeyan Bhargavan},
title = {{TreeKEM}: A Modular Machine-Checked Symbolic Security Analysis of Group Key Agreement in Messaging Layer Security},
howpublished = {Cryptology {ePrint} Archive, Paper 2025/410},
year = {2025},
url = {https://eprint.iacr.org/2025/410}
}
