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
-
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}
}
