Models and Tools for cryptographic proofs

The University of Bristol in collaboration with INRIA and LORIA, with the support of the H2020 EU project ECYPT-CSA are organizing a summer school on formal verification of cryptographic systems, at Loria, between July 10th and July 13th.

Official website

Organized by the University of Bristol, Ecrypt and Loria


Aims, audience, and prerequisites

The school aims to introduce the participants to the principles of computer aided analysis of cryptographic systems. The primary audience are PhD students working on topics closely related to the focus of the school, but also researchers in cryptography that would like to learn more about tool support for cryptographic proofs. The school offers a view that complements the so-called “provable security” framework, so we encourage the participation of students that are familiar with this approach. While no specific prior knowledge on cryptography is required, familiarity with basic concepts from the theory of formal languages and theory of programming languages is recommended.

Topics and format

The school is about foundations of computer aided verification for cryptographic systems. The talks will introduce several existent methods (e.g. Hoare logic, theorem proving, type inference), will introduce some of the existing tools (Proverif, F*, Easycrypt) and will consider a range of applications from the security of basic primitives to that of key exchange protocols. Each topic will have allocated a couple of lectures and a problem class.

Lecturers