Cryptology ePrint Archive: Report 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.

Category / Keywords: public-key cryptography / automated theorem-proving, proof-checking, public key cryptography, signatures, encryption

Publication Info: This is a slightly expanded version of a paper to appear in the Journal of Mathematical Cryptology.

Date: received 17 Oct 2007

Contact author: koblitz at math washington edu

Available format(s): PDF | BibTeX Citation

Version: 20071021:182751 (All versions of this report)

Discussion forum: Show discussion | Start new discussion

[ Cryptology ePrint archive ]