CryptoDB
A Cryptographically Sound Security Proof of the Needham-Schroeder-Lowe Public-Key Protocol
| Authors: | |
|---|---|
| Download: | |
| 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. |
BibTeX
@misc{eprint-2003-11836,
title={A Cryptographically Sound Security Proof of the Needham-Schroeder-Lowe Public-Key Protocol},
booktitle={IACR Eprint archive},
keywords={foundations / cryptographic protocols, formal methods, universal composition, Needham-Schroeder},
url={http://eprint.iacr.org/2003/121},
note={ mbc@zurich.ibm.com 12213 received 10 Jun 2003},
author={Michael Backes and Birgit Pfitzmann},
year=2003
}