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 de l'École normale supérieure, 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.
Type de document :
Communication dans un congrès
CCS '12 - ACM conference on Computer and communications security, Oct 2012, Raleigh, NC, United States. ACM, pp.724-735, 2012, 〈10.1145/2382196.2382272〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00764871
Contributeur : David Pointcheval <>
Soumis le : jeudi 13 décembre 2012 - 15:09:56
Dernière modification le : vendredi 25 mai 2018 - 12:02:05

Lien texte intégral

Identifiants

Collections

Citation

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. ACM, pp.724-735, 2012, 〈10.1145/2382196.2382272〉. 〈hal-00764871〉

Partager

Métriques

Consultations de la notice

189