Fully Automated Analysis of Padding-Based Encryption in the Computational Model

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.

2013.CCS.pdf
PDF file

In  20th ACM Conference on Computer and Communications Security, CCS 2013

Publisher  ACM

Details

TypeInproceedings
URLhttp://dx.doi.org/10.1145/2508859.2516663
Pages1247-1260
> Publications > Fully Automated Analysis of Padding-Based Encryption in the Computational Model