06084478

a

06084478 Barthe, Gilles Crespo, Juan Manuel Gr\'egoire, Benjamin Kunz, C\'esar Zanella B\'eguelin, Santiago Computer-aided cryptographic proofs. Beringer, Lennart (ed.) et al., Interactive theorem proving. Third international conference, ITP 2012, Princeton, NJ, USA, August 13--15, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-32346-1/pbk). Lecture Notes in Computer Science 7406, 11-27 (2012). 2012 Berlin: Springer EN

doi:10.1007/978-3-642-32347-8_2

Summary: 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.