Pourquoi les preuves informelles ne suffisent pas

Les concepteurs de protocoles produisent régulièrement des arguments informels de sécurité : des raisonnements en prose expliquant pourquoi un attaquant ne peut pas réussir. L'histoire montre que ces arguments sont souvent erronés, même lorsqu'ils sont élaborés par des experts.

Needham-Schroeder (1978) a été conçu pour l'authentification mutuelle. En 1995, Gavin Lowe a découvert une attaque de l'homme du milieu à l'aide d'une vérification automatisée, 17 ans après la publication. La preuve informelle n'avait pas détecté un rejeu subtil.

WEP a été approuvé par l'IEEE en 1997 avec des affirmations de sécurité informelles. En 2001, des chercheurs ont découvert la réutilisation du flux de clés RC4, des collisions de vecteurs d'initialisation et l'absence d'intégrité, ce qui a permis de le casser en quelques minutes. Le raisonnement informel n'avait rien détecté.

La sécurité des protocoles dépend des interactions entre de nombreuses sessions concurrentes, des attaquants actifs et des hypothèses cryptographiques. Le raisonnement humain peine face à l'explosion du nombre d'états et aux exécutions concurrentes entrelacées.

Les méthodes formelles modélisent mathématiquement le protocole et démontrent, ou réfutent, des propriétés de sécurité (secret, authentification, confidentialité persistante) pour toutes les stratégies d'attaque possibles, et pas seulement pour celles envisagées par le concepteur.

Symbolique (Dolev-Yao) : la cryptographie est une boîte noire parfaite ; l'accent est mis sur la logique du protocole. Calculatoire : jeux de sécurité probabilistes réels, plus proches des garanties du monde réel. Les deux modèles détectent des erreurs réelles.

POODLE (2014) a exploité un oracle de remplissage dans CBC de SSL 3.0. La vulnérabilité était une erreur de conception au niveau du protocole, et non une erreur d'implémentation. Une analyse formelle de la spécification SSL 3.0 aurait signalé l'oracle avant le déploiement.

TLS 1.3 (RFC 8446) a été conçu parallèlement à des analyses formelles utilisant ProVerif et miTLS. La spécification a été améliorée en fonction des résultats formels, ce qui constitue une étape majeure dans l'adoption des méthodes formelles par les organismes de normalisation.

Les outils formels vérifient le modèle du protocole, pas l'implémentation. Un protocole vérifié formellement peut néanmoins avoir une implémentation non sécurisée. F* / HACL* étend la vérification au code cryptographique lui-même.

La vérification formelle est coûteuse : la modélisation d'un protocole prend des semaines et exige une expertise spécialisée. Mais pour les cibles à forte valeur (TLS, SSH, Signal), le coût est justifié : une seule erreur de protocole peut toucher des milliards d'utilisateurs.

Les preuves informelles échouent parce que le raisonnement humain ne détecte pas les interactions entre sessions concurrentes ni les stratégies des attaquants. Needham-Schroeder, WEP et POODLE reposaient tous sur des arguments de sécurité informels. TLS 1.3 a intégré une analyse formelle dès sa conception. Les outils formels détectent les erreurs au niveau du protocole avant le déploiement.