Skip to Main content Skip to Navigation
Reports

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

https://hal.inria.fr/hal-02425229
Contributor : Bhargavan Karthikeyan <>
Submitted on : Wednesday, December 9, 2020 - 12:54:40 AM
Last modification on : Wednesday, December 9, 2020 - 9:24:24 AM
Long-term archiving on: : Wednesday, March 10, 2021 - 6:21:59 PM

File

mls-treekem.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02425229, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

291

Files downloads

287