Tamarin et preuves computationnelles
Utilisez le prouveur Tamarin pour la réécriture de multisets et la vérification fondée sur des traces.
Tamarin et preuves computationnelles est une leçon Cryptology Academy gratuite sur CoddyKit. Ceci est la leçon 4 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 Tamarin ?
Tamarin (ETH Zurich, 2012) est un vérificateur de protocoles de sécurité fondé sur la réécriture de multiensembles. Contrairement à l’approche par clauses de Horn de ProVerif, Tamarin raisonne sur les traces des exécutions de protocoles avec un démonstrateur interactif.
Tamarin et ProVerif
ProVerif : entièrement automatisé, peut indiquer « impossible à démontrer ». Tamarin : assistant de preuve interactif et mode automatisé, prenant en charge les théories équationnelles (XOR, Diffie-Hellman, applications bilinéaires). Il est plus expressif, mais sa courbe d’apprentissage est plus exigeante.
Règles de réécriture de multiensembles
Tamarin modélise les protocoles comme des règles de réécriture portant sur des faits. Les faits représentent l’état. Une règle [ L ] --[ A ]-> [ R ] consomme les faits de gauche L, produit les faits de droite R et consigne l’action A dans la trace.
Langage d’entrée de Tamarin (.spthy)
Un fichier de théorie Tamarin déclare des fonctions, des équations, des règles et des lemmes :
/* Diffie-Hellman key exchange */
builtins: diffie-hellman
rule Alice_1:
[ Fr(~a) ] /* fresh random a */
--[ AliceSent($A, $B, 'g'^~a) ]->
[ Alice_St($A, $B, ~a), Out('g'^~a) ]
rule Bob_1:
[ In(ga), Fr(~b) ]
--[ BobReceived($A, $B, ga) ]->
[ Bob_St($A, $B, ~b, ga^~b), Out('g'^~b) ]Énoncer des lemmes
Les objectifs de sécurité sont exprimés sous forme de lemmes portant sur les traces :
/* Secrecy: shared secret not known to attacker */
lemma secret_key:
"All A B k #i #j.
AliceKey(A, B, k) @ i &
BobKey(A, B, k) @ j
==> not (Ex #r. K(k) @ r)"
/* Authentication: if Bob has key, Alice sent it */
lemma authentication:
"All A B k #j. BobKey(A, B, k) @ j
==> Ex #i. AliceKey(A, B, k) @ i & i < j"Exécuter Tamarin
Lancez la GUI interactive de Tamarin : tamarin-prover interactive my_protocol.spthy. L’interface du navigateur affiche les obligations de preuve ; vous guidez les stratégies automatisées ou appliquez des étapes manuelles dans les cas qui ne se terminent pas.
Solidité computationnelle
Les preuves symboliques (ProVerif, Tamarin) garantissent la sécurité sous des hypothèses de cryptographie parfaite. Les théorèmes de solidité computationnelle (Cortier, Backes) transposent les preuves symboliques en garanties de sécurité computationnelle lorsque le protocole est instancié avec des primitives dont la sécurité est démontrée.
F* et HACL* : implémentations vérifiées
F* (Microsoft Research) est un langage de programmation orienté vers les preuves. HACL* est une bibliothèque cryptographique écrite en F*, accompagnée de preuves vérifiées mécaniquement de sa correction et de sa résistance aux attaques par canal auxiliaire. Elle est utilisée dans Firefox NSS et mbedTLS.
EasyCrypt : preuves computationnelles fondées sur des jeux
EasyCrypt permet de réaliser des preuves de sécurité entièrement computationnelles (fondées sur des jeux) pour des constructions cryptographiques, et pas seulement pour des protocoles. La couche d’enregistrement de TLS 1.3 et ChaCha20-Poly1305 ont été vérifiées dans EasyCrypt.
Impact pratique
La cryptographie vérifiée formellement entre en production : NSS (Firefox) utilise HACL*, AWS utilise s2n-tls avec des assertions accompagnées de preuves, et le protocole Signal a été vérifié dans ProVerif et Tamarin. Les méthodes formelles ne sont plus réservées au monde universitaire.
Vérification des connaissances
En quoi Tamarin se distingue-t-il de ProVerif dans la gestion des cas où l’automatisation échoue ?
Récapitulatif de la leçon
Tamarin utilise la réécriture de multiensembles et un raisonnement fondé sur les traces avec une GUI de preuve interactive. Il prend en charge les théories équationnelles de DH et de XOR. Les lemmes expriment les objectifs de confidentialité et d’authentification. La solidité computationnelle fait le lien entre les preuves symboliques et la sécurité réelle. HACL* et EasyCrypt étendent la vérification aux implémentations et aux constructions cryptographiques.
Questions Fréquemment Posées
La leçon « Tamarin et preuves computationnelles » est-elle gratuite ?
Oui — le texte complet de « Tamarin et preuves computationnelles » 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 « Tamarin et preuves computationnelles » ?
Utilisez le prouveur Tamarin pour la réécriture de multisets et la vérification fondée sur des traces. 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 4 sur 4.
Combien de temps prend la leçon « Tamarin et preuves computationnelles » ?
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