💻 computer science

Game Hopping in Lean

Este artigo introduz o HOPSCOTCH, um framework em Lean 4 que mecaniza provas criptográficas baseadas em jogos e computacionalmente sólidas usando uma metodologia de incorporação rasa e abstração de estado para verificar formalmente propriedades de segurança complexas, como a construção GGM e a segurança IND-CCA.

Autores originais: Stefan Dziembowski, Grzegorz Fabiański, Daniele Micciancio, Rafał{} Stefański

Publicado 2026-08-07

📖 8 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: Stefan Dziembowski, Grzegorz Fabiański, Daniele Micciancio, Rafał{} Stefański

Artigo original sob licença CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta é uma explicação gerada por IA do artigo abaixo. Não foi escrita nem endossada pelos autores. Para precisão técnica, consulte o artigo original. Ler aviso legal completo

Imagine que você é um mestre chaveiro tentando provar que seu novo cofre é inquebrável. Você não diz apenas: "É forte!". Você tem que mostrar uma sequência de passos: "Se você não consegue quebrar esta pequena fechadura, não pode quebrar a porta; se não pode quebrar a porta, não pode quebrar o cofre". É assim que a criptografia moderna funciona. Especialistas usam "jogos" para testar a segurança, onde um hacker tenta adivinhar um segredo e a segurança de um sistema é provada mostrando que quebrá-lo é tão difícil quanto resolver um enigma conhecido e impossível. Mas aqui está o problema: fazer essas provas à mão é como tentar equilibrar uma casa de cartas em um furacão. É fácil cometer um erro minúsculo, perder um detalhe sutil ou se perder na complexidade e, se você perder um único passo, toda a prova desmorona. É por isso que cientistas têm procurado uma maneira de fazer um computador verificar cada uma das cartas, garantindo que a casa permaneça de pé.

É aqui que entra o artigo. Os autores construíram um workshop digital chamado HOPSCOTCH (um nome lúdico para um jogo de saltos) dentro de um poderoso programa de computador chamado Lean 4. Pense no HOPSCOTCH como um revisor de provas robótico e superinteligente que não apenas verifica sua matemática; ele entende a história da prova de segurança. Em vez de forçar os criptógrafos a escreverem em uma linguagem estranha e limitada, o HOPSCOTCH permite que eles escrevam provas usando as mesmas ferramentas que usam para toda a sua outra matemática. Ele transforma o processo de "saltar entre jogos" — pulando de um cenário de segurança para o próximo — em um objeto claro, que o computador pode inspecionar, verificar e até automatizar. Os autores não apenas construíram a ferramenta; eles a usaram para provar com sucesso a segurança de vários métodos de criptografia famosos, incluindo uma construção complexa chamada GGM, mostrando que este "revisor de provas robótico" pode lidar com desafios criptográficos do mundo real sem se confundir.

O Panorama Geral: Por Que Precisamos de um Robô Revisor

No mundo da segurança digital, dependemos da "segurança provável". Isso significa que não apenas esperamos que nossos códigos sejam seguros; tentamos provar isso. A maneira padrão de fazer isso é a abordagem baseada em "jogos". Imagine um segurança (o sistema) e um ladrão (o adversário). O segurança tem um segredo e o ladrão tenta adivinhá-lo. Para provar que o segurança é seguro, não dizemos apenas "ele é bom". Criamos uma série de "jogos" ou cenários.

O Jogo Real: O ladrão tenta quebrar o sistema real.
O Salto: Imaginamos um jogo ligeiramente diferente que é quase o mesmo, mas mais fácil de analisar. Provamos que, se o ladrão puder vencer o Jogo Real, ele também poderá vencer este novo jogo, ligeiramente diferente.
A Corrente: Continuamos saltando de um jogo para outro, mudando as regras um pouquinho de cada vez, até chegarmos a um jogo final que é obviamente impossível de vencer (como acertar o lançamento de uma moeda um milhão de vezes seguidas).

Se pudermos provar que cada um dos "saltos" é seguro, então toda a corrente é segura. Isso é chamado de "prova de salto de jogo" (game-hopping proof).

O problema é que os humanos são péssimos em fazer isso perfeitamente. Essas provas são longas, bagunçadas e cheias de detalhes minúsculos. Um único detalhe perdido pode tornar a prova errada e o sistema inseguro. Por anos, pesquisadores tentaram construir ferramentas de computador especiais para verificar essas provas, mas essas ferramentas costumam falar uma língua diferente dos matemáticos. Elas são como um tradutor que fala apenas "Segurança", mas não "Matemática", forçando os especialistas a traduzirem suas ideias de ida e volta, o que é lento e propenso a erros.

Surge o HOPSCOTCH: O Tradutor Universal

Os autores deste artigo, Stefan Dziembowski, Grzegor Fabiański, Daniele Micciancio e Rafał Stefański, decidiram construir uma ponte. Eles criaram o HOPSCOTCH, um framework dentro do Lean 4, um popular programa de computador usado para verificar provas matemáticas.

Aqui está a magia do HOPSCOTCH:

Sem Nova Linguagem: Ao contrário de outras ferramentas que forçam você a aprender uma nova maneira restrita de escrever código, o HOPSCOTCH permite que você escreva provas usando o Lean padrão. É como deixar um chef cozinhar com suas próprias facas favoritas em vez de forçá-lo a usar facas de plástico.
Provas como Objetos: No HOPSCOTCH, uma prova não é apenas um amontoado de texto. É um objeto estruturado, como um modelo de LEGO. Cada "salto" no jogo é uma peça específica de LEGO. Você pode encaixá-las e o computador verifica se elas se ajustam perfeitamente. Se você tentar conectar duas peças que não combinam, o computador diz: "Não, isso não funciona".
O Truque da "Abstração": Uma das partes mais difíceis dessas provas é mostrar que dois sistemas diferentes parecem se comportar exatamente da mesma forma. O HOPSCOTCH usa um truque inteligente chamado "abstração de estado". Imagine que você tem dois robôs. Um tem um diagrama de fiação interna bagunçado e o outro tem um diagrama limpo. O HOPSCOTCH permite que você desenhe um mapa (uma função de abstração) que mostra como os fios bagunçados correspondem aos fios limpos. Se o mapa estiver correto, o computador sabe que os robôs são idênticos em comportamento, mesmo que pareçam diferentes por dentro.

O Que Eles Realmente Fizeram e Descobriram

Os autores não apenas construíram a ferramenta; eles a colocaram à prova. Eles usaram o HOPSCOTCH para verificar formalmente a segurança de quatro grandes conceitos criptográficos:

Encrypt-then-MAC: Um método para tornar as mensagens tanto secretas quanto à prova de adulteração. Eles provaram que, se a criptografia subjacente e a "etiquetagem" (MAC) forem seguras, todo o conjunto é seguro contra até mesmo os hackers mais inteligentes.
Criptografia ElGamal: Uma forma famosa de enviar mensagens secretas usando chaves públicas. Eles mostraram como provar a segurança baseada em um problema matemático difícil chamado suposição Decisional Diffie-Hellman (DDH).
Segredo de Uso Único para IND-CPA: Eles provaram que, se um sistema é seguro para uma única mensagem, ele pode ser tornado seguro para muitas mensagens, um passo crucial na construção de criptografias robustas.
A Construção GGM: Esta é a principal. O método GGM transforma um simples gerador de números aleatórios em uma "função pseudorandom" complexa (um gerador de números pseudoaleatórios que parece real). Provas de computador anteriores só consegravam lidar com versões muito rasas disso (como uma árvore de 3 níveis). Os autores usaram o HOPSCOTCH para provar a segurança do GGM para profundidade não constante, o que significa que ele funciona para árvores de qualquer tamanho. Tanto quanto é do conhecimento deles, esta é a primeira vez que um assistente de prova de uso geral verifica com sucesso essa construção específica e complexa.

Como Eles Fizeram (A Mecânica do "Jogo")

O artigo explica que o HOPSCOTCH funciona dividindo a prova em passos específicos, ou "construtores":

Equivalência Observacional: Provar que dois jogos parecem iguais para um observador externo.
Reduções: Mostrar que, se você pode quebrar o Jogo A, você também pode quebrar o Jogo B.
Sequências de Híbridos: Encadear muitos pequenos passos.

O framework inclui "táticas" (ajudantes automatizados) que tentam resolver esses passos para você. Por exemplo, se você precisar provar que dois oráculos (os sistemas de jogo) são iguais, o computador pode tentar automaticamente encontrar um mapa de "abstração de estado". Se não conseguir encontrar um, ele deixa o passo para o humano resolver, mas mantém a estrutura para que o humano saiba exatamente onde está.

Os autores também provaram um "teorema de correção computacional". Esta é uma forma elegante de dizer: "Se o computador diz que esta prova é válida, então ela é realmente válida no mundo real". Eles mostraram que, para cada objeto de prova que o HOPSCOTCH cria, você pode calcular matematicamente exatamente quanto de "vantagem" um hacker teria, com base nas suposições usadas na prova. Isso garante que o computador não está apenas jogando um jogo consigo mesmo; ele está dando uma garantia de segurança real e concreta.

A Conclusão

O artigo conclui que o HOPSCOTCH consegue, com sucesso, unir a conveniência das ferramentas de segurança especializadas ao poder dos assistentes matemáticos de uso geral. Ele permite que os criptógrafos escrevam provas que são mais fáceis de ler, mais fáceis de verificar e menos propensas ao erro humano. Embora os autores admitam que o computador ainda não verifica se o "hacker" está rodando rápido o suficiente (um detalhe técnico chamado tempo polinomial), eles lançaram as bases para provas de segurança totalmente automatizadas e confiáveis.

Eles também sugerem o futuro: com esses objetos de prova estruturados, pode ser possível em breve usar IA para ajudar a escrever essas provas automaticamente, ou estender o sistema para lidar com cenários ainda mais complexos envolvendo "eventos ruins" e probabilidade. Mas, por enquanto, a principal conquista é clara: eles construíram uma maneira confiável, flexível e poderosa de permitir que os computadores nos ajudem a provar que nossos segredos digitais estão seguros.

Resumo Técnico: Game Hopping em Lean

Declaração do Problema

A criptografia moderna depende fortemente do paradigma da segurança provável, tipicamente formalizada através de definições baseadas em jogos computacionais. Neste framework, a segurança é estabelecida através da construção de uma sequência de "game hops" (ou argumentos de híbridos) que reduzem a vantagem de um adversário a problemas computacionais difíceis conhecidos. No entanto, provas manuais baseadas em jogos são notoriamente propensas a erros, monotonicamente complexas e suscetíveis a lacunas sutis.

Embora ferramentas de domínio específico como EasyCrypt e CryptoVerif tenham automatizado com sucesso grandes classes dessas reduções, elas operam fora de provadores de teoremas interativos de propósito geral. Isso força um compromelo: desenvolvedores devem escolher entre a conveniência automatizada de ferramentas especializadas e a expressividade e o rigor fundamentais de provadores de teoremas de propósito geral como o Lean. Frameworks de propósito geral existentes frequentemente carecem do suporte estrutural específico necessário para representar os passos explícitos de um argumento de game-hopping como objetos de primeira classe.

Metodologia: O Framework HOPSCOTCH

Os autores apresentam o HOPSCOTCH, um framework para Lean 4 projetado para mecanizar provas criptográficas baseadas em jogos computacionalmente sólidas. O framework faz a ponte entre a automação especializada e a verificação de propósito geral através dos seguintes pilares metodológicos:

1. Shallow Embedding e Indistinguibilidade de Oráculos

O HOPSCOTCH emprega um shallow embedding: oráculos, reduções e adversários são definidos como funções e tipos comuns do Lean, em vez de uma linguagem de domínio específico separada.

Definições de Segurança: Noções de segurança são expressas como indistinguibilidade entre oráculos probabilísticos com estado. Um oráculo é modelado como um procedimento com estado que responde a consultas, representado usando o monad RState (StateT sobre Funções de Massa de Probabilidade).
Reduções: Reduções de oráculo são modeladas como computações abstratas (OracleComp) que podem consultar um oráculo subjacente enquanto mantêm seu próprio estado. A composição é tratada via uma operação simulateQ, denotada pela notação de diamante ( $R \diamond O$ ).

2. Objetos de Prova Explícitos

Ao contrário das provas padrão do Lean, que são frequentemente scripts não estruturados, uma prova do HOPSCOTCH é um objeto formal explícito do tipo IndistinguishabilityI. Os construtores deste tipo indutivo correspondem diretamente aos passos de um argumento de game-hopping:

obsEq: Hops baseados em equivalência observacional (identidade semântica).
reduction: Hops obtidos aplicando uma redução de oráculo a ambos os lados de uma afirmação de indistinguibilidade.
assumption: Hops justificados por uma suposição criptográfica (um par de oráculos indistinguíveis).
symm e trans: Regras estruturais para simetria e transitividade.
longSequence: Um construtor para argumentos de híbridos onde o comprimento da sequência depende de parâmetros (por exemplo, o parâmetro de segurança $\kappa$ ou limites de consultas), em vez de ser fixo.

3. Equivalência Observacional via Abstração

Para provar que dois oráculos são observacionalmente equivalentes (ou seja, indistinguíveis por qualquer observador), o HOPSCOTCH utiliza uma metodologia de abstração de estado. Em vez de depender de lógicas de programas relacionais complexas, o usuário fornece uma função de abstração mapeando o estado de um oráculo para o estado de outro.

Abstração Determinística: Uma função $f: S_1 \to S_2$ que preserva estados iniciais e comuta com transições de consulta.
Abstração Randomizada: Uma função $f: S_1 \to \text{PMF}(S_2)$ que lida com transformações de estado probabilísticas, como substituir amostragem ávida (eager) por amostragem adiada (deferred).
Esta abordagem suporta padrões de prova comuns como esquecer estado irrelevante, introduzir redundância de estado e reorganizar (reshuffle) o estado.

4. Automação e Táticas

O framework inclui táticas de domínio específico, principalmente game_hopping, que automatiza a construção de objetos de prova.

A tática aceita uma lista de oráculos intermediários e gera subobjetivos (subgoals) para hops adjacentes.
Ela tenta resolver esses subobjetivos automaticamente reconhecendo padrões de redução ou aplicando lemas de abstração de estado.
Se a automação falhar, o usuário pode fornecer manualmente a função de abstração usando by_abstraction ou by_rand_abstraction.

5. Solidez Computacional

O framework prova um teorema de solidez computacional geral. Este teorema interpreta o objeto de prova explícito construindo reduções concretas contra as suposições usadas na prova.

Para cada distinguidor contra os oráculos finais, o teorema constrói um distinguidor para cada suposição usada na prova.
Ele deriva um limite concreto na vantagem original como uma soma das vantagens contra as suposições, ponderada pelo número de vezes que cada suposição é usada (levando em conta reversões de simetria).
O framework não verifica formalmente a complexidade de tempo polinomial dentro do Lean; em vez disso, ele se baseia em limites de segurança concretos e na verificação externa da natureza de tempo polinomial das reduções construídas.

Contribuições Principais e Resultados

O artigo demonstra a utilidade do HOPSCOTCH formalizando várias provas criptográficas representativas:

IND-RAND para IND-CPA: Uma prova formal mostrando que a segurança real-ou-aleatória implica indistinguibilidade sob ataque de texto claro escolhido, ilustrando o uso de reduções de oráculo e equivalência observacional.
Encrypt-then-MAC: Uma prova de segurança IND-CCA para a construção Encrypt-then-MAC. Este estudo de caso destaca o uso de abstrações de reorganização (reempacotamento de estado) e introdução de redundância (provando equivalência quando campos de estado são duplicados).
Criptografia ElGamal: Uma prova de segurança baseada na suposição de Diffie-Hellman Decisional (DDH). Este estudo de caso utiliza esquecimento de informação irrelevante e abstrações de aleatoriedade adiada (amostragem adiada vs. ávida), além de lemas de simplificação específicos de grupos.
Secrecy de Uso Único para IND-CPA: Uma prova demonstrando que a secreção de uso único implica segurança pública IND-CPA. Isto utiliza equivalência observacional limitada e sequências longas onde o comprimento do argumento híbrido depende do limite de consultas do adversário.
Construção de Função Pseudorandom GGM: Uma formalização da construção GGM transformando um PRG em um PRF.
- Esta prova apresenta uma sequência híbrida de comprimento $\kappa$ (o parâmetro de segurança).
- Aplica o idioma de aleatoriedade adiada a caches inteiros de rótulos aleatórios em vez de valores individuais.
- Significância: Tanto quanto o conhecimento dos autores, esta é a primeira prova mecanizada da construção GGM para profundidade não constante em um provador de teoremas de propósito geral (trabalhos anteriores por CryptoZoo formalizaram profundidade 3).

Significância e Alegações

Os autores alegam que o HOPSCOTCH consegue fazer a ponte entre ferramentas especializadas de game-hopping e provadores de teoremas de propósito geral. Sua significância reside em:

Solidez Fundamental: Ao usar o kernel do Lean e todo o ecossistema Mathlib (incluindo teoria de grupos finitos), o framework garante que as provas estejam fundamentadas em uma base confiável, ao contrário de ferramentas de domínio específico que dependem de verificadores customizados.
Estrutura Explícita: Representar provas como objetos explícitos permite melhor inspeção, automação e a derivação de limites de segurança concretos que rastreiam o uso de suposições.
Expressividade: O framework suporta argumentos de híbridos dependentes de parâmetros e transformações de estado complexas (via abstração randomizada) que são difíceis de modelar em outros sistemas.
Automação: A combinação de objetos de prova explícitos e táticas de domínio específico reduz o código repetitivo (boilerplate), tornando as provas formais mais curtas e legíveis, mantendo o poder da automação de propósito geral.

O artigo conclui que, embora ainda não formalize totalmente a complexidade de tempo polinomial assintótica (deixando isso como uma condição externa), os limites de segurança concretos fornecidos pelo teorema de solidez são suficientes para recuperar noções assintóticas padrão sob suposições externas razoáveis. Os autores veem o framework como um alvo promissor para futura geração de provas assistida por máquina e integração de transições com limites de erro.