Revisiting Post-Compromise Security Guarantees in Group Messaging.

Cas J. F. Cremers, Britta Hale, Konrad Kohbrok

Published May 10, 2019• 4 citations

Abstract

Modern secure messaging protocols can offer strong security guarantees such as Post-Compromise Security (PCS), which enables participants to heal after compromise. The core PCS mechanism in protocols like Signal is designed for pairwise communication, making it inefficient for large groups, while recently proposed designs for secure group messaging, ART, IETF's MLS Draft-11/TreeKEM, use group keys derived from tree structures to efficiently provide PCS to large groups. Until now, research on PCS designs only considered healing behaviour within a single group. In this work we provide the first analysis of the healing behaviour when a user participates in multiple groups. Our analysis reveals that the currently proposed protocols based on group keys, such as ART and TreeKEM/MLS Draft-11, provide significantly weaker PCS guarantees than group protocols based on pairwise PCS channels. In fact, we show that if new users can be created dynamically, ART, TreeKEM, and MLS Draft-11 never fully heal authentication. We map the design space of healing mechanisms, analyzing security and overhead of possible solutions. This leads us to a promising solution based on (i) global updates that affect all current and future groups, and (ii) post-compromise secure signatures. Our solution allows group messaging protocols such ART and MLS to achieve substantially stronger PCS guarantees. We provide a security definition for post-compromise secure signatures and an instantiation.

DOI: 10.60882/cispa.25435252

Related papers

On Ends-to-Ends Encryption: Asynchronous Group Messaging with Strong Security Guarantees

Katriel Cohn-Gordon, Cas J. F. Cremers, Luke Garratt +2 more

In the past few years secure messaging has become mainstream, with over a billion active users of end-to-end encryption protocols such as Signal. The Signal Protocol provides a strong property called post-compromise security to its users. However, it turns out that many of its implementations provide, without notification, a weaker property for group messaging: an adversary who compromises a single group member can read and inject messages indefinitely. We show for the first time that post-compromise security can be achieved in realistic, asynchronous group messaging systems. We present a design called Asynchronous Ratcheting Trees (ART), which uses tree-based Diffie-Hellman key exchange to allow a group of users to derive a shared symmetric key even if no two are ever online at the same time. ART scales to groups containing thousands of members, while still providing provable security guarantees. It has seen significant interest from industry, and forms the basis for two draft IETF RFCs and a chartered working group. Our results show that strong security guarantees for group messaging are practically achievable in a modern setting.

Jul 1, 201818 citations

Keep the Dirt: Tainted TreeKEM, Adaptively and Actively Secure Continuous Group Key Agreement

Karen Klein, Guillermo Pascual-Perez, Michael Walter +7 more

While messaging systems with strong security guarantees are widely used in practice, designing a protocol that scales efficiently to large groups and enjoys similar security guarantees remains largely open. The two existing proposals to date are ART (Cohn-Gordon et al., CCS18) and TreeKEM (IETF, The Messaging Layer Security Protocol, draft). TreeKEM is the currently considered candidate by the IETF MLS working group, but dynamic group operations (i.e. adding and removing users) can cause efficiency issues. In this paper we formalize and analyze a variant of TreeKEM which we term Tainted TreeKEM (TTKEM for short). The basic idea underlying TTKEM was suggested by Millican (MLS mailing list, February 2018). This version is more efficient than TreeKEM for some natural distributions of group operations, we quantify this through simulations.Our second contribution is two security proofs for TTKEM which establish post compromise and forward secrecy even against adaptive attackers. The security loss (to the underlying PKE) in the Random Oracle Model is a polynomial factor, and a quasipolynomial one in the Standard Model. Our proofs can be adapted to TreeKEM as well. Before our work no security proof for any TreeKEM-like protocol establishing tight security against an adversary who can adaptively choose the sequence of operations was known. We also are the first to prove (or even formalize) active security where the server can arbitrarily deviate from the protocol specification. Proving fully active security – where also the users can arbitrarily deviate – remains open.

IEEE Symposium on Security and Privacy (S&P)May 1, 202130 citations

Security and Efficiency of Secure Group Messaging Protocols

Guirec Lebrun

Secure Group Messagings are cryptographic protocols that allow safe group conversation within potentially large user groups. They are based on a dedicated type of group key exchange mechanism named Continuous Group Key Agreement (CGKA), which generates a continuously evolving group key in a safe and efficient way. Messaging Layer Security (MLS) is an IETF-standardized secure group messaging protocol which uses a protocol called TreeKEM as its CGKA.We study in this thesis the security and the efficiency of the CGKAs used within secure group messagings. Firstly, we propose a variant of TreeKEM (called Quarantined-TreeKEM) that solves a security issue related to inactive users, whose behavior prevents fundamental security properties to be fulfilled. Moreover, we improve the efficiency of TreeKEM, especially regarding its communication cost, by considering the best way to manage the tree graph used by that CGKA. Finally, we show that in the particular – yet common – use case where only a subset of users is granted the administration rights, we can design a new CGKA whose performances outperform those of regular decentralized CGKAs such as TreeKEM.This thesis thus aims to improve the state-of-the-art in secure group messaging protocols, in a context where strong security and energy sobriety are necessary features.

Dec 1, 20250 citations

Quarantined-TreeKEM: A Continuous Group Key Agreement for MLS, Secure in Presence of Inactive Users

Céline Chevalier, Guirec Lebrun, Ange Martinelli +1 more

The recently standardized secure group messaging protocol Messaging Layer Security (MLS) is designed to ensure asynchronous communications within large groups, with an almost-optimal communication cost and the same security level as point-to-point secure messaging protocols such as Signal. In particular, the core sub-protocol of MLS, a Continuous Group Key Agreement (CGKA) called TreeKEM, must generate a common group key that respects the fundamental security properties of post-compromise security and forward secrecy which mitigate the effects of user corruption over time

ACM SIGSAC Conference on Computer and Communications Security (CCS)Dec 2, 20243 citations

On Post-compromise Security

Katriel Cohn-Gordon, Cas J. F. Cremers, Luke Garratt

In this work we study communication with a party whose secrets have already been compromised. At first sight, it may seem impossible to provide any type of security in this scenario. However, under some conditions, practically relevant guarantees can still be achieved. We call such guarantees "post-compromise security". We provide the first informal and formal definitions for post-compromise security, and show that it can be achieved in several scenarios. At a technical level, we instantiate our informal definitions in the setting of authenticated key exchange (AKE) protocols, and develop two new strong security models for two different threat models. We show that both of these security models can be satisfied, by proposing two concrete protocol constructions and proving they are secure in the models. Our work leads to crucial insights on how post-compromise security can (and cannot) be achieved, paving the way for applications in other domains.

IEEE Computer Security Foundations Workshop (CSFW)Jun 1, 2016141 citations

Realistic, strong and provable key exchange security

Luke Garratt

Authenticated key exchange protocols are ubiquitous in modern-day life. They are used to secure numerous types of data exchange, ranging from online banking to instant messaging conversations. In this thesis, we extend the state of the art for authenticated key exchange security, following the three themes of realistic, strong and provable. First, we tackle the theme of provable security. We develop generic techniques, applicable to a wide range of security models, to assist in proofs of security of cryptographic schemes. Specifically, a "game hopping" proof is a powerful technique to prove strong statements about the security of a protocol. However, the proof technique often involves esoteric and repetitive steps. We demystify the methodology and prove generic theorems to reduce the length and complexity of a wide class of game hopping proofs. Next, we use this new framework to analyse strong and previously unstudied formal security guarantees of authenticated key exchange protocols. These protocols are able to achieve strong security guarantees because they share and update state across sessions. Using our framework, we are able to push the state of the art by defying the folklore of what was previously thought provable of authenticated key exchange protocols. Specifically, it was previously thought that no protocol can achieve a security guarantee about communication with a peer if the peer was already fully compromised. We show that this is not true by formally defining a new concept, which we name post-compromise security. We capture an intuitive "self-healing" property of protocols. We then construct and formally prove protocols can achieve this strong security notion. Finally, we leverage all of this work to analyse realistic protocols. Signal, which is used to encrypt messages in WhatsApp, Facebook Messenger and Google Allo amongst others, is one such protocol we consider. Despite being used by billions of people, Signal was completely unstudied in the academic literature prior to this work. Two reasons for this were that Signal had no documentation at the time and it did not fit into existing models: it shares state across sessions and has over ten different types of key, most of which continually update. Despite its complexity, we are able to use the other work in this thesis to give the first ever analysis and proof of security of Signal. Overall, this thesis aims to bridge the gap between theory and practice in the current state of the art of authenticated key exchange protocols.

Jan 1, 20180 citations