To: seminaire@pauillac.inria.fr From: Didier.Remy@inria.fr Subject: SEM - INRIA : Cristal - 30/03/01 - Paris - FR Vous pouvez maintenant vous abonner à nos annonces de séminaires http://pauillac.inria.fr/seminaires/subscribe.html S E M I N A I R E . ___ / _ _ / _ / / / \ / \ / / __| / |___ |_/ |_/ / |__ |_/ |_ ___ . / / ___ __ /_ _ / _/ /| /| _ __ __ _ _ / / / /_ / __| / / |/ | / \ /_ / / \ | / __| |___ / / __/ |_ |_/ |_ / | |_/__/ |_ |_/ |/ |_/ I N R I A - Rocquencourt Salle de conference du Bat 11 Vendredi 30 mars, 10h30 -------------- Bruno Blanchet -------------- Projet Moscova ====================================================================== Preuve de propriétés de secret dans des protocoles cryptographiques, par typage d'une part et par un vérificateur automatique d'autre part. ====================================================================== Cet exposé comprendra deux parties. Dans la première partie, je présenterai un calcul de processus pour les protocoles cryptographiques, et un système de types pour ce calcul, dans lequel les types expriment des propriétés de secret. Ce calcul traite les primitives de communication asymétriques, en particulier le chiffrement à clé publique. Ces primitives présentent des difficultés particulières, car elles utilisent des capabilités liées (par exemple, clés publiques et secrètes) avec des niveaux de secret et des portées différents. Ce travail a été effectué en collaboration avec Martín Abadi. Dans la deuxième partie, je présenterai un vérificateur de protocoles cryptographiques, qui prouve également des propriétés de secret. Ce vérificateur utilise une représentation simple du protocole par des règles Prolog. L'algorithme usuel de Prolog ne termine jamais sur ces règles, donc j'ai conçu un nouvel algorithme efficace, qui détermine si un fait peut ou non être prouvé à partir des règles. Ce vérificateur évite le problème de l'explosion de l'espace d'états et n'impose pas de limiter le nombre d'exécutions du protocole pour le vérifier. Les résultats expérimentaux montrent que beaucoup d'exemples de protocoles de la littérature, dont Skeme, peuvent être analysés par cet outil, rapidement et en utilisant peu de mémoire.