International Association for Cryptologic Research

International Association
for Cryptologic Research


Paper: Another Look at Automated Theorem-Proving

Neal Koblitz
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.
  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},
  note={This is a slightly expanded version of a paper to appear in the Journal of Mathematical Cryptology. 13803 received 17 Oct 2007},
  author={Neal Koblitz},