Recent work by Krawczyk [10] and Menezes [14] has highlighted the importance of under-standing well the guarantees and limitations of formal security models when using them to prove the security of protocols. In this paper we focus on security models for authenticated key exchange (AKE) protocols. We observe that there are several classes of attacks on AKE protocols that lie outside the scope of the Canetti-Krawczyk model. Some of these additional attacks have already been considered by Krawczyk [10]. In an attempt to bring these attacks within the scope of the security model we extend the Canetti-Krawczyk model for AKE security by providing significantly greater powers to the adversary. Our contribution is a more compact, integrated, and comprehensive formulation of the security model. We then introduce a new AKE protocol called NAXOS and prove that it is secure against these stronger adversaries. 1
Recent work by Krawczyk [10] and Menezes [14] has highlighted the importance of under-standing well the guarantees and limitations of formal security models when using them to prove the security of protocols. In this paper we focus on security models for authenticated key exchange (AKE) protocols. We observe that there are several classes of attacks on AKE protocols that lie outside the scope of the Canetti-Krawczyk model. Some of these additional attacks have already been considered by Krawczyk [10]. In an attempt to bring these attacks within the scope of the security model we extend the Canetti-Krawczyk model for AKE security by providing significantly greater powers to the adversary. Our contribution is a more compact, integrated, and comprehensive formulation of the security model. We then introduce a new AKE protocol called NAXOS and prove that it is secure against these stronger adversaries. 1
Since Bellare and Rogaway presented the first formal security model for authenticated key exchange (AKE) protocols in 1993, many formal security models have been proposed. The extended Canetti-Krawczyk (eCK) model proposed by LaMacchia et al. is currently regarded as the strongest security model for two-party AKE protocols. In this paper, we first generalize the eCK model for tripartite AKE protocols, called teCK model, and enhance the security of the new model by adding a new reveal query. In the teCK model, the adversary has stronger powers, and can learn more secret information. Then we present a new tripartite AKE protocol based on the NAXOS protocol, called T-NAXOS protocol, and analyze its security in the teCK model under the random oracle assumption.
Abstract. In this paper, we present a new authenticated key exchange(AKE) protocol and prove its security under the random oracle assumption and the computational Diffie-Hellman(CDH) assumption. In the extended Canetti-Krawczyk model, there has been no known AKE protocol based on the CDH assumption. Our protocol, called NAXOS+, is obtained by slightly modifying the NAXOS protocol proposed by LaMacchia, Lauter and Mityagin. We establish a formal security proof of NAXOS+ in the extended Canetti-Krawczyk model using as a main tool the trapdoor test presented by Cash, Kiltz and Shoup. Key words: authenticated key exchange, trapdoor test, computational Diffie-Hellman assumption, extended Canetti-Krawzcyk model 1
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.
Two-party key exchange protocol is a mechanism in which two parties communicate with each other over an insecure channel and output the same session key.A key exchange protocol that is secure against an active adversary who can control and modify the exchanged messages is called authenticated key exchange (AKE) protocol.LaMacchia, Lauter and Mityagin presented a strong security definition for public key infrastructure (PKI) based two-pass protocol, which we call the extended Canetti-Krawczyk (eCK) security model, and some researchers have provided eCK-secure AKE protocols in recent years.However, almost all protocols are provably secure in the random oracle model or rely on a special implementation technique so-called the NAXOS trick.In this paper, we present a PKI-based two-pass AKE protocol that is secure in the eCK security model.The security of the proposed protocol is proven without random oracles (under three assumptions), and does not rely on implementation techniques such as the NAXOS trick.
In the paper, 'stronger security of authenticated key exchange' (LaMacchia et al., 2006, 2007), a new security model for authenticated key exchange protocols (eCK) is proposed. The new model is suggested to be at least as strong as previous models for key exchange protocols, such as the CK model (Canetti and Krawczyk, 2001; Krawczyk, 2005). The model includes a new notion of an EphemeralKeyReveal adversary query, which is claimed in e.g., LaMacchia et al. (2006), Okamoto (2007), and Ustaoglu (2008), to be at least as strong as the Session-StateReveal query. We investigate the relation between the two models by focusing on the difference in adversary queries. We formally model the NAXOS protocol and a variant of the eCK model, called eCK', in which the EphemeralKeyReveal query is replaced by the Session-StateReveal query. Using Scyther, a formal protocol analysis tool, we automatically find attacks on the protocol, showing that the protocol is insecure in the eCK' model. Our attacks prove that the Session-StateReveal query is stronger than the EphemeralKeyReveal query and that the eCK security model is incomparable to the CK model, disproving several claims made in the literature.
Protocols for authenticated key exchange (AKE) allow parties within an insecure network to establish a common session key which can then be used to secure their future communication. It is fair to say that group AKE is currently less well understood than the case of two-party AKE; in particular, attacks by malicious insiders --- a concern specific to the group setting --- have so far been considered only in a relatively "ad-hoc" fashion. The main contribution of this work is to address this deficiency by providing a formal, comprehensive model and definition of security for group AKE which automatically encompasses insider attacks. We do so by defining an appropriate ideal functionality for group AKE within the universal composability (UC) framework. As a side benefit, any protocol secure with respect to our definition is secure even when run concurrently with other protocols, and the key generated by any such protocol may be used securely in any subsequent application.In addition to proposing this definition, we show that the resulting notion of security is strictly stronger than the one proposed by Bresson, et al. (termed "AKE-security"), and that our definition implies all previously-suggested notions of security against insider attacks. We also show a simple technique for converting any AKE-secure protocol into one secure with respect to our definition.