💻 computer science

Game Hopping in Lean

Este artículo presenta HOPSCOTCH, un marco de trabajo de Lean 4 que mecaniza pruebas criptográficas basadas en juegos y computacionalmente sólidas mediante un método de incrustación superficial y abstracción de estado para verificar formalmente propiedades de seguridad complejas como la construcción GGM y la seguridad IND-CCA.

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

Publicado 2026-08-07

📖 8 min de lectura🧠 Análisis profundo

CC BY 4.0

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

Artículo original bajo licencia CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta es una explicación generada por IA del artículo a continuación. No ha sido escrita ni avalada por los autores. Para mayor precisión técnica, consulte el artículo original. Leer descargo de responsabilidad completo

Imagina que eres un maestro cerrajero tratando de demostrar que tu nueva caja fuerte es inquebrantable. No te limitas a decir: "¡Es fuerte!". Tienes que mostrar una secuencia de pasos: "Si no puedes romper esta pequeña cerradura, no puedes romper la puerta; si no puedes romper la puerta, no puedes romper la caja fuerte". Así es como funciona la criptografía moderna. Los expertos utilizan "juegos" para probar la seguridad, donde un hacker intenta adivinar un secreto, y la seguridad de un sistema se demuestra mostrando que romperlo es tan difícil como resolver un rompecabezas conocido e imposible. Pero aquí está el truco: hacer estas demostraciones a mano es como intentar equilibrar una casa de naipes en un huracán. Es fácil cometer un error minúsculo, pasar por alto un vacío sutil o perderse en la complejidad, y si te saltas un solo paso, toda la demostración colapsa. Por eso, los científicos han estado buscando una forma de lograr que una computadora revise cada una de las cartas, asegurando que la casa se mantenga en pie.

Aquí es donde entra en juego este artículo. Los autores han construido un taller digital llamado HOPSCOTCH (un nombre lúdico para un juego de saltos) dentro de un potente programa de computadora llamado Lean 4. Piensa en HOPSCOTCH como un lector de pruebas robótico y superinteligente que no solo revisa tus matemáticas, sino que entiende la historia de la demostración de seguridad. En lugar de obligar a los criptógrafos a escribir en un lenguaje extraño y limitado, HOPSCOTCH les permite escribir demostraciones utilizando las mismas herramientas que usan para todo su otro trabajo matemático. Convierte el proceso de "salto de juegos" —saltar de un escenario de seguridad al siguiente— en un objeto claro y paso a paso que la computadora puede inspeccionar, verificar e incluso ayudar a automatizar. Los autores no solo construyeron la herramienta; la utilizaron para demostrar con éxito la seguridad de varios métodos de cifrado famosos, incluyendo una construcción compleja llamada GGM, demostrando que este "lector de pruebas robótico" puede manejar desafíos criptográficos del mundo real sin confundirse.

El panorama general: Por qué necesitamos un robot lector de pruebas

En el mundo de la seguridad digital, dependemos de la "seguridad demostrable". Esto significa que no solo esperamos que nuestros códigos sean seguros, sino que intentamos demostrarlo. La forma estándar de hacer esto es el enfoque basado en "juegos". Imagina a un guardia de seguridad (el sistema) y a un ladrón (el adversario). El guardia tiene un secreto y el ladrón intenta adivlarlo. Para demostrar que el guardia es seguro, no nos limitamos a decir "es bueno". Creamos una serie de "juegos" o escenarios.

El Juego Real: El ladrón intenta romper el sistema real.
El Salto: Imaginamos un juego ligeramente diferente que es casi igual pero más fácil de analizar. Demostramos que si el ladrón puede ganar el Juego Real, también puede ganar este nuevo juego, ligeramente distinto.
La Cadena: Seguimos saltando de un juego a otro, cambiando las reglas un poquito cada vez, hasta llegar a un juego final que es obviamente imposible de ganar (como adivinar correctamente el lanzamiento de una moneda un millón de veces seguidas).

Si podemos demostrar que cada uno de estos "saltos" es seguro, entonces toda la cadena es segura. Esto se llama una "demostración de salto de juegos" (game-hopping proof).

El problema es que los humanos somos terribles haciendo esto de manera perfecta. Estas demostraciones son largas, desordenadas y llenas de detalles minúsculos. Un solo detalle omitido puede hacer que toda la demostración sea errónea y que el sistema sea inseguro. Durante años, los investigadores han intentado construir herramientas informáticas especiales para revisar estas demostraciones, pero estas herramientas a menudo hablan un lenguaje diferente al de los matemáticos. Son como un traductor que solo habla "Seguridad" pero no "Matemáticas", obligando a los expertos a traducir sus ideas de un lado a otro, lo cual es lento y propenso a errores.

Entra HOPSCOTCH: El traductor universal

Los autores de este artículo, Stefan Dziembowski, Grzegor Fabiański, Daniele Micciancio y Rafał Stefański, decidieron construir un puente. Crearon HOPSCOTCH, un marco de trabajo dentro de Lean 4, un programa de computadora popular utilizado para verificar demostraciones matemáticas.

He aquí la magia de HOPSCOTCH:

Sin un nuevo lenguaje: A diferencia de otras herramientas que te obligan a aprender una forma nueva y restringida de escribir código, HOPSCOTCH te permite escribir demostraciones usando el Lean estándar. Es como dejar que un chef cocine con sus propios cuchillos favoritos en lugar de obligarlo a usar de plástico.
Demostraciones como objetos: En HOPSCOTCH, una demostración no es solo un montón de texto. Es un objeto estructurado, como un modelo de LEGO. Cada "salto" en el juego es un bloque de LEGO específico. Puedes ensamblarlos y la computadora verifica si encajan perfectamente. Si intentas conectar dos bloques que no coinciden, la computadora dice: "No, esto no funciona".
El truco de la "Abstracción": Una de las partes más difíciles de estas demostraciones es mostrar que dos sistemas diferentes se comportan exactamente igual. HOPSKOTCH utiliza un trucción ingenioso llamado "abstracción de estado". Imagina que tienes dos robots. Uno tiene un diagrama de cableado interno desordenado y el otro tiene uno ordenado. HOPSCOTCH te permite dibujar un mapa (una función de abstracción) que muestra cómo los cables desordenados corresponden a los ordenados. Si el mapa es correcto, la computadora sabe que los robots son idénticos en su comportamiento, aunque se vean diferentes por dentro.

Lo que realmente hicieron y encontraron

Los autores no solo construyeron la herramienta; la pusieron a prueba. Utilizaron HOPSCOTCH para verificar formalmente la seguridad de cuatro conceptos criptográficos importantes:

Encrypt-then-MAC: Un método para hacer que los mensajes sean tanto secretos como a prueba de manipulaciones. Demostraron que si el cifrado subyacente y la "etiquetación" (MAC) son seguros, todo el conjunto es seguro incluso contra los hackers más inteligentes.
Cifrado ElGamal: Una forma famosa de enviar mensajes secretos utilizando claves públicas. Mostraron cómo demostrar su seguridad basándose en un problema matemático difícil llamado supuesto de Diffie-Hellman Decisional (DDH).
Secreto de un solo uso a IND-CPA: Demostraron que si un sistema es seguro para un solo mensaje, puede hacerse seguro para muchos mensajes, un paso crucial para construir un cifrado robusto.
La Construcción GGM: Este es el gran reto. El método GGM convierte un simple generador de números aleatorios en una función pseudialeatoria compleja (un generador de números aleatorios falsos que parece real). Las demostraciones computacionales previas solo podían manejar versiones muy superficiales de esto (como un árbol de 3 niveles). Los autores utilizaron HOPSCOTCH para demostrar la seguridad de GGM para una profundidad no constante, lo que significa que funciona para árboles de cualquier tamaño. Hasta donde saben, esta es la primera vez que un asistente de prueba de propósito general verifica con éxito esta construcción específica y compleja.

Cómo lo hicieron (La mecánica del "Juego")

El artículo explica que HOPSCOTCH funciona dividiendo la demostración en pasos específicos, o constructores:

Equivalencia Observacional: Demostrar que dos juegos se ven iguales para un observador externo.
Reducciones: Mostrar que si puedes romper el Juego A, también puedes romper el Juego B.
Secuencias de Híbridos: Encadenar muchos pasos pequeños.

El marco incluye "tácticas" (ayudantes automatizados) que intentan resolver estos pasos por ti. Por ejemplo, si necesitas demostrar que dos oráculos (los sistemas de juego) son iguales, la computadora podría intentar automáticamente encontrar un "mapa de abstracción de estado". Si no puede encontrarlo, deja el paso para que el humano lo resuelva, pero mantiene la estructura para que el humano sepa exactamente dónde se encuentra.

Los autores también demostraron un "teorema de solidez computacional". Esta es una forma elegante de decir: "Si la computadora dice que esta demostración es válida, entonces es realmente válida en el mundo real". Demostraron que para cada objeto de demostración que crea HOPSCOTCH, se puede calcular matemáticamente exactamente cuánta "ventaja" tendría un hacker, basándose en los supuestos utilizados en la demostración. Esto asegura que la computadora no esté simplemente jugando un juego consigo misma; está dando una garantía de seguridad real y concreta.

La conclusión

El artículo concluye que HOPSCOTCH logra cerrar la brecha entre la conveniencia de las herramientas especializadas en seguridad y el poder de los asistentes matemáticos de propósito general. Permite a los criptógrafos escribir demostraciones que son más fáciles de leer, más fáciles de verificar y menos propensas al error humano. Aunque los autores admiten que la computadora aún no verifica si el "hacker" está operando con rapidez suficiente (un detalle técnico llamado tiempo polinómico), han sentado las bases para demostraciones de seguridad totalmente automatizadas y confiables.

También sugieren el futuro: con estos objetos de demostración estructurados, pronto podría ser posible usar la IA para ayudar a escribir estas demostraciones automáticamente, o extender el sistema para manejar escenarios aún más complejos que involucren "eventos adversos" y probabilidad. Pero por ahora, el logro principal es claro: han construido una forma fiable, flexible y poderosa de permitir que las computadoras nos ayuden a demostrar que nuestros secretos digitales están seguros.

=== RESUMEN ===

Resumen Técnico: Game Hopping en Lean

Declaración del Problema

La criptografía moderna depende fuertemente del paradigma de la seguridad demostrable, típicamente formalizada a través de definiciones basadas en juegos computacionales. En este marco, la seguridad se establece construyendo una secuencia de "saltos de juego" (o argumentos de híbridos) que reducen la ventaja de un adversario a problemas computacionales difíciles conocidos. Sin embargo, las demostraciones manuales basadas en juegos son notoriamente propensas a errores, monolíticamente complejas y susceptibles de lagunas sutiles.

Si bien las herramientas de dominio específico como EasyCrypt y CryptoVerif han automatizado con éxito grandes clases de estas reducciones, operan fuera de los probadores de teoremas interactivos de propósito general. Esto fuerza un compromiso: los desarrolladores deben elegir entre la conveniencia de la automatización especializada y la expresividad fundacional y la solidez de los probadores de propósito general como Lean. Los marcos existentes de propósito general a menudo carecen del soporte estructural específico necesario para representar los pasos explícitos de un argumento de salto de juego como objetos de primera clase.

Metodología: El Marco HOPSCOTCH

Los autores presentan HOPSCOTCH, un marco de trabajo en Lean 4 diseñado para mecanizar demostraciones criptográficas basadas en juegos y computacionalmente sólidas. El marco cierra la brecha entre la automatización especializada y la verificación de propósito general a través de los siguientes pilares metodológicos:

1. Incrustación Superficial (Shallow Embedding) y la Indistinguibilidad de Oráculos

HOPSCOTCH emplea una incrustación superficial: los oráculos, las reducciones y los adversarios se definen como funciones y tipos ordinarios de Lean en lugar de un lenguaje de dominio específico separado.

Definiciones de Seguridad: Las nociones de seguridad se expresan como la indistinguibilidad entre oráculos de estado dependientes del estado. Un oráculo se modela como un procedimiento con estado que responde consultas, representado mediante el monad RState (StateT sobre Funciones de Masa de Probabilidad).
Reducciones: Las reducciones de oráculo se modelan como computaciones abstractas (OracleComp) que pueden consultar un oráculo subyacente mientras mantienen su propio estado. La composición se gestiona mediante una operación simulateQ, denotada por la notación de diamante ( $R \diamond O$ ).

2. Objetos de Prueba Explícitos

A diferencia de las demostraciones estándar de Lean, que suelen ser scripts no estructurados, una demostración de HOPSCOTCH es un objeto formal explícito del tipo IndistinguishabilityI. Los constructores de este tipo inductivo corresponden directamente a los pasos de un argumento de salto de juego:

obsEq: Saltos basados en la equivalencia observacional (identidad semántica).
reduction: Saltos obtenidos al aplicar una reducción de oráculo a ambos lados de una declaración de indistinguibilidad.
assumption: Saltos justificados por una suposición criptográfica (un par de oráculos indistinguibles).
symm y trans: Reglas estructurales para simetría y transitividad.
longSequence: Un constructor para argumentos de híbridos donde la longitud de la secuencia depende de parámetros (por ejemplo, el parámetro de seguridad $\kappa$ o los límites de consultas), en lugar de ser fija.

3. Equivalencia Observacional mediante Abstracción

Para demostrar que dos oráculos son observacionalmente equivalentes (es decir, indistinguibles por cualquier observador), HOPSCOTCH utiliza una metodología de abstracción de estado. En lugar de depender de lógicas de programas relacionales complejas, el usuario proporciona una función de abstracción que mapea el estado de un oráculo al estado de otro.

Abstracción Determinista: Una función $f: S_1 \to S_2$ que preserva los estados iniciales y conmuta con las transiciones de consulta.
Abstracción Aleatoria: Una función $f: S_1 \to \text{PMF}(S_2)$ que maneja transformaciones de estado probabilísticas, tales como reemplazar el muestreo eager (ávido) por el muestreo deferred (diferido).
Este enfoque soporta patrones de prueba comunes como el olvido de estado irrelevante, la introducción de estado redundante y el reordenamiento de estado.

4. Automatización y Tácticas

El marco incluye tácticas de dominio específico, principalmente game_hopping, que automatiza la construcción de objetos de prueba.

La táctica acepta una lista de oráculos intermedios y genera subobjetivos para los saltos adyacentes.
Intenta resolver estos subobjetivos automáticamente reconociendo patrones de reducción o aplicando lemas de abstracción de estado.
Si la automatización falla, el usuario puede suministrar manualmente la función de abstracción usando by_abstraction o by_rand_abstraction.

5. Solidez Computacional

El marco demuestra un teorema de solidez computacional general. Este teorema interpreta el objeto de prueba explícito construyendo reducciones concretas contra las suposiciones utilizadas en la prueba.

Para cada distinguidor contra los oráculos finales, el teorema construye un distinguidor para cada suposición utilizada en la prueba.
Deriva un límite concreto sobre la ventaja original como una suma de las ventajas contra las suposiciones, ponderadas por el número de veces que cada suposición es utilizada (teniendo en cuenta las reversiones de simetría).
El marco no verifica formalmente la complejidad de tiempo polinomial dentro de Lean; en su lugar, confía en límites de seguridad concretos y en la verificación externa de la naturaleza de tiempo polinomial de las reducciones construidas.

Contribuciones Clave y Resultados

El artículo demuestra la utilidad de HOPSCOTCH formalizando varias demostraciones criptográficas representativas:

IND-RAND a IND-CPA: Una demostración formal que muestra que la seguridad real-o-aleatoria implica la indistinguibilidad bajo ataque de texto plano elegido, ilustrando el uso de reducciones de oráculo y equivalencia observacional.
Encrypt-then-MAC: Una demostración de la seguridad IND-CCA para la construcción Encrypt-then-MAC. Este caso de estudio destaca el uso de abstracciones de reordenamiento (reempaquetado de estado) e introducción de redundancia (demostrar la equivalencia cuando los campos de estado se duplican).
Cifrado ElGamal: Una demostración de seguridad basada en la suposición de Diffie-Hellman Decisional (DDH). Este caso de estudio utiliza abstracciones de olvido de información irrelevante y aleatoriedad diferida (muestreo deferred vs. eager) junto con lemas de simplificación específicos de grupos.
Secreto de un solo uso a IND-CPA: Una demostración que muestra que el secreto de un solo uso implica la seguridad de clave pública IND-CPA. Esto utiliza equivalencia observacional acotada y secuencias largas donde la longitud del argumento de híbrido depende del límite de consultas del adversario.
Construcción de Función Pseudorandom GGM: Una formalización de la construcción GGM que transforma un PRG en un PRF.
- Esta demostración presenta una secuencia de híbridos de longitud $\kappa$ (el parámetro de seguridad).
- Aplica el idioma de aleatoriedad diferida a cachés enteros de etiquetas aleatorias en lugar de valores individuales.
- Significado: Según el conocimiento de los autores, esta es la primera demostración mecanizada de la construcción GGM para profundidad no constante en un probador de propósito general (trabajos previos por CryptoZoo formalizaron la profundidad 3).

Significado y Reivindicaciones

Los autores afirman que HOPSCOTCH logra cerrar la brecha entre las herramientas especializadas de salto de juego y los probadores de teoremas de propósito general. Su importancia radica en:

Solidez Fundacional: Al utilizar el kernel de Lean y todo el ecosistema Mathlib (incluyendo la teoría de grupos finitos), el marco asegura que las demostraciones estén fundamentadas en una base confiable, a diferencia de las herramientas de dominio específico que dependen de verificadores personalizados.
Estructura Explícita: Representar las demostraciones como objetos explícitos permite una mejor inspección, automatización y la derivación de límites de seguridad concretos que rastrean el uso de las suposiciones.
Expresividad: El marco soporta argumentos de híbridos dependientes de parámetros y transformaciones de estado complejas (vía abstracción aleatoria) que son difíciles de modelar en otros sistemas.
Automatización: La combinación de objetos de prueba explícitos y tácticas de dominio específico reduce el código repetitivo (boilerplate), haciendo que las demostraciones formales sean más cortas y legibles mientras se mantiene el poder de la automatización de propósito general.

El artículo concluye que, aunque aún no formaliza completamente la complejidad de tiempo polinomial asintótica (dejándola como una condición externa), los límites de seguridad concretos proporcionados por el teorema de solidez son suficientes para recuperar las nociones asintóticas estándar bajo suposiciones externas razonables. Los autores ven el marco como un objetivo prometedor para la futura generación de demostraciones asistida por máquina y la integración de transiciones con límites de error.