Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

Key exchange security in constructive cryptography

Christian Badertscher

Published Jan 1, 2012• 0 citations
Publisher

Abstract

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

DOI
10.3929/ethz-a-007568849

Related papers

Future-Proofing Key Exchange Protocols

Jacqueline Brendel

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.

•Jan 1, 2019•0 citations

Security Models and Proofs for Key Establishment Protocols

Eddie M. Ng

In this thesis we study the problem of secure key establishment, motivated by the construction of secure channels protocols to protect information transmitted over an open network. In the past, the purported security of a key establishment protocol was justified if it could be shown to withstand popular attack scenarios by heuristic analysis. Since this approach does not account for all possible attacks, the security guarantees are limited and often insufficient. \nThis thesis examines the provable security approach to the analysis of key establishment protocols. We present the security models and definitions developed in 2001 and 2002 by Canetti and Krawczyk, critique the appropriateness of the models, and provide several security proofs under the definitions. In addition, we consider the importance of the key compromise impersonation resilience property in the context of these models. We list some open problems that were encountered in the study.

•Jan 1, 2005•5 citations

Authentication in Key-Exchange: Definitions, Relations and Composition

Cyprien Delpech de Saint Guilhem, Marc Fischlin, Bogdan Warinschi

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.

IEEE Computer Security Foundations Workshop (CSFW)•Jun 1, 2020•32 citations

A Formal Treatment of the Limits of Authenticated Key Exchange Security

Michèle Feltz, Cas J. F. Cremers

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.

•Jan 1, 2026•0 citations

Universally Composable Notions of Key Exchange and Secure Channels (Extended Abstract)

Ran Canetti, Hugo Krawczyk

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.

•Jan 1, 2002•19 citations

On Formal Models for Secure Key Exchange.

Victor Shoup

A new formal security model for session key exchange protocols in the public key setting is proposed, and several efficient protocols are analyzed in this model. The relationship between this new model and previously proposed models is explored, and several interesting, subtle distinctions between static and adaptive adversaries are explored. We also give a brief account of anonymous users. 1 Introduction In this paper, we investigate formal models of security for authenticated key exchange protocols in a public key setting where the only trusted party is an off-line certification authority. Our work follows up on that of Bellare, Canetti, and Krawczyk [2], which is grounded in the multi-party simulatability tradition (see, e.g., [1]). This approach seems very attractive, because it formulates security in terms of the service a session key protocol should provide to a higher level protocol, rather than getting mired in the details of session key protocols themselves, many of which ar...

•Jan 1, 1999•323 citations
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
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 thesis we study the problem of secure key establishment, motivated by the construction of secure channels protocols to protect information transmitted over an open network. In the past, the purported security of a key establishment protocol was justified if it could be shown to withstand popular attack scenarios by heuristic analysis. Since this approach does not account for all possible attacks, the security guarantees are limited and often insufficient. \nThis thesis examines the provable security approach to the analysis of key establishment protocols. We present the security models and definitions developed in 2001 and 2002 by Canetti and Krawczyk, critique the appropriateness of the models, and provide several security proofs under the definitions. In addition, we consider the importance of the key compromise impersonation resilience property in the context of these models. We list some open problems that were encountered in the study.
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.
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.
A new formal security model for session key exchange protocols in the public key setting is proposed, and several efficient protocols are analyzed in this model. The relationship between this new model and previously proposed models is explored, and several interesting, subtle distinctions between static and adaptive adversaries are explored. We also give a brief account of anonymous users. 1 Introduction In this paper, we investigate formal models of security for authenticated key exchange protocols in a public key setting where the only trusted party is an off-line certification authority. Our work follows up on that of Bellare, Canetti, and Krawczyk [2], which is grounded in the multi-party simulatability tradition (see, e.g., [1]). This approach seems very attractive, because it formulates security in terms of the service a session key protocol should provide to a higher level protocol, rather than getting mired in the details of session key protocols themselves, many of which ar...