### Verified Security of Redundancy-Free Encryption from Rabin and RSA

Gilles Barthe, 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.

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

CC BY

BibTeX

@misc{cryptoeprint:2012/308,
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{https://eprint.iacr.org/2012/308}},
url = {https://eprint.iacr.org/2012/308}
}

Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.