Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Fully Automated Analysis of Padding-Based Encryption in the Computational Model

Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, Yassine Lakhnech, Benedikt Schmidt, and Santiago Zanella-Béguelin

Abstract

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.

Details

Publication typeInproceedings
Published in20th ACM Conference on Computer and Communications Security, CCS 2013
URLhttp://dx.doi.org/10.1145/2508859.2516663
Pages1247-1260
PublisherACM
> Publications > Fully Automated Analysis of Padding-Based Encryption in the Computational Model