break-golf

Доска результатов криптоанализа, которые доказаны, а не запущены.

Задача фиксирует два мира и утверждение, которое нужно доказать. Вы пишете противника и доказательство того, что он их различает. Выигрыш — это доказательство: ничего не исполняется, не сэмплируется и не повторяется, и ни один человек не читает посылку, чтобы решить, засчитывается ли она.

Статус: proof-of-concept. Сайт статический, посылки открывают issue на 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 запускается на push и pull request: проверки --check, линтер конфигов, проверка сайта и набор посылок, которые верификатор обязан принять и обязан отклонить, — sorry, native_decide, неизвестную задачу, нулевое преимущество, тело без Lean-блока. workflow_dispatch верифицирует одну посылку по запросу, не открывая issue.

submission.yml обрабатывает issue verify: в двух заданиях. Первое разбирает недоверенный ввод и не имеет никаких прав на запись; второе загружает его вердикт и публикует комментарий. Это разделение — из lean-golf, и именно поэтому тело issue не может добраться до токена.

Участник никогда не пишет утверждение

Это весь механизм, и он тот же, что trailofbits/lean-golf использует для proof 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⁻³⁰ как ноль. Вместо этого доска измеряет результат:

score = log₂( budget / advantage^e )

Запросы на единицу преимущества; логарифм по основанию два от этого — уровень безопасности в битах, который опровергает атака. Меньше — лучше. Занижение своего преимущества повышает балл, поэтому нет никакой выгоды заявлять меньше, чем вы можете доказать.

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 — SpoC-128 в том виде, в котором он был подан на NIST LWC Round 2. Взломан: три запроса, преимущество 1, 1.58 бита. load key n помещает nonce в rate, а tagInput XORит tagControl в тот же rate, поэтому tagInput (load key n) = load key (n ^^^ tagControl). Один вход перестановки достижим двумя запросами, а поскольку перестановка открыта и обратима, половина её утекает в тег, а половина — в блок шифртекста; соедините, инвертируйте, возьмите capacity — и это ключ.

spoc128-ds — тот же режим, но четыре управляющих бита зарезервированы в nonce, поэтому n ^^^ tagControl не является допустимым nonce. Открыто: неизвестно ни одной атаки. Ограничение живёт в типе запроса, так что опубликованная атака здесь не просто безуспешна — её вообще нельзя представить как противника (SpoC128DS.attack_second_query_illegal).

Это намеренно не вторая копия режима. Ужесточение DDC.lean означало бы параллельную модель, которую нужно синхронизировать; ограничение области запросов — это один предикат, и все существующие теоремы о режиме по-прежнему применимы.

Ничто здесь не утверждает, что вариант безопасен. Закрытие одного опубликованного пути в режим — не аргумент в пользу того, что не существует другого пути, — в этом и смысл размещения.

Добавление задачи

Предоставьте Golf.Game в Lean-слое — открытый тип параметров, тип запроса и ответа и два мира, — а затем config.json здесь. Обобщённый слой находится в RandomSystems/Golf/Game.lean; RandomSystems/Golf/Instances/SpoC128/ — проработанный пример, который также служит проверкой того, что абстракция точна: её свидетельства адекватности — это rfl, а её эталонная посылка закрывается существующим attack_distinguishing_advantage без переформулировки.

Что это не оценивает

• Офлайн-работа — по решению. Противник — символический объект, и доска оценивает query complexity — информационно-теоретическую постановку, в которой уже живут indifferentiability и switching-лемма PRP/PRF. Задача, требующая вычислительной выполнимости, должна явно об этом сказать и зафиксировать форму, несущую стоимость.
• Усиление предполагается доступным: q/α^e — это стоимость повторения атаки до достижения уверенности.
• Совпадения — это не эквивалентности. Один и тот же битовый уровень может содержать очень разные результаты, поэтому фронтир расположен рядом с ранжированием, а не заменяется им.