Cryptology ePrint Archive: Report 2011/485

Another Look at Automated Theorem-Proving. II

Neal Koblitz

Abstract: I continue the discussion initiated in part I of whether or not computer-assisted proofs are a promising approach to preventing errors in reductionist security arguments. I examine some recent papers that describe automated security proofs for hashed ElGamal encryption, Boneh-Franklin identity-based encryption, and OAEP.

Category / Keywords: public-key cryptography / public-key cryptography, automated proofs, proof checking, encryption

Publication Info: not submitted yet

Date: received 8 Sep 2011

Contact author: koblitz at uw edu

Available format(s): PDF | BibTeX Citation

Version: 20110910:014736 (All versions of this report)

Short URL: ia.cr/2011/485

Discussion forum: Show discussion | Start new discussion