Another Look at Automated Theorem-Proving

Neal Koblitz

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-proving proof-checking public key cryptography signatures encryption
Contact author(s): koblitz @ math washington edu
History: 2007-10-21: received
Short URL: https://ia.cr/2007/401
License: 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}
}