Paper 2005/097 Original: eprint.iacr.org/2005/097 ↗
Computationally Sound Verification of Security Protocols Using Diffie-Hellman Exponentiation
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- Category
- Cryptographic protocols
- Publication info
- Preprint.
- History
- 2005-04-05: last updated
- 2005-04-05: published
- Short URL
- https://ia.cr/2005/097
- License
- https://creativecommons.org/licenses/by/4.0/
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}
}