Many recent key exchange (KE) protocols have been proven secure in the CK, CK-HMQV, or eCK security models. The exact relation between these security models, and hence the relation between the security guarantees provided by the protocols, is unclear. We show first that the CK, CK-HMQV, and eCK security models are formally incomparable. Second, we show that these models are also practically incomparable, by providing for each model attacks on protocols from the literature that are not considered by the other models. Third, our analysis enables us to find previously unreported flaws in protocol security proofs from the literature. We identify the causes of these flaws and show how they can be avoided.
Many recent key exchange (KE) protocols have been proven secure in the CK, CK-HMQV, or eCK security models. The exact relation between these security models, and hence the relation between the security guarantees provided by the protocols, is unclear. We show first that the CK, CK-HMQV, and eCK security models are formally incomparable. Second, we show that these models are also practically incomparable, by providing for each model attacks on protocols from the literature that are not considered by the other models. Third, our analysis enables us to find previously unreported flaws in protocol security proofs from the literature. We identify the causes of these flaws and show how they can be avoided.
Many recent protocols for Authenticated Key Exchange have been proven correct in the CK, CK-HMQV, or eCK security models. The exact relation between the security models, and hence between the security guarantees provided by the protocols, is unclear. We show that the CK, CK-HMQV, and eCK security models are formally incomparable for a number of reasons. Second, we show that these models are also practically incomparable, by providing for each model attacks on existing protocols that are not considered by the other models. Our analysis exposes many subtleties of these models, some of which can even be generalized to reveal shortcomings in security proofs in related AKE security models.
The key exchange is a fundamental building block in the cryptography. Several provable security models for the key exchange protocol are proposed. To determine the exact properties required by the protocols, a single unified security model is essential. The eCK', eCK and CK models are examined and the result is proved that the eCK' model is the strongest provable security model for the key exchange. The relative security strength among these models is analyzed. To support the implication or non-implication relations among these models, the formal proofs and the counter-examples are given.
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.
Abstract. In 2001, Canetti and Krawczyk proposed a security model (CKmodel) for authentication protocols. They also gave an indistinguishabilitybased definition for key exchange protocols. Since then the model has almost exclusively been used for analyzing key exchange protocols, although it can be applied to authentication protocols in general. The model not only captures a large class of attacks but also provides a modular approach to the design of authentication protocols. However, the model does not capture the property of Key Compromise Impersonation (KCI) Resilience. Until now, analysis concerning this property has mostly been done heuristically and restricted to key exchange protocols only. Previous attempts on formalizing KCI have mostly been done in some ad hoc manner and additional proofs have to be given specifically for the security of KCI resilience. In this paper, we propose an extension to the CK-model, which allows, for the first time, the KCI attacks to be considered in authentication protocols in general, rather than restricted to key exchange protocols, and no more additional proofs are required specifically for KCI security. With the revival of interest in identity-based (ID-based) cryptography, there have been many new ID-based key exchange protocols proposed. Despite the fact that some of them have been proven in some restricted versions of a model proposed by Bellare and Rogaway in 1993 and some others have been proven in the original CK-model, there is no rigorous model specifically for ID-based key exchange security. In particular, forward secrecy against compromised Key Generation Server (KGS-FS) has never been captured even though this notion is more important and stronger than the perfect forward secrecy in ID-based key exchange. For this, we further extend our model to ID-based setting and capture the property of KGS-FS for ID-based key exchange security. 1
Abstract. An unresolved problem in research on authenticated key exchange (AKE) is to construct a secure protocol against advanced attacks such as key compromise impersonation and maximal exposure attacks without relying on random oracles. HMQV, a state of the art AKE protocol, achieves both efficiency and the strong security proposed by Krawczyk (we call it the CK + model), which includes resistance to advanced attacks. However, the security proof is given under the random oracle model. We propose a generic construction of AKE from a key encapsulation mechanism (KEM). The construction is based on a chosen-ciphertext secure KEM, and the resultant AKE protocol is CK + secure in the standard model. The construction gives the first CK + secure AKE protocols based on the hardness of integer factorization problem, code-based problems, or learning problems with errors. In addition, instantiations under the Diffie-Hellman assumption or its variant can be proved to have strong security without non-standard assumptions such as πPRF and KEA1. Furthermore, we extend the CK + model to identity-based (called the id-CK + model), and propose a generic construction of identity-based AKE (ID-AKE) based on identity-based KEM, which satisfies id-CK + security. The construction leads first strongly secure ID-AKE protocols under the hardness of integer factorization problem, or learning problems with errors.
In this paper, we propose two authenticated key exchange (AKE) protocols and prove their security in the extended Canetti-Krawczyk model. The first protocol, called NAXOS+, is obtained by slightly modifying the NAXOS protocol proposed by LaMacchia, Lauter and Mityagin [15]. We prove its security under the Computational Diffie-Hellman (CDH) assumption by using the trapdoor test introduced in [6]. To the authors' knowledge, this is the first AKE protocol which is secure under the CDH assumption in the eCK model. The second protocol, called NETS, enjoys a simple and tight security reduction compared to existing schemes including HMQV and CMQV without using the Forking Lemma. Since each session of the NETS protocol requires only three exponentiations per party, its efficiency is also comparable to MQV, HMQV and CMQV.