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 contribution||A Computational Analysis of the Needham-Schroeder protocol|
|Title of host publication||Proceedings of 16th Computer Science Foundation Workshop|
|Publisher||IEEE Computer Society|
|Publication status||Published - 2003|
Bibliographical noteOther page information: 248-262
Conference Proceedings/Title of Journal: Proceedings of 16th Computer Science Foundation Workshop
Other identifier: 2000646