break-golf

Ein Board für kryptanalytische Ergebnisse, die bewiesen, nicht ausgeführt werden.

Eine Challenge legt zwei Welten und die Aussage fest, die du beweisen musst. Du schreibst einen Angreifer und einen Beweis, dass er die Welten unterscheidet. Der Sieg ist der Beweis: Nichts wird ausgeführt, abgetastet oder abgespielt, und kein Mensch liest die Einreichung, um zu entscheiden, ob sie zählt.

Status: Proof-of-Concept. Die Website ist statisch, Einreichungen eröffnen ein GitHub-Issue, und ein Mensch entscheidet. Dahinter steht noch kein Lean-Verifier.

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 läuft bei Push und Pull-Request: die --check-Gates, der Config-Lint, der Site-Check und eine Reihe von Einreichungen, die der Verifier akzeptieren und ablehnen muss — ein sorry, ein native_decide, eine unbekannte Challenge, ein Null-Vorteil, ein Body ohne Lean-Block. workflow_dispatch verifiziert eine Einreichung auf Abruf, ohne ein Issue zu eröffnen.

submission.yml behandelt ein verify:-Issue in zwei Jobs. Der erste parst nicht vertrauenswürdige Eingabe und hat keine Schreibrechte; der zweite lädt dessen Urteil herunter und postet den Kommentar. Diese Trennung stammt von lean-golf, und sie ist der Grund, warum ein Issue-Body kein Token erreichen kann.

Der Einreichende schreibt die Aussage nie selbst

Das ist der gesamte Mechanismus, und es ist derselbe, den trailofbits/lean-golf für Proof Golf verwendet. Der Verifier baut seine eigene Kopie von Challenge.lean. Eine Einreichung liefert nur:

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 und advantage aus dem Formular. attack und score werden in Challenge.lean aus diesen Zahlen zusammengesetzt, sodass eine Einreichung kein größeres Budget ausgeben kann, als ihr zugrunde gelegt wird, oder eine schwächere Schranke beweisen kann, als sie behauptet — nicht weil wir es prüfen, sondern weil sie bei keinem der beiden Objekte den Stift in der Hand hat.

Vier Ablehnungen, die ein Verifier ausspricht, ohne etwas zu lesen:

Auch native_decide, maxHeartbeats und maxRecDepth werden abgelehnt: Ein Beweis, der nur mit erhöhtem Limit abschließt, ist ein Beweis, den sich der Verifier nicht leisten kann.

Bewertung

Nichts ist im Voraus festgelegt. Bei einem Schema, das niemand untersucht hat, ist die Forschungsfrage, welcher Vorteil zu welchen Kosten erreichbar ist, also ist jedes Ziel eine Vermutung — und ein zu hoch angesetztes Ziel bewertet einen echten 2⁻³⁰-Distinguisher mit null. Das Board misst stattdessen das Ergebnis:

score = log₂( budget / advantage^e )

Abfragen pro Einheit Vorteil; ihr Logarithmus zur Basis zwei ist das Sicherheitsniveau in Bits, das der Angriff widerlegt. Niedriger ist besser. Den eigenen Vorteil niedriger anzugeben erhöht den Score, also gibt es nichts zu gewinnen, wenn man weniger behauptet, als man beweisen kann.

e ist pro Challenge festgelegt und hat keinen Standardwert. e = 2 für ein Entscheidungsspiel — ein Vorteil α benötigt etwa α⁻² Wiederholungen, um verstärkt zu werden — und e = 1 für ein suchartiges. Beide Konventionen finden sich in der Literatur, und die Inkonsistenz ist bekannt (Micciancio–Walter, On the Bit Security of Cryptographic Primitives), daher gibt eine Challenge an, welche sie verwendet.

Par ist die eigene Behauptung des Designers, aus der Spezifikation übernommen, sodass nirgendwo eine Vermutung über die Angriffsschwierigkeit auftaucht. Ein Ergebnis unter Par ist ein Bruch der Behauptung.

Die Frontier ist der primäre Datensatz: Ein Ergebnis kommt hinzu, wenn nichts anderes es gleichzeitig bei Abfragen und Vorteil übertrifft. Der Bit-Score ist die danebenstehende Rangspalte, und zwei geprüfte Lemmata in der Lean-Schicht (Score.workFactor_lt_of_dominates, Score.onFrontier_of_workFactor_min) garantieren, dass das Ranking nie ein Ergebnis begräbt, das auf beiden Achsen gewinnt.

Challenges

spoc128 — SpoC-128, wie bei NIST LWC Runde 2 eingereicht. Gebrochen: drei Abfragen, Vorteil 1, 1,58 Bits. load key n legt die Nonce in die Rate und tagInput XORt tagControl in dieselbe Rate, also gilt tagInput (load key n) = load key (n ^^^ tagControl). Ein Permutationseingang ist über zwei Abfragen erreichbar, und da die Permutation öffentlich und invertierbar ist, leckt eine Hälfte davon in einem Tag und eine Hälfte in einem Chiffratblock; füge zusammen, invertiere, nimm die Kapazität, und das ist der Schlüssel.

spoc128-ds — derselbe Modus, wobei die vier Steuerbits in der Nonce reserviert sind, sodass n ^^^ tagControl keine zulässige Nonce ist. Offen: kein Angriff bekannt. Die Einschränkung lebt im Typ einer Abfrage, daher ist der veröffentlichte Angriff hier nicht bloß erfolglos — er kann überhaupt nicht als Angreifer formuliert werden (SpoC128DS.attack_second_query_illegal).

Das ist bewusst keine zweite Kopie des Modus. DDC.lean abzuhärten würde ein paralleles Modell bedeuten, das synchron gehalten werden müsste; den Abfragebereich einzuschränken ist ein einziges Prädikat, und jedes vorhandene Theorem über den Modus gilt weiterhin.

Hier wird nicht behauptet, dass die Variante sicher ist. Eine veröffentlichte Route in einen Modus zu schließen ist kein Argument dafür, dass keine andere Route existiert — genau das ist der Sinn, sie hier zu präsentieren.

Eine Challenge hinzufügen

Stelle ein Golf.Game in der Lean-Schicht bereit — einen öffentlichen Parametertyp, einen Abfrage- und Antworttyp und die zwei Welten — und dazu eine config.json hier. Die generische Schicht liegt in RandomSystems/Golf/Game.lean; RandomSystems/Golf/Instances/SpoC128/ ist das ausgearbeitete Beispiel und dient zugleich als Prüfung, dass die Abstraktion treu ist: Ihre Adäquatheitsbelege sind rfl, und ihre Referenzeinreichung wird durch das vorhandene attack_distinguishing_advantage ohne Neuformulierung abgeschlossen.

Was hier nicht bewertet wird

• Offline-Arbeit, ausdrücklich. Der Angreifer ist ein symbolisches Objekt, und das Board bewertet die Abfragekomplexität — das informationstheoretische Setting, in dem Indifferentiability und das PRP/PRF-Switching-Lemma bereits leben. Eine Challenge, die rechnerische Machbarkeit erfordert, muss das sagen und eine kostenbehaftete Form festlegen.
• Verstärkung wird als verfügbar angenommen: q/α^e ist der Preis, einen Angriff bis zur Konfidenz zu wiederholen.
• Gleichstände sind keine Äquivalenzen. Dasselbe Bit-Niveau kann sehr unterschiedliche Ergebnisse enthalten — deshalb steht die Frontier neben dem Ranking, statt von ihm ersetzt zu werden.