«Когда говорят о формальной верификации протоколов, обычно вспоминают сложные инструменты вроде ProVerif или Tamarin. Но есть более старый, почти забытый подход — BAN-логика. Он не требует глубоких знаний математики, работает с убеждениями агентов и до сих пор помогает находить тонкие уязвимости, которые ускользают от автоматических анализаторов.»
Что такое BAN-логика и почему она появилась
BAN-логика, это формальная система для анализа протоколов аутентификации и распределения ключей. Её создали в конце 1980-х годов Майкл Берроуз, Мартин Абади и Роджер Нидхэм. Аббревиатура BAN образована от первых букв их фамилий.
В то время протоколы безопасности разрабатывались и проверялись в основном интуитивно. Разработчики полагались на словесные описания и неформальные рассуждения о доверии. Это часто приводило к ошибкам: протокол выглядел корректным, но содержал скрытые уязвимости, которые обнаруживались спустя годы. Классический пример — уязвимости в ранних версиях протокола Needham-Schroeder.
Авторы BAN-логики предложили перейти от описания процессов обмена сообщениями к анализу убеждений участников. Основная идея: протокол корректен, если в его конце участники приходят к определённым, заранее заданным убеждениям. Например, Алиса должна верить, что она общается именно с Бобом, и что сессионный ключ свежий и известен только им двоим.
Логика оперирует объектами нескольких типов:
- Принципалы (P, Q, R): участники протокола — люди, серверы, устройства.
- Ключи (K): симметричные или асимметричные ключи.
- Высказывания (X, Y): фрагменты данных, передаваемые в сообщениях.
- Формулы: выражения, описывающие убеждения и знания принципалов.
Базовые конструкции и правила вывода
Сила BAN-логики — в небольшом наборе интуитивно понятных конструкций и правил. Они позволяют шаг за шагом выводить новые убеждения из исходных посылок протокола.
Основные модальности (убеждения)
- P believes X: Принципал P верит, что X истинно. Это центральное понятие.
- P sees X: P получил сообщение, содержащее X, и может его прочитать.
- P said X: В какой-то момент P отправил сообщение, содержащее X. Это не означает, что он верит в X сейчас, лишь факт отправки.
- P controls X: P имеет полномочия по установлению истинности X (например, сервер управления ключами).
- fresh(X): X является «свежим», то есть не использовался в предыдущих сеансах протокола. Критично для защиты от replay-атак.
- P <–> Q: P и Q разделяют общий секретный ключ K.
- –> P: Открытый ключ принципала P.
Ключевые правила вывода
Правила позволяют делать логические выводы. Например:
- Правило сообщения-означающего (Message-Meaning Rule): Если P верит, что ключ K общий с Q, и P видит сообщение, зашифрованное этим ключом, то P может заключить, что Q когда-то сказал содержимое этого сообщения. Формально: P believes (P <–> Q), P sees {X}_K ⊢ P believes (Q said X).
- Правило проверки юрисдикции (Jurisdiction Rule): Если P верит, что Q контролирует X, и P верит, что Q верит в X, то P тоже начинает верить в X. P believes (Q controls X), P believes (Q believes X) ⊢ P believes X.
- Правило свежести (Freshness Rule): Если часть сообщения свежа, то всё сообщение считается свежим. P believes fresh(X) ⊢ P believes fresh(X, Y).
- Правило неспецификации (Nonce-Verification Rule): Если P верит, что X свежо, и что Q сказал X, то P верит, что Q верит в X. P believes fresh(X), P believes (Q said X) ⊢ P believes (Q believes X). Это правило критично для установления актуальности убеждений.
Как работает анализ протокола: шаг за шагом
Анализ протокола с помощью BAN-логики, это формализованная процедура.
- Идеализация. Текст протокола переводится в последовательность формул BAN-логики. Это самый тонкий момент: нужно корректно интерпретировать намерения разработчика. Например, не каждое переданное число является nonce (свежим числом), а только то, которое задумано для обеспечения свежести.
- Определение начальных убеждений (assumptions). Записываются исходные условия: кто каким ключам доверяет, кто контролирует какие параметры. Например: «Алиса верит, что она разделяет секретный ключ с сервером».
- Применение правил вывода. Для каждого шага протокола анализируется, как полученное сообщение меняет убеждения участников. Применяются правила, описанные выше.
- Проверка целей (goals). В конце проверяется, достигнуты ли целевые убеждения, ради которых протокол создавался. Например: «Алиса верит, что сессионный ключ свежий и общий с Бобом».
Если, применяя правила к идеализированному протоколу и начальным убеждениям, мы не можем вывести целевые убеждения — в протоколе есть изъян. Возможно, не хватает какого-то сообщения для передачи свежести или неверно распределены полномочия.
Классический пример: поиск уязвимости в протоколе Needham-Schroeder
Именно анализ с помощью BAN-логики позволил обнаружить известную атаку на протокол Нидхэма-Шрёдера, о которой сами авторы протокола не подозревали 17 лет.
Упрощённая схема протокола (симметричный вариант):
- A → S: A, B, Na
- S → A: {Na, B, Kab, {Kab, A}_Kbs}_Kas
- A → B: {Kab, A}_Kbs
- B → A: {Nb}_Kab
- A → B: {Nb-1}_Kab
Где S — сервер, Kab — сессионный ключ между A и B, Na, Nb — nonce.
Формальный анализ показал, что после выполнения протокола у Алисы (A) не возникает убеждения B believes Kab. Она знает ключ, но у неё нет формальных оснований полагать, что Боб его тоже знает и верит в его связь с Алисой. Эта логическая брешь и была использована в атаке типа «man-in-the-middle». Злоумышленник мог заставить Боба поверить, что он устанавливает сессию со злоумышленником, а не с Алисой.
Этот пример наглядно показывает силу подхода: неформально протокол выглядел работоспособным, но формальный анализ убеждений выявил фундаментальный недостаток в распределении доверия.
Ограничения классической BAN-логики
Несмотря на элегантность, у исходной логики есть ряд ограничений, которые не позволяют анализировать современные сложные протоколы.
- Отсутствие временной логики. Понятие «сказал» (said) не привязано ко времени. Невозможно выразить «сказал в течение текущего сеанса».
- Нет моделирования действий злоумышленника. Логика анализирует честное выполнение протокола. Она может показать, что цели не достижимы, но не моделирует активного противника, который перехватывает, подменяет и генерирует сообщения.
- Проблема идеализации. Перевод реального протокола в формулы — творческий процесс. Разная идеализация может привести к разным выводам. Критики называли это «искусством».
- Только аутентификация. Логика плохо приспособлена для анализа свойств вроде конфиденциальности данных или устойчивости к DoS.
- Статичность. Не учитывается динамическое создание новых принципалов или ключей в ходе выполнения.
Расширения и модификации BAN-логики
Чтобы преодолеть эти ограничения, исследователи предложили десятки расширений. Некоторые из них стали стандартными инструментами в своей нише.
GNY-логика (Gong, Needham, Yahalom)
Одно из первых и наиболее значимых расширений. GNY вводит важные усовершенствования:
- Явное различие между получением данных и возможностью их прочесть (possesses). Принципал может получить зашифрованный блок, но не обладать ключом для его расшифровки.
- Более строгие правила для работы с составными сообщениями, что снижает субъективность при идеализации.
- Вводится понятие «распознавания» (recognizable) данных, что важно для защиты от подмены.
Логика SVO (Syverson, van Oorschot)
SVO, это попытка создать унифицированный и более строгий формализм. Она включает в себя элементы BAN, GNY и других логик как частные случаи. SVO использует минимальный набор аксиом и модальных операторов, что делает её более последовательной для компьютерной реализации. Многие современные расширения основываются на принципах SVO.
Временные расширения
Для анализа протоколов с временными метками или ограниченным временем жизни ключей были созданы расширения, добавляющие временные операторы: P believes X at time T, fresh(X, T). Это позволяет обнаруживать уязвимости, связанные с задержкой сообщений или использованием просроченных сертификатов.
Логики для групповых протоколов
Классическая BAN-логика работает с парными взаимодействиями. Для анализа протоколов групповой аутентификации и многостороннего доверия (например, для конференц-связи или блокчейн-консенсуса) были разработаны специализированные расширения. Они вводят операторы вида group_key(G, K) и правила для вывода убеждений о членстве в группе.
BAN-логика сегодня: нишевый, но живой инструмент
Сегодня BAN-логика не является основным инструментом для промышленной верификации. Её место заняли более мощные автоматизированные средства, такие как ProVerif (основанный на исчислении процессов) или Tamarin (работающий с правилами переписывания и временной логикой). Эти инструменты могут автоматически моделировать активного злоумышленника и доказывать свойства безопасности для неограниченного числа сеансов.
Однако BAN-логика не умерла. Она находит применение в других областях:
- Образовательный инструмент. Это, пожалуй, её главная роль сегодня. BAN-логика — идеальный способ научиться мыслить в терминах формальных убеждений и доверия. Она наглядно показывает, как из небольших аксиом строятся сложные выводы о безопасности протокола.
- Быстрый эскизный анализ. На ранних стадиях проектирования протокола, когда писать спецификацию для Tamarin ещё рано, можно быстро набросать его идеализацию в BAN-логике. Это помогает отсеять очевидно порочные конструкции.
- Анализ человеко-машинных интерфейсов. Некоторые исследователи адаптируют идеи BAN-логики для анализа протоколов, где одним из принципалов является человек. Можно формализовать, во что должен верить пользователь после нажатия кнопки «Подтвердить» в интерфейсе.
- Базис для специализированных логик. Принцип работы с убеждениями живёт в новых областях. Например, в анализе протоколов для интернета вещих или смарт-контрактов иногда создают кастомные логики, вдохновлённые BAN.
Заключение: между интуицией и формализмом
BAN-логика занимает уникальное место на стыке интуитивного понимания протоколов и строгого формального анализа. Она не даёт абсолютных гарантий, как современные автоматические верификаторы, но зато требует от аналитика глубокого проникновения в суть протокола — его цели, распределение доверия и предполагаемые убеждения участников.
Изучение BAN-логики и её расширений, это не столько про освоение устаревшего инструмента, сколько про тренировку особого типа мышления. Это мышление, которое заставляет видеть за потоком байтов в сетевом пакете — эволюцию убеждений агентов, за обменом nonce — установление свежести, а за шифрованием на ключе — акт доверия к отправителю. Такой взгляд остаётся ценным даже при использовании самых современных средств автоматической верификации.