Yassine Lakhnech and Laurent Mazare
Computationally Sound Verification of Security Protocols Using Diffie-Hellman Exponentiation (2005)
Computationally Sound Verification of Security Protocols Using Diffie-Hellman Exponentiation (2005)
TR-2005-7.pdf
TR-2005-7.ps
Keywords: Cryptographic Protocols, Diffie-Hellman, Soundness of Formal Encryption, Probabilistic Encryption
Abstract: In this paper, we follow the recent trend in bridging the gap that separates the symbolic and computational views of cryptographic protocols. Recent papers have proven that computational security can be automatically verified using the Dolev-Yao abstraction. We extend these results by adding a widely used component for cryptographic protocols: Diffie-Hellman exponentiation. Thus our main result is: if the Decisional Diffie-Hellman assumption is verified and the cryptographic primitives used to implement the protocol are secure, then safety in the symbolic world implies safety in the computational world. Therefore, it is possible to prove automatically safety in the computational world.
