International Association for Cryptologic Research

International Association
for Cryptologic Research

CryptoDB

Another Look at Automated Theorem-Proving

Authors:
Neal Koblitz
Download:
URL: http://eprint.iacr.org/2007/401
Search ePrint
Search Google
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.
BibTeX
@misc{eprint-2007-13681,
  title={Another Look at Automated Theorem-Proving},
  booktitle={IACR Eprint archive},
  keywords={public-key cryptography / automated theorem-proving, proof-checking, public key cryptography, signatures, encryption},
  url={http://eprint.iacr.org/2007/401},
  note={This is a slightly expanded version of a paper to appear in the Journal of Mathematical Cryptology. koblitz@math.washington.edu 13803 received 17 Oct 2007},
  author={Neal Koblitz},
  year=2007
}