eprint.iacr.org will be offline for approximately an hour for routine maintenance again at 10pm UTC on Wednesday, April 17.

Paper 2007/401

Another Look at Automated Theorem-Proving

Neal Koblitz

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
Published elsewhere. This is a slightly expanded version of a paper to appear in the Journal of Mathematical Cryptology.
Keywords
automated theorem-provingproof-checkingpublic key cryptographysignaturesencryption
Contact author(s)
koblitz @ math washington edu
History
2007-10-21: received
Short URL
https://ia.cr/2007/401
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2007/401,
      author = {Neal Koblitz},
      title = {Another Look at Automated Theorem-Proving},
      howpublished = {Cryptology ePrint Archive, Paper 2007/401},
      year = {2007},
      note = {\url{https://eprint.iacr.org/2007/401}},
      url = {https://eprint.iacr.org/2007/401}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.