Another look at automated theorem-proving
Journal of Mathematical Cryptology, 1 (2007), 385-403.
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