Computer-Aided Cryptographic Design and Analysis

Gilles Barthe and Yassine Lakhnech / PERSYVAL-Lab

Computer-aided cryptography aims to develop tools that support the design, analysis, and secure implementation of cryptographic constructions.  In this presentation, I will give an overview of EasyCrypt (www.easycrypt.info), an interactive framework for building and verifying cryptographic proofs. I will outline its design principles, and then introduce the relational program verification technique which it uses to capture common patterns of reasoning in provable security. Finally, I will report on some recent developments to extend EasyCrypt to reason about cryptographic implementations in C, and to connect with the CompCert verified compiler to generate provably secure assembly code for cryptographic algorithms.