break-golf

Un tablero para resultados de criptoanálisis que están demostrados, no ejecutados.

Un desafío fija dos mundos y el enunciado que debes demostrar. Escribes un adversario y una prueba de que los distingue. La victoria es la prueba: no se ejecuta, muestrea ni reproduce nada, y ningún humano lee el envío para decidir si cuenta.

Estado: prueba de concepto. El sitio es estático, los envíos abren un issue de GitHub y un humano decide. Todavía no hay un verificador de Lean detrás.

Layout

python3 tools/manifest.py          # rewrite the manifest
python3 tools/manifest.py --check  # fail if stale
python3 tools/ledger.py            # rewrite the ledger with scores and frontier
python3 tools/lint_challenges.py   # configs are complete
python3 tools/check_site.py        # the site can render what the tools generate

printf '%s' "$BODY" | python3 tools/verify.py spoc128    # one submission

CI

verify.yml se ejecuta en push y pull request: las comprobaciones --check, el lint de configuración, la verificación del sitio y una batería de envíos que el verificador debe aceptar y debe rechazar — un sorry, un native_decide, un desafío desconocido, una ventaja cero, un cuerpo sin bloque de Lean. workflow_dispatch verifica un envío bajo demanda sin abrir un issue.

submission.yml gestiona un issue verify: en dos trabajos. El primero analiza la entrada no confiable y no tiene ningún permiso de escritura; el segundo descarga su veredicto y publica el comentario. Esa división es la de lean-golf y es la razón por la que el cuerpo de un issue no puede alcanzar un token.

El remitente nunca escribe el enunciado

Este es todo el mecanismo, y es el mismo que trailofbits/lean-golf usa para el golf de pruebas. El verificador construye su propia copia de Challenge.lean. Un envío proporciona solo:

def strategy : game.Param → PFunDDS.DDE game.Query game.Response
def verdict  : List (game.Query × Option game.Response) → Bool
theorem attackWins : attack.Wins score.budget score.advantage

además de budget y advantage en el formulario. attack y score se ensamblan a partir de esos números en Challenge.lean, por lo que un envío no puede gastar un presupuesto mayor que aquel por el que se le puntúa, ni demostrar una cota más débil de la que afirma — no porque lo comprobemos, sino porque nunca sostiene la pluma sobre ninguno de los dos objetos.

Cuatro rechazos que un verificador emite sin leer nada:

native_decide, maxHeartbeats y maxRecDepth también se rechazan: una prueba que solo se cierra con un límite aumentado es una prueba que el verificador no puede permitirse.

Scoring

Nada se fija de antemano. En un esquema que nadie ha estudiado, qué ventaja es alcanzable a qué coste es la pregunta de investigación, así que cualquier objetivo es una conjetura — y un objetivo fijado demasiado alto puntúa como cero un distinguidor genuino de 2⁻³⁰. El tablero, en cambio, mide el resultado:

score = log₂( budget / advantage^e )

Consultas por unidad de ventaja; su logaritmo en base dos es el nivel de seguridad en bits que el ataque refuta. Cuanto más bajo, mejor. Subestimar tu ventaja aumenta la puntuación, así que no hay nada que ganar afirmando menos de lo que puedes demostrar.

e es específico de cada desafío y no tiene valor por defecto. e = 2 para un juego de decisión — una ventaja α necesita unas α⁻² repeticiones para amplificarse — y e = 1 para uno orientado a la búsqueda. Ambas convenciones están en la literatura y la inconsistencia es conocida (Micciancio–Walter, On the Bit Security of Cryptographic Primitives), así que cada desafío indica cuál usa.

El par es la afirmación del propio diseñador, tomada de la especificación, de modo que no aparece ninguna conjetura sobre la dificultad del ataque en ningún sitio. Estar bajo par es una ruptura de la afirmación.

La frontera es el registro principal: un resultado se une a ella cuando nada más lo supera en consultas y ventaja a la vez. La puntuación de bits es la columna clasificada junto a ella, y dos lemas verificados en la capa de Lean (Score.workFactor_lt_of_dominates, Score.onFrontier_of_workFactor_min) garantizan que la clasificación nunca entierre un resultado que gane en ambos ejes.

Challenges

spoc128 — SpoC-128 tal como se presentó a la Ronda 2 de NIST LWC. Roto: tres consultas, ventaja 1, 1,58 bits. load key n coloca el nonce en la tasa y tagInput hace XOR de tagControl en la misma tasa, por lo que tagInput (load key n) = load key (n ^^^ tagControl). Una entrada de permutación es alcanzable mediante dos consultas y, como la permutación es pública e invertible, la mitad se filtra en una etiqueta y la mitad en un bloque de cifrado; únelas, invierte, toma la capacidad, y esa es la clave.

spoc128-ds — el mismo modo con los cuatro bits de control reservados en el nonce, por lo que n ^^^ tagControl no es un nonce válido. Abierto: no se conoce ningún ataque. La restricción vive en el tipo de una consulta, por lo que el ataque publicado no es simplemente infructuoso aquí: no puede presentarse como adversario en absoluto (SpoC128DS.attack_second_query_illegal).

Esto no es, deliberadamente, una segunda copia del modo. Blindar DDC.lean supondría un modelo paralelo que mantener sincronizado; restringir el dominio de consulta es un predicado, y todo teorema existente sobre el modo sigue aplicándose.

Nada de esto afirma que la variante sea segura. Cerrar una ruta publicada hacia un modo no es un argumento de que no exista otra ruta — que es el punto de ponerla sobre el tablero.

Añadir un desafío

Proporciona un Golf.Game en la capa de Lean — un tipo de parámetro público, un tipo de consulta y respuesta, y los dos mundos — y luego un config.json aquí. La capa genérica vive en RandomSystems/Golf/Game.lean; RandomSystems/Golf/Instances/SpoC128/ es el ejemplo resuelto y sirve también como comprobación de que la abstracción es fiel: sus pruebas de adecuación son rfl y su envío de referencia se resuelve mediante el attack_distinguishing_advantage existente sin reformulación.

Lo que esto no puntúa

• Trabajo fuera de línea, por decisión. El adversario es un objeto simbólico y el tablero puntúa la complejidad de consultas, el marco de teoría de la información en el que ya viven la indiferenciabilidad y el lema de conmutación PRP/PRF. Un desafío que necesite viabilidad computacional debe decirlo y fijar una forma que conlleve coste.
• Amplificación se asume disponible: q/α^e es el coste de repetir un ataque para alcanzar confianza.
• Los empates no son equivalencias. El mismo nivel de bits puede albergar resultados muy diferentes, por eso la frontera se sitúa junto a la clasificación en lugar de ser reemplazada por ella.