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.