Santiago Zanella-Béguelin, Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, and Yassine Lakhnech
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.
Publisher International Association for Cryptologic Research
|Book title||IACR Cryptology ePrint Archive 2012|