Models and Tools for Cryptographic Proofs

Nancy, France (10th of July 2017 - 13th of July 2017)

The University of Bristol in collaboration with INRIA and LORIA, Nancy with the support of the H2020 EU project ECYPT-CSA are organizing a summer school on formal verification of cryptographic systems.

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.



The lectures will cover proofs in: F* (Catalin Hritcu and Markulf Kohlweiss), Proverif (Veronique Cortier and Steve Kremer) and Easycrypt (Gilles Barthe and Francois Dupressoir).

Monday Tuesday Wednesday Thursday
9:00-10:30 Kohlweiss/Hritcu Cortier/Kremer Barthe/Dupressoir Barthe/Dupressoir
10:30-11:00 Coffee break Coffee break Coffee break Coffee break
11:00-12:30 Kohlweiss/Hritcu Cortier/Kremer Barthe/Dupressoir Barthe/Dupressoir
12:30-14:00 Lunch Lunch Lunch Lunch
14:00-15:30 Kohlweiss/Hritcu Cortier/Kremer Cortier/Kremer Barthe/Dupressoir
15:30-16:00 Coffee break Cofee break Coffee break Coffee break
16:00-17:30 Kohlweiss/Hritcu Kohlweiss/Hritcu Cortier/Kremer Good bye


  • Veronique Cortier
  • Bogdan Warinschi


To ensure an interactive learning environment, the number of places is limited. Interested participants are invited to submit their application by email to Sarah Rogers at the University of Bristol ( . The subject of the email should be: "Summer school application -- your name". The application should include a brief CV (at most two A4 pages) and a statement of interest (at most one A4 page). The registration fee is 150GPB and covers coffee breaks and lunch for the duration of the school, as well as a social event. Please register your interest by May 30th 2017. Applicants will be notified of their acceptance soon after. A limited number of scholarships that partially cover participation and accommodation fees are also available. Please state clearly whether you require support in your application.


The school will be held at Loria, Nancy, France.

Travel info

Arrival information and information on the location can be found HERE