Conception of a language for cryptographic reductions
Leo Ducas
Abstract:
Recently, many efforts have been directed into developing formal frameworks to prove security of cryptographic constructions and protocols. While many security properties can be automatically proved or certified in existing frameworks, there are still some recent cryptographic results that are out of the reach of these formal models, such as impossibility results via meta-reductions, or security proofs based on the forking lemma. The goal of this master thesis was to design a language and its semantics, that makes it possible to state and prove such modern cryptographic results in a constructive way, that is, as suggested by Rogaway, by programming cryptographic reductions explicitly. Accordingly, we defined a dedicated lambda-calculus "a la Moggi", with a denotational semantic, references, algebraic data structure, monadic types and polymorphic types. interpreter and three examples were implemented, allowing us to run and test constructions, but also cryptographic reductions. One of them uses polymorphic types to formalize generic models in an elegant and -- to our knowledge -- original way. We sketched how to apply the theory of parametricity to our language in order to use our definition of genericity in existing cryptographic proofs.