Computer-aided security proofs

One week, intense PhD-course with an emphasize on the easycrypt proof assistant and the F* programming language. The course of loosely based on the course in Nancy.


François Dupressoir (Surrey)

Cătălin Hriţcu (INRIA)

Cédric Fournet (Microsoft)      

Bas Spitters (Aarhus University) (Organizer)

Pierre-Yves Strub  (École Polytechnique)              

Aseem Rastogi (Microsoft Research)

Aims, audience, and prerequisites
The course aims to introduce the participants to the principles of computer aided security proofs. The primary audience are PhD students working on topics related to the focus of the school, but also researchers and advanced master students in cryptography or programming language that would like to learn more about tool support for cryptographic proofs. The course 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 lectures will introduce several methods (e.g. Hoare logic, theorem proving, type inference), will introduce tools (F*, Easycrypt) and will consider a range of applications from the security. Each topic will have allocated a couple of lectures and a problem class.


Course assessment
Credits will be given based on active participation and completion of the exercises. More credits are available based on projects.

Students should bring their laptop and are expected to have easycrypt and F* installed. F* can also be used via the web-interface.

Time and place
Week 41 (9-13 Oct)
Room: Ada-333, Katrinebjerg, Aarhus N (Might change)

1ECTS, with a possibility for more based on projects.

Deadline for registration is October 2, 2017.