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

Summary

The Messaging Layer Security protocol MLS is standardized in IETF’s RFC$$\text {RFC}$$  9420$$\text {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$$\text {RFC}$$  9420$$\text {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$$\text {RFC}$$  9420$$\text {9420}$$. To this end, we formalize ETK$$\textsf{ETK} $$ : External-Operations TreeKEM, which models RFC$$\text {RFC}$$  9420$$\text {9420}$$ and includes the external commits and proposals. We propose a corresponding ideal functionality FECGKA$$\mathcal {F_\textrm{ECGKA}}$$ and prove that ETK$$\textsf{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 ETK$$\textsf{ETK} $$ protocol is by far the closest to the final MLS RFC$$\text {RFC}$$  9420$$\text {9420}$$ standard.Our analysis implies that the core of MLS in RFC$$\text {RFC}$$  9420$$\text {9420}$$ is an ETK$$\textsf{ETK} $$ protocol that realizes FECGKA$$\mathcal {F_\textrm{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 ETKPSK$$\textsf{ETK} ^\textrm{PSK} $$ and ideal functionality FECGKAPSK$$\mathcal {F} _{\textrm{ECGKA}^\textrm{PSK}}$$.