Computer-Aided Cryptographic Proofs
- Gilles Barthe ,
- Juan Manuel Crespo ,
- Benjamin Grégoire ,
- César Kunz ,
- Santiago Zanella-Béguelin
3rd International Conference on Interactive Theorem Proving, ITP 2012 |
Published by Springer
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.