Paper 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.

Metadata
Available format(s)
PDF PS
Category
Cryptographic protocols
Publication info
Published elsewhere. Unknown where it was published
Keywords
Cryptographic ProtocolsDiffie-HellmanSoundness of Formal EncryptionProbabilistic Encryption
Contact author(s)
laurent mazare @ imag fr
History
2005-04-05: received
Short URL
https://ia.cr/2005/097
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2005/097,
      author = {Yassine Lakhnech and Laurent Mazare},
      title = {Computationally Sound Verification of Security Protocols Using Diffie-Hellman Exponentiation},
      howpublished = {Cryptology {ePrint} Archive, Paper 2005/097},
      year = {2005},
      url = {https://eprint.iacr.org/2005/097}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.