Cryptology ePrint Archive: Report 2012/695

Automated Analysis and Synthesis of Padding-Based Encryption Schemes

Gilles Barthe and Juan Manuel Crespo and Benjamin Grégoire and César Kunz and Yassine Lakhnech and Santiago Zanella-Béguelin

Abstract: Verifiable security is an emerging approach in cryptography that advocates the use of principled tools for building machine-checked security proofs of cryptographic constructions. Existing tools following this approach, such as EasyCrypt or CryptoVerif, fall short of finding proofs automatically for many interesting constructions. In fact, devising automated methods for analyzing the security of large classes of cryptographic constructions is a long-standing problem which precludes a systematic exploration of the space of possible designs. This paper addresses this issue for padding-based encryption schemes, a class of public-key encryption schemes built from hash functions and trapdoor permutations, which includes widely used constructions such as RSA-OAEP.

Firstly, we provide algorithms to search for proofs of security against chosen-plaintext and chosen-ciphertext attacks in the random oracle model. These algorithms are based on domain-specific logics with a computational interpretation and yield quantitative security guarantees; for proofs of chosen-plaintext security, we output machine-checked proofs in EasyCrypt. Secondly, we provide a crawler for exhaustively exploring the space of padding-based encryption schemes under user-specified restrictions (e.g. on the size of their description), using filters to prune the search space. Lastly, we provide a calculator that computes the security level and efficiency of provably secure schemes that use RSA as trapdoor permutation.

Using these three tools, we explore over 1.3 million encryption schemes, including more than 100 variants of OAEP studied in the literature, and prove chosen-plaintext and chosen-ciphertext security for more than 250,000 and 17,000 schemes, respectively.

Category / Keywords: public-key cryptography / public-key cryptography, synthesis, provable security, one-way functions, RSA, OAEP, EasyCrypt

Publication Info: An abridged version of this paper is under submission. This is the full version.

Date: received 11 Dec 2012, last revised 13 Dec 2012

Contact author: santiago at microsoft com

Available formats: PDF | BibTeX Citation

Version: 20121214:185243 (All versions of this report)

Discussion forum: Show discussion | Start new discussion