Quantum Cryptography and Autoformalization in Lean

No mundo da comunicação segura, os cadeados mais confiáveis não são feitos de aço, mas das leis fundamentais da física. Este é o reino da distribuição de chaves quânticas, um método onde duas pessoas, tradicionalmente chamadas de Alice e Bob, geram um código secreto compartilhado para proteger suas mensagens. Diferente da criptografia tradicional, que se baseia na dificuldade de resolver problemas matemáticos complexos, esta abordagem baseia-se no fato de que medir uma partícula minúscula de luz, ou um fóton, inevitavelmente a altera. Se uma terceira parte, uma espiã chamada Eve, tentar ouvir, ela deixará um traço detectável de sua interferência. Durante décadas, cientistas desenvolveram protocolos para criar essas chaves, mas provar que esses sistemas são verdadeiramente seguros tem sido um processo frágil. As provas frequentemente dependiam de uma cadeia de argumentos matemáticos costurados a partir de diferentes artigos, cada um com seu próprio conjunto de suposições. Se um elo nessa corrente estivesse ligeiramente desalinhado com outro, ou se uma suposição oculta fosse negligenciada, toda a garantia de segurança poderia ser comprometida sem que ninguém percebesse.

Uma equipe de pesquisadores do Instituto de Tecnologia de Massachusetts (MIT) abordou agora essa fragilidade ao construir uma prova de segurança do zero, utilizando um programa de computador projetado para verificar a lógica matemática. Eles focaram em um método específico e amplamente utilizado chamado protocolo BB84, que utiliza pares de partículas emaranhadas para gerar chaves. Em vez de confiar em um humano para verificar se cada etapa da lógica se sustenta, eles traduziram todo o argumento de segurança para uma linguagem formal que um computador pode ler e verificar com precisão absoluta. O resultado é uma prova verificada por máquina que não deixa margem para lacunas ocultas ou suposições desalinhadas. Ela confirma que o protocolo permanece seguro mesmo quando o número de partículas trocadas é limitado, uma restrição comum do mundo real que frequentemente enfraquece as estimativas de segurança. Além disso, o mesmo sistema de computador que verificou a prova foi usado para descobrir um novo limite matemático mais estreito, que reduz a penalidade de tamanho finito na taxa de chave.

Os pesquisadores começaram criando uma linguagem digital dentro do sistema de computador que impõe estritamente as regras de operações locais e comunicação clássica. No contexto da criptografia quântica, isso significa que o computador garante que Alice e Bob possam apenas realizar ações em suas próprias partículas e só possam compartilhar informações através de canais públicos, nunca acessando magicamente os dados privados um do outro. Esta linguagem atua como um trilho de proteção, impedindo o tipo de erros lógicos que podem passar despercebidos por revisores humanos. Por exemplo, em tentativas anteriores de formalizar essas provas, um agente de inteligência artificial propôs um método onde a chave final era criada combinando sequências que nenhuma das partes possuía de fato. As regras estritas do computador sinalizaram imediatamente que isso era impossível, forçando a equipe a refinar sua abordagem. Ao construir o protocolo passo a passo dentro deste ambiente restrito, a equipe garantiu que o teorema de segurança final descrevesse exatamente o processo físico que pretendiam proteger.

Uma vez construído o protocolo, a equipe pediu ao computador para verificar sua segurança contra um tipo poderoso de ataque conhecido como ataque coerente, onde uma espiã interage com todas as partículas simultaneamente, em vez de uma por uma. O computador verificou cada etapa lógica, desde a medição inicial das partículas até as etapas finais de correção de erros e amplificação de privacidade. Ele confirmou que o protocolo é seguro, o que significa que, se o sistema não abortar, a chave resultante é indistinguível de uma chave secreta perfeita e aleatória, mesmo para um espião com poder computacional ilimitado. Crucialmente, a prova levou em conta o fato de que sistemas do mundo real operam com um número finito de partículas, não um fluxo infinito. Esse efeito de tamanho finito geralmente força os cientistas a serem excessivamente conservadores, descartando mais material de chave potencial para garantir a segurança. A nova prova, porém, forneceu um cálculo preciso de quanto material de chave pode ser mantido com segurança, reduzindo a penalidade imposta por esses limites finitos.

Em uma reviravolta surpreendente, os pesquisadores usaram o mesmo pipeline de computador não apenas para verificar seu trabalho, mas para melhorá-lo. Enquanto o sistema estava verificando a lógica, ele ajudou a equipe a identificar um limite mais estreito para a variância da entropia condicional usada para estimar a segurança desses sistemas. A fórmula existente era muito frouxa, levando a uma redução desnecessária no comprimento da chave secreta. A equipe, guiada pela capacidade do computador de testar e comparar diferentes limites matemáticos, derivou uma nova desigualdade mais precisa. Este novo limite é mais estreito, permitindo que o sistema gere chaves com uma penalidade de tamanho finito reduzida em comparação ao que a fórmula antiga permitiria, sem sacrificar a segurança. Esta descoberta não foi um palpite; foi um resultado matemático rigoroso que o computador verificou como verdadeiro, demonstrando que motores de prova formal podem fazer mais do que apenas checar o trabalho — eles podem acelerar ativamente a descoberta científica ao encontrar melhores soluções para problemas antigos.

O trabalho também serve como um modelo de como futuros sistemas criptográficos devem ser validados. Ao lançar a biblioteca subjacente de definições e teoremas como código aberto, os pesquisadores forneceram um kit de ferramentas reutilizável para a comunidade. Esta biblioteca inclui as definições formais de estados quânticos, canais e a linguagem específica para descrever protocolos, permitindo que outros cientistas construam sobre este fundamento. Isso significa que futuras provas para diferentes protocolos quânticos, ou mesmo para outras áreas da ciência da informação quântica, podem ser construídas com o mesmo nível de rigor. A equipe mostrou que, ao combinar a intuição humana com a precisão implacável da lógica verificada por máquina, é possível eliminar as incertezas ocultas que há muito tempo assolam o campo. O resultado é um novo padrão para argumentos de segurança, um onde a confiabilidade de uma chave quântica não é apenas uma afirmação feita por um pesquisador, mas um fato verificado por uma máquina.