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.
Type de document :
Communication dans un congrès
2013 ACM SIGSAC Conference on Computer and Communications Security, Nov 2013, Berlin, Germany. ACM, pp.1247-1260, 2013, Proceedings of the 2013 ACM SIGSAC conference on Computer & communications security. 〈10.1145/2508859.2516663〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00935737
Contributeur : Benjamin Gregoire <>
Soumis le : vendredi 24 janvier 2014 - 07:07:26
Dernière modification le : vendredi 6 juillet 2018 - 10:08:02

Lien texte intégral

Identifiants

Collections

Citation

Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, Yassine Lakhnech, et al.. Fully automated analysis of padding-based encryption in the computational model. 2013 ACM SIGSAC Conference on Computer and Communications Security, Nov 2013, Berlin, Germany. ACM, pp.1247-1260, 2013, Proceedings of the 2013 ACM SIGSAC conference on Computer & communications security. 〈10.1145/2508859.2516663〉. 〈hal-00935737〉

Partager

Métriques

Consultations de la notice

239