Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Computer-Aided Cryptographic Proofs

Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, and Santiago Zanella-Béguelin

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.

Details

Publication typeInproceedings
Published in3rd International Conference on Interactive Theorem Proving, ITP 2012
URLhttp://dx.doi.org/10.1007/978-3-642-32347-8_2
Pages11-27
Number7406
SeriesLecture Notes in Computer Science
PublisherSpringer
> Publications > Computer-Aided Cryptographic Proofs