Paper 2012/308

Verified Security of Redundancy-Free Encryption from Rabin and RSA

Gilles Barthe, David Pointcheval, and Santiago Zanella-Béguelin


Verified security provides a firm foundation for cryptographic proofs by means of rigorous programming language techniques and verification methods. EasyCrypt is a framework that realizes the verified security paradigm and supports the machine-checked construction and verification of cryptographic proofs using state-of-the-art SMT solvers, automated theorem provers and interactive proof assistants. Previous experiments have shown that EasyCrypt is effective for a posteriori validation of cryptographic systems. In this paper, we report on the first application of verified security to a novel cryptographic construction, with strong security properties and interesting practical features. Specifically, we use EasyCrypt to prove the IND-CCA security of a redundancy-free public-key encryption scheme based on trapdoor one-way permutations. Somewhat surprisingly, we show that even with a zero-length redundancy, Boneh's SAEP scheme (an OAEP-like construction with a single-round Feistel network rather than two) converts a trapdoor one-way permutation into an IND-CCA-secure scheme, provided the permutation satisfies two additional properties. We then prove that the Rabin function and RSA with short exponent enjoy these properties, and thus can be used to instantiate the construction we propose to obtain efficient encryption schemes. The reduction that justifies the security of our construction is tight enough to achieve practical security with reasonable key sizes.

Note: Added publication information.

Available format(s)
Public-key cryptography
Publication info
Published elsewhere. To appear in 19th ACM Conference on Computer and Communications Security, CCS 2012. ACM Press, 2012.
Public-key encryptionprovable securitymachine-checked proofsOAEPSAEPZAEP
Contact author(s)
santiago @ microsoft com
2012-08-06: last of 2 revisions
2012-06-03: received
See all versions
Short URL
Creative Commons Attribution


      author = {Gilles Barthe and David Pointcheval and Santiago Zanella-Béguelin},
      title = {Verified Security of Redundancy-Free Encryption from Rabin and RSA},
      howpublished = {Cryptology ePrint Archive, Paper 2012/308},
      year = {2012},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.