IMDEA Software

IMDEA initiative

Home > Events > Software Seminar Series > 2013 > Fully Automated Analysis of Padding-Based Encryption in the Computational Model

Benedikt Schmidt

Tuesday, October 29, 2013

11:00am Meeting room 302 (Mountain View), level 3

Benedikt Schmidt, Post-doctoral Researcher, IMDEA Software Institute

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

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 meets this challenge for public-key encryption schemes built from trapdoor permutations and hash functions. Using a novel combination of techniques from 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. Building on these proof systems, we develop a toolset that bundles together fully automated proof and attack finding algorithms. We use this toolset to build a comprehensive database of encryption schemes that records attacks against insecure schemes, and proofs with concrete bounds for secure ones.