break-golf

Una bacheca per risultati di crittanalisi che sono dimostrati, non eseguiti.

Una sfida fissa due mondi e l'enunciato che devi dimostrare. Scrivi un avversario e una dimostrazione che li distingue. La vittoria è la dimostrazione: nulla viene eseguito, campionato o riprodotto, e nessun umano legge la sottomissione per decidere se è valida.

Stato: prova di concetto. Il sito è statico, le sottomissioni aprono una issue GitHub e decide un umano. Dietro non c'è ancora un verificatore Lean.

Struttura

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 viene eseguito su push e pull request: i gate --check, il lint delle config, il controllo del sito e una batteria di sottomissioni che il verificatore deve accettare e deve rifiutare — un sorry, un native_decide, una sfida sconosciuta, un vantaggio zero, un corpo senza blocco Lean. workflow_dispatch verifica una sottomissione su richiesta senza aprire una issue.

submission.yml gestisce una issue verify: in due job. Il primo analizza input non fidato e non ha alcun permesso di scrittura; il secondo scarica il suo verdetto e pubblica il commento. Questa separazione è quella di lean-golf ed è il motivo per cui il corpo di una issue non può raggiungere un token.

Chi invia non scrive mai l'enunciato

Questo è l'intero meccanismo, ed è lo stesso che trailofbits/lean-golf usa per il proof golf. Il verificatore costruisce una propria copia di Challenge.lean. Una sottomissione fornisce 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

più budget e advantage nel modulo. attack e score vengono assemblati da quei numeri in Challenge.lean, quindi una sottomissione non può spendere un budget più grande di quello per cui viene valutata, né dimostrare un bound più debole di quello che dichiara — non perché lo controlliamo, ma perché non ha mai la penna in mano su nessuno dei due oggetti.

Quattro rifiuti che il verificatore emette senza leggere nulla:

Anche native_decide, maxHeartbeats e maxRecDepth vengono rifiutati: una dimostrazione che si chiude solo con un limite aumentato è una dimostrazione che il verificatore non può permettersi.

Punteggio

Niente è fissato in anticipo. Su uno schema che nessuno ha studiato, quale vantaggio sia raggiungibile a quale costo è la domanda di ricerca, quindi qualsiasi obiettivo è una congettura — e un obiettivo fissato troppo alto valuta un autentico distinguisher 2⁻³⁰ come zero. La bacheca misura invece il risultato:

score = log₂( budget / advantage^e )

Query per unità di vantaggio; il suo logaritmo in base due è il livello di sicurezza in bit che l'attacco confuta. Più basso è, meglio è. Sottostimare il proprio vantaggio alza il punteggio, quindi non c'è nulla da guadagnare dichiarando meno di quanto puoi dimostrare.

e è specifico per sfida e non ha un default. e = 2 per un gioco decisionale — un vantaggio α richiede circa α⁻² ripetizioni per essere amplificato — e e = 1 per uno orientato alla ricerca. Entrambe le convenzioni sono presenti in letteratura e l'inconsistenza è nota (Micciancio–Walter, On the Bit Security of Cryptographic Primitives), quindi ogni sfida dichiara quale usa.

Il par è l'affermazione del progettista stesso, presa dalla specifica, quindi da nessuna parte compare una congettura sulla difficoltà dell'attacco. Essere sotto il par è una rottura dell'affermazione.

La frontiera è il registro principale: un risultato vi entra quando nessun altro lo batte contemporaneamente sia in query sia in vantaggio. Il punteggio in bit è la colonna classificata accanto, e due lemmi verificati nel layer Lean (Score.workFactor_lt_of_dominates, Score.onFrontier_of_workFactor_min) garantiscono che la classifica non seppellisca mai un risultato che vince su entrambi gli assi.

Sfide

spoc128 — SpoC-128 come presentato a NIST LWC Round 2. Rotto: tre query, vantaggio 1, 1.58 bit. load key n mette il nonce nel rate e tagInput fa lo XOR di tagControl nello stesso rate, quindi tagInput (load key n) = load key (n ^^^ tagControl). Un input della permutazione è raggiungibile da due query e, poiché la permutazione è pubblica e invertibile, metà di esso trapela in un tag e metà in un blocco di ciphertext; combina, inverti, prendi la capacità, e quella è la chiave.

spoc128-ds — lo stesso modo con i quattro bit di controllo riservati nel nonce, quindi n ^^^ tagControl non è un nonce legale. Aperta: nessun attacco è noto. La restrizione vive nel tipo di una query, quindi l'attacco pubblicato qui non è semplicemente infruttuoso — non può proprio essere presentato come un avversario (SpoC128DS.attack_second_query_illegal).

Non è volutamente una seconda copia del modo. Irrobustire DDC.lean significherebbe un modello parallelo da tenere sincronizzato; restringere il dominio delle query è un solo predicato, e ogni teorema esistente sul modo continua a valere.

Niente qui afferma che la variante sia sicura. Chiudere una via pubblicata verso un modo non è un argomento per dire che non esista nessun'altra via — ed è questo il punto di pubblicarla.

Aggiungere una sfida

Fornisci un Golf.Game nel layer Lean — un tipo di parametro pubblico, un tipo per query e risposta, e i due mondi — poi un config.json qui. Il layer generico vive in RandomSystems/Golf/Game.lean; RandomSystems/Golf/Instances/SpoC128/ è l'esempio svolto, e funge anche da controllo che l'astrazione sia fedele: le sue ricevute di adeguatezza sono rfl e la sua sottomissione di riferimento è chiusa dall'esistente attack_distinguishing_advantage senza riformulazioni.

Cosa non viene valutato

• Lavoro offline, per scelta. L'avversario è un oggetto simbolico e la bacheca valuta la complessità di query, il contesto della teoria dell'informazione in cui già vivono l'indifferentiabilità e il lemma di switching PRP/PRF. Una sfida che richiede fattibilità computazionale deve dirlo e vincolare una forma che comporti un costo.
• Amplificazione si assume disponibile: q/α^e è il costo del ripetere un attacco fino alla confidenza.
• I pareggi non sono equivalenze. Lo stesso livello in bit può contenere risultati molto diversi, ed è per questo che la frontiera sta accanto alla classifica invece di esserne sostituita.