International Association for Cryptologic Research

International Association
for Cryptologic Research

CryptoDB

Computationally Sound Verification of Security Protocols Using Diffie-Hellman Exponentiation

Authors:
Yassine Lakhnech
Laurent Mazare
Download:
URL: http://eprint.iacr.org/2005/097
Search ePrint
Search Google
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.
BibTeX
@misc{eprint-2005-12433,
  title={Computationally Sound Verification of Security Protocols Using Diffie-Hellman Exponentiation},
  booktitle={IACR Eprint archive},
  keywords={cryptographic protocols / Cryptographic Protocols, Diffie-Hellman, Soundness of Formal Encryption, Probabilistic Encryption},
  url={http://eprint.iacr.org/2005/097},
  note={ laurent.mazare@imag.fr 12867 received 25 Mar 2005},
  author={Yassine Lakhnech and Laurent Mazare},
  year=2005
}