Session-StateReveal is stronger than eCKs EphemeralKeyReveal: using automatic analysis to attack the NAXOS protocol. (31st January 2011)

• Record Type: Journal Article
• Authors: Cremers, Cas J.F.
• Is Part Of: International journal of applied cryptography. Volume 2:Number 2(2010)
• Page Start: 83
• Page End: 99
• Publication Date: 2011-01-31
• Subjects: 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; Data encryption (Computer science) -- Periodicals; Cryptography -- Periodicals; Computer security -- Periodicals; 652.8
• Languages: English
• ISSNs: 1753-0563

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.