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.
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.
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.
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.
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.
Assessing the security of key exchange protocols is a crucial task and turned out to be highly non-trivial.Many protocols proposed in the past have subsequently been broken.In order to provide a formal framework for security proofs, various security models have been defined.In this thesis, we analyse several such security models for key exchange protocols using the paradigm of constructive cryptography.We examine the exact constructive security guarantees and semantics that these notions provide.In particular, we compare constructive security definitions with a model proposed by Bellare and Rogaway, SK-security by Canetti and Krawczyk and a formal model for secure key exchange proposed by Shoup.i
We present a systematic approach to define and study authentication notions in authenticated key-exchange protocols. We propose and use a flexible and expressive predicate-based definitional framework. Our definitions capture key and entity authentication, in both implicit and explicit variants, as well as key and entity confirmation, for authenticated key-exchange protocols. In particular, we capture critical notions in the authentication space such as key-compromise impersonation resistance and security against unknown key-share attacks. We first discuss these definitions within the Bellare-Rogaway model and then extend them to Canetti-Krawczyk-style models. We then show two useful applications of our framework. First, we look at the authentication guarantees of three representative protocols to draw several useful lessons for protocol design. The core technical contribution of this paper is then to formally establish that composition of secure implicitly authenticated key-exchange with subsequent confirmation protocols yields explicit authentication guarantees. Without a formal separation of implicit and explicit authentication from secrecy, a proof of this folklore result could not have been established.
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.