Fully Automated Analysis of Padding-Based Encryption in the Computational Model

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.