Conception of a language for cryptographic reductions
Léo Ducas (Master Thesis). Internship Supervised by Mathieu Baudet. ANSSI.L'objectif de ce stage est de concevoir un langage minimaliste permettant de programmer explicitement (au moins en theorie) toutes les reductions algorithmiques sousjacentes aux preuves de securite en cryptographie. La semantique du langage permettra de donner un sens mathematique rigoureux aux protocoles et aux reductions programmes. (On pourra supposer les operations algebriques sur les objets mathematiques predefinies dans le langage.) De plus, le systeme de typage du langage devra etre en mesure de garantir la bonne formation des programmes en tant que protocole, contexte d'attaque ou reduction cryptographique valide (gestion correcte de l'alea, respect de l'etat interne des oracles, etc). Une piste interessante et encore peu exploree pour la definition d'un tel langage est de recourir a un lambda-calcul avec monades. Il est raisonnable de penser qu'un tel langage, purement fonctionnel, sera plus commode a analyser de maniere automatique (ne serait-ce que pour le typage au sens ci-dessus) ou a manipuler dans un assistant de preuve comme Coq, ouvrant ainsi la voie a d'autres applications. Une fois le langage defini, on pourra etudier la formalisation et la preuve par reduction de plusieurs enonces cryptographiques simples, de preference dans le cadre de la securite concrete (i.e. non asymptotique). Si le temps le permet, on pourra egalement investiguer differentes techniques de preuve sur les proprietes des programmes du langage, par exemple en s'inspirant des methodes existantes en cryptographie.
Repport (French) (PDF)
Slides (English) (PDF)