Cryptology ePrint Archive: Report 2012/308

Verified Security of Redundancy-Free Encryption from Rabin and RSA

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

Abstract: 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.

Category / Keywords: public-key cryptography / Public-key encryption, provable security, machine-checked proofs, OAEP, SAEP, ZAEP

Publication Info: To appear in 19th ACM Conference on Computer and Communications Security, CCS 2012. ACM Press, 2012.

Date: received 31 May 2012, last revised 6 Aug 2012

Contact author: santiago at microsoft com

Available formats: PDF | BibTeX Citation

Note: Added publication information.

Version: 20120806:140616 (All versions of this report)

Discussion forum: Show discussion | Start new discussion