Design and Analysis of Diffie-Hellman-Based Key Exchange Using One-time ID by SVO Logic

Authenticated key exchange protocols have been developed to establish secure channel on the Internet. In this paper, we consider following attacks against an authenticated key exchange using shared secret: eavesdropping, DoS attack, replay attack, and impersonation. Besides prevention from all these attacks, efficiency is also important. In this paper, we propose a three-party authenticated key exchange protocol based on Diffie-Hellman key exchange with one-time ID, which is a user's extraordinary identity used only once [K. Imamoto, K. Sakurai, Notes on Dynamic Information Management for Authenticated Key Exchange, ISEC, March 2003; H. Krawczyk, The IKE-SIGMA Protocol, Internet Draft, Nov 2001. http://www.ee.technion.ac.il/~hugo/draft-krawczyk-ipsec-ike-sigma-00.txt]. Moreover, we analyze our proposal by SVO Logic, which is one of formal methods to analyze cryptographic protocols [P. Syverson and P. C. van Oorschot. A Unified Cryptographic Protocol Logic. NRL CHAOS Report, 5540-227, 1996; P. Syverson and I. Cervesato. The Logic of Authentication Protocols. FOSAD'00, LNCS2171, pp.63-137, 2001], and show what assumptions are needed.