Skip to Main content Skip to Navigation
Conference papers

Verified security of redundancy-free encryption from Rabin and RSA

Gilles Barthe 1 David Pointcheval 2 Santiago Zanella-Béguelin 3 
2 CASCADE - Construction and Analysis of Systems for Confidentiality and Authenticity of Data and Entities
DI-ENS - Département d'informatique - ENS Paris, Inria Paris-Rocquencourt, CNRS - Centre National de la Recherche Scientifique : UMR 8548
Abstract : Verified security provides a firm foundation for crypto-graphic proofs by means of rigorous programming language techniques and verification methods. EasyCrypt is a frame-work 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 in the Random Oracle Model 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.
Document type :
Conference papers
Complete list of metadata
Contributor : David Pointcheval Connect in order to contact the contributor
Submitted on : Thursday, December 13, 2012 - 3:09:56 PM
Last modification on : Thursday, March 17, 2022 - 10:08:36 AM

Links full text




Gilles Barthe, David Pointcheval, Santiago Zanella-Béguelin. Verified security of redundancy-free encryption from Rabin and RSA. CCS '12 - ACM conference on Computer and communications security, Oct 2012, Raleigh, NC, United States. pp.724-735, ⟨10.1145/2382196.2382272⟩. ⟨hal-00764871⟩



Record views