Title: Computer-aided cryptography

Lecturer: Dr. Gilles Barthes

Period: May 28: 16-18;  29, 30:  9-12 / June 3,4,5,6: 9-12 / Sala Seminari W

Computer-aided cryptography is an emerging approach to designing and analyzing cryptographic constructions. Its primary focus is to build machine-checked frameworks for the construction and verification of security proofs of cryptographic systems. In the form of tools like EasyCrypt, verified security has been used for verifying emblematic examples of public-key encryption schemes, digital signature schemes, hash function designs, and block cipher modes of operation. Moreover, computer-aided cryptography allows narrowing the gap between provable security and cryptographic implementations, which remains one major issue in the deployment of cryptographic systems. However, the role of computer-aided cryptography is not limited to security proofs, and there exist automated tools for discovering new cryptographic constructions, or automatically finding attacks on existing ones.

The purpose of the course is to motivate the role of computer-aided cryptography, and to give an overview of some recent developments. The main emphasis of the course will be on computer-aided cryptographic proofs, and more specifically on EasyCrypt. The course will describe the foundations of EasyCrypt, provide an introduction to provable security using EasyCrypt, and will cover some representative topics in computer-aided cryptography.

Tentative schedule (2 hours each)

Lecture 1: Introduction

Lecture 2: Provable security (security definitions, assumptions, game-based technique)

Lecture 3: Probabilistic programs (syntax, semantics, probabilistic Hoare logic)

Lecture 4: Relational Hoare Logic

Lecture 5: Advanced verification techniques (eager/lazy sampling, modular proofs, hybrid arguments)

Lecture 6: Padding-based encryption schemes (automated proofs, synthesis, symbolic attack discovery)

Lecture 7: Cryptographic implementations (side-channel attacks, verified C implementations, code generation)

Lecture 8: Key-exchange protocols (models, formalization, NAXOS)

Lecture 9: Differential privacy

Lecture 10: Higher-order programs