Title: Session-StateReveal is stronger than eCKs EphemeralKeyReveal: using automatic analysis to attack the NAXOS protocol

Authors: Cas J.F. Cremers

Addresses: Department of Computer Science, ETH Zurich, 8092 Zurich, Switzerland

Abstract: 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.

Keywords: provable security; authenticated key exchange; AKE; session state reveal; ephemeral key reveal; automatic analysis; tools; eCK; CK; NAXOS; security models; adversary queries; protocol attacks; cryptography.

DOI: 10.1504/IJACT.2010.038304

International Journal of Applied Cryptography, 2010 Vol.2 No.2, pp.83 - 99

Published online: 28 Jan 2011 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article