Sciweavers

Share
FSTTCS
2003
Springer

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

9 years 1 months ago
A Cryptographically Sound Security Proof of the Needham-Schroeder-Lowe Public-Key Protocol
We prove the Needham-Schroeder-Lowe public-key protocol secure under real, active cryptographic attacks including concurrent protocol runs. This proof is based on an abstract cryptographic library, which is a provably secure abstraction of a real cryptographic library. Together with composition and integrity preservation theorems from the underlying model, this allows us to perform the actual proof effort in a deterministic setting corresponding to a slightly extended Dolev-Yao model. Our proof is one of the two first independent cryptographically sound security proofs of this protocol. e first protocol proof over an abstract Dolev-Yao-style library that is in the scope of formal proof tools and that automatically yields cryptographic soundness. We hope that it paves the way for the actual use of automatic proof tools for this and many similar cryptographically sound proofs of security protocols.
Michael Backes, Birgit Pfitzmann
Added 06 Jul 2010
Updated 06 Jul 2010
Type Conference
Year 2003
Where FSTTCS
Authors Michael Backes, Birgit Pfitzmann
Comments (0)
books