Computer-Aided Cryptographic Proofs

Gilles Barthe 1 Juan Manuel Crespo 1 Benjamin Grégoire 2 Cesar Kunz 1 Santiago Zanella-Béguelin 3
1 Institute IMDEA Software [Madrid]
2 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
3 Microsoft - Microsoft Research [Cambridge]
Abstract : EasyCrypt is an automated tool that supports the machine-checked construction and verification of security proofs of cryptographic systems, and that has been used to verify emblematic examples of public-key encryption schemes, digital signature schemes, hash function designs, and block cipher modes of operation. The purpose of this paper is to motivate the role of computer-aided proofs in the broader context of provable security and to illustrate the workings of EasyCrypt through simple introductory examples.
Type de document :
Communication dans un congrès
ITP 2012, Aug 2012, Princeton N.J., United States. Springer, 7406, 2012, Lecture Notes in Computer Science. 〈10.1007/978-3-642-32347-8_2〉
Liste complète des métadonnées
https://hal.inria.fr/hal-00765842
Contributeur : Benjamin Gregoire <>
Soumis le : mardi 18 décembre 2012 - 11:34:54
Dernière modification le : jeudi 11 janvier 2018 - 16:23:00
Document(s) archivé(s) le : mardi 19 mars 2013 - 03:53:24

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

INRIA | UNIV-COTEDAZUR

Citation

Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, Cesar Kunz, Santiago Zanella-Béguelin. Computer-Aided Cryptographic Proofs. ITP 2012, Aug 2012, Princeton N.J., United States. Springer, 7406, 2012, Lecture Notes in Computer Science. 〈10.1007/978-3-642-32347-8_2〉. 〈hal-00765842〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

255

Téléchargements de fichiers

164

Contact


archive-ouverte@inria.fr