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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

• 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