Логика Бэрроуза — Абади — Нидхэма (Lkintg >zjjkr[g — GQg;n — Un;]zbg)

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

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

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

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

Как и любая формальная логика, 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-логики

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

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

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

{\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}}

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

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

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

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

Исходный протокол преобразуется в идеализованный (то есть записанный в терминах 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-логики (то есть какие логические утверждения должны быть выведены из предположений протокола, с учетом последовательности шагов (утверждений), выполняемых в данном протоколе):^[6]^[7]

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

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

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

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

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$ получает первое сообщение, из которого можно сделать следующие выводы:

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

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

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

Увидев послание, зашифрованное ключом $K_{bs}$ , клиент $B$ понимает, что оно было отправлено $S$ .
Временная вставка $T_{S}$ доказывает $B$ , что все сообщение было послано недавно.
Ввиду свежести сообщения, $B$ заключает, что $S$ доверяет всему посланному.
В частности, $B$ верит в то, что $S$ доверяет второй части сообщения.
Но $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$ получил нужный ключ.

Критика

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

Примечания

↑ Н. Смарт, «Криптография», p. 175.
↑ B. Schneier, «Applied Cryptography», p. 66.
↑ M. Burrows, M. Abadi, R. Needham, «A Logic of Authentication», p. 3.
↑ M. Burrows, M. Abadi, R. Needham, «A Logic of Authentication», p. 11.
↑ B. Schneier, «Applied Cryptography», p. 67.
↑ ¹ ² Н. Смарт, «Криптография», p. 177.
↑ M. Burrows, M. Abadi, R. Needham, «A Logic of Authentication», p. 13.
↑ Н. Смарт, «Криптография», p. 169—170.
↑ D.M. Nessett, «A Critique of the Burrows, Abadi, and Needham Logic», pp. 35-38.
↑ ¹ ² Boyd,C. and Mao, W. «On a Limitation of BAN Logic»
↑ P.F. Syverson, «The Use of Logic in the Analysis of Cryptographic Protocols»

Литература

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

[1] Н. Смарт, «Криптография», p. 175.

[2] B. Schneier, «Applied Cryptography», p. 66.

[3] M. Burrows, M. Abadi, R. Needham, «A Logic of Authentication», p. 3.

[4] M. Burrows, M. Abadi, R. Needham, «A Logic of Authentication», p. 11.

[5] B. Schneier, «Applied Cryptography», p. 67.

[autogenerated1-6] ¹ ² Н. Смарт, «Криптография», p. 177.

[7] M. Burrows, M. Abadi, R. Needham, «A Logic of Authentication», p. 13.

[8] Н. Смарт, «Криптография», p. 169—170.

[9] D.M. Nessett, «A Critique of the Burrows, Abadi, and Needham Logic», pp. 35-38.

[autogenerated2-10] ¹ ² Boyd,C. and Mao, W. «On a Limitation of BAN Logic»

[11] P.F. Syverson, «The Use of Logic in the Analysis of Cryptographic Protocols»

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]