Почему неформальных доказательств недостаточно

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

Протокол Needham-Schroeder (1978) был разработан для взаимной аутентификации. В 1995 году Gavin Lowe обнаружил атаку посредника с помощью автоматизированной проверки — через 17 лет после публикации. В неформальном доказательстве не была замечена тонкая атака с повторной передачей.

WEP был одобрен IEEE в 1997 году на основании неформальных заявлений о безопасности. К 2001 году исследователи обнаружили повторное использование потока ключей RC4, коллизии векторов инициализации и отсутствие целостности — протокол удалось взломать за считанные минуты. Неформальные рассуждения не выявили ни одной из этих проблем.

Безопасность протокола зависит от взаимодействия множества параллельных сеансов, активных злоумышленников и криптографических предположений. Человеку трудно рассуждать о взрывном росте числа состояний и чередующихся параллельных выполнениях.

Формальные методы математически моделируют протокол и доказывают или опровергают свойства безопасности (секретность, аутентификацию, совершенную прямую секретность) для всех возможных стратегий злоумышленника, а не только для тех, которые рассматривал разработчик.

Символьная модель (Dolev-Yao): криптография — идеальный чёрный ящик, внимание сосредоточено на логике протокола. Вычислительная модель: реальные вероятностные игры безопасности, более близкие к гарантиям в реальном мире. Обе модели выявляют реальные ошибки.

POODLE (2014) использовала оракул дополнения в CBC-режиме SSL 3.0. Уязвимость была недостатком проектирования на уровне протокола, а не ошибкой реализации. Формальный анализ спецификации SSL 3.0 выявил бы наличие оракула до развёртывания протокола.

TLS 1.3 (RFC 8446) разрабатывался одновременно с формальным анализом с использованием ProVerif и miTLS. Спецификация дорабатывалась с учётом результатов формального анализа — это важная веха во внедрении формальных методов органами стандартизации.

Формальные инструменты проверяют модель протокола, а не реализацию. Даже формально проверенный протокол может иметь небезопасную реализацию. F* / HACL* расширяет проверку на сам криптографический код.

Формальная проверка требует больших затрат: моделирование протокола занимает недели и требует специальных знаний. Но для критически важных целей (TLS, SSH, Signal) эти затраты оправданы — один недостаток протокола может затронуть миллиарды пользователей.

Почему открытие Лоу, сделанное в 1995 году, о существовании атаки на Needham-Schroeder имело большое значение?

Неформальные доказательства терпят неудачу, потому что человеческое рассуждение не учитывает взаимодействия параллельных сеансов и стратегии злоумышленника. Для Needham-Schroeder, WEP и POODLE существовали неформальные обоснования безопасности. TLS 1.3 включал формальный анализ уже на этапе проектирования. Формальные инструменты выявляют ошибки протокола до его развёртывания.