Quantum Cryptography and Autoformalization in Lean

Dans le monde de la communication sécurisée, les verrous les plus fiables ne sont pas faits d'acier, mais des lois fondamentales de la physique. C'est le domaine de la distribution quantique de clés, une méthode où deux personnes, traditionnellement appelées Alice et Bob, génèrent un code secret partagé pour protéger leurs messages. Contrairement au chiffrement traditionnel, qui repose sur la difficulté de résoudre des problèmes mathématiques complexes, cette approche repose sur le fait que la mesure d'une infime particule de lumière, ou photon, la modifie inévitablement. Si une tierce partie, une espionne nommée Eve, tente d'écouter, elle laisse une trace détectable de son interférence. Pendant des décennies, les scientifiques ont développé des protocoles pour créer ces clés, mais prouver que ces systèmes sont véritablement sûrs a été un processus fragile. Les preuves reposaient souvent sur une chaîne d'arguments mathématiques assemblés à partir de différents articles, chacun ayant son propre ensemble d'hypothèses. Si un maillon de cette chaîne était légèrement décalé par rapport à un autre, ou si une hypothèse cachée était négligée, toute la garantie de sécurité pouvait être compromise sans que personne ne s'en aperçoive.

Une équipe de chercheurs du Massachusetts Institute of Technology a maintenant abordé cette fragilité en construisant une preuve de sécurité de fond en comble en utilisant un programme informatique conçu pour vérifier la logique mathématique. Ils se sont concentrés sur une méthode spécifique et largement utilisée appelée protocole BB84, qui utilise des paires de particules intriquées pour générer des clés. Au lieu de faire confiance à un humain pour vérifier que chaque étape de la logique tient debout, ils ont traduit l'ensemble de l'argument de sécurité dans un langage formel qu'un ordinateur peut lire et vérifier avec une précision absolue. Le résultat est une preuve vérifiée par machine qui ne laisse aucune place aux lacunes cachées ou aux hypothèses discordantes. Elle confirme que le protocole reste sûr même lorsque le nombre de particules échangées est limité, une contrainte du monde réel qui affaiblit souvent les estimations de sécurité. De plus, le même système informatique qui a vérifié la preuve a été utilisé pour découvrir une nouvelle borne mathématique plus serrée, ce qui réduit la pénalité de taille finie sur le taux de clé.

Les chercheurs ont commencé par créer un langage numérique au sein du système informatique qui impose strictement les règles des opérations locales et de la communication classique. Dans le contexte de la cryptographie quantique, cela signifie que l'ordinateur garantit qu'Alice et Bob ne peuvent effectuer des actions que sur leurs propres particules et ne peuvent partager des informations que via des canaux publics, sans jamais accéder magiquement aux données privées de l'autre. Ce langage agit comme un garde-fou, empêchant le genre d'erreurs logiques qui peuvent échapper aux réviseurs humains. Par exemple, dans des tentatives antérieures de formalisation de ces preuves, un agent d'intelligence artificielle a un jour proposé une méthode où la clé finale était créée en combinant des chaînes que ni l'une ni l'autre des parties ne possédait réellement. Les règles strictes de l'ordinateur ont immédiatement signalé cela comme impossible, forçant l'équipe à affiner son approche. En construisant le protocole étape par étape dans cet environnement contraint, l'équipe s'est assurée que le théorème de sécurité final décrit exactement le processus physique qu'ils entendaient protéger.

Une fois le protocole construit, l'équipe a demandé à l'ordinateur de vérifier sa sécurité contre un type d'attaque puissant connu sous le nom d'attaque cohérente, où un espion interagit avec toutes les particules simultanément plutôt qu'une par une. L'ordinateur a vérifié chaque étape logique, de la mesure initiale des particules aux étapes finales de correction d'erreurs et d'amplification de la confidentialité. Il a confirmé que le protocole est sûr, ce qui signifie que si le système ne s'interrompt pas, la clé résultante est indiscernable d'une clé secrète parfaite et aléatoire, même pour un espion doté d'une puissance de calcul illimitée. Crucialement, la preuve a pris en compte le fait que les systèmes réels fonctionnent avec un nombre fini de particules, et non un flux infini. Cet effet de taille finie force habituellement les scientifiques à être excessivement conservateurs, en écartant davantage de matériel de clé potentiel pour garantir la sécurité. La nouvelle preuve a toutefois fourni un calcul précis de la quantité de matériel de clé pouvant être conservée en toute sécurité, réduisant la pénalité imposée par ces limites finies.

Dans un tournant surprenant, les chercheurs ont utilisé le même pipeline informatique non seulement pour vérifier leur travail, mais aussi pour l'améliorer. Tandis que le système vérifiait la logique, il a aidé l'équipe à identifier une borne plus serrée sur la variance de l'entropie conditionnelle utilisée pour estimer la sécurité de ces systèmes. La formule existante était trop lâche, entraînant une réduction inutile de la longueur de la clé secrète. L'équipe, guidée par la capacité de l'ordinateur à tester et comparer différentes bornes mathématiques, a dérivé une nouvelle inégalité plus précise. Cette nouvelle borne est plus serrée, permettant au système de générer des clés avec une pénalité de taille finie réduite par rapport à ce que l'ancienne formule aurait permis, sans sacrifier la sécurité. Cette découverte n'était pas une supposition ; c'était un résultat mathématique rigoureux que l'ordinateur a vérifié comme étant vrai, démontant que les moteurs de preuve formelle peuvent faire plus que simplement vérifier le travail — ils peuvent activement accélérer la découverte scientifique en trouvant de meilleures solutions à de vieux problèmes.

Le travail sert également de modèle pour la manière dont les futurs systèmes cryptographiques devraient être validés. En publiant la bibliothèque de définitions et de théorèmes sous licence open source, les chercheurs ont fourni un kit d'outils réutilisable pour la communauté. Cette bibliothèque comprend les définitions formelles des états quantiques, des canaux et le langage spécifique pour décrire les protocoles, permettant à d'autres scientifiques de construire sur cette base. Cela signifie que les futures preuves pour différents protocoles quantiques, ou même pour d'autres domaines de la science de l'information quantique, peuvent être construites avec le même niveau de rigueur. L'équipe a montré qu'en combinant l'intuition humaine avec la précision implacable de la logique vérifiée par machine, il est possible d'éliminer les incertitudes cachées qui ont longtemps tourmenté le domaine. Le résultat est un nouveau standard pour les arguments de sécurité, un standard où la fiabilité d'une clé quantique n'est pas seulement une affirmation faite par un chercheur, mais un fait vérifié par une machine.