Vérifier un protocole cryptographique avec Tamarin ou ProVerif

« Prouvé avec Tamarin », « vérifié avec ProVerif » : la mention fleurit dans les articles de recherche, les normes et, depuis peu, les plaquettes. Ces deux outils cherchent mécaniquement si un attaquant maître du réseau peut casser un protocole cryptographique, quel que soit le nombre de sessions. Reste à savoir quand commander une telle analyse, avec lequel des deux, et ce que le verdict couvre réellement.

→ Lire l’explication complète de la marmotte

Modèle symbolique de Dolev-Yao : ce que Tamarin et ProVerif vérifient

Les deux outils travaillent dans le modèle symbolique, hérité de Dolev et Yao (1983). L’attaquant y possède le réseau : il lit tout, bloque, rejoue, réordonne, injecte, et fabrique n’importe quel message à partir de ce qu’il connaît déjà. En échange, la cryptographie est supposée parfaite. Un chiffré n’est pas une suite d’octets mais un terme, du genre « chiffrement de m sous k », et la seule façon d’en tirer m est de posséder k. Les propriétés algébriques des primitives sont déclarées par des équations (déchiffrer avec la bonne clé rend le clair), et rien d’autre n’existe : ni bits, ni probabilités, ni temps de calcul.

Ce modèle attrape une famille précise de défauts : les erreurs de logique. Identité manquante dans un message, nonce non lié à la session, messages interchangeables entre deux rôles, mélange de sessions parallèles. C’est la famille qui survit à tous les tests fonctionnels, puisque les tests ne jouent que des exécutions honnêtes.

Deuxième caractéristique : le nombre de sessions n’est pas borné. L’outil ne teste pas trois exécutions entrelacées, il raisonne sur toutes. Le prix est connu depuis longtemps : dans ce cadre, le secret est indécidable. Aucun algorithme ne peut répondre à coup sûr pour tout protocole. D’où trois issues possibles, et pas deux, comme le montre la chaîne ci-dessous : il faut y lire que la traduction de la spécification en modèle est manuelle, et que le verdict ne vaut que pour ce modèle.

Un outil qui répond « je ne sais pas » reste plus honnête que la moitié des slides du secteur.

À ne pas confondre avec le modèle calculatoire, celui des cryptographes : messages en chaînes de bits, attaquant probabiliste en temps polynomial, preuve par réduction à une hypothèse de difficulté. CryptoVerif et EasyCrypt y opèrent. Une preuve symbolique dit « aucune attaque logique n’existe si les primitives sont idéales » ; une preuve calculatoire dit « casser le protocole revient à casser telle hypothèse, avec telle borne ». La seconde est plus forte et bien plus coûteuse. Les deux se complètent, et les analyses sérieuses de standards combinent souvent les deux. La façon de lire l’une et l’autre sans leur faire dire plus qu’elles ne disent est détaillée dans Lire une garantie sans la surinterpréter.

Autre frontière : les outils généralistes. TLA+ (Temporal Logic of Actions) vérifie des algorithmes distribués sans adversaire cryptographique intégré, Coq (Rocq) prouve à peu près tout à condition d’y passer le temps. La page Méthodes formelles TLA+ et Coq (Rocq) couvre ce terrain. Ici, l’attaquant actif est fourni d’office, c’est tout l’intérêt.

ProVerif : pi-calcul appliqué, clauses de Horn et verdict automatique

ProVerif est développé par Bruno Blanchet à l’Inria (Institut national de recherche en informatique et en automatique). Le protocole s’écrit en pi-calcul appliqué : des processus qui émettent et reçoivent sur des canaux, créent des noms frais (nonces, clés) et se répliquent à volonté. L’outil traduit le tout en clauses de Horn, c’est-à-dire en règles logiques de la forme « si l’attaquant connaît ceci et cela, alors il connaît aussi cela », puis sature cet ensemble par résolution. Aucune intervention humaine pendant le calcul.

La traduction est une sur-approximation, et c’est le point à retenir pour lire un résultat. Les clauses oublient combien de fois une action a eu lieu : un message émis une fois est traité comme disponible à l’infini. Conséquences :

une propriété déclarée vraie l’est réellement dans le modèle, pour un nombre non borné de sessions ;
une dérivation d’attaque peut être un artefact de l’abstraction. ProVerif tente alors de reconstruire une trace concrète : s’il y parvient, l’attaque est réelle (dans le modèle) ; sinon il répond « ne peut pas être prouvé », ce qui ne tranche ni dans un sens ni dans l’autre.

Trois familles de requêtes :

secret : l’attaquant peut-il obtenir ce terme ?
correspondance : si Bob termine une session en croyant parler à Alice, Alice a-t-elle bien lancé cette session, avec ces paramètres ? C’est la formalisation de l’authentification, en version injective (pas de rejeu) ou non ;
équivalence : deux variantes du protocole sont-elles indistinguables pour l’attaquant ? ProVerif prouve la diff-équivalence, une notion plus stricte que l’équivalence observationnelle, entre deux processus de même structure qui ne diffèrent que par certains termes. C’est par là que passent anonymat, non-traçabilité, secret fort (l’attaquant ne distingue pas un changement de la valeur secrète) et résistance à la devinette hors ligne d’un mot de passe faible.

Les limites découlent de l’abstraction. L’état global mutable passe mal : un compteur, une clé qui évolue, un « ce jeton ne sert qu’une fois » se heurtent à des clauses qui ne savent pas compter, et produisent de fausses attaques. Les versions récentes ont ajouté lemmes, axiomes et restrictions pour limiter la casse, sans changer la nature du problème. Côté algèbre, l’exponentiation de Diffie-Hellman est modélisée de façon restreinte (en général la seule commutativité des exposants), et le XOR (ou exclusif), associatif et commutatif, n’est pas pris en charge nativement. Un protocole dont la sécurité dépend d’une propriété algébrique fine du groupe sort du cadre (les propriétés en question sont décrites dans Établir une clé : Diffie-Hellman, KEM et HPKE).

Tamarin : réécriture de multi-ensembles, lemmes et preuve guidée

Tamarin est né à l’ETH Zurich (École polytechnique fédérale de Zurich) et vit aujourd’hui entre plusieurs équipes, dont le CISPA (Helmholtz Center for Information Security) et l’Inria Nancy. Le protocole n’y est pas un processus mais un ensemble de règles de réécriture de multi-ensembles : chaque règle consomme des faits (un état de session, un message reçu), en produit d’autres (nouvel état, message émis) et étiquette la transition avec des actions. Certains faits sont linéaires, consommés à l’usage, d’autres persistants. L’état mutable est donc natif : compteurs, machines à états, boucles, clés à cliquet se modélisent sans contorsion.

Les propriétés sont des lemmes : des formules de logique du premier ordre sur les traces, avec des instants explicites. « Pour toute session acceptée par Bob avec Alice, il existe un instant antérieur où Alice a lancé cette session, sauf si la clé longue durée d’Alice a été révélée avant. » La clause « sauf si » est le grand atout de l’outil : les règles de compromission (clé longue durée, clé éphémère, clé de session, état interne) s’écrivent à la main, et chaque lemme dit lesquelles il tolère. Secret persistant, résistance à l’usurpation après compromission de sa propre clé, sécurité après compromission : autant de propriétés graduées qui s’expriment directement.

Le raisonnement procède par résolution de contraintes, en remontant depuis une violation supposée jusqu’à une contradiction (preuve) ou une trace complète (attaque). Pas de sur-approximation du type ProVerif : une trace rendue est une vraie exécution du modèle. Les théories équationnelles intégrées sont plus riches, avec un Diffie-Hellman qui traite les exposants comme un groupe abélien (produits, inverses) et le XOR. Un mode d’équivalence observationnelle existe aussi.

Deux modes d’emploi : automatique, et interactif, où l’on choisit à la main quel but résoudre ensuite en visualisant le graphe de dépendances. Ce second mode n’est pas un gadget. Dès que le modèle grossit, la recherche automatique part en boucle et il faut la guider : lemmes auxiliaires (dont les lemmes de sources, qui expliquent à l’outil d’où peut venir un terme), heuristiques, oracles ou tactiques qui classent les buts. Le logiciel est gratuit ; les semaines d’expert pour écrire ces lemmes ne le sont pas. Et la terminaison n’est jamais garantie.

ProVerif ou Tamarin : comparatif et choix de l’outil

Critère	ProVerif	Tamarin
Langage de modélisation	Pi-calcul appliqué (processus)	Règles de réécriture de multi-ensembles
Moteur	Clauses de Horn, résolution	Résolution de contraintes sur les traces
Automatisation	Totale	Automatique ou interactive
Abstraction	Sur-approximation : fausses attaques possibles	Pas de fausse trace, mais non-terminaison fréquente
Propriétés	Secret, correspondances, diff-équivalence	Lemmes du premier ordre sur les traces, équivalence observationnelle
État mutable, compteurs, boucles	Point faible	Natif
Diffie-Hellman	Modélisation restreinte	Théorie intégrée plus riche
XOR	Non natif	Intégré
Compromissions graduées	Possibles, moins naturelles	Idiomatiques (règles de révélation)
Coût humain	Faible à modéré	Élevé dès que le modèle est gros
Échec typique	« Ne peut pas être prouvé »	Calcul sans fin, mémoire saturée

Le compromis central tient en une ligne : ProVerif achète l’automatisation avec de l’imprécision, Tamarin achète la précision avec du temps d’expert. D’où une règle d’ordre. Protocole sans état riche, besoin d’une réponse rapide, propriétés de confidentialité de type anonymat : ProVerif d’abord. État, compteurs, cliquets, Diffie-Hellman dont l’algèbre compte, compromissions fines : Tamarin, en acceptant la facture.

Mais pour la plupart des équipes, la vraie décision est en amont : ne pas inventer de protocole. TLS (Transport Layer Security) 1.3, les schémas du cadre Noise et WireGuard ont absorbé des années d’analyse par des gens dont c’est le métier. Les réutiliser tels quels dispense de toute vérification maison. L’analyse ne se commande que lorsqu’on s’en écarte : profil restreint ou étendu, message ajouté, composition inédite de deux mécanismes. Le protocole maison présenté comme « trois messages, rien de compliqué » est typiquement celui où il manque une identité dans le deuxième.

L’arbre suivant résume l’ordre des questions ; la première branche est celle qui évite le plus de travail.

Autour de ces deux outils gravitent Scyther (rapide, moins expressif), DeepSec (équivalences pour un nombre borné de sessions), Verifpal (syntaxe abordable, garanties plus modestes) et SAPIC+ (Stateful Applied Pi Calculus), qui part d’un modèle unique et l’exporte vers Tamarin, ProVerif et DeepSec. Ce dernier mérite un regard quand on hésite : un seul modèle, plusieurs moteurs.

Exemple : l’attaque de Lowe sur Needham-Schroeder en trace symbolique

Le protocole à clé publique de Needham et Schroeder date de 1978. Trois messages : Alice envoie à son correspondant un nonce Na et son nom, chiffrés pour lui ; le correspondant renvoie Na et un nonce Nb, chiffrés pour Alice ; Alice renvoie Nb. Chacun en conclut qu’il parle au bon interlocuteur. En 1995, Gavin Lowe publie une attaque, puis montre l’année suivante que le vérificateur FDR (Failures-Divergences Refinement) la trouve mécaniquement et valide la correction : dix-sept ans de relectures humaines étaient passées à côté.

L’attaque n’exige aucune faiblesse du chiffrement. Il faut seulement qu’Alice accepte, une fois, de parler à Mallory, participant malhonnête mais légitime. La séquence entrelace deux sessions.

À la fin, Bob est convaincu d’avoir authentifié Alice, alors qu’Alice n’a jamais cherché à lui parler. Alice sert d’oracle de déchiffrement sans le savoir. La correction de Lowe tient en un champ : ajouter le nom de l’émetteur dans le deuxième message ({Na, Nb, Bob}), ce qui fait échouer la session 1 côté Alice, qui attendait Mallory.

C’est l’exercice d’école des deux outils, et il se reproduit en quelques dizaines de lignes de modèle. Dans ProVerif, la requête de correspondance « si Bob termine avec Alice, alors Alice a commencé avec Bob » est déclarée fausse, trace reconstruite à l’appui. Dans Tamarin, le lemme d’accord est falsifié et l’interface dessine le graphe de la trace ci-dessus. Le secret de Nb vu par Bob tombe du même coup. Ce que la machine apporte : l’entrelacement de deux sessions, que personne ne dessine spontanément au tableau.

Résultats publiés avec Tamarin et ProVerif sur des protocoles déployés

Les résultats cités partout ne viennent pas tous du même outil ni du même modèle. Le tableau ci-dessous rend à chacun le sien.

Protocole	Outil	Auteurs	Apport
TLS 1.3	Tamarin	Cremers, Horvat, Hoyland, Scott, van der Merwe (2017)	Analyse symbolique d’ensemble de la poignée de main et de ses modes, menée sur les brouillons de la norme
TLS 1.3	ProVerif et CryptoVerif	Bhargavan, Blanchet, Kobeissi (2017)	Modèles symbolique et calculatoire, adossés à une implémentation de référence
5G AKA (Authentication and Key Agreement)	Tamarin	Basin et al. (2018)	Propriétés exigées mais non assurées sans hypothèses absentes de la norme, et attaque de traçabilité des abonnés
Signal	ProVerif (complété par CryptoVerif)	Kobeissi, Bhargavan, Blanchet (2017)	Vérification automatisée d’une variante du protocole de messagerie
WireGuard	Tamarin	Donenfeld, Milner	Preuve symbolique des propriétés de la poignée de main
EMV (Europay Mastercard Visa) sans contact	Tamarin	Basin, Sasse, Toro-Pozo (2021)	Contournement du PIN (Personal Identification Number), trouvé par l’analyse du modèle puis démontré en pratique
Noise	ProVerif (via Noise Explorer)	Kobeissi, Nicolas, Bhargavan	Génération automatique de modèles et de garanties par schéma et par message

Deux lectures à en tirer. D’abord, l’analyse formelle a pesé là où elle a accompagné la rédaction : TLS 1.3 a été analysé pendant ses brouillons, avant la publication de la RFC (Request for Comments) 8446, et non après coup. Ensuite, sur 5G AKA comme sur EMV, les trouvailles portent sur des normes relues par des comités entiers pendant des années. Les comités relisent des phrases ; l’outil exécute toutes les combinaisons. Les déclinaisons pratiques sont traitées dans Sécuriser un canal : TLS, HTTPS et mTLS et dans WireGuard et VPN maillés.

Ce qu’une preuve Tamarin ou ProVerif ne garantit pas

« Formellement vérifié » sur une plaquette a la valeur informative de « testé cliniquement » sur un shampoing : tout dépend de ce qui a été testé, et la plaquette ne le dit pas. Six angles morts, systématiques.

L’écart entre modèle, spécification et implémentation. Le modèle est une lecture humaine de la spécification, et le code une autre. Machine à états qui accepte un message hors séquence, analyseur syntaxique qui interprète différemment un champ, nonce réutilisé sous la même clé : rien de tout cela n’existe dans des termes abstraits. Les défauts mémoire non plus (voir Rust et la sécurité mémoire).

Les primitives supposées parfaites. Malléabilité d’un mode de chiffrement, collisions de hachage, courbes ou groupes mal validés, tailles de clé : hors champ, sauf à les modéliser explicitement par des équations supplémentaires. C’est le rôle du modèle calculatoire et de la cryptanalyse, et l’analyse formelle n’est qu’une des pièces d’un audit (voir Tester, auditer, répondre et migrer).

Les canaux auxiliaires. Temps de réponse, consommation, cache, messages d’erreur distincts : l’attaquant symbolique ne voit que des termes. Le sujet est traité dans Attaques par canaux auxiliaires, dans Quand l’implémentation parle pour les oracles et les fautes, et, côté théorie, dans Quantifier les fuites par théorie de l’information.

Les propriétés non demandées. L’outil répond aux questions posées, à aucune autre. Un protocole prouvé pour le secret de la clé de session peut être traçable, rejouable ou vulnérable au déni de service sans contredire la preuve. La question de lecture numéro un devant un résultat : quelle est la liste des lemmes ?

Le modèle d’attaquant choisi par le modélisateur. Quelles clés peuvent être compromises, et quand ? L’état d’un terminal peut-il fuir ? L’horloge est-elle fiable ? Un lemme vrai « tant qu’aucune clé longue durée n’est révélée » ne dit rien du secret persistant.

Les lemmes de cohérence oubliés. Un modèle trop contraint, où le protocole ne peut jamais aller au bout, satisfait toutes les propriétés de sûreté : aucune trace, aucune violation. Preuve verte, contenu nul. D’où les lemmes d’exécutabilité (dans Tamarin, des lemmes d’existence de trace), qui montrent qu’une session honnête complète existe. Leur absence dans un rapport doit faire lever un sourcil.

L’exemple canonique : la poignée de main en quatre temps de WPA2 (Wi-Fi Protected Access 2) disposait d’une preuve formelle depuis le milieu des années 2000 (une preuve manuelle, antérieure aux deux outils). En 2017, l’attaque KRACK (Key Reinstallation Attack) est passée quand même, sans contredire la preuve. Rejouer le troisième message conduit le client à réinstaller une clé déjà en service, donc à remettre à zéro les nonces de chiffrement. Le modèle prouvait que la clé négociée restait secrète ; il ne décrivait pas son installation. La propriété prouvée était vraie, et à côté du problème. Des modèles ultérieurs, écrits avec l’état adéquat, ont intégré la réinstallation.

Prérequis et conditions d’exploitation d’un modèle formel

Avant de lancer quoi que ce soit, quatre choses doivent exister :

une spécification écrite et figée, message par message, avec la machine à états de chaque rôle. Modéliser à partir du code ou d’un schéma de principe revient à vérifier une intention ;
la liste des propriétés attendues, formulées du point de vue de chaque rôle (qui est authentifié auprès de qui, quel secret, face à quelles compromissions) ;
le modèle de menace : capacités de l’attaquant, clés révélables, hypothèses sur les canaux déjà protégés ;
l’outillage. ProVerif s’installe via l’écosystème OCaml. Tamarin demande la chaîne Haskell, le moteur de réécriture Maude dans une version compatible et Graphviz pour l’interface. Les gros modèles Tamarin (ceux d’un standard complet) peuvent demander des dizaines de gigaoctets de mémoire vive et des heures de calcul.

Ensuite, un modèle se maintient comme du code, ou il pourrit :

versionner le modèle à côté de la spécification, avec une correspondance explicite entre sections du texte et règles du modèle ;
rejouer les preuves à chaque modification du protocole, en intégration continue, avec un budget de temps au-delà duquel l’échec est signalé ;
figer la version de l’outil. Les heuristiques de recherche changent d’une version à l’autre : une preuve automatique qui terminait peut ne plus terminer après mise à jour, sans que le protocole ait bougé ;
conserver oracles, lemmes auxiliaires et preuves interactives dans le dépôt. Sans eux, le résultat n’est pas reproductible ;
faire relire le modèle par quelqu’un qui n’a pas conçu le protocole. Le concepteur modélise ce qu’il a voulu écrire, pas ce qu’il a écrit.

Devant un résultat tiers, la grille de lecture tient en cinq questions : quel outil et quel modèle (symbolique ou calculatoire) ; quelle version de la spécification ; quels lemmes exactement ; quelles compromissions tolérées ; le modèle et ses lemmes d’exécutabilité sont-ils publiés ? Une réponse « confidentiel » à la dernière ramène la preuve au rang d’argument commercial.

FAQ

Une preuve Tamarin vaut-elle plus qu’une preuve ProVerif ?

Non. Les deux établissent la même chose : la propriété tient dans le modèle, pour un nombre non borné de sessions. La différence porte sur ce que le modèle peut exprimer (état, algèbre, compromissions) et sur l’effort pour y arriver. Un modèle ProVerif fidèle vaut mieux qu’un modèle Tamarin simplifié pour faire terminer la preuve.

Faut-il faire vérifier un profil restreint d’un standard déjà analysé ?

Retirer des options (suites, modes) reste en général dans le périmètre des analyses existantes, à condition de vérifier qu’elles couvraient bien le mode conservé. Ajouter un message, changer ce qui est signé ou composer deux protocoles en sort : c’est un nouveau protocole, quel que soit le nom qu’on lui garde.

Que faire quand l’outil ne termine pas ?

Avec ProVerif, reformuler : réduire l’état, découper les requêtes, ajouter des lemmes. Avec Tamarin, passer en mode interactif pour repérer la boucle, puis écrire le lemme auxiliaire ou l’oracle qui la casse. Si rien n’y fait, borner le modèle (moins de rôles, moins de modes) et écrire noir sur blanc ce qui a été retiré : une preuve partielle documentée vaut mieux qu’une preuve totale imaginaire.

🐝 Ce qui arrive si on s’en passe

Sans analyse symbolique, un protocole maison n’est jugé que sur ses exécutions honnêtes : les tests passent, puisque personne n’y entrelace deux sessions ni n’y rejoue un message dans le mauvais rôle. Les défauts de logique restent donc en place jusqu’à ce qu’un tiers les trouve, à un moment où le format des messages est figé dans des équipements déployés et où la correction impose une migration. Autre perte, plus discrète : sans lemmes écrits, personne ne sait dire ce que le protocole promet exactement. Chaque évolution se fait alors sans filet, faute de pouvoir rejouer quoi que ce soit, et une affirmation de fournisseur « prouvé formellement » ne peut être ni contestée ni comparée.

🦫 Explication de la marmotte 🍫

Un protocole est une suite de messages que deux machines échangent pour se reconnaître et se mettre d’accord sur une clé secrète. Pour le vérifier, une personne commence par le réécrire dans un langage que le logiciel comprend : qui envoie quoi, dans quel ordre, avec quelles clés. Elle écrit ensuite les promesses à tenir, par exemple « personne d’autre ne connaît la clé » ou « Bob parle bien à Alice ». Le logiciel suppose alors un adversaire qui contrôle tout le réseau : il lit, bloque, copie et fabrique des messages, mais ne peut pas ouvrir un message chiffré sans la clé. Le logiciel examine toutes les façons de mélanger autant de conversations qu’on veut. Trois résultats sont possibles : la promesse tient toujours, ou bien le logiciel montre pas à pas une attaque, ou bien il n’arrive pas à conclure. ProVerif travaille seul et vite, mais signale parfois des attaques qui n’existent pas. Tamarin décrit mieux les protocoles qui gardent une mémoire, mais demande souvent l’aide d’un spécialiste. Dans tous les cas, le résultat porte sur la description écrite, pas sur le programme réel : une erreur de programmation, un calcul de chiffrement fragile ou une promesse que personne n’a pensé à écrire échappent à la vérification.

Pages voisines

La citent

Parler le langage des clés, des messages et des attaquants

Vérifier un protocole cryptographique avec Tamarin ou ProVerif

Elle cite

: les deux pages se citent l’une l’autre.

Vérifier un protocole cryptographique avec Tamarin ou ProVerif

Vérifier un protocole cryptographique avec Tamarin ou ProVerif

Modèle symbolique de Dolev-Yao : ce que Tamarin et ProVerif vérifient

ProVerif : pi-calcul appliqué, clauses de Horn et verdict automatique

Tamarin : réécriture de multi-ensembles, lemmes et preuve guidée

ProVerif ou Tamarin : comparatif et choix de l’outil

Exemple : l’attaque de Lowe sur Needham-Schroeder en trace symbolique

Résultats publiés avec Tamarin et ProVerif sur des protocoles déployés

Ce qu’une preuve Tamarin ou ProVerif ne garantit pas

Prérequis et conditions d’exploitation d’un modèle formel

FAQ

Une preuve Tamarin vaut-elle plus qu’une preuve ProVerif ?

Faut-il faire vérifier un profil restreint d’un standard déjà analysé ?

Que faire quand l’outil ne termine pas ?

🐝 Ce qui arrive si on s’en passe

🦫 Explication de la marmotte 🍫

À lire aussi

Pages voisines