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

@incollection{citeulike:6089213, abstract = {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 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. It is the 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.}, author = {Backes, Michael and Pfitzmann, Birgit}, citeulike-article-id = {6089213}, citeulike-linkout-0 = {http://www.springerlink.com/content/xab6u4b6e5rbfapb}, journal = {FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science}, keywords = {security}, pages = {1--12}, posted-at = {2009-11-09 15:27:01}, priority = {0}, title = {A Cryptographically Sound Security Proof of the Needham-Schroeder-Lowe Public-Key Protocol}, url = {http://www.springerlink.com/content/xab6u4b6e5rbfapb}, year = {2003} }

TY - CHAP ID - citeulike:6089213 L3 - citeulike-article-id:6089213 N2 - 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 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. It is the 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. JF - FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science EP - 12 TI - A Cryptographically Sound Security Proof of the Needham-Schroeder-Lowe Public-Key Protocol SP - 1 KW - security AU - Backes, Michael AU - Pfitzmann, Birgit PY - 2003/// UR - http://www.springerlink.com/content/xab6u4b6e5rbfapb ER -