Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Automated Analysis and Synthesis of Padding-Based Encryption Schemes

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.


Publication typeOther
Book titleIACR Cryptology ePrint Archive 2012
PublisherInternational Association for Cryptologic Research
> Publications > Automated Analysis and Synthesis of Padding-Based Encryption Schemes