Program - Computer-aided security proofs

Time and place

  • Week 41 (9-13 Oct)
  • Room: Ada-333, Department of Computer Science, Aarhus University. Åbogade 34, 8200 Aarhus N


Preliminary Program

Monday starts at 10 for the people travelling from far.

Lunch each day 12:00-13:00



10:00-11:00 Everest project (CF)

11:00-12:00 Introduction to F* (CH)

13:00-17:00 Introduction to F* (CH)


9:00 -12:00 Cryptography in F* (CF)

13:00-16:00 Verification of crypto in F* (AR)

16:00-17:00 Secure file transfer (AR)



 9:00-11:00 Foundations of F*: type system and SMT (AR)

11:00-12:00 Relational probabilistic programming in F* (AR)

13:00-15:30: Introduction to Interactive Theorem Proving/Formal Proofs (PYS)

15:30-17:00: Introduction to Game-Based Code-Based Cryptography (FD)

18:30: Dinner at restaurant Italia



9:00-12:00: EC tutorial – Guided Walkthrough of a Formal Crypto Proof (FD)

13:00-17:00: EC exercises – Cryptographic Proofs for Simple Functionalities (FD and PYS)



9:00-12:00: Advanced Techniques (PYS and FD)

13:00-14:00: Secure Multiparty computation in Easycrypt (BS)

14:00-15:30: Reasoning about Implementations and Side-Channel Security (FD)

15:30-17:00: EasyCrypt for probabilistic programming (PYS)