Certification d'une implantation de PGP

Sujet:

Le groupe CROAP 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 des programmes d'encodage de données les plus répandus aujourd'hui PGP (Pretty Good Privacy). PGP (ref[2]) est composé de 4 algorithmes principaux:

  1. un algorithme de codage symétrique IDEA
  2. un algorithme de codage asymétrique RSA
  3. une function de hachage MD5
  4. un générateur de nombre de clés ANSI X9.17
Une des préoccupations des gens qui utilisent PGP est de s'assurer que leur implantation de PGP ne contienne pas de cheval de Troie (ref [3]), c'est-à-dire qu'en plus des informations encodées le programme ne génére pas d'information supplémentaire permettant de le décoder. Le but de ce stage est de montrer comment appliquer la technologie de certification de programme pour obtenir une implantation de PGP dont on peut assurer qu'elle ne contient pas de trappe.

Encadrement:

Loïc Pottier, Laurent Théry

Contact:

Tel: 04 92 38 78 19 ou 04 92 38 78 16

E-mail : Loic.Pottier@sophia.inria.fr , Laurent.Thery@sophia.inria.fr

Laboratoire d'accueil:

Projet CROAP, INRIA Sophia Antipolis

Matériel:

Station de travail ou PC

Durée:

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 .

    [2]K. Thompson, Reflections on Trusting Trust , dans ACM Turing award lectures : the first twenty years, Addison-Wesley Ed.., 1987 .

    Laurent Théry

    Retour à la page du projet