Imaginez que vous êtes un maître serrurier essayant de prouver que votre nouveau coffre-fort est incassable. Vous ne vous contentez pas de dire : « Il est solide ! ». Vous devez présenter une séquence d'étapes : « Si vous ne pouvez pas briser cette petite serrure, vous ne pouvez pas briser la porte ; si vous ne pouvez pas briser la porte, vous ne pouvez pas briser le coffre-fort. » C'est ainsi que fonctionne la cryptographie moderne. Les experts utilisent des « jeux » pour tester la sécurité, où un pirate tente de deviner un secret, et la sécurité d'un système est prouvée en montrant que le briser est aussi difficile que de résoudre un casse-tête connu et impossible. Mais voici le piège : réaliser ces preuves à la main, c'est comme essayer de faire tenir debout un château de cartes dans un ouragan. Il est facile de commettre une minuscule erreur, de manquer une faille subtile ou de se perdre dans la complexité, et si vous manquez une seule étape, toute la preuve s'effondre. C'est pourquoi les scientifiques cherchent un moyen de faire en sorte qu'un ordinateur vérifie chaque carte, garantissant que le château tient debout.

C'est ici qu'intervient le papier. Les auteurs ont construit un atelier numérique appelé HOPSCOTCH (un nom ludique pour un jeu de saut) à l'intérieur d'un puissant programme informatique appelé Lean 4. Considérez HOPSCOTCH comme un relecteur de preuves super intelligent et robotique qui ne se contente pas de vérifier vos mathématiques ; il comprend l'histoire de la preuve de sécurité. Au lieu de forcer les cryptographes à écrire dans un langage étrange et limité, HOPSCOTCH leur permet d'écrire des preuves en utilisant les mêmes outils qu'ils utilisent pour tous leurs autres calculs. Il transforme le processus de « saut de jeu » — passer d'un scénario de sécurité à un autre — en un objet clair, étape par étape, que l'ordinateur peut inspecter, vérifier et même aider à automatiser. Les auteurs n'ont pas seulement construit l'outil ; ils l'ont utilisé pour prouver avec succès la sécurité de plusieurs méthodes de chiffrement célèbres, y compris une construction complexe appelée GGM, démontant que ce « relecteur de preuves robotique » peut gérer des défis cryptographiques réels sans s'embrouiller.

La vue d'ensemble : Pourquoi avons-nous besoin d'un robot relecteur ?

Dans le monde de la sécurité numérique, nous comptons sur la « sécurité prouvable ». Cela signifie que nous ne nous contentons pas d'espérer que nos codes sont sûrs ; nous essayons de le prouver. La méthode standard consiste à utiliser l'approche par « jeux ». Imaginez un garde de sécurité (le système) et un cambrioleur (l'adversaire). Le garde possède un secret, et le cambrioleur tente de le deviner. Pour prouver que le garde est sûr, nous ne disons pas simplement « il est bon ». Nous créons une série de « jeux » ou de scénarios.

1. Le Jeu Réel : Le cambrioleur tente de briser le système réel.
2. Le Saut : Nous imaginons un jeu légèrement différent, presque identique, mais plus facile à analyser. Nous prouvons que si le cambrioleur peut gagner au Jeu Réel, il peut aussi gagner à ce nouveau jeu, légèrement différent.
3. La Chaîne : Nous continuons à sauter d'un jeu à un autre, en changeant les règles très légèrement à chaque fois, jusqu'à atteindre un dernier jeu qui est manifestement impossible à gagner (comme deviner correctement un lancer de pièce un million de fois de suite).

Si nous pouvons prouver que chaque « saut » est sûr, alors toute la chaîne est sûre. C'est ce qu'on appelle une « preuve par saut de jeu » (game-hopping proof).

Le problème est que les humains sont très mauvais pour faire cela parfaitement. Ces preuves sont longues, désordonnées et pleines de détails minuscules. Un seul détail manqué peut rendre toute la preuve fausse et le système vulnérable. Pendant des années, les chercheurs ont tenté de construire des outils informatiques spécialisés pour vérifier ces preuves, mais ces outils parlent souvent une langue différente de celle des mathématiciens. Ils sont comme un traducteur qui ne parlerait que la « Sécurité » mais pas les « Mathématiques », forçant les experts à traduire leurs idées de l'un vers l'autre, ce qui est lent et source d'erreurs.

Entrée en scène : HOPSCOTCH, le traducteur universel

Les auteurs de ce papier, Stefan Dziembowski, Grzegor Fabiański, Daniele Micciancio et Rafał Stefański, ont décidé de construire un pont. Ils ont créé HOPSCOTCH, un cadre à l'intérieur de Lean 4, un programme informatique populaire utilisé pour vérifier des preuves mathématiques.

Voici la magie de HOPSCOTCH :

• Pas de nouveau langage : Contrairement à d'autres outils qui vous obligent à apprendre une nouvelle façon restreinte d'écrire du code, HOPSCOTCH vous permet d'écrire des preuves en utilisant le Lean standard. C'est comme laisser un chef cuisiner avec ses propres couteaux préférés plutôt que de le forcer à utiliser des couteaux en plastique.
• Des preuves comme des objets : Dans HOPSCHOTCH, une preuve n'est pas seulement un tas de texte. C'est un objet structuré, comme un modèle Lego. Chaque « saut » dans le jeu est une brique Lego spécifique. Vous pouvez les assembler, et l'ordinateur vérifie s'ils s'emboîtent parfaitement. Si vous essayez de connecter deux briques qui ne correspondent pas, l'ordinateur dit : « Non, ça ne marche pas. »
• L'astuce de l'« Abstraction » : L'une des parties les plus difficiles de ces preuves est de montrer que deux systèmes différents ayant des apparences distinctes se comportent exactement de la même manière. HOPSCOTCH utilise une astuce ingénieuse appelée « abstraction d'état ». Imaginez que vous avez deux robots. L'un a un schéma de câblage interne désordonné, et l'autre en a un bien net. HOPSCOTCH vous permet de dessiner une carte (une fonction d'abstraction) qui montre comment les fils désordonnés correspondent aux fils nets. Si la carte est correcte, l'ordinateur sait que les robots sont identiques dans leur comportement, même s'ils sont différents à l'intérieur.

Ce qu'ils ont réellement fait et trouvé

Les auteurs n'ont pas seulement construit l'outil ; ils l'ont mis à l'épreuve. Ils ont utilisé HOPSCOTCH pour vérifier formellement la sécurité de quatre concepts cryptographiques majeurs :

1. Encrypt-then-MAC : Une méthode pour rendre les messages à la fois secrets et protégés contre les falsifications. Ils ont prouvé que si le chiffrement sous-jacent et le « marquage » (MAC) sont sûrs, l'ensemble est sûr, même face aux pirates les plus intelligents.
2. Chiffrement ElGamal : Une façon célèbre d'envoyer des messages secrets en utilisant des clés publiques. Ils ont montré comment prouver la sécurité de ce système en se basant sur un problème mathématique difficile appelé l'hypothèse de Diffie-Hellman décisionnelle (DDH).
3. Secret de temps unique vers IND-CPA : Ils ont prouvé que si un système est sûr pour un seul message, il peut être rendu sûr pour de nombreux messages, une étape cruciale pour construire un chiffrement robuste.
4. La construction GGM : C'est le point majeur. La méthode GGM transforme un simple générateur de nombres aléatoires en une fonction pseudorandom complexe (un générateur de nombres pseudo-aléatoires qui semble réel). Les preuves informatiques précédentes ne pouvaient gérer que des versions très peu profondes (comme un arbre de 3 étapes). Les auteurs ont utilisé HOPSCOTCH pour prouver la sécurité de GGM pour une profondeur non constante, ce qui signifie qu'elle fonctionne pour des arbres de n'importe quelle taille. À leur connaissance, c'est la première fois qu'un assistant de preuve à usage général vérifie avec succès cette construction spécifique et complexe.

Comment ils l'ont fait (La mécanique du « Jeu »)

Le papier explique que HOPSCOTCH fonctionne en décomposant la preuve en étapes spécifiques, ou « constructeurs » :

• Équivalence observationnelle : Prouver que deux jeux se ressemblent pour un observateur extérieur.
• Réductions : Montrer que si vous pouvez briser le Jeu A, vous pouvez briser le Jeu B.
• Séquences d'hybrides : Enchaîner de nombreuses petites étapes.

Le cadre comprend des « tactiques » (des aides automatisées) qui tentent de résoudre ces étapes pour vous. Par exemple, si vous devez prouver que deux oracles (les systèmes de jeu) sont les mêmes, l'ordinateur peut tenter automatiquement de trouver une « abstraction d'état ». S'il n'y parvient pas, il laisse l'étape à la résolution humaine, mais il conserve la structure afin que l'humain sache exactement où il en est.

Les auteurs ont également prouvé un « théorème de validité computationnelle ». C'est une façon sophistiquée de dire : « Si l'ordinateur dit que cette preuve est valide, alors elle est réellement valide dans le monde réel. » Ils ont montré que pour chaque objet de preuve créé par HOPSCOTCH, on peut calculer mathématiquement l'« avantage » exact dont un pirate disposerait, sur la base des hypothèses utilisées dans la preuve. Cela garantit que l'ordinateur ne joue pas seulement un jeu avec lui-même ; il fournit une garantie de sécurité réelle et concrète.

L'essentiel

Le papier conclut que HOPSCOTCH réussit à combler le fossé entre la commodité des outils de sécurité spécialisés et la puissance des assistants mathématiques à usage général. Il permet aux cryptographes d'écrire des preuves plus faciles à lire, plus faciles à vérifier et moins sujettes à l'erreur humaine. Bien que les auteurs admettent que l'ordinateur ne vérifie pas encore si le « pirate » exécute ses actions assez rapidement (un détail technique appelé temps polynomial), ils ont jeté les bases de preuves de sécurité entièrement automatisées et dignes de confiance.

Ils évoquent également l'avenir : avec ces objets de preuve structurés, il pourrait bientôt être possible d'utiliser l'IA pour aider à écrire ces preuves automatiquement, ou d'étendre le système pour gérer des scénarios encore plus complexes impliquant des « événements indésirables » et des probabilités. Mais pour l'instant, la principale réussite est claire : ils ont construit un moyen fiable, flexible et puissant de permettre aux ordinateurs de nous aider à prouver que nos secrets numériques sont en sécurité.