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.
Speakers
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.
Literature
Bellare Rogoway, Code-Based Game-Playing Proofs and the Security of Triple Encryption
Course assessment
Credits will be given based on active participation and completion of the exercises. More credits are available based on projects.
Preparation
Students should bring their laptop and are expected to have easycrypt and F* installed. F* can also be used via the web-interface. A virtual machine for easycrypt: https://www.easycrypt.info/binaries/
http://prosecco.gforge.inria.fr/personal/hritcu/teaching/aarhus2017/
https://www.fstar-lang.org/run.php
For people who want to get F* installed on their machine there are 2 easy options:
1. Using the latest binary release (v0.9.5.0)
https://github.com/FStarLang/FStar/blob/master/INSTALL.md#binary-releases
https://github.com/FStarLang/FStar/releases/tag/v0.9.5.0
2. Using the OPAM package (especially for people already using OCaml)
https://github.com/FStarLang/FStar/blob/master/INSTALL.md#opam-package
For people who are more motivated, there are even more ways including building things from sources. It's all documented in the INSTALL.md file, which you already link:
https://github.com/FStarLang/FStar/blob/master/INSTALL.md
Time and place
Week 41 (9-13 Oct)
Room: Ada-333, Katrinebjerg, Aarhus N (Might change)
See the full program
Credits
1ECTS, with a possibility for more based on projects.
Registration: https://auws.au.dk/Computer-aided-security-proof
Deadline for registration is October 2, 2017.
