Vérification de protocoles : la plate-forme AVISPA
Vérifier automatiquement les protocoles de sécurité

En pratique, les protocoles Internet peuvent s'exécuter en parallèle (on parle alors de sessions de protocoles). Ils sont donc fortement sujets aux attaques de type man in the middle. La question qui se pose alors, lorsqu'un protocole est mis au point, est de savoir s'il est sûr vis-à-vis de ces failles.

La technique générale est la suivante :

•  on modélise le système dans un langage mathématique ;

• on modélise dans un langage compatible les propriétés que doit vérifier le système ;

•  on confronte les deux modélisations pour savoir si le système est correct vis-à-vis des propriétés.

Lorsque l'on parle de vérification informatique de systèmes (le terme système a ici un sens générique et désigne aussi bien un programme qu'un protocole ou un régulateur de vitesse), la démarche générale est la suivante :

• On commence par modéliser le système, c'est-à-dire le représenter par des objets mathématiques sur lesquels on pourra effectuer des démonstrations. Dans le cadre du projet AVISPA, les protocoles sont modélisés à l'aide de systèmes de réécriture : il s'agit de règles de transformation syntaxique exprimant l'évolution du transit sur le réseau en fonction des messages précédemment échangés. L'écriture d'un tel système étant technique un langage de haut niveau intuitif, HLPSL (High Level Protocol Specification Language) , a été développé afin de décrire le protocole. Ensuite, un traducteur automatique le transforme en un système de réécriture, appelé IF pour Intermediate Format. Voici, par exemple, le morceau de la spécification HLPSL du protocole NSPK pour Alice dont nous donnons une description intuitive :

  role alice (A, B: agent,

  Ka, Kb: public_key,

  SND, RCV: channel (dy))

  played_by A def=

  local State : nat,

  Na, Nb: text

  init State := 0

  transition

  0. State = 0 /\ RCV(start) =|>

  State' := 2 /\ Na' := new () /\ SND({Na'.A}_Kb)

  2. State = 2 /\ RCV ({Na.Nb'}_Ka) =|>

  State'...