Логика Бэрроуза — Абади — Нидхэма

Логика Бэрроуза — Абади — Нидхэма (англ. Burrows-Abadi-Needham logic) или BAN-логика (англ. BAN logic) — это формальная логическая модель для анализа знания и доверия, широко используемая при анализе протоколов аутентификации.

Основная идея BAN-логики состоит в том, что при анализе подобных протоколов в первую очередь следует обратить внимание на то, как стороны, участвующие в процессе аутентификации, воспринимают информацию — что они принимают на веру, а что доподлинно им известно или может быть выведено логическим путём из достоверных для них фактов.

Обычно протоколы аутентификации описываются путём последовательного перечисления сообщений, передаваемых между участниками протокола. На каждом шаге описывается содержимое сообщения, а также указывается его отправитель и получатель. BAN-логика рассматривает подлинность сообщения как функцию от его целостности и новизны, используя логические правила для отслеживания состояния этих атрибутов на протяжении всего протокола.

В BAN-логике существует три типа объектов: участники, ключи шифрования и формулы, их связывающие. При формальном анализе протокола каждое сообщение преобразуется в логическую формулу; затем логические формулы связываются утверждениями. Тем самым, BAN-логика во многом схожа с логикой Хоара. Единственной логической операцией, применяемой в данной логике, является конъюнкция. Также вводятся различные предикаты, например, устанавливающие отношения между участниками и высказываниями (отношение доверия, юрисдикции и т. д.) или выражающие какие-либо свойства высказываний (таких, как свежесть, то есть утверждение, что высказывание получено недавно).

Как и любая формальная логика, BAN-логика снабжена аксиомами и правилами вывода. Формальный анализ протокола состоит в доказательстве некоторого набора утверждений, выраженного формулами BAN-логики, с помощью правил вывода. Например, минимальное требование к любому протоколу аутенификации состоит в следующем: оба участника должны поверить в то, что они нашли секретный ключ для обмена информацией друг с другом.

Основные предикаты и их обозначения

• $P|\equiv X$ означает, что $P$ верит в высказывание $X$. Это значит, что $P$ станет действовать так, как будто $X$ — истинная информация.
• $P\vartriangleleft X$ подразумевает, что $P$ видит $X$, то есть $P$ принял сообщение, в котором содержится $X$. То есть $P$ может прочитать и воспроизвести (возможно, после процедуры расшифрования) сообщение $X$.
• $P|\sim X$ означает, что $P$ однажды высказал $X$, то есть в какой-то момент времени $P$ послал сообщение, содержащее $X$.
• $P|\Rightarrow X$ означает, что $X$ входит в юрисдикцию $P$ (или $P$ имеет юрисдикцию над $X$), то есть $P$ обладает авторитетом по вопросу относительно $X$.
• $\#X$ означает, что высказывание $X$ получено недавно. То есть сообщение $X$ не было послано когда-то в прошлом (до момента запуска протокола).
• $P{\stackrel {k}{\longleftrightarrow }}Q$ означает, что $P$ и $Q$ используют для общения разделенный ключ $k$.
• $\lbrace X\rbrace _{k}$ подразумевает, что данные $X$ зашифрованы ключом $k$.

Другие обозначения

Операция конъюнкции обозначается запятой, а логическое следование — горизонтальной чертой. Таким образом, логическое правило $A\wedge B\Rightarrow C$ в обозначениях BAN-логики записывается как ${\dfrac {A,B}{C}}$

Аксиомы BAN-логики

1. Время делится на две эпохи: прошлое и настоящее. Настоящее начинается с момента запуска протокола.
2. Участник $P$, высказывающий $X$, верит в истинность $X$.
3. Шифрование считается абсолютно надежным: зашифрованное сообщение не может быть расшифровано участником, не знающим ключа.

Правила вывода

• Правило о значении сообщения:

${\dfrac {A|\equiv A{\stackrel {K}{\longleftrightarrow }}B,A\vartriangleleft \lbrace X\rbrace _{K}}{A|\equiv B|\sim X}}$

Эквивалентная словесная формулировка: из предположений о том, что $A$ верит в совместное использование ключа $K$ с $B$, и $A$ видит сообщение $X$, зашифрованное ключом $K$, следует, что $A$ верит, что $B$ в какой-то момент высказал $X$.

Заметим, что здесь неявно предполагается, что сам $A$ никогда не высказывал $X$.

• Правило проверки уникальности числовых вставок:

${\dfrac {A|\equiv \#X,A|\equiv B|\sim X}{A|\equiv B|\equiv X}}$

то есть если $A$ верит в новизну $X$ и в то, что $B$ когда-то высказал $X$, то $A$ верит, что $B$ по-прежнему доверяет $X$.

• Правило юрисдикции:

${\dfrac {A|\equiv B|\Rightarrow X,A|\equiv B|\equiv X}{A|\equiv X}}$

утверждает, что если $A$ верит в полномочия $B$ относительно $X$, и $A$ верит в то, что $B$ верит в $X$, то $A$ должен верить в $X$.

• Другие правила

Оператор доверия и конъюнкция подчиняются следующим соотношениям:

${\dfrac {A|\equiv X,A|\equiv Y}{A|\equiv (X,Y)}}$

${\dfrac {A|\equiv (X,Y)}{A|\equiv X}}$

${\dfrac {A|\equiv B|\equiv (X,Y)}{A|\equiv B|\equiv X}}$

По сути, данные правила устанавливают следующее требование: $A$ доверяет какому-то набору утверждений тогда и только тогда, когда $A$ доверяет каждому утверждению по отдельности.

Аналогичное правило существует для оператора $|\sim$:

${\dfrac {A|\equiv B|\sim (X,Y)}{A|\equiv B|\sim X}}$

Следует заметить, что из $A|\equiv B|\sim X$ и $A|\equiv B|\sim Y$ не следует $A|\equiv B|\sim (X,Y)$, поскольку $X$ и $Y$ могли быть высказаны в разные моменты времени.

Наконец, если какая-то часть высказывания получена недавно, то это же можно утверждать и про все высказывание целиком:

${\dfrac {A|\equiv \#X}{A|\equiv \#(X,Y)}}$

Формальный подход к анализу протоколов аутентификации

С практической точки зрения, анализ протокола осуществляется следующим образом:

• Исходный протокол преобразуется в идеализованный (то есть записанный в терминах BAN-логики).
• Добавляются предположения о начальном состоянии протокола.
• С каждым высказыванием связывается логическая формула, то есть логическое утверждение о состоянии протокола после каждого высказывания.
• К предположениям и утверждениям протокола применяются правила вывода и аксиомы для того, чтобы определить состояние доверия сторон по завершении работы протокола.

Поясним смысл данной процедуры. Первый шаг носит название идеализации и состоит в следующем: каждый шаг протокола, записанный в виде $P\longrightarrow Q:message$, преобразуется в набор логических утверждений, касающихся передающей и принимающей стороны. Пусть, например, один из шагов протокола выглядит следующим образом:

$A\longrightarrow B:\lbrace A,K_{ab}\rbrace _{K_{bs}}$

Это сообщение говорит участнику $B$ (обладающему ключом $K_{bs}$), что ключ $K_{ab}$ должен быть использован для сообщения с $A$. Соответствующая логическая формула для данного сообщения имеет вид:

$A\longrightarrow B:\lbrace A{\stackrel {K_{ab}}{\longleftrightarrow }}B\rbrace _{K_{bs}}$

Когда данное сообщение доставляется $B$, справедливо утверждение:

$B\vartriangleleft \lbrace A{\stackrel {K_{ab}}{\longleftrightarrow }}B\rbrace _{K_{bs}}$

то есть $B$ видит данное сообщение и в дальнейшем будет действовать в соответствии с ним.

После идеализации протокол выглядит как последовательность высказываний и утверждений, связывающих эти высказывания. Начальное утверждение состоит из исходных предположений протокола, конечное утверждение — результат работы протокола:

$[assumptions]S_{1}[assertion1]\cdots [assertion(n-1)]S_{n}[conclusions]$

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

Цели протоколов аутентификации

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

$A|\equiv A{\stackrel {K}{\longleftrightarrow }}B$ и $B|\equiv A{\stackrel {K}{\longleftrightarrow }}B$

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

$A|\equiv B|\equiv A{\stackrel {K}{\longleftrightarrow }}B$ и $B|\equiv A|\equiv A{\stackrel {K}{\longleftrightarrow }}B$

то есть подтверждения приема ключа.

Анализ протокола широкоротой лягушки с помощью BAN-логики

Рассмотрим простой протокол аутентификации — протокол широкоротой лягушки — который позволяет двум сторонам, $A$ и $B$, установить защищённое соединение, используя сервер $S$, которому они оба доверяют, и синхронизированные часы. В стандартных обозначениях протокол записывается следующим образом:

$A\rightarrow S:A,\{T_{A},K_{ab},B\}_{K_{as}}$

$S\rightarrow B:\{T_{S},K_{ab},A\}_{K_{bs}}$

После идеализации шаги протокола приобретают вид:

$A\rightarrow S:\{T_{A},A{\stackrel {K_{ab}}{\longleftrightarrow }}B\}_{K_{as}}$

$S\rightarrow B:\{T_{S},A|\equiv A{\stackrel {K_{ab}}{\longleftrightarrow }}B\}_{K_{bs}}$

Запишем исходные предположения протокола. Стороны $A$ и $B$ обладают ключами $K_{as}$ и $K_{bs}$ соответственно, для защищённой связи с сервером $S$, что на языке BAN-логики может быть выражено как:

$A|\equiv A{\stackrel {K_{as}}{\longleftrightarrow }}S$

$S|\equiv A{\stackrel {K_{as}}{\longleftrightarrow }}S$

$B|\equiv B{\stackrel {K_{bs}}{\longleftrightarrow }}S$

$S|\equiv B{\stackrel {K_{bs}}{\longleftrightarrow }}S$

Также имеются предположения о временных вставках:

$S|\equiv \#T_{A}$

$B|\equiv \#T_{S}$

Помимо этого, есть несколько предположений о ключе шифрования:

• $B$ полагается на $A$ в выборе хорошего ключа:

$B|\equiv A|\Rightarrow (A{\stackrel {K_{ab}}{\longleftrightarrow }}B)$

• $B$ доверяет $S$ передать ключ от $A$:

$B|\equiv S|\Rightarrow (A|\equiv A{\stackrel {K_{ab}}{\longleftrightarrow }}B)$

• $A$ верит, что сеансовый ключ принят:

$A|\equiv (A{\stackrel {K_{ab}}{\longleftrightarrow }}B)$

Приступим к анализу протокола.

• $S$ получает первое сообщение, из которого можно сделать следующие выводы:

1. $S$, видя сообщение, зашифрованное ключом $K_{as}$, делает вывод, что оно было послано $A$ (правило о значении сообщения).
2. Наличие свежей временной вставки $T_{A}$ позволяет заключить, что и все сообщение написано недавно (правило для оператора $\#$).
3. Из свежести всего сообщения $S$ может заключить, что $A$ верил в то, что послал (правило проверки уникальности числовых вставок).

Следовательно, $S|\equiv A|\equiv (A{\stackrel {K_{ab}}{\longleftrightarrow }}B)$.

• $B$ получает второе сообщение протокола, из которого следует:

1. Увидев послание, зашифрованное ключом $K_{bs}$, клиент $B$ понимает, что оно было отправлено $S$.
2. Временная вставка $T_{S}$ доказывает $B$, что все сообщение было послано недавно.
3. Ввиду свежести сообщения, $B$ заключает, что $S$ доверяет всему посланному.
4. В частности, $B$ верит в то, что $S$ доверяет второй части сообщения.
5. Но $B$ верит и в то, что в юрисдикцию $S$ входит выяснить, знает ли его партнер $A$ секретный ключ, и поэтому $B$ вверяет $A$ полномочия по генерированию ключа.

Из этих рассуждений можно сделать следующие выводы:

$B|\equiv (A{\stackrel {K_{ab}}{\longleftrightarrow }}B)$

$B|\equiv A|\equiv (A{\stackrel {K_{ab}}{\longleftrightarrow }}B)$

С учетом исходного предположения о том, что $A|\equiv (A{\stackrel {K_{ab}}{\longleftrightarrow }}B)$, получаем, что анализируемый протокол обоснован. Единственное, чего нельзя утверждать:

$A|\equiv B|\equiv (A{\stackrel {K_{ab}}{\longleftrightarrow }}B)$

то есть $A$ не добился подтверждения того, что $B$ получил нужный ключ.

Критика

Наибольшей критике подвергается процесс идеализации, поскольку идеализованный протокол может некорректно отражать свой реальный аналог. Это связано с тем, что описание протоколов не дается в формальной манере, что иногда ставит под сомнение саму возможность корректной идеализации. Более того, ряд критиков пытается показать, что BAN-логика может получить и очевидно неправильные характеристики протоколов. Кроме того, результат анализа протокола с помощью BAN-логики не может считаться доказательством его безопасности, поскольку данная формальная логика занимается исключительно вопросами доверия.

Литература

• M. Burrows, M. Abadi, R. Needham. A Logic of Authentication (неопр.) // Systems Research Center of Digital Equipment Corporation in Palo Alto. — 1989. — December (т. 426). — С. 44—54.

• Monniaux, D. Decision procedures for the analysis of cryptographic protocols by logics of belief (англ.) // Computer Security Foundations Workshop, 1999. Proceedings of the 12th IEEE : journal. — 1999. — P. 44—54.

• Boyd, Colin; Mao, Wenbo. On a Limitation of BAN Logic // Advances in Cryptology — EUROCRYPT ’93 (неопр.) / Helleseth, Tor. — Springer Berlin / Heidelberg, 1994. — С. 240—247. — ISBN 978-3-540-57600-6.

• Н. Смарт. Криптография. — Москва: Техносфера, 2005. — С. 162—179. — 528 с. — ISBN 5-94836-043-1.

• B. Schneier. Applied Cryptography (неопр.). — John Wiley & Sons, 1995. — С. 66—69. — 662 с. — ISBN 0-47111-709-9. Архивная копия от 3 сентября 2012 на Wayback Machine

• А. Алферов, А. Кузьмин, А. Зубов, А. Черемушкин. Основы криптографии. — Москва: Гелиос АРВ, 2002. — С. 378—385, 404—406. — 480 с. — ISBN 5-85438-025-0.

Ссылки

• UT Austin CS course material on BAN logic (PDF) Архивная копия от 26 января 2020 на Wayback Machine
• Логика аутентификации (зеркало), первоисточник Michael Burrows, Martín Abadi, and Roger Needham.
• Источник: The Burrows-Abadi-Needham logic
• BAN logic in context, from UT Austin CS (PDF) Архивная копия от 26 января 2020 на Wayback Machine