[Resource Topic] 2007/401: Another Look at Automated Theorem-Proving

Welcome to the resource topic for 2007/401

Title:
Another Look at Automated Theorem-Proving

Authors: Neal Koblitz

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.

ePrint: https://eprint.iacr.org/2007/401

See all topics related to this paper.

Feel free to post resources that are related to this paper below.

Example resources include: implementations, explanation materials, talks, slides, links to previous discussions on other websites.

For more information, see the rules for Resource Topics .