In the paper, we provide a detailed yet accessible description of TreeKEM internals (Section 2). If you always wanted to know how TreeKEM works but were too scared to read the huge and intimidating RFC, this is another reason to read the paper! eprint.iacr.org/2025/410

In turn, our security theorem implies many nice properties on TreeKEM's shared secret, such as forward secrecy and post-compromise security. Furthermore, the security theorem can be audited and provides insights on the secure deployments of MLS, that we reported to the MLS Working Group.

Our theorem consider an active attacker that may steal secret keys of the group participants (e.g. if a smartphone is scanned at a border control). We prove that if an attacker knows TreeKEM's shared secret, they must have stolen some participant's secret keys (and tell precisely which secret keys).

In this paper, we provide a machine-checked security proof for TreeKEM. To our knowledge, this is the first machine-checked security proof for a group key exchange in the context of dynamic groups (participants can join and leave). Furthermore, our specification is bit-precise and interoperable!

TreeKEM is a sub-protocol of MLS in charge of establishing a shared secret keys between participants of a group, which is then used by another sub-protocol to encrypt messages. Hence, the strong confidentiality guarantees provided by MLS rely on the strong secrecy of TreeKEM's shared secret.

MLS is a recent secure group messaging protocol designed to handle large groups while providing strong confidentiality guarantees, such as forward secrecy and post-compromise security (more on these notions here www.twal.org/blog/0001_wh... ).

New paper on the formal analysis of TreeKEM is out!
Some explanations below. 🧵