CryptoDB
Another Look at Automated Theorem-Proving
Authors: | |
---|---|
Download: | |
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. |
BibTeX
@misc{eprint-2007-13681, title={Another Look at Automated Theorem-Proving}, booktitle={IACR Eprint archive}, keywords={public-key cryptography / automated theorem-proving, proof-checking, public key cryptography, signatures, encryption}, url={http://eprint.iacr.org/2007/401}, note={This is a slightly expanded version of a paper to appear in the Journal of Mathematical Cryptology. koblitz@math.washington.edu 13803 received 17 Oct 2007}, author={Neal Koblitz}, year=2007 }