A Computational Analysis of the Needham-Schroeder Protocol

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.