IACR News item: 03 June 2012
Gilles Barthe, David Pointcheval, Santiago Zanella-Béguelin
ePrint Reportby 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.
Additional news items may be found on the IACR news page.