break-golf

실행이 아니라 증명된 암호분석 결과를 위한 보드.

챌린지는 두 세계와 당신이 증명해야 할 명제를 고정한다. 당신은 적대자와 그것이 그 두 세계를 구별한다는 증명을 작성한다. 승리는 증명이다: 아무것도 실행되거나, 샘플링되거나, 재실행되지 않으며, 제출물이 유효한지 판단하기 위해 어떤 사람도 읽지 않는다.

상태: 개념 증명. 사이트는 정적이며, 제출물은 GitHub 이슈를 열고, 사람이 판정한다. 아직 그 뒤에는 Lean 검증기가 없다.

구성

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은 푸시와 풀 리퀘스트에서 실행된다: --check 게이트, 설정 린트, 사이트 점검, 그리고 검증기가 반드시 받아들여야 하고 반드시 거부해야 하는 일련의 제출물들 — sorry, native_decide, 알 수 없는 챌린지, 이점이 0인 경우, Lean 블록이 없는 본문. workflow_dispatch는 이슈를 열지 않고 요청 시 제출물 하나를 검증한다.

submission.yml은 verify: 이슈를 두 작업으로 처리한다. 첫 번째는 신뢰할 수 없는 입력을 파싱하며 쓰기 권한 범위가 없다; 두 번째는 판정을 내려받아 코멘트를 게시한다. 그 분리는 lean-golf의 방식이며, 이슈 본문이 토큰에 닿을 수 없는 이유다.

제출자는 명제를 결코 작성하지 않는다

이것이 메커니즘의 전부이며, trailofbits/lean-golf가 증명 골프에 사용하는 것과 동일하다. 검증기는 Challenge.lean의 자체 사본을 만든다. 제출물은 다음만 제공한다:

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

여기에 폼의 budget과 advantage가 더해진다. attack과 score는 Challenge.lean에서 그 숫자들로 조립되므로, 제출물은 점수가 매겨진 것보다 더 큰 예산을 쓸 수 없고, 주장하는 것보다 더 약한 경계를 증명할 수도 없다 — 우리가 확인하기 때문이 아니라, 두 객체 중 어느 것도 제출물이 직접 작성하지 않기 때문이다.

검증기가 아무것도 읽지 않고 내리는 네 가지 거부:

native_decide, maxHeartbeats 및 maxRecDepth도 거부된다: 한계를 올려야만 닫히는 증명은 검증기가 감당할 수 없는 증명이다.

점수 산정

미리 정해진 것은 없다. 아무도 연구하지 않은 방식에서 어떤 비용으로 어떤 이점에 도달할 수 있는지가 연구 질문이므로, 어떤 목표든 추측이다 — 그리고 너무 높게 잡은 목표는 진짜 2⁻³⁰ 구별자를 0점으로 매긴다. 보드는 대신 결과를 측정한다:

score = log₂( budget / advantage^e )

단위 이점당 쿼리 수; 이 값의 밑 2 로그는 공격이 반박하는 비트 단위 보안 수준이다. 낮을수록 좋다. 이점을 과소 기재하면 점수가 올라가므로, 증명할 수 있는 것보다 적게 주장해서 얻을 것이 없다.

e는 챌린지마다 정해지며 기본값이 없다. 결정 게임에는 e = 2 — 이점 α는 증폭에 약 α⁻²회의 반복이 필요하다 — 탐색 성향 게임에는 e = 1이다. 두 관례 모두 문헌에 있으며 그 불일치도 알려져 있다(Micciancio–Walter, On the Bit Security of Cryptographic Primitives). 그래서 각 챌린지는 어느 것을 사용하는지 명시한다.

파는 설계자 자신의 주장이다. 명세에서 가져온 것이므로 공격 난이도에 대한 추측이 어디에도 나타나지 않는다. 파 미만이면 그 주장이 깨진 것이다.

프런티어가 기본 기록이다: 다른 어떤 결과도 쿼리와 이점 양쪽에서 동시에 이기지 못할 때 그 결과가 합류한다. 비트 점수는 그 옆의 순위 열이며, Lean 계층의 두 검증된 보조정리(Score.workFactor_lt_of_dominates, Score.onFrontier_of_workFactor_min)는 순위가 두 축 모두에서 이기는 결과를 결코 묻어버리지 않음을 보장한다.

챌린지

spoc128 — NIST LWC 2라운드에 제출된 SpoC-128. 깨졌다: 쿼리 3회, 이점 1, 1.58비트. load key n은 논스를 레이트에 넣고 tagInput은 tagControl을 같은 레이트에 XOR하므로, tagInput (load key n) = load key (n ^^^ tagControl)이다. 하나의 순열 입력이 두 쿼리로 도달 가능하며, 순열이 공개적이고 가역적이므로 그것의 절반은 태그로, 절반은 암호문 블록으로 새어 나간다; 합치고, 역산하고, 캐퍼시티를 취하면 그것이 키가 된다.

spoc128-ds — 동일한 모드이지만 네 개의 제어 비트가 논스에 예약되어 있어 n ^^^ tagControl은 유효한 논스가 아니다. 미해결: 알려진 공격이 없다. 제한은 쿼리의 타입에 있으므로, 발표된 공격은 여기서 단순히 실패하는 것이 아니다 — 애초에 적대자로 제시될 수조차 없다(SpoC128DS.attack_second_query_illegal).

이것은 의도적으로 모드의 두 번째 사본이 아니다. DDC.lean을 강화하는 것은 동기화를 유지해야 하는 병렬 모델을 의미할 것이다; 쿼리 도메인을 제한하는 것은 술어 하나일 뿐이며, 모드에 대한 모든 기존 정리는 여전히 적용된다.

여기의 어떤 것도 이 변형이 안전하다고 주장하지 않는다. 모드로 통하는 발표된 경로 하나를 막는 것은 다른 경로가 존재하지 않는다는 논증이 아니다 — 그것이 이 변형을 올려 둔 이유다.

챌린지 추가하기

Lean 계층에 Golf.Game을 제공하라 — 공개 매개변수 타입, 쿼리와 응답 타입, 그리고 두 세계 — 그런 다음 여기에 config.json을 둔다. 일반 계층은 RandomSystems/Golf/Game.lean에 있고, RandomSystems/Golf/Instances/SpoC128/이 구체적 예제이며, 추상화가 충실한지 확인하는 역할도 겸한다: 그 적절성 증명들은 rfl이고, 참조 제출물은 기존의 attack_distinguishing_advantage로 재기술 없이 해소된다.

점수로 매기지 않는 것

• 오프라인 작업, 의도적 결정이다. 적대자는 기호 객체이며 보드는 쿼리 복잡도를 점수로 매긴다 — 무차별성과 PRP/PRF 스위칭 보조정리가 이미 속해 있는 정보이론적 설정이다. 계산적 실현 가능성이 필요한 챌린지는 그렇게 명시하고 비용을 수반하는 형태를 고정해야 한다.
• 증폭은 가능하다고 가정한다: q/α^e는 공격을 신뢰 수준까지 반복하는 비용이다.
• 동률은 동등이 아니다. 같은 비트 수준은 매우 다른 결과들을 품을 수 있으며, 그래서 프런티어는 순위로 대체되지 않고 순위 옆에 자리한다.