Cryptology ePrint Archive: Report 2012/695
Fully Automated Analysis of Padding-Based Encryption in the Computational Model
Gilles Barthe and Juan Manuel Crespo and Benjamin Grégoire and César Kunz and Yassine Lakhnech and 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
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.
Category / Keywords: Public-key cryptography / Attack finding, automated proofs, EasyCrypt, provable security, public-key encryption, static equivalence
Publication Info: An abridged version of this paper is under submission. This is the full version.
Date: received 11 Dec 2012, last revised 3 Jul 2013
Contact author: santiago at microsoft com
Available format(s): PDF | BibTeX Citation
Version: 20130703:160407 (All versions of this report)
Short URL: ia.cr/2012/695
[ Cryptology ePrint archive ]