International Association
for Cryptologic Research

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.