Paper 2007/401 Original: eprint.iacr.org/2007/401 ↗
Another Look at Automated Theorem-Proving
Abstract
I examine the use of automated theorem-proving for reductionist security arguments in cryptography and discuss three papers that purport to show the potential of computer-assisted proof-writing and proof-checking. I look at the proofs that the authors give to illustrate the "game-hopping" technique -- for Full-Domain Hash signatures, ElGamal encryption, and Cramer-Shoup encryption -- and ask whether there is evidence that automated theorem-proving can contribute anything of value to the security analysis of cryptographic protocols.
Metadata
- Available format(s)
PDF- Category
- Public-key cryptography
- Publication info
- Preprint.
- History
- 2007-10-21: last updated
- 2007-10-21: published
- Short URL
- https://ia.cr/2007/401
- License
- https://creativecommons.org/licenses/by/4.0/
BibTeX
@misc{cryptoeprint:2007/401,
author = {Neal Koblitz},
title = {Another Look at Automated Theorem-Proving},
howpublished = {Cryptology {ePrint} Archive, Paper 2007/401},
year = {2007},
url = {https://eprint.iacr.org/2007/401}
}