Paper 2012/695

Fully Automated Analysis of Padding-Based Encryption in the Computational Model

Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, Yassine Lakhnech, Benedikt Schmidt, and Santiago Zanella-Béguelin


Computer-aided verification provides effective means of analyzing the security of cryptographic primitives. However, it has remained a challenge to achieve fully automated analyses yielding guarantees that hold against computational (rather than symbolic) attacks. This paper meets this challenge for public-key encryption schemes built from trapdoor permutations and hash functions. Using a novel combination of techniques from computational and symbolic cryptography, we present proof systems for analyzing the chosen-plaintext and chosen-ciphertext security of such schemes in the random oracle model. Building on these proof systems, we develop a toolset that bundles together fully automated proof and attack finding algorithms. We use this toolset to build a comprehensive database of encryption schemes that records attacks against insecure schemes, and proofs with concrete bounds for secure ones.

Available format(s)
Public-key cryptography
Publication info
Published elsewhere. An abridged version of this paper is under submission. This is the full version.
Attack findingautomated proofsEasyCryptprovable securitypublic-key encryptionstatic equivalence
Contact author(s)
santiago @ microsoft com
2013-07-03: last of 2 revisions
2012-12-14: received
See all versions
Short URL
Creative Commons Attribution


      author = {Gilles Barthe and Juan Manuel Crespo and Benjamin Grégoire and César Kunz and Yassine Lakhnech and Benedikt Schmidt and Santiago Zanella-Béguelin},
      title = {Fully Automated Analysis of Padding-Based Encryption in the Computational Model},
      howpublished = {Cryptology ePrint Archive, Paper 2012/695},
      year = {2012},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.