Skip to Main content Skip to Navigation
New interface
Reports (Research report)

Formal Models and Verified Protocols for Group Messaging: Attacks and Proofs for IETF MLS

Abstract : Group conversations are supported by most modern messaging applications, but the security guarantees they offer are significantly weaker than those for two-party protocols like Signal. The problem is that mechanisms that are efficient for two parties do not scale well to large dynamic groups where members may be regularly added and removed. Further, group messaging introduces subtle new security requirements that require new solutions. The IETF Messaging Layer Security (MLS) working group is standardizing a new asynchronous group messaging protocol that aims to achieve strong guarantees like forward secrecy and post-compromise security for large dynamic groups. In this paper, we define a formal framework for group messaging in the F language and use it to compare the security and performance of several candidate MLS protocols up to draft 7. We present a succinct, executable, formal specification and symbolic security proof for TreeKEMB, the group key establishment protocol in MLS draft 7. Our analysis finds new attacks and we propose verified fixes, which are now being incorporated into MLS. Ours is the first mechanically checked proof for MLS, and our analysis technique is of independent interest, since it accounts for groups of unbounded size, stateful recursive data structures, and fine-grained compromise.
Complete list of metadata
Contributor : Bhargavan Karthikeyan Connect in order to contact the contributor
Submitted on : Wednesday, December 9, 2020 - 12:54:40 AM
Last modification on : Thursday, October 27, 2022 - 4:02:31 AM
Long-term archiving on: : Wednesday, March 10, 2021 - 6:21:59 PM


Files produced by the author(s)


  • HAL Id : hal-02425229, version 1


Karthikeyan Bhargavan, Benjamin Beurdouche, Prasad Naldurg. Formal Models and Verified Protocols for Group Messaging: Attacks and Proofs for IETF MLS. [Research Report] Inria Paris. 2019. ⟨hal-02425229⟩



Record views


Files downloads