Computer-aided security proofs

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

 

Course parameters:

Language: English

Level of course: PhD course (but open to advanced Master’s students)

Time of year: Week 41 (9-13 October 2017)

No. of contact hours/hours in total incl. preparation, assignment(s) or the like: 37

Capacity limits: None

 

Objectives of the course:

The course aims to introduce the participants to the principles of computer aided security proofs. The primary audience is 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.

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

 

Learning outcomes and competences:

At the end of the course, the student should be able to:

- understand the principles of computer aided security proofs

- understand “provable security” framework

 

Compulsory programme:

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

 

Course contents:

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.

 

Prerequisites:

No specific prior knowledge on cryptography is required, but familiarity with basic concepts from the theory of formal languages and theory of programming languages is recommended.

 

Name of lecturers:

·         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)

 

Type of course/teaching methods: Lectures followed by exercises.

 

Literature: Students should bring their laptop and are expected to have easycrypt and F* installed. F* can also be used via the web-interface.  Please read: Bellare Rogoway, Code-Based Game-Playing Proofs and the Security of Triple Encryption.

 

Course homepage: http://cs.au.dk/research/logic-and-semantics/courses/

 

Course assessment:

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

 

Provider: Department of Computer Science, Aarhus University. Organizer: Associate Professor Bas Spitters

Time: Week 41 (9-13 October 2017). See full program here.

 

Place: Department of Computer Science, Åbogade 34, 8200 Aarhus N, Denmark. Room: Ada-333 (might change)

 

Registration:

Deadline for registration is 2 October, 2017. Sign up here: https://auws.au.dk/Computer-aided-security-proofs.

 

If you have any questions, please contact;

·         Course contents: Bas Spitters, e-mail: spitters@cs.au.dk

·         Registration or other practicalities: Sofia Rasmussen, e-mail: sofia@cs.au.dk