Résultats et limites
Protocoles cryptographiques : analyse par méthodes formelles

5.1 Outils d’analyse automatiques

Dans ce cadre formel, la préservation du secret par un protocole est cependant un problème indécidable, c’est-à-dire qu’on peut démontrer [5] qu’il est impossible de construire un algorithme qui, étant donné un protocole, réponde si celui-ci préserve le secret demandé. L’indécidabilité de ce problème provient du fait que de nombreux paramètres ne sont pas bornés :

• le nombre d’agents est arbitraire ;

• le nombre de sessions est arbitraire ;

• à chaque étape, le nombre d’actions possibles est arbitraire car l’adversaire peut envoyer n’importe quel message déductible de son choix ;

• de nouvelles constantes arbitraires (représentant les nonces) peuvent être introduites à chaque étape.

Pour construire des algorithmes, il faut donc borner certains de ces paramètres.

5.1.1 Nombre de sessions borné

Une première solution est de limiter le nombre de sessions. Dans ce cas, on peut construire des algorithmes pour décider si un protocole vérifie des propriétés d’authentification ou de secret. Ainsi, de nombreux prototypes d’outils logiciels ont été construits pour vérifier les protocoles pour un nombre de sessions borné (fixé par l’utilisateur).

La plate-forme AVISPA regroupe par exemple plusieurs outils permettant de vérifier les protocoles. Ils sont utilisables en ligne à l’adresse :

Lorsqu’une attaque est détectée par un des outils, une trace de l’attaque est générée sous forme d’un schéma.

Cependant, les algorithmes de décisions permettant une telle vérification sont NP-complets [15]. Cela signifie que leur implémentation a une complexité exponentielle en la taille de l’entrée, en particulier le nombre de sessions. Aussi, les temps de vérification sont de l’ordre de la seconde pour deux sessions, de la minute pour trois sessions, de plusieurs heures voire plus pour quatre sessions et, au-delà, l’analyse est généralement...