Fully Automated Analysis of Padding-Based Encryption in the Computational Model - Barthe, Gilles; Crespo, Juan Manuel; Kunz, César; Schmidt, Benedikt; Grégoire, Benjamin; Lakhnech, Yassine; Zanella-Béguelin, Santiago (20th ACM Conference on Computer and Communications Security, CCS 2013, 2013)
Computer-aided verification provides effective means of analyzing the security of cryptographic primitives. However, it has remained a challenge to achieve fully automated analyses yielding guarantees that hold against computational (rather than symbolic) attacks. This paper solves this challenge for public-key encryption schemes built from trapdoor permutations and hash functions. Using a novel methodology to combine computational and symbolic cryptography, we present proof systems for analyzing the chosen-plaintext and chosen-ciphertext security of such schemes in the random oracle model, and a toolset, coined ZooCrypt, that bundles together fully automated proof search and attack finding algorithms. Using the toolset in batch mode, we build a comprehensive database of encryption schemes that records attacks against insecure schemes, and proofs with concrete bounds for secure ones.