Auteur : Nicolas Pouillard -  ITU (IT University of Copenhagen), DemTech project

Titre : Proving cryptographic schemes in Agda
Sous-titre :  Dependently typed functional programming for Alice and Bob


Abstract : 

 In order to gain confidence in cryptographic schemes and primitive
 operations, cryptographers use a combination of theories. These
 theories enable us to mathematically prove security properties of
 these constructions. Probability theory, game theory, number theory
 and complexity theory are often all needed at the same time. We aim
 at realizing these proof arguments in Type Theory using Agda. Our
 current approach is to carefully use abstractions and dependently
 typed functional programming techniques to elegantly prove security
 properties. Finally we aim at reducing the usual gap between the
 formal description of the construction and its actual implementation.
 We do so by writing in a functional style supporting extraction into
 low level circuits.