break-golf

実行されるのではなく、証明された暗号解析結果のためのボード。

チャレンジは、2つのワールドとあなたが証明しなければならないステートメントを固定する。あなたは、それらを区別する敵対者（adversary）と証明を書く。勝利は証明である。何も実行・サンプリング・再生はされず、また、それが有効かどうかを判断するために人間が提出物を読むこともない。

ステータス: 概念実証。 サイトは静的であり、提出はGitHub issueを開き、人間が判断する。背後にはまだ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 はpushおよびpull requestで実行される: --check ゲート、設定のlint、サイトチェック、そして検証器が受け入れなければならない/拒否しなければならない一連の提出物 — sorry、native_decide、未知のチャレンジ、ゼロアドバンテージ、Leanブロックを含まないボディ。workflow_dispatch は、issueを開かずにオンデマンドで1件の提出を検証する。

submission.yml は verify: issue を2つのジョブで処理する。最初のジョブは信頼できない入力を解析し、書き込みスコープを持たない。2番目のジョブはその判定をダウンロードしてコメントを投稿する。この分割はlean-golfのものであり、issueのボディがトークンに到達できない理由である。

提出者は決してステートメントを書かない

これが仕組みの全体であり、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 の中でそれらの数値から組み立てられる。したがって、提出物はスコア付けされる予算より大きな予算を使うことも、主張するより弱いバウンドを証明することもできない。それは私たちがチェックするからではなく、提出物がどちらのオブジェクトについても記述することが決してないからである。

検証器が何も読まずに行う4つの拒否:

native_decide、maxHeartbeats、maxRecDepth も拒否される。制限を引き上げて初めて閉じる証明は、検証器が負担できない証明である。

スコアリング

事前に固定されたものは何もない。誰も研究したことのないスキームでは、どのコストでどのアドバンテージが到達可能かが研究課題である。したがって、任意の目標は推測である — そして高すぎる目標は、本物の 2⁻³⁰ 識別子をゼロとスコア付けする。ボードは代わりに結果を測定する:

score = log₂( budget / advantage^e )

単位アドバンテージあたりのクエリ数。その底2の対数は、攻撃が反駁するビット単位のセキュリティ水準である。低いほど良い。自分のアドバンテージを過小報告するとスコアは 上がる。したがって、証明できる量より少なく主張しても得るものは何もない。

e はチャレンジごとに設定され、デフォルトはない。決定ゲームでは e = 2 — アドバンテージ α の増幅には約 α⁻² 回の繰り返しが必要 — であり、探索寄りのゲームでは e = 1 である。どちらの慣行も文献にあり、その不整合は知られている（Micciancio–Walter, On the Bit Security of Cryptographic Primitives）。したがって、チャレンジはどちらを使用するかを明記する。

パーは設計者自身の主張であり、仕様から取られる。したがって、攻撃の難しさに関する推測はどこにも現れない。パーを下回ることは、その主張を破ることを意味する。

フロンティアは主要な記録である。ある結果は、クエリ数とアドバンテージの両方で同時に他のどの結果にも上回られないとき、それに加わる。ビットスコアはその隣の順位付けされた列であり、Lean層の2つの検証済み補題（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)。1つの置換入力は2つのクエリで到達可能であり、置換は公開かつ可逆であるため、その半分はタグに漏れ、半分は暗号文ブロックに漏れる。結合し、逆変換し、キャパシティを取り出せば、それが鍵である。

spoc128-ds — ノンスに4つの制御ビットが予約されている同じモード。したがって、n ^^^ tagControl は合法なノンスではない。未解決: 既知の攻撃はない。 この制限はクエリの 型 に存在する。そのため、公表された攻撃はここでは単に成功しないだけでなく、そもそも敵対者として提示することすらできない（SpoC128DS.attack_second_query_illegal）。

これは意図的に、このモードの2番目のコピーではない。DDC.lean を強化することは、同期を保つ並行モデルを意味するだろう。クエリ領域を制限することは1つの述語であり、このモードに関する既存のすべての定理は依然として適用される。

ここにあるものは、この変種が安全であると主張しているわけではない。モードへの公表された経路を1つ塞いだことは、他の経路が存在しないという論拠にはならない — それがこれを公開するポイントである。

チャレンジの追加

Lean層に Golf.Game を提供する — 公開パラメータ型、クエリとレスポンスの型、そして2つのワールド — 次に、ここに config.json を置く。汎用層は RandomSystems/Golf/Game.lean にあり、RandomSystems/Golf/Instances/SpoC128/ は実例であり、抽象化が忠実であることを確認するチェックを兼ねている。その妥当性の証拠は rfl であり、その参照提出物は既存の attack_distinguishing_advantage によって再記述なしに証明される。

スコア対象外のもの

• オフライン作業は、設計判断として対象外。敵対者はシンボリックなオブジェクトであり、ボードは クエリ複雑性 をスコア付けする。これは、indifferentiability と PRP/PRF スイッチング補題がすでに存在する情報理論的な設定である。計算量的な実現可能性を必要とするチャレンジは、そのことを明言し、コストを伴う形式を固定しなければならない。
• 増幅（Amplification） は利用可能と想定される: q/α^e は、攻撃を確信度まで繰り返すためのコストである。
• 同点は等価ではない。 同じビット水準は非常に異なる結果を含み得る。だからこそ、フロンティアはランキングによって置き換えられるのではなく、その隣に置かれているのである。