The standard view of cryptography is that secure systems should be built by implementing known primitives whose theoretical security guarantees are well understood. In this work we take the opposite approach, taking inspiration from existing systems and providing the theoretical basis with which to understand their security goals. Our particular inspirations are modern secure messaging apps (e.g. Signal, WhatsApp) which have deployed new techniques with the goal of maintaining some security against attackers which sometimes gain temporary access to honest users’ devices.We propose that these security goals should be studied in a modular manner where distinct cryptographic components are studied in isolation. Towards this we separately provide formal models for understanding the initial exchange of cryptographic secrets and their later use for the exchange of messages in this setting. We provide provable secure constructions of these separate components (often achieving better security than what is currently deployed by messaging apps) and a composition result which generically proves security when these isolated components are used together.
The standard view of cryptography is that secure systems should be built by implementing known primitives whose theoretical security guarantees are well understood. In this work we take the opposite approach, taking inspiration from existing systems and providing the theoretical basis with which to understand their security goals. Our particular inspirations are modern secure messaging apps (e.g. Signal, WhatsApp) which have deployed new techniques with the goal of maintaining some security against attackers which sometimes gain temporary access to honest users’ devices.We propose that these security goals should be studied in a modular manner where distinct cryptographic components are studied in isolation. Towards this we separately provide formal models for understanding the initial exchange of cryptographic secrets and their later use for the exchange of messages in this setting. We provide provable secure constructions of these separate components (often achieving better security than what is currently deployed by messaging apps) and a composition result which generically proves security when these isolated components are used together.
Signal is a new security protocol and accompanying app that provides end-to-end encryption for instant messaging. The core protocol has recently been adopted by WhatsApp, Facebook Messenger, and Google Allo among many others, the first two of these have at least 1 billion active users. Signal includes several uncommon security properties (such as "future secrecy" or "post-compromise security"), enabled by a novel technique called ratcheting in which session keys are updated with every message sent. Despite its importance and novelty, there has been little to no academic analysis of the Signal protocol. We conduct the first security analysis of Signal's key agreement and double ratchet as a multi-stage key exchange protocol. We extract from the implementation a formal description of the abstract protocol, and define a security model which can capture the "ratcheting" key update structure. We then prove the security of Signal's core in our model, demonstrating several standard security properties. We have found no major flaws in the design, and hope that our presentation and results can serve as a starting point for other analyses of this widely adopted protocol.
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.
Secure communication has become an essential ingredient of our daily life. Mostly unnoticed, cryptography is protecting our interactions today when we read emails or do banking over the Internet, withdraw cash at an ATM, or chat with friends on our smartphone. Security in such communication is enabled through two components. First, two parties that wish to communicate securely engage in a key exchange protocol in order to establish a shared secret key known only to them. The established key is then used in a follow-up secure channel protocol in order to protect the actual data communicated against eavesdropping or malicious modification on the way. In modern cryptography, security is formalized through abstract mathematical security models which describe the considered class of attacks a cryptographic system is supposed to withstand. Such models enable formal reasoning that no attacker can, in reasonable time, break the security of a system assuming the security of its underlying building blocks or that certain mathematical problems are hard to solve. Given that the assumptions made are valid, security proofs in that sense hence rule out a certain class of attackers with well-defined capabilities. In order for such results to be meaningful for the actually deployed cryptographic systems, it is of utmost importance that security models capture the system's behavior and threats faced in that 'real world' as accurately as possible, yet not be overly demanding in order to still allow for efficient constructions. If a security model fails to capture a realistic attack in practice, such an attack remains viable on a cryptographic system despite a proof of security in that model, at worst voiding the system's overall practical security. In this thesis, we reconsider the established security models for key exchange and secure channel protocols. To this end, we study novel and advanced security aspects that have been introduced in recent designs of some of the most important security protocols deployed, or that escaped a formal treatment so far. We introduce enhanced security models in order to capture these advanced aspects and apply them to analyze the security of major practical key exchange and secure channel protocols, either directly or through comparatively close generic protocol designs. Key exchange protocols have so far always been understood as establishing a single secret key, and then terminating their operation. This changed in recent practical designs, specifically of Google's QUIC ("Quick UDP Internet Connections") protocol and the upcoming version 1.3 of the Transport Layer Security (TLS) protocol, the latter being the de-facto standard for security protocols. Both protocols derive multiple keys in what we formalize in this thesis as a multi-stage key exchange (MSKE) protocol, with the derived keys potentially depending on each other and differing in cryptographic strength. Our MSKE security model allows us to capture such dependencies and differences between all keys established in a single framework. In this thesis, we apply our model to assess the security of both the QUIC and the TLS 1.3 key exchange design. For QUIC, we are able to confirm the intended overall security but at the same time highlight an undesirable dependency between the two keys QUIC derives. For TLS 1.3, we begin by analyzing the main key exchange mode as well as a reduced resumption mode. Our analysis attests that TLS 1.3 achieves strong security for all keys derived without undesired dependencies, in particular confirming several of this new TLS version's design goals. We then also compare the QUIC and TLS 1.3 designs with respect to a novel 'zero round-trip time' key exchange mode establishing an initial key with minimal latency, studying how differences in these designs affect the achievable key exchange security. As this thesis' last contribution in the realm of key exchange, we formalize the notion of key confirmation which ensures one party in a key exchange execution that the other party indeed holds the same key. Despite being frequently mentioned in practical protocol specifications, key confirmation was never comprehensively treated so far. In particular, our formalization exposes an inherent, slight difference in the confirmation guarantees both communication partners can obtain and enables us to analyze the key confirmation properties of TLS 1.3. Secure channels have so far been modeled as protecting a sequence of distinct messages using a single secret key. Our first contribution in the realm of channels originates from the observation that, in practice, secure channel protocols like TLS actually do not allow an application to transmit distinct, or atomic, messages. Instead, they provide applications with a streaming interface to transmit a stream of bits without any inherent demarcation of individual messages. Necessarily, the security guarantees of such an interface differ significantly from those considered in cryptographic models so far. In particular, messages may be fragmented in transport, and the recipient may obtain the sent stream in a different fragmentation, which has in the past led to confusion and practical attacks on major application protocol implementations. In this thesis, we formalize such stream-based channels and introduce corresponding security notions of confidentiality and integrity capturing the inherently increased complexity. We then present a generic construction of a stream-based channel based on authenticated encryption with associated data (AEAD) that achieves the strongest security notions in our model and serves as validation of the similar TLS channel design. We also study the security of such applications whose messages are inherently atomic and which need to safely transport these messages over a streaming, i.e., possibly fragmenting, channel. Formalizing the desired security properties in terms of confidentiality and integrity in such a setting, we investigate and confirm the security of the widely adopted approach to encode the application's messages into the continuous data stream. Finally, we study a novel paradigm employed in the TLS 1.3 channel design, namely to update the keys used to secure a channel during that channel's lifetime in order to strengthen its security. We propose and formalize the notion of multi-key channels deploying such sequences of keys and capture their advanced security properties in a hierarchical framework of confidentiality and integrity notions. We show that our hierarchy of notions naturally connects to the established notions for single-key channels and instantiate its strongest security notions with a generic AEAD-based construction. Being comparatively close to the TLS 1.3 channel protocol, our construction furthermore enables a comparative design discussion.
Messaging between two parties and in the group setting has enjoyed widespread attention both in practice, and, more recently, from the cryptographic community. One of the main challenges in the area is constructing secure (end-to-end encrypted) and efficient messaging protocols for group conversations. The popular messaging applications WhatsApp and Signal utilise a protocol in which, instead of sharing a single group key, members have individual \textit{sender keys}, which are shared with all other group members. The Sender Keys protocol is claimed to offer forward security guarantees. However, despite its broad adoption in practice, it has never been studied formally in the cryptographic literature. In this paper we present the first analysis of the Sender Keys protocol along with some prospective improvements. To this end, we introduce a new cryptographic primitive, develop a game-based security model, present a security analysis in the passive and active settings, and propose several improvements to the protocol.
The original cryptographic problem is for Alice and Bob to have a conversation using some insecure communications channel, but preventing Eve both from eavesdropping and in and improper manner tampering with their conversation. This chapter develops the theory of messaging protocols, which is the answer to the original cryptographic problem. The chapter develops a framework for messaging protocols and related security notions. The framework also captures symmetric key channels as a special case. The chapter in particular analyses compositional constructions based on key exchange protocols and channels. The results provides solid solutions for the original cryptographic problem. The chapter also investigates stronger notions of security for messaging protocols, including a design based on role-symmetric key exchange. One important societal goal is to defend against mass surveillance. While cryptography cannot solve this problem on its own, this chapter discusses techniques for preventing messaging protocols from making mass surveillance trivial.
The Signal Protocol is a two-party secure messaging protocol used in applications such as Signal, WhatsApp, Google Messages and Facebook Messenger and is used by billions daily. It consists of two core components, one of which is the Double Ratchet protocol that has been the subject of a line of work that aims to understand and formalise exactly what security it provides. Existing models capture strong guarantees including resilience to state exposure in both forward security (protecting past secrets) and post-compromise security (restoring security), adaptive state corruptions, message injections and out-of-order message delivery. Due to this complexity, prior work has failed to provide security guarantees that do not degrade in the number of interactions, even in the single-session setting.