An essential cornerstone of the definition of security for key exchange protocols is the notion of partnering. The de-facto standard definition of partnering is that of (partial) matching conversations (MC), which essentially states that two processes are partnered if every message sent by the first is actually received by the second and vice versa. We show that proving security under MC-based definitions is error-prone. To this end, we introduce no-match attacks, a new class of attacks that renders many existing security proofs invalid. We show that no-match attacks are often hard to avoid in MC-based security definitions without a) modifications of the original protocol or b) resorting to the use of cryptographic primitives with special properties. Finally, we show several ways to thwart no-match attacks. Most notably and as one of our major contributions, we provide a conceptually new definition of partnering that circumvents the problems of a MC-based partnering notion while preserving all its advantages. Our new notion of partnering not only makes security definitions for key exchange model practice much more closely. In contrast to many other security notions of key exchange it also adheres to the high standards of good cryptographic definitions: it is general, supports cryptographic intuition, allows for efficient falsification, and provides a fundamental composition property that MC-based notions lack.
An essential cornerstone of the definition of security for key exchange protocols is the notion of partnering. The de-facto standard definition of partnering is that of (partial) matching conversations (MC), which essentially states that two processes are partnered if every message sent by the first is actually received by the second and vice versa. We show that proving security under MC-based definitions is error-prone. To this end, we introduce no-match attacks, a new class of attacks that renders many existing security proofs invalid. We show that no-match attacks are often hard to avoid in MC-based security definitions without a) modifications of the original protocol or b) resorting to the use of cryptographic primitives with special properties. Finally, we show several ways to thwart no-match attacks. Most notably and as one of our major contributions, we provide a conceptually new definition of partnering that circumvents the problems of a MC-based partnering notion while preserving all its advantages. Our new notion of partnering not only makes security definitions for key exchange model practice much more closely. In contrast to many other security notions of key exchange it also adheres to the high standards of good cryptographic definitions: it is general, supports cryptographic intuition, allows for efficient falsification, and provides a fundamental composition property that MC-based notions lack.
An essential cornerstone of the definition of security for key exchange protocols is the notion of partnering. The de-facto standard definition of partnering is that of (partial) matching conversations (MC), which essentially states that two processes are partnered if every message sent by the first is actually received by the second and vice versa. We show that proving security under MC-based definitions is error-prone. To this end, we introduce no-match attacks, a new class of attacks that renders many existing security proofs invalid. We show that no-match attacks are often hard to avoid in MC-based security definitions without a) modifications of the original protocol or b) resorting to the use of cryptographic primitives with special properties. Finally, we show several ways to thwart no-match attacks. Most notably and as one of our major contributions, we provide a conceptually new definition of partnering that circumvents the problems of a MC-based partnering notion while preserving all its advantages. Our new notion of partnering not only makes security definitions for key exchange model practice much more closely. In contrast to many other security notions of key exchange it also adheres to the high standards of good cryptographic definitions: it is general, supports cryptographic intuition, allows for efficient falsification, and provides a fundamental composition property that MC-based notions lack.
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.
Abstract. Secure communication is a fundamental cryptographic primitive. Typically, security is achieved by relying on an existing credential infrastructure, such as a PKI or passwords, for identifying the end points to each other. But what can be obtained when no such credential infrastructure is available? Clearly, when there is no pre-existing credential infrastructure, an adversary can mount successful “man in the middle ” attacks by modifying the communication between the legitimate endpoints. Still, we show that not all is lost, as long as the adversary’s control over the communication is not complete: We present relatively efficient key exchange and secure session protocols that provide the full guarantee of secure communication as long as the adversary fails to intercept even a single message between the legitimate endpoints. To obtain this guarantee we strengthen the notion of key exchange to require that the keys exchanged in any two sessions are independent of each other as long as each session has at least one honest endpoint, even if both sessions has an adversarial endpoint. We call this notion credential-free key exchange. We then strengthen the existing notion of secure session protocols to provide the above guarantee given a CFKE (existing definitions and constructions are insufficient for this purpose). We provide two alternative definitions and constructions of CFKE, a game-based one with a construction in the RO model, and a UC one with a construction in the CRS model.
We develop a compositional method for proving cryptographically sound security properties of key exchange protocols, based on a symbolic logic that is interpreted over conventional runs of a protocol against a probabilistic polynomial-time attacker. Since reasoning about an unbounded number of runs of a protocol involves induction-like arguments about properties preserved by each run, we formulate a specification of secure key exchange that, unlike conventional key indistinguishability, is closed under general composition with steps that use the key.
In this paper, we investigate the notion of partnership as found in security models for key exchange protocols. Several different approaches have been pursued to define partnership, with varying degrees of success. We aim to provide an overview and criticism of the various definitions and point out some pitfalls that can be encountered when trying to define partnership. As a result, we propose an intuitive way of defining partnership directly from equality of session keys. In addition, we show that authentication can be captured using a definition of partnership by equality of partner identifiers, and give proofs that both definitions achieve what we expect from them.
In this work we construct an alternative model for Authenticated Key Exchange, intended to build a theoretic security framework for protocols whose characteristics may not always concur with the specifics of already existing models for authenticated exchanges. This model is constructed in a modular way, from the notion of commitment schemes and employing ephemeral information, therefore avoiding the exchange of long-term cryptographic material. From this model, we propose a number of Commitment-based protocols to establish a shared secret between two parties, and study their resistance over unauthenticated channels. This means analyzing the security of the protocol itself, and its robustness against Man-in-the-Middle attacks, by formalizing their security under this model. The protocols are constructed from Key Agreement (KA) and Key Encapsulation (KEM) primitives, to show that this model can be applied to both established and new paradigms. We highlight the differences that arise naturally, due to the nature of KEM constructions, in terms of the protocol itself and the types of attacks that they are subject to. We provide practical go-to protocols instances to migrate to, both for KEM-based and KA-based cryptographic primitives.