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


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.


Publication typeInproceedings
Published in3rd International Conference on Interactive Theorem Proving, ITP 2012
SeriesLecture Notes in Computer Science
> Publications > Computer-Aided Cryptographic Proofs