Another look at automated theorem-proving. II

Neal Koblitz
Journal of Mathematical Cryptology, 5 (2011), 205-224.

Abstract: I continue the discussion initiated in my earlier paper 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.

Journal paper       Eprint paper