Key exchange protocols allow two parties to agree on a shared secret over an untrusted channel. A huge number of scientific works on key exchange have been published since the discovery of the first key exchange protocol, designed in 1976 by Diffie and Hellman [DH76]. The most prominent of these works is the game-based security model by Bellare and Rogaway [BR93], published in 1993 and, today, known as the "golden standard" for the security of key exchange protocols. The main purpose of key exchange protocols is to establish keys for a symmetric-key protocol such as a secure channel. Ideally, if both, the key exchange protocol and the channel protocol, are secure, then we would hope that they can be securely composed. While this is true for simulation-based security models [Can01, KT11, BPW03], game-based models usually lack composition theorems altogether. That is unfortunate, as they are often more suitable for real-life protocols such as TLS. Our first two composition theorems address the composition of BR-secure key exchange protocols with arbitrary symmetric-key protocols. We formally establish that an additional condition is necessary, namely, the key exchange requires a public session matching algorithm. Maybe surprisingly, many important key agreement protocols are not BR-secure due to the popular technique of explicit key confirmation. We devise a more flexible yet sufficiently strong model for this class of protocols and prove that it is closed under reductions. Overall, we devellop a tool for the modular analysis of real-life protocols and exemplify the use of our framwork on a profile of the TLS protocol. As in the case of most practical cryptography, information-theoretic security for key exchange protocols is out of reach, i.e., impossible in a formal sense. Therefore, protocols such as TLS rely on computational assumptions, e.g., the Diffie-Hellmann assumption or the hardness of factoring numbers. As the security of protocols is tightly related to the underlying complexity assumptions, researchers have been striving for simpler and weaker assumptions. The holy grail in this area is to base key agreement, one-way functions or simply any type of cryptography on the mere assumptions that NP does not equal P [FF93, BT03, AGGM06]. While positive results in this area remain elusive, there has been some recent progress on negative results [HMX10, PTV11], showing that cryptographic primitives such as hash functions cannot be based on NP-hardness unless coAM is contained in NP. In this thesis, we provide two oracle results that show that, via relativizing techniques, these negative results do not carry over to key agreement and regular one-way functions. In particular, we give an oracle relative to which the intersection of NP and coNP is easy while infinitely many often secure key agreement exists; and we give an oracle relative to which languages in the intersection of AM and coAM is easy while regular function families exists that are infinitely many often one-way.
Key exchange protocols allow two parties to agree on a shared secret over an untrusted channel. A huge number of scientific works on key exchange have been published since the discovery of the first key exchange protocol, designed in 1976 by Diffie and Hellman [DH76]. The most prominent of these works is the game-based security model by Bellare and Rogaway [BR93], published in 1993 and, today, known as the "golden standard" for the security of key exchange protocols. The main purpose of key exchange protocols is to establish keys for a symmetric-key protocol such as a secure channel. Ideally, if both, the key exchange protocol and the channel protocol, are secure, then we would hope that they can be securely composed. While this is true for simulation-based security models [Can01, KT11, BPW03], game-based models usually lack composition theorems altogether. That is unfortunate, as they are often more suitable for real-life protocols such as TLS. Our first two composition theorems address the composition of BR-secure key exchange protocols with arbitrary symmetric-key protocols. We formally establish that an additional condition is necessary, namely, the key exchange requires a public session matching algorithm. Maybe surprisingly, many important key agreement protocols are not BR-secure due to the popular technique of explicit key confirmation. We devise a more flexible yet sufficiently strong model for this class of protocols and prove that it is closed under reductions. Overall, we devellop a tool for the modular analysis of real-life protocols and exemplify the use of our framwork on a profile of the TLS protocol. As in the case of most practical cryptography, information-theoretic security for key exchange protocols is out of reach, i.e., impossible in a formal sense. Therefore, protocols such as TLS rely on computational assumptions, e.g., the Diffie-Hellmann assumption or the hardness of factoring numbers. As the security of protocols is tightly related to the underlying complexity assumptions, researchers have been striving for simpler and weaker assumptions. The holy grail in this area is to base key agreement, one-way functions or simply any type of cryptography on the mere assumptions that NP does not equal P [FF93, BT03, AGGM06]. While positive results in this area remain elusive, there has been some recent progress on negative results [HMX10, PTV11], showing that cryptographic primitives such as hash functions cannot be based on NP-hardness unless coAM is contained in NP. In this thesis, we provide two oracle results that show that, via relativizing techniques, these negative results do not carry over to key agreement and regular one-way functions. In particular, we give an oracle relative to which the intersection of NP and coNP is easy while infinitely many often secure key agreement exists; and we give an oracle relative to which languages in the intersection of AM and coAM is easy while regular function families exists that are infinitely many often one-way.
Key exchange protocols, first introduced by Diffie and Hellman in 1976, are one of the most widely-deployed cryptographic protocols. They allow two parties, that have never interacted before, to establish shared secrets. These shared cryptographic keys may subsequently be used to establish a secure communication channel. Use cases include the classic client-server setting that is for example at play when browsing the internet, but also chats via end-to-end-encrypted instant messaging applications. Security-wise, we generally demand of key exchange protocols to achieve key secrecy and authentication. While, informally, authentication ensures that the communicating parties have confidence in the identity of their peers, key secrecy ensures that any shared cryptographic key that is established via the key exchange protocol is only known to the participants in the protocol and can be used securely in cryptographic protocols, i.e., is sufficiently random. In 1993, Bellare and Rogaway gave a first formalization of key exchange protocol security that captures these properties with respect to powerful adversaries with full control over the network. Their model constitutes the basis of the many subsequent treatments of authenticated key exchange security, including the models presented in this thesis. The common methodological approach underlying all of these formalizations is the provable security paradigm, which has become a standard tool in assessing the security of cryptographic protocols and primitives. So-called security models specify the expected security guarantees of the scheme in question with regards to a well-defined class of adversaries. Proofs that validate these security claims do so by reducing the security of the overall scheme to the security of the underlying cryptographic primitives and hardness assumptions. However, advances in computational power and more sophisticated cryptanalytic capabilities often render exactly these components insecure. Especially the advent of quantum computers will have a devastating effect on much of today's public key cryptography. This is especially true for key exchange protocols since they rely crucially on public-key algorithms. In this thesis, our focus in future-proofing key exchange protocols is two-fold. First, we focus on extending security models for key exchange protocols to capture the (un)expected break of cryptographic primitives and hardness assumptions. The aim is to gain assurances with respect to future adversaries and to investigate the effects of primitive failures on key exchange protocols. More specifically, we explore how key exchange protocols can be safely transitioned to new, post-quantum secure algorithms with hybrid techniques. Hybrids combine classical and post-quantum algorithms such that the overall key agreement scheme remains secure as long as one of the two base schemes remains secure. For this, we introduce security notions for key encapsulation mechanisms that account for adversaries with varying levels of quantum capabilities and present three new constructions for hybrid key encapsulation mechanisms. Our hybrid designs are practice-inspired and for example capture draft proposals for hybrid modes in the Transport Layer Security (TLS) protocol, which is one of the most widely-deployed cryptographic protocols that enables key agreement. Furthermore, our notion of breakdown resilience for key exchange protocols allows to gauge the security of past session keys in the event of a failure of a cryptographic component in the key exchange. We exercise our model on variants of the post-quantum secure key exchange protocol NewHope by Alkim et al. Thereby, we confirm the intuition that, in order to guard against adversaries that only have access to quantum computing power in the (more distant) future, it is sufficient to use classically-secure authentication mechanisms alongside post-quantum key agreement to achieve authenticated key exchange. As with any mathematical statement, theorems in the provable security paradigm are only as valid as the underlying assumptions. A careful consideration of any newly made assumption is thus essential to ensure the meaningfulness of the statement itself and make the assumption a viable tool for future analyses. Thus, secondly, we systematically classify the PRF-ODH assumption, a complexity-theoretic hardness assumption that has been used in key exchange security analyses of such prominent protocols as TLS, Signal, and Wireguard. In particular, we give a unified, parametrized definition of the assumption encompassing different variants that are present in the literature. We relate the resulting parametrized notions in terms of their strength and show where these assumptions fit in the collection of well-understood related hardness assumptions. We finally sketch our result on the impossibility of instantiating this assumption in the standard model, thereby disposing of the uncertainty in the community whether PRF-ODH is in fact a standard model assumption, i.e., removes the usage of some idealized assumptions in key exchange protocol proofs.
In this paper we examine composability properties for the fundamental task of key exchange. Roughly speaking, we show that key exchange protocols secure in the prevalent model of Bellare and Rogaway can be composed with arbitrary protocols that require symmetrically distributed keys. This composition theorem holds if the key exchange protocol satisfies an additional technical requirement that our analysis brings to light: it should be possible to determine which sessions derive equal keys given only the publicly available information. What distinguishes our results from virtually all existing work is that we do not rely, neither directly nor indirectly, on the simulation paradigm. Instead, our security notions and composition theorems exclusively use a game-based formalism.We thus avoid several undesirable consequences of simulation-based security notions and support applicability to a broader class of protocols. In particular, we offer an abstract formalization of game-based security that should be of independent interest in other investigations using game-based formalisms.
The analysis of real-world protocols, in particular key exchange protocols and protocols building on these protocols, is a very complex, error-prone, and tedious task. Besides the complexity of the protocols itself, one important reason for this is that the security of the protocols has to be reduced to the security of the underlying cryptographic primitives for every protocol time and again. We would therefore like to get rid of reduction proofs for real-world key exchange protocols as much as possible and in many cases altogether, also for higher-level protocols which use the exchanged keys. So far some first steps have been taken in this direction. But existing work is still quite limited, and, for example, does not support Diffie-Hellman (DH) key exchange, a prevalent cryptographic primitive for real-world protocols. In this paper, building on work by Kusters and Tuengerthal, we provide an ideal functionality in the universal composability setting which supports several common cryptographic primitives, including DH key exchange. This functionality helps to avoid reduction proofs in the analysis of real-world protocols and often eliminates them completely. We also propose a new general ideal key exchange functionality which allows higherlevel protocols to use exchanged keys in an ideal way. As a proof of concept, we apply our framework to three practical DH key exchange protocols, namely ISO 9798-3, SIGMA, and OPTLS.
Recently, Canetti and Krawczyk (Eurocrypt'2001) formu- lated a notion of security for key-exchange (ke) protocols, called SK- security, and showed that this notion suffices for constructing secure channels. However, their model and proofs do not suffice for proving more general composability properties of SK-secure ke protocols. We show that while the notion of SK-security is strictly weaker than a fully-idealized notion of key exchange security, it is sufficiently robust for providing secure composition with arbitrary protocols. In particular, SK-security guarantees the security of the key for any application that desires to set-up secret keys between pairs of parties. We also provide new definitions of secure-channels protocols with similarly strong com- posability properties, and show that SK-security suffices for obtaining these definitions. To obtain these results we use the recently proposed framework of uni- versally composable (UC) security. We also use a new tool, called non- information oracles, which will probably find applications beyond the present case. These tools allow us to bridge between seemingly limited indistinguishability-based definitions such as SK-security and more pow- erful, simulation-based definitions, such as UC security, where general composition theorems can be proven. Furthermore, based on such compo- sition theorems we reduce the analysis of a full-fledged multi-session key- exchange protocol to the (simpler) analysis of individual, stand-alone, key-exchange sessions.
Authenticated Key Exchange (AKE) protocols are a core building block of all modern communications, connecting the distribution benefits of public-key cryptography to the performance benefits of symmetric-key cryptography. Modern AKE protocols are proven secure in game-based security models that offer considerably more security guarantees than the seminal Bellare-Rogaway model from 1993, in order to capture real-world security properties such as various notions of forward secrecy and resistance against predictable or bad pseudorandom number generators. For most of these security models, it is claimed that they offer “the best possible security”, based on informal arguments that at best hold under unstated assumptions. This has led to a fragmented landscape of AKE security models with seemingly contradictory results.We provide the first systematization of the limits of game-based security models for two-party AKE protocols. Our treatment covers classical stateless protocols as well as a restricted class of modern stateful protocols. Our analysis uncovers how the details of the considered protocol class have crucial implications for (im)possibility results, and reveals how different security goals can be achieved in different relevant classes of AKE protocols. From our formal impossibility results, we derive strong security models for these classes and give protocols that satisfy them.
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.