Program synthesis offers an effective means to exhaustively explore the design space of a class of algorithms: it can serve as a basis for understanding existing algorithms as points into a well-mapped space and for showing that they are optimal or, on the contrary, for discovering better alternatives. These benefits make synthesis of cryptographic constructions particularly attractive. However, applying synthesis to cryptography has remained challenging, partly because cryptographic constructions are probabilistic algorithms and because their security is formulated as a probabilistic indistinguishability property.

We have developed an automated tool which synthesises provably secure public-key encryption schemes based on trapdoor permutations and hash functions. The tool comprises three independent components: 1) a generation algorithm that synthesises candidate schemes, using simple yet effective symbolic filters that ensure some baseline properties of interest; 2) a checker which verifies that a candidate is IND-CPA and generates a certificate in the form of a reduction with concrete security bounds (independently verifiable in Easycrypt); and 3) a checker which verifies that a candidate is IND-CCA and computes concrete security bounds although not yet a certificate.

The applicability of our techniques is illustrated by generating and analysing the security of over 120,000 schemes. Our tool synthesises (and proves secure) most schemes from the literature, as well many schemes that have not been studied before. In particular, we analyse 120 variants of OAEP, a widely used padding scheme commonly used for strengthening RSA encryption. Our tool proves most secure variants of OAEP and computes security bounds that in many cases match the best known bounds from the literature.

In this talk, I will try to present a high level description of the tool, as well as some details of the first two components.