Information Trust Institute block of abstract images
Information Trust Institute block of abstract images

Computer-Aided Cryptographic Proofs


Gilles Barthe
Research Professor
IMDEA Software Institute, Spain

Watch These Sessions

Part 1 - (Video runs from 00:17:55 to 01:22:09)

Parts 2 and 3 - (Video runs from 00:04:50 to 02:08:28)

Part 4 - (Video runs from 00:05:00 to 01:08:34)


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 lecture 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.

Suggested Reading:

"EasyCyrpt: Computer-Aided Cryptographic Proofs"


Gilles Barthe received a Ph.D. in Mathematics from the University of Manchester, UK, in  1993, and an Habilitation à diriger les recherches in Computer Science from the University of Nice, France, in 2004. He joined the IMDEA Software Institute in April 2008. His research interests include formal methods, programming languages and program verification, security and cryptography. Since 2006, he is working on the development of formal verification tools for cryptographic proofs.