Cryptology ePrint Archive: Report 2005/097

Computationally Sound Verification of Security Protocols Using Diffie-Hellman Exponentiation

Yassine Lakhnech and Laurent Mazare

Abstract: Recently, it has been proved 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.

Category / Keywords: cryptographic protocols / Cryptographic Protocols, Diffie-Hellman, Soundness of Formal Encryption, Probabilistic Encryption

Date: received 25 Mar 2005

Contact author: laurent mazare at imag fr

Available formats: Postscript (PS) | Compressed Postscript (PS.GZ) | PDF | BibTeX Citation

Version: 20050405:071457 (All versions of this report)

Discussion forum: Show discussion | Start new discussion