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

Available format(s)
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
Short URL
https://ia.cr/2005/097

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},
note = {\url{https://eprint.iacr.org/2005/097}},
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.