Session-StateReveal is stronger than eCKs Ephemeral Key Reveal: using automatic analysis to attack the NAXOS protocol

摘要

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.