Paper 2025/229 Original: eprint.iacr.org/2025/229 ↗

ETK: External-Operations TreeKEM and the Security of MLS in RFC 9420

Abstract

The Messaging Layer Security protocol MLS is standardized in IETF's RFC 9420 and allows a group of parties to securely establish and evolve group keys even if the servers are malicious. The core design of MLS is based on the TreeKEM protocol, which was significantly modified and extended during the standard's development. Over the last years, several partial security analyses have appeared of incomplete drafts of the standard. One of the major additions to MLS RFC 9420 (the final version of the standard) are the external operations, i.e., external commits and proposals. These additional operations have not been considered in any previous security analysis, while they can have a significant impact on the standard's security. In this work, we prove the consistency, confidentiality and authentication of MLS in RFC 9420. To this end, we formalize $\mathsf{ETK}$: External-Operations TreeKEM, which models RFC 9420 and includes the external commits and proposals. We propose a corresponding ideal functionality $\mathcal{F}_{\mathrm{ECGKA}}$ and prove that $\mathsf{ETK}$ realizes it. Our work is the first cryptographic analysis that considers both the final changes to the standard, and the first approach overall to cover external proposals and external commits. Compared to previous works that considered MLS drafts, our $\mathsf{ETK}$ protocol is by far the closest to the final MLS RFC 9420 standard. Our analysis implies that the core of MLS in RFC 9420 is an $\mathsf{ETK}$ protocol that realizes $\mathcal{F}_{\mathrm{ECGKA}}$. Notably, we show that when external proposals and commits are allowed, MLS achieves a weaker form of security than was suggested by previous analyses, because the external operations can be exploited to violate Post-Compromise Security guarantees. We show that the security of the protocol can be further strengthened by leveraging the standard's optional PSK mechanism, allowing another form of healing, and give a corresponding construction $\mathsf{ETK}^{\mathrm{PSK}}$ and ideal functionality $\mathcal{F}_{\mathrm{ECGKA}^{\mathrm{PSK}}}$.