Paper 2012/695 Original: eprint.iacr.org/2012/695 ↗
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.
Metadata
- Available format(s)
PDF- Category
- Public-key cryptography
- Publication info
- Preprint.
- History
- 2013-07-03: last updated
- 2012-12-14: published
- Short URL
- https://ia.cr/2012/695
- License
- https://creativecommons.org/licenses/by/4.0/
BibTeX
@misc{cryptoeprint:2012/695,
author = {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},
title = {Fully Automated Analysis of Padding-Based Encryption in the Computational Model},
howpublished = {Cryptology {ePrint} Archive, Paper 2012/695},
year = {2012},
url = {https://eprint.iacr.org/2012/695}
}