Lire une garantie sans la surinterpréter

« Prouvé sûr » figure dans bien des documentations commerciales, avec la même valeur que « cliniquement testé » sur un flacon de shampoing. En cryptographie, une preuve de sécurité est un objet rigoureux et précieux, mais elle affirme une chose précise, dans un modèle précis, sous une hypothèse précise. Ce chapitre apprend à extraire ces trois éléments d’une preuve, à comprendre ce qu’est une réduction et ce qu’elle coûte, à situer le modèle de l’oracle aléatoire, et à mesurer tout ce qu’une preuve laisse ouvert : implémentation, paramètres, composition, canaux auxiliaires et erreurs humaines.

→ Lire l’explication complète de la marmotte

Sur quoi repose une garantie ?

Presque toute la cryptographie à clé publique repose sur des fonctions à sens unique : faciles à calculer, difficiles à inverser. Multiplier deux nombres premiers de 1024 bits prend une fraction de milliseconde ; retrouver ces facteurs à partir de leur produit de 2048 bits dépasse, en l’état des connaissances publiques, toute capacité de calcul classique. Une fonction à trappe est une fonction à sens unique qui devient facile à inverser pour qui connaît un secret, la trappe : dans RSA, élever à la puissance e modulo n est facile pour tous, extraire la racine e-ième est facile seulement pour qui connaît la factorisation de n. La page Les problèmes difficiles qui rendent la clé publique possible présente ces problèmes.

Point capital : l’existence même de fonctions à sens unique n’est pas démontrée. Elle impliquerait que P est différent de NP, question ouverte depuis plus de cinquante ans. Toute la sécurité « prouvée » est donc conditionnelle : elle dit « si ce problème est difficile, alors ce schéma est sûr ». C’est l’hypothèse de dureté, et elle n’est ni un théorème, ni un standard : un standard choisit des paramètres en se fondant sur l’hypothèse, il ne la rend pas plus vraie.

Ce qu’une preuve affirme

Une preuve de sécurité bien écrite contient quatre éléments, et lire une preuve consiste d’abord à les retrouver.

Un énoncé précis : une notion de sécurité nommée, par exemple IND-CCA2 (indistinguabilité face à un attaquant qui peut faire déchiffrer des messages de son choix) pour un chiffrement, ou EUF-CMA (infalsifiabilité existentielle face à des messages choisis) pour une signature ou un MAC (Message Authentication Code).
Un adversaire modélisé : ce qu’il voit, ce qu’il peut demander, combien de temps il calcule, combien de requêtes il fait.
Un avantage borné : la probabilité que l’adversaire gagne, au-delà du hasard, est inférieure à une quantité explicite.
Une hypothèse externe : le problème supposé difficile, ou la fonction supposée idéale.

Atelier de lecture, sur un résumé typique : « Le schéma S est IND-CCA2 dans le modèle de l’oracle aléatoire, sous l’hypothèse RSA ; tout adversaire faisant q requêtes à l’oracle a un avantage au plus q fois celui d’un inverseur de RSA. » L’hypothèse est la difficulté d’inverser RSA ; la conclusion est l’indistinguabilité sous attaque à chiffrés choisis ; l’adversaire est borné en requêtes et en temps ; le modèle est celui de l’oracle aléatoire, ce qui signifie que la fonction de hachage est idéalisée. Quatre lignes, quatre conditions, et aucune ne mentionne la qualité de l’implémentation.

Réductions et pertes

La technique centrale est la réduction. Pour prouver que le schéma est sûr si le problème P est difficile, on montre la contraposée : à partir de n’importe quel attaquant A qui casse le schéma, on construit un attaquant B qui résout P. B simule pour A l’environnement attendu (clés publiques, réponses aux requêtes), et transforme le succès de A en solution de P. Si P est réellement difficile, B ne peut pas exister, donc A non plus.

La réduction a un prix, la perte de réduction. Si l’on démontre que Avantage(A) ≤ q × Avantage(B), et que l’attaquant peut faire q = 2⁶⁰ requêtes, alors une hypothèse qui garantit un avantage au plus 2⁻¹²⁸ pour B ne garantit plus que 2⁻⁶⁸ pour A. Une réduction est dite serrée quand la perte est faible, lâche quand elle est importante. Une preuve lâche reste une preuve, mais pour en tirer la garantie annoncée, il faut augmenter la taille des paramètres en conséquence, ce que l’on oublie volontiers.

Une preuve peut aussi être fausse. L’exemple le plus cité concerne OAEP (Optimal Asymmetric Encryption Padding), le remplissage de RSA proposé par Bellare et Rogaway en 1994 avec une preuve de sécurité. En 2001, Victor Shoup a montré que cette preuve ne démontrait pas la propriété annoncée dans le cas général. Le schéma n’était pas cassé pour autant : Fujisaki, Okamoto, Pointcheval et Stern ont rétabli la preuve pour RSA la même année. Mais pendant sept ans, une preuve incorrecte a été citée comme garantie. Une preuve est un argument relu par des humains, avec les mêmes faiblesses que tout argument relu par des humains.

L’oracle aléatoire et le modèle standard

Le modèle de l’oracle aléatoire, formalisé par Bellare et Rogaway en 1993, remplace la fonction de hachage par un oracle idéal qui répond par une valeur parfaitement aléatoire à chaque nouvelle question. Il rend possibles des preuves simples pour des schémas efficaces, et la plupart des signatures et chiffrements déployés ont des preuves dans ce modèle.

Mais aucune fonction réelle n’est un oracle aléatoire. En 1998, Canetti, Goldreich et Halevi ont construit des schémas, artificiels mais valides, sûrs dans ce modèle et cassés pour toute fonction de hachage concrète qui remplacerait l’oracle. La conclusion pratique n’est pas de rejeter ces preuves : aucun schéma naturel n’a été cassé de cette façon. Elle est de savoir qu’une preuve en oracle aléatoire est une heuristique solide, pas une garantie dans le modèle standard, où la fonction de hachage n’est supposée avoir que des propriétés précises comme la résistance aux collisions. Une preuve dans le modèle standard est plus forte, souvent au prix d’un schéma plus lourd.

Ce que la preuve laisse ouvert

Une preuve porte sur un objet mathématique. Le système réel en diffère par au moins cinq portes.

L’implémentation. La preuve ignore le code. Un dépassement de tampon, une comparaison de tag non constante en temps ou une erreur de gestion mémoire ne sont pas couverts.

Les paramètres. Une preuve donne une borne en fonction de la taille des paramètres ; utilisée avec une clé RSA de 512 bits, elle garantit sérieusement quelque chose de risible. Une preuve ancienne appliquée avec des paramètres dépassés ne garantit plus rien.

La composition. Deux briques sûres séparément peuvent former un ensemble fragile. L’exemple classique est l’ordre entre chiffrement et MAC : Bellare et Namprempre en 2000, puis Krawczyk en 2001, ont montré que « chiffrer puis authentifier le chiffré » est sûr de manière générique, tandis que « authentifier puis chiffrer » ne l’est pas en général. TLS jusqu’à la version 1.2 utilisait ce second ordre avec le mode CBC (Cipher Block Chaining), et les attaques par oracle de remplissage, dont Lucky Thirteen en 2013, en ont exploité les conséquences. La page Attaque par oracle de remplissage CBC détaille ce mécanisme.

Les canaux auxiliaires. Le temps de calcul, la consommation électrique, les messages d’erreur sont hors modèle. L’attaque de Bleichenbacher de 1998 contre le remplissage PKCS #1 v1.5 exploitait simplement le fait qu’un serveur répondait différemment selon que le remplissage était correct ou non. La page Quand l’implémentation parle est consacrée à ces fuites.

Les erreurs utilisateur. Un mot de passe faible, une clé copiée dans un dépôt public ou un avertissement de certificat ignoré sortent par construction de tout modèle mathématique.

Atelier : sécurité d’un MAC et sécurité d’un protocole

Un MAC comme HMAC-SHA-256 est prouvé EUF-CMA sous des hypothèses sur la fonction de compression : un attaquant ne peut pas produire un couple (message, tag) valide pour un message qu’il n’a pas fait authentifier. C’est tout. Considérons un protocole de commande où le client envoie virement 100 € vers compte 42 suivi de son tag. Un attaquant qui enregistre ce message et le renvoie dix fois obtient dix virements : aucun tag n’a été falsifié, la sécurité du MAC est intacte, et le protocole est cassé par rejeu. La propriété du MAC ne dit rien de la fraîcheur, du destinataire ou du contexte. Le protocole doit ajouter un compteur ou un nonce, l’identité du destinataire et un identifiant de session dans les données authentifiées. La sécurité d’un composant n’est jamais celle du protocole qui l’emploie.

Protocoles analysés

Pour les protocoles d’authentification et d’échange de clés, l’analyse formelle modélise les messages, les participants et un attaquant de type Dolev-Yao (qui contrôle entièrement le réseau mais ne casse pas les primitives), puis vérifie automatiquement des propriétés. Les principales sont les suivantes.

L’authentification mutuelle, formalisée comme un accord : si B termine une session en croyant parler à A avec les paramètres X, alors A a bien démarré une session avec B avec les mêmes paramètres X. La fraîcheur (freshness) : la clé ou le message provient de la session en cours, pas d’une session passée rejouée. La résistance au unknown key-share (partage de clé à l’insu) : A et B ne doivent pas finir avec la même clé tout en ayant des idées différentes de leur interlocuteur ; ce défaut, qui touchait des variantes du protocole Station-to-Station, se corrige en incluant les identités dans ce qui est signé ou dérivé. La résistance au downgrade : un attaquant ne doit pas pouvoir forcer les parties à négocier une version ou un algorithme plus faible que ce qu’elles supportent toutes les deux.

Écrire une propriété vérifiable d’échange de clés ressemble à ceci, en langage courant rigoureux : « Pour toute session terminée par B avec un pair nommé A et une clé K, si les clés à long terme de A et de B n’ont pas été compromises avant la fin de la session, alors A a démarré une session avec B, a dérivé la même clé K et la même transcription, et l’attaquant ne connaît pas K. » Chaque mot y compte : « terminée », « avant la fin », « même transcription ». Des outils comme ProVerif et Tamarin vérifient de telles propriétés sur des modèles symboliques ; CryptoVerif et EasyCrypt travaillent dans le modèle calculatoire, plus proche des preuves par réduction. TLS 1.3 a été conçu en dialogue avec ce type d’analyses avant sa publication en 2018, ce qui est une première pour un protocole de cette diffusion.

L’analyse formelle n’est pas un test de code : elle vérifie un modèle du protocole, et un écart entre le modèle et l’implémentation passe au travers. Elle n’est pas non plus un audit, qui examine une implémentation, une configuration et un contexte de déploiement. Et la sécurité théorique n’est pas l’assurance opérationnelle, qui exige en plus surveillance, mise à jour et réponse aux incidents.

🐝 Ce qui arrive si on s’en passe

Lue comme une garantie absolue, une preuve de sécurité devient un argument pour ne plus rien vérifier : la revue de code est allégée, les tests d’implémentation sont jugés superflus, et les fuites que le modèle ne couvre pas passent sans examen. La brèche « la question qui rend le module bavard » en donne l’illustration : un schéma dont les mathématiques tiennent, servi par un module qui répond différemment selon la forme du message reçu, et qui livre ainsi, question après question, ce que la preuve déclarait hors d’atteinte. La ruche avait un certificat de solidité pour ses murs ; l’intrus est entré en demandant son chemin.

🦫 Explication de la marmotte 🍫

Une preuve de sécurité est un raisonnement mathématique qui affirme une chose précise : contre un adversaire décrit à l’avance, disposant de moyens définis, l’avantage de cet adversaire reste très faible, à condition qu’une hypothèse soit vraie. Cette hypothèse porte souvent sur une fonction à sens unique, facile à calculer mais très difficile à inverser, parfois avec une trappe, un secret qui rend l’inversion facile à son détenteur. La preuve procède par réduction : on montre que si un attaquant A cassait le système, on pourrait construire à partir de lui un attaquant B qui résoudrait le problème réputé difficile. Plus la construction de B est coûteuse, plus la preuve perd de sa force. Certaines preuves supposent un oracle aléatoire, c’est-à-dire une fonction idéale qu’aucune fonction réelle n’égale tout à fait. La preuve laisse ouverts de nombreux points : l’implémentation, les paramètres choisis, l’assemblage avec d’autres composants, les fuites physiques comme le temps de calcul, et les erreurs des utilisateurs. Deux briques prouvées sûres séparément peuvent former un ensemble fragile. Pour les protocoles d’authentification et d’échange de clés, l’analyse formelle vérifie des propriétés comme la fraîcheur des messages, l’accord sur l’identité du partenaire ou la résistance au retour forcé vers une version plus faible. Une preuve ancienne, appliquée avec des paramètres dépassés, ne garantit plus rien.

Pages voisines

La citent

Lire une garantie sans la surinterpréter

Elle cite

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

Lire une garantie sans la surinterpréter

Lire une garantie sans la surinterpréter

Sur quoi repose une garantie ?

Ce qu’une preuve affirme

Réductions et pertes

L’oracle aléatoire et le modèle standard

Ce que la preuve laisse ouvert

Atelier : sécurité d’un MAC et sécurité d’un protocole

Protocoles analysés

🐝 Ce qui arrive si on s’en passe

🦫 Explication de la marmotte 🍫

À lire aussi

Pages voisines