Another look at automated theorem-proving

Neal Koblitz
Journal of Mathematical Cryptology, 1 (2007), 385-403.

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.

Journal paper       Eprint paper