Cryptology ePrint Archive: Report 2007/401
Another Look at Automated Theorem-Proving
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 ]