break-golf

Un tableau de résultats de cryptanalyse qui sont prouvés, et non exécutés.

Un défi fixe deux mondes et l'énoncé que vous devez prouver. Vous écrivez un adversaire et une preuve qu'il les distingue. La victoire, c'est la preuve : rien n'est exécuté, échantillonné ni rejoué, et aucun humain ne lit la soumission pour décider si elle compte.

Statut : preuve de concept. Le site est statique, les soumissions ouvrent une issue GitHub, et un humain décide. Il n'y a pas encore de vérificateur Lean derrière.

Structure

python3 tools/manifest.py          # réécrit le manifeste
python3 tools/manifest.py --check  # échoue si obsolète
python3 tools/ledger.py            # réécrit le registre avec les scores et la frontière
python3 tools/lint_challenges.py   # les configs sont complètes
python3 tools/check_site.py        # le site peut afficher ce que les outils génèrent

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

CI

verify.yml s'exécute sur push et pull request : les contrôles --check, le lint des configs, la vérification du site, et une batterie de soumissions que le vérificateur doit accepter et doit rejeter — un sorry, un native_decide, un défi inconnu, un avantage nul, un corps sans bloc Lean. workflow_dispatch vérifie une soumission à la demande sans ouvrir d'issue.

submission.yml traite une issue verify: en deux jobs. Le premier analyse les entrées non fiables et ne détient aucun périmètre d'écriture ; le second télécharge son verdict et publie le commentaire. Cette séparation vient de lean-golf et c'est la raison pour laquelle un corps d'issue ne peut pas atteindre un token.

Le soumissionnaire n'écrit jamais l'énoncé

C'est là tout le mécanisme, et c'est le même que celui qu'utilise trailofbits/lean-golf pour le golf de preuves. Le vérificateur construit sa propre copie de Challenge.lean. Une soumission ne fournit que :

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

plus budget et advantage sur le formulaire. attack et score sont assemblés à partir de ces nombres dans Challenge.lean, si bien qu'une soumission ne peut pas dépenser un budget plus grand que celui pour lequel elle est notée, ni prouver une borne plus faible que celle qu'elle revendique — non pas parce que nous vérifions, mais parce qu'elle ne tient jamais la plume sur aucun de ces deux objets.

Quatre rejets qu'un vérificateur effectue sans rien lire :

native_decide, maxHeartbeats et maxRecDepth sont également rejetés : une preuve qui ne se conclut qu'avec une limite relevée est une preuve que le vérificateur ne peut pas se permettre.

Notation

Rien n'est fixé à l'avance. Sur un schéma que personne n'a étudié, quel avantage est atteignable à quel coût est la question de recherche, donc toute cible est une supposition — et une cible fixée trop haut note un véritable distinguisher 2⁻³⁰ comme zéro. Le tableau mesure plutôt le résultat :

score = log₂( budget / advantage^e )

Requêtes par unité d'avantage ; son logarithme en base deux est le niveau de sécurité en bits que l'attaque réfute. Plus bas est mieux. Sous-estimer votre avantage augmente le score, donc il n'y a rien à gagner à revendiquer moins que ce que vous pouvez prouver.

e est propre à chaque défi et n'a pas de valeur par défaut. e = 2 pour un jeu de décision — un avantage α nécessite environ α⁻² répétitions pour être amplifié — et e = 1 pour un jeu à saveur de recherche. Les deux conventions figurent dans la littérature et l'incohérence est connue (Micciancio–Walter, On the Bit Security of Cryptographic Primitives), donc chaque défi précise laquelle il utilise.

Le par est la propre revendication du concepteur, tirée de la spécification, donc aucune supposition sur la difficulté d'attaque n'apparaît nulle part. Un résultat sous le par brise la revendication.

La frontière est le registre principal : un résultat la rejoint lorsque rien d'autre ne le bat à la fois sur les requêtes et sur l'avantage. Le score en bits est la colonne classée à côté, et deux lemmes vérifiés dans la couche Lean (Score.workFactor_lt_of_dominates, Score.onFrontier_of_workFactor_min) garantissent que le classement n'enterre jamais un résultat qui gagne sur les deux axes.

Défis

spoc128 — SpoC-128 tel que soumis au NIST LWC Round 2. Cassé : trois requêtes, avantage 1, 1,58 bits. load key n place le nonce dans le rate et tagInput fait un XOR de tagControl dans le même rate, si bien que tagInput (load key n) = load key (n ^^^ tagControl). Une entrée de permutation est atteignable par deux requêtes, et comme la permutation est publique et inversible, la moitié fuit dans un tag et la moitié dans un bloc de texte chiffré ; assemblez, inversez, prenez la capacité, et voilà la clé.

spoc128-ds — le même mode avec les quatre bits de contrôle réservés dans le nonce, si bien que n ^^^ tagControl n'est pas un nonce légal. Ouvert : aucune attaque connue. La restriction vit dans le type d'une requête, si bien que l'attaque publiée n'est pas simplement infructueuse ici — elle ne peut pas du tout être présentée comme un adversaire (SpoC128DS.attack_second_query_illegal).

Ce n'est délibérément pas une seconde copie du mode. Durcir DDC.lean signifierait un modèle parallèle à maintenir synchronisé ; restreindre le domaine des requêtes est un prédicat, et tous les théorèmes existants sur le mode s'appliquent toujours.

Rien ici ne prétend que la variante est sûre. Fermer une route publiée vers un mode n'est pas un argument pour affirmer qu'aucune autre route n'existe — c'est tout l'intérêt de la mettre en ligne.

Ajouter un défi

Fournissez un Golf.Game dans la couche Lean — un type de paramètre public, un type de requête et de réponse, et les deux mondes — puis un config.json ici. La couche générique vit dans RandomSystems/Golf/Game.lean ; RandomSystems/Golf/Instances/SpoC128/ est l'exemple traité, et sert aussi de vérification que l'abstraction est fidèle : ses preuves d'adéquation sont des rfl et sa soumission de référence est déchargée par l'attack_distinguishing_advantage existant sans reformulation.

Ce que cela ne note pas

• Le travail hors ligne, par décision. L'adversaire est un objet symbolique et le tableau évalue la complexité en requêtes, le cadre de la théorie de l'information dans lequel vivent déjà l'indifférentiabilité et le lemme de commutation PRP/PRF. Un défi nécessitant une faisabilité computationnelle doit le préciser et fixer une forme qui porte un coût.
• L'amplification est supposée disponible : q/α^e est le coût de répétition d'une attaque pour atteindre la confiance.
• Les égalités ne sont pas des équivalences. Le même niveau de bits peut contenir des résultats très différents, c'est pourquoi la frontière se tient à côté du classement plutôt que d'être remplacée par lui.