Computational soundness of Diffie-Hellman key exchange against active attackers

Significant progress was made in proving that symbolic models offering basic cryptographic operations such as encryption and digital signatures can be sound with respect to actual cryptographic realizations and security definitions. In this paper, we first introduce an extension of the Dolev-Yao algebra that allows protocol designers to express the Diffie-Hellman scheme as part of their protocols. We prove that even in the presence of arbitrary active adversaries, any Dolev-Yao attack that violates the formal version of the Diffie-Hellman assumption maps to a computational algorithm that violates the computational Diffie-Hellman assumption also. This yields the first computational soundness result for Diffie-Hellman key exchange against active adversaries.