A Computational Analysis of the Needham-Schroeder Protocol

Research output: Chapter in Book/Report/Conference proceedingConference Contribution (Conference Proceeding)


We provide the first computational analysis of the well known Needham-\Schroeder(-Lowe) protocol. We show that Lowe's attack to the original protocol can naturally be cast to the computational framework. Then we prove that chosen-plaintext security for encryption schemes is not sufficient to ensure soundness of formal proofs with respect to the computational setting, by exhibiting an attack against the corrected version of the protocol implemented using an ElGamal encryption scheme. Our main result is a proof that, when implemented using an encryption scheme that satisfies indistinguishability under chosen-ciphertext attack, the Needham-\Schroeder-Lowe protocol is indeed a secure mutual authentication protocol. The technical details of our proof reveal new insights regarding the relation between formal and computational models for system security.
Translated title of the contributionA Computational Analysis of the Needham-Schroeder protocol
Original languageEnglish
Title of host publicationProceedings of 16th Computer Science Foundation Workshop
PublisherIEEE Computer Society
Publication statusPublished - 2003

Bibliographical note

Other page information: 248-262
Conference Proceedings/Title of Journal: Proceedings of 16th Computer Science Foundation Workshop
Other identifier: 2000646

Fingerprint Dive into the research topics of 'A Computational Analysis of the Needham-Schroeder Protocol'. Together they form a unique fingerprint.

Cite this