Théophile Wallez
LightNews LightNews
twal.org
Théophile Wallez
@twal.org
80 followers 37 following 7 posts
Post-doc researcher at CISPA, working on secure group messaging & machine-checked security proofs.
Posts Replies Media Videos
twal.org
New paper on the formal analysis of TreeKEM is out!
Some explanations below. 🧵
eprint.ing.bot ePrint Updates @eprint.ing.bot · Mar 4
TreeKEM: A Modular Machine-Checked Symbolic Security Analysis of Group Key Agreement in Messaging Layer Security (Théophile Wallez, Jonathan Protzenko, Karthikeyan Bhargavan) ia.cr/2025/410
Abstract. 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.
March 4, 2025 at 7:02 PM