Certification d'une implantation de l'algorithme de Diffie-Hellmann

Sujet:

Le groupe LEMME s'intéresse au développement de programmes certifiés et efficaces. Pour cela on utilise l'assistant de preuve Coq (ref [1]) pour développer en parallèle l'algorithme et sa preuve de correction. Les algorithmes définis dans Coq peuvent ensuite être efficacement compilés en OCaml.

Dans ce stage on s'attaquera à un algorithme d'échange de clés de Diffie-Hellmann. Cet algorithme se base sur des opérations sur les courbes elliptiques (ref[3]). Le travail consistera donc dans un premier temps à formaliser la notion de courbe elliptique dans le système Coq. Ensuite on fournira un programme de génération de clés dont on prouvera la correction.

Encadrement:

Laurent Théry

Contact:

Tel: 04 92 38 78 16

E-mail : Laurent.Thery@sophia.inria.fr

Laboratoire d'accueil:

Projet LEMME, INRIA Sophia Antipolis

Matériel:

Station de travail ou PC

Durée:

2-3 mois

Objectifs:

  • Apprentissage du démonstrateur Coq.
  • Définition de l'algorithme en Coq.
  • Preuve partielle de correction.

    • Références;

    [1] G. Huet, G. Kahn, C. Paulin-Mohring, The Coq Proof Assistant : A Tutorial : Version 6.1, Rapport Technique INRIA 0204, août 1997.

    [2]B. Schneier, Applied Cryptography: protocols, algorithms and source code in C , J.Wiley and sons Ed., 1996 .

    [3]J.W.S Cassels, Lectures on Elliptic Curves, London Mathematical Society Student Text.

    Laurent Théry

    Retour à la page du projet