Computer-Aided Security Proofs for the Working Cryptographer

Gilles Barthe 1 Benjamin Grégoire 2 Santiago Zanella-Béguelin 3 Sylvain Heraud 2
1 Institute IMDEA Software [Madrid]
2 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
3 Microsoft - Microsoft Research [Cambridge]
Abstract : We present EasyCrypt, an automated tool for elaborating security proofs of cryptographic systems from proof sketches–compact, formal representations of the essence of a proof as a sequence of games and hints. Proof sketches are checked automatically using off-the-shelf SMT solvers and automated theorem provers, and then compiled into verifiable proofs in the CertiCrypt framework. The tool supports most common reasoning patterns and is significantly easier to use than its predecessors. We argue that EasyCrypt is a plausible candidate for adoption by working cryptographers and illustrate its application to security proofs of the Cramer-Shoup and Hashed ElGamal cryptosystems.
Type de document :
Communication dans un congrès
Advances in Cryptology - 2011 - 31st Annual Cryptology Conference, 2011, Santa Barbara, United States. Advances in Cryptology - 2011 - 31st Annual Cryptology Conference, Santa Barbara, CA, USA, August 14-18, 2011. Proceedings, 2011, 〈10.1007/978-3-642-22792-9_5〉
Liste complète des métadonnées
https://hal.inria.fr/hal-01112075
Contributeur : Benjamin Gregoire <>
Soumis le : lundi 2 février 2015 - 11:26:43
Dernière modification le : jeudi 11 janvier 2018 - 16:23:51

Lien texte intégral

openaccess

Identifiants

Collections

INRIA | UNIV-COTEDAZUR

Citation

Gilles Barthe, Benjamin Grégoire, Santiago Zanella-Béguelin, Sylvain Heraud. Computer-Aided Security Proofs for the Working Cryptographer. Advances in Cryptology - 2011 - 31st Annual Cryptology Conference, 2011, Santa Barbara, United States. Advances in Cryptology - 2011 - 31st Annual Cryptology Conference, Santa Barbara, CA, USA, August 14-18, 2011. Proceedings, 2011, 〈10.1007/978-3-642-22792-9_5〉. 〈hal-01112075〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

119

Contact


archive-ouverte@inria.fr