break-golf

Um quadro para resultados de criptoanálise que são provados, não executados.

Um desafio fixa dois mundos e o enunciado que você deve provar. Você escreve um adversário e uma prova de que ele os distingue. A vitória é a prova: nada é executado, amostrado ou reproduzido, e nenhum humano lê a submissão para decidir se ela conta.

Status: prova de conceito. O site é estático, submissões abrem uma issue no GitHub e um humano decide. Ainda não há um verificador Lean por trás disso.

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 roda em push e pull request: as verificações --check, o lint da configuração, a verificação do site e uma bateria de submissões que o verificador deve aceitar e deve rejeitar — um sorry, um native_decide, um desafio desconhecido, uma vantagem zero, um corpo sem bloco Lean. workflow_dispatch verifica uma submissão sob demanda sem abrir uma issue.

submission.yml trata de uma issue verify: em dois jobs. O primeiro analisa entrada não confiável e não detém nenhum escopo de escrita; o segundo baixa o veredito e publica o comentário. Essa divisão é a do lean-golf e é a razão pela qual o corpo de uma issue não consegue alcançar um token.

O submissor nunca escreve o enunciado

Este é o mecanismo inteiro, e é o mesmo que trailofbits/lean-golf usa para golfe de provas. O verificador constrói a sua própria cópia de Challenge.lean. Uma submissão fornece apenas:

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

mais budget e advantage no formulário. attack e score são montados a partir desses números em Challenge.lean, então uma submissão não pode gastar um orçamento maior do que aquele pelo qual é pontuada, nem provar um limite mais fraco do que afirma — não porque nós verificamos, mas porque ela nunca segura a caneta sobre nenhum dos dois objetos.

Quatro rejeições que um verificador faz sem ler nada:

native_decide, maxHeartbeats e maxRecDepth também são rejeitados: uma prova que só se conclui com um limite elevado é uma prova que o verificador não pode bancar.

Pontuação

Nada é fixado antecipadamente. Em um esquema que ninguém estudou, qual vantagem é alcançável a que custo é a questão de pesquisa, então qualquer alvo é um palpite — e um alvo definido alto demais pontua um distinguidor genuíno de 2⁻³⁰ como zero. O quadro mede o resultado em vez disso:

score = log₂( budget / advantage^e )

Consultas por unidade de vantagem; seu logaritmo na base dois é o nível de segurança em bits que o ataque refuta. Menor é melhor. Subestimar sua vantagem aumenta a pontuação, então não há nada a ganhar ao afirmar menos do que você consegue provar.

e é por desafio e não tem valor padrão. e = 2 para um jogo de decisão — uma vantagem α precisa de cerca de α⁻² repetições para ser amplificada — e e = 1 para um com sabor de busca. Ambas as convenções estão na literatura e a inconsistência é conhecida (Micciancio–Walter, On the Bit Security of Cryptographic Primitives), então um desafio declara qual delas usa.

Par é a afirmação do próprio projetista, tirada da especificação, então nenhum palpite sobre a dificuldade do ataque aparece em lugar nenhum. Ficar abaixo do par é uma quebra da afirmação.

A fronteira é o registro principal: um resultado entra nela quando nada mais o supera tanto em consultas quanto em vantagem ao mesmo tempo. A pontuação em bits é a coluna ranqueada ao lado dela, e dois lemas verificados na camada Lean (Score.workFactor_lt_of_dominates, Score.onFrontier_of_workFactor_min) garantem que o ranking nunca enterra um resultado que vence nos dois eixos.

Desafios

spoc128 — SpoC-128 como submetido ao NIST LWC Round 2. Quebrado: três consultas, vantagem 1, 1,58 bits. load key n coloca o nonce na taxa e tagInput faz XOR de tagControl na mesma taxa, então tagInput (load key n) = load key (n ^^^ tagControl). Uma entrada da permutação é alcançável por duas consultas e, como a permutação é pública e invertível, metade dela vaza em um tag e metade em um bloco de texto cifrado; junte, inverta, pegue a capacidade, e essa é a chave.

spoc128-ds — o mesmo modo com os quatro bits de controle reservados no nonce, então n ^^^ tagControl não é um nonce válido. Em aberto: nenhum ataque é conhecido. A restrição vive no tipo de uma consulta, então o ataque publicado não é meramente malsucedido aqui — ele não pode ser apresentado como adversário de forma alguma (SpoC128DS.attack_second_query_illegal).

Isto não é, deliberadamente, uma segunda cópia do modo. Blindar DDC.lean significaria um modelo paralelo para manter em sincronia; restringir o domínio de consulta é um predicado, e todo teorema existente sobre o modo ainda se aplica.

Nada aqui afirma que a variante é segura. Fechar uma rota publicada para um modo não é um argumento de que nenhuma outra rota existe — esse é o ponto de colocá-la no quadro.

Adicionando um desafio

Forneça um Golf.Game na camada Lean — um tipo de parâmetro público, um tipo de consulta e resposta, e os dois mundos — depois um config.json aqui. A camada genérica vive em RandomSystems/Golf/Game.lean; RandomSystems/Golf/Instances/SpoC128/ é o exemplo trabalhado e também serve como a verificação de que a abstração é fiel: seus comprovantes de adequação são rfl e sua submissão de referência é descarregada pelo attack_distinguishing_advantage existente, sem reformulação.

O que isto não pontua

• Trabalho offline, por decisão. O adversário é um objeto simbólico e o quadro pontua complexidade de consultas, o cenário da teoria da informação em que a indiferenciabilidade e o lema de troca PRP/PRF já habitam. Um desafio que precise de viabilidade computacional deve dizer isso e fixar uma forma que carregue custo.
• Amplificação é assumida como disponível: q/α^e é o custo de repetir um ataque até obter confiança.
• Empates não são equivalências. O mesmo nível de bits pode conter resultados muito diferentes, e é por isso que a fronteira fica ao lado do ranking em vez de ser substituída por ele.