Résultats

La première phase du projet EVA a consisté à définir précisément le langage LAEVA utilisé pour spécifier les protocoles et à construire une base de test qui sera ensuite utilisée pour expérimenter les outils développés dans le projet. Les résultats obtenus à l'issue de cette période sont les suivants :
  1. Une syntaxe concrète pour le langage de spécification de protocoles et de propriétés.
  2. Une syntaxe abstraite pour le langage de spécification de protocoles et la sémantique associée.
  3. Une traduction de la syntaxe concrète vers la syntaxe abstraite.
  4. Une base de protocoles cryptographiques.
La syntaxe concrète et les motivations des choix effectués sont consignés dans le rapport [1] . La syntaxe abstraite a ensuite été définie sous la forme de programmes munis d'une sémantique opérationnelle. Une procédure de traduction de la syntaxe concrète vers la syntaxe abstraite présentée permet d'étendre la sémantique au langage défini dans [1] . La syntaxe abstraite et la traduction sont décrites dans le document [2] . Le document complémentaire [3] , plus technique,  sert de manuel de référence pour une version actualisée des syntaxes précédentes. La base de test qui a été construite pour expérimenter les outils développés dans le projet est présentée dans [4] . Chacun des protocoles identifiés est décrit dans le langage de EVA [1] et associé dans la base à ses propriétés attendues aussi bien que ses failles et analyses connues (le cas échéant).

Bibliographie

[1]
Rapport Technique EVA No 1, Langage de spécification de protocoles cryptographiques de EVA : syntaxe concrète, Florent Jacquemard, Daniel Le Métayer, novembre 2001.
 PDF
[2]
Rapport Technique EVA No 2, Langage de spécification de protocoles cryptographiques de EVA : syntaxe abstraite et sémantique, Jean Goubault-Larrecq, novembre 2001.
 PDF
[3]
Rapport Technique EVA No 3, Les syntaxes et la sémantique du langage de spécification EVA, Jean Goubault-Larrecq, novembre 2001.
 PS.gz   PDF
[4]
Rapport Technique EVA No 4, EVA test base, Dominique Bolignano, Francesca Fiorenza, Florent Jacquemard, Daniel Le Métayer, novembre 2001.
 PS.gz    PDF
[5]
Rapport Technique EVA No 5, Pattern-based Abstraction for Verifying Secrecy in Protocols, Liana Bozga, Yassine Lakhnech, Michael Périn , novembre 2002.
   PDF
[6]
Rapport Technique EVA No 6, L'outil de vérification HERMES,   Liana Bozga, Yassine Lakhnech, Michael Périn , mai 2002.
  PDF
[7]
Rapport Technique EVA No 7, L'outil de vérification SECURIFY,   Véronique Cortier , mai 2002.
  PDF
[8]
Rapport Technique EVA No 8, Outils CPV et CPV2, Jean Goubault-Larrecq , mai 2002.
  PDF
[9]
Rapport Technique EVA No 9, The EVA translator, Florent Jacquemard, juillet , 2003.
  PDF
[10]
Rapport Technique EVA No 10, Abstract Interpretation for Secrecy using Patterns, Liana Bozga, Yassine Lakhnech, Michael Périn, novembre, 2003.
 PS.gz   PDF
[11]
Rapport Technique EVA No 11, A symbolic calculus for cryptographic protocols, Liana Bozga, Cristian Ene, Yassine Lakhnech, novembre , 2003.
  PDF
[12]
Rapport Technique EVA No 12, Symbolic verification of cryptographic protocols with time stamps, Liana Bozga, Cristian Ene, Yassine Lakhnech, decembre , 2003.
  PDF
[13]
Rapport Technique EVA No 13, A guide for SECURIFY,   Véronique Cortier , decembre 2003.
  PDF
[14]
Rapport Technique EVA No 14, Coq certification for verification with HERMES tool, R. Janvier, M. P\'erin, Y. Lakhnech and L. Bozga, novembre, 2003.
  PDF
[15]
Rapport Technique EVA No 15, The EVA environment: Experimentation Report, Gustavo Betarte, Daniel Le Métayer (with contributions from Véronique Cortier, Michael Périn and Yassine Lakhnech), decembre , 2003.
  PDF
[16]
Rapport Technique EVA No 16, Using Unification For Opacity Properties, Laurent Mazaré, decembre , 2003.
  PDF