## 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