ProVerif : vérification automatisée des protocoles
Spécifiez et vérifiez les propriétés de la poignée de main TLS avec ProVerif.
ProVerif : vérification automatisée des protocoles est une leçon Cryptology Academy gratuite sur CoddyKit. Ceci est la leçon 3 sur 4. Tu peux lire la leçon complète ci-dessous gratuitement — puis la pratiquer en direct dans le navigateur avec un éditeur de code intégré et un tuteur IA 24/7. Elle fait partie du parcours d'apprentissage Cryptology Academy, et ta progression se synchronise sur le web et l'application CoddyKit. Le cours Cryptology Academy comprend 4 leçons au total.
Qu’est-ce que ProVerif ?
ProVerif (Bruno Blanchet, 2001) est un vérificateur automatisé de protocoles cryptographiques. Il reçoit un protocole décrit dans le calcul pi appliqué et détermine automatiquement les propriétés de confidentialité et d’authentification.
Fonctionnement de ProVerif
ProVerif traduit le protocole en clauses de Horn et applique un algorithme fondé sur la résolution pour déduire ce que l’attaquant peut apprendre. Si un fait de confidentialité est dérivable, le protocole est compromis ; sinon, sa sécurité est démontrée.
Langage d’entrée de ProVerif
Les protocoles sont décrits de manière déclarative : déclarer les canaux, les types, les fonctions (enc, dec, sign, verify), les équations (dec(enc(m,k),k)=m) et les processus qui communiquent par des canaux.
Déclarer les primitives cryptographiques
Exemple de déclarations ProVerif :
(* Symmetric encryption *)
fun senc(bitstring, key): bitstring.
fun sdec(bitstring, key): bitstring.
equation forall m: bitstring, k: key; sdec(senc(m, k), k) = m.
(* Asymmetric encryption *)
fun pk(skey): pkey.
fun aenc(bitstring, pkey): bitstring.
fun adec(bitstring, skey): bitstring.
equation forall m: bitstring, sk: skey; adec(aenc(m, pk(sk)), sk) = m.Écrire un processus de protocole simple
Modéliser Alice et Bob comme des processus parallèles :
(* Alice sends nonce to Bob, encrypted *)
let Alice(skA: skey, pkB: pkey) =
new na: nonce;
out(c, aenc((na, pk(skA)), pkB));
in(c, m: bitstring);
let nb = adec(m, skA) in
out(c, aenc(nb, pkB)).
(* Main process: run attacker with full channel control *)
process
new skA: skey; new skB: skey;
out(c, pk(skA)); out(c, pk(skB)); (* publish public keys *)
(Alice(skA, pk(skB)) | Bob(skB, pk(skA)))Énoncer les requêtes de sécurité
ProVerif vérifie des requêtes telles que :
(* Secrecy: attacker cannot learn na *)
query attacker(na).
(* Authentication: if Bob completes, Alice started *)
query event(BobFinished(nb)) ==> event(AliceStarted(nb)).Interpréter la sortie de ProVerif
ProVerif produit « RESULT ... is true » (sécurité démontrée) ou « RESULT ... is false » et affiche une trace d’attaque constituant un contre-exemple, qui montre les messages de l’attaquant. La trace montre exactement comment l’attaque fonctionne.
Vérifier TLS 1.3 avec ProVerif
Bhargavan et al. (2016) ont utilisé ProVerif pour analyser un modèle de TLS 1.3. Ils ont découvert et signalé une attaque contre le mécanisme de reprise 0-RTT, qui a été corrigée avant la finalisation de la RFC.
Limites : approximation et boucles
ProVerif utilise une surapproximation : il peut signaler de fausses attaques (dire « false » alors que le protocole est en réalité sécurisé), mais ne manque jamais les attaques réelles. Les sessions de protocole non bornées peuvent ne pas se terminer — ProVerif déroule les boucles de manière heuristique.
Quand ProVerif indique « CANNOT BE PROVED »
Si ProVerif ne peut pas déterminer le résultat dans le cadre de son approximation, il produit « CANNOT BE PROVED. ». Cela ne constitue pas une preuve d’insécurité : cela signifie que l’outil a atteint les limites de ses heuristiques. Tamarin peut réussir dans ces cas.
Vérification des connaissances
Que signifie une sortie ProVerif « RESULT ... is false » pour une requête de confidentialité ?
Récapitulatif de la leçon
ProVerif automatise la vérification des protocoles au moyen de la résolution de clauses de Horn. Les protocoles sont écrits dans le calcul pi appliqué avec des équations cryptographiques. Les requêtes portent sur la confidentialité et l’authentification. false signifie que la sécurité est démontrée ; true signifie que le protocole est compromis, avec une trace d’attaque. Limites : les approximations peuvent produire « impossible à démontrer ».
Questions Fréquemment Posées
La leçon « ProVerif : vérification automatisée des protocoles » est-elle gratuite ?
Oui — le texte complet de « ProVerif : vérification automatisée des protocoles » est gratuit à lire ici sur le web. Pour la pratiquer de manière interactive (un éditeur de code intégré et un tuteur IA 24/7) et déverrouiller le reste du cours Cryptology Academy, passe à CoddyKit PRO. Le cours Cryptology Academy comprend 4 leçons au total.
Qu'est-ce que j'apprendrai dans « ProVerif : vérification automatisée des protocoles » ?
Spécifiez et vérifiez les propriétés de la poignée de main TLS avec ProVerif. Tu pratiques Cryptology Academy avec du code pratique que tu exécutes directement dans le navigateur, et un tuteur IA 24/7 répond à tes questions au fur et à mesure que tu avances dans la leçon.
Dois-je avoir de l'expérience pour commencer Cryptology Academy ?
Aucune expérience préalable n'est requise. Cryptology Academy sur CoddyKit est structuré pour les débutants jusqu'aux apprenants avancés, donc tu peux commencer ici ou depuis le début et avancer à ton rythme. Ceci est la leçon 3 sur 4.
Combien de temps prend la leçon « ProVerif : vérification automatisée des protocoles » ?
La plupart des leçons CoddyKit prennent environ 5–10 minutes. Chacune est courte et interactive, tu progresses régulièrement et tu repiques exactement où tu t'es arrêté sur le web et l'app.
Peux-tu écrire et exécuter du code dans cette leçon Cryptology Academy ?
Oui. Chaque leçon Cryptology Academy inclut un éditeur de code intégré, tu écris et exécutes du vrai code directement dans ton navigateur et tu reçois des retours IA instantanés — aucune configuration locale requise.
Toutes les leçons de ce cours
- Pourquoi les preuves informelles ne suffisent pas
- Modèle d’attaquant de Dolev-Yao et cryptographie symbolique
- ProVerif : vérification automatisée des protocoles
- Tamarin et preuves computationnelles