Cryptology ePrint Archive: Report 2003/121

A Cryptographically Sound Security Proof of the Needham-Schroeder-Lowe Public-Key Protocol

Michael Backes and Birgit Pfitzmann

Abstract: We present the first cryptographically sound security proof of the well-known Needham-Schroeder-Lowe public-key protocol. More precisely, we show that the protocol is secure against arbitrary active attacks if it is implemented using provably secure cryptographic primitives. Although we achieve security under cryptographic definitions, our proof does not have to deal with probabilistic aspects of cryptography and is hence in the scope of current proof tools. The reason is that we exploit a recently proposed ideal cryptographic library, which has a provably secure cryptographic implementation. Besides establishing the cryptographic security of the Needham-Schroeder-Lowe protocol, our result also exemplifies the potential of this cryptographic library and paves the way for cryptographically sound verification of security protocols by means of formal proof tools.

Category / Keywords: foundations / cryptographic protocols, formal methods, universal composition, Needham-Schroeder

Date: received 10 Jun 2003

Contact author: mbc at zurich ibm com

Available format(s): Postscript (PS) | Compressed Postscript (PS.GZ) | BibTeX Citation

Version: 20030610:162512 (All versions of this report)

Short URL: ia.cr/2003/121

Discussion forum: Show discussion | Start new discussion