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

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

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

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

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

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

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

$P | \equiv X$ означает, что $P$ верит в высказывание $X$ . Это значит, что $P$ станет действовать так, как будто $X$ — истинная информация.
$P ⊲ 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 \overset{k}{⟷} Q$ означает, что $P$ и $Q$ используют для общения разделенный ключ $k$ .
${X}_{k}$ подразумевает, что данные $X$ зашифрованы ключом $k$ .

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

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

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

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

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

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

\frac{A | \equiv A \overset{K}{⟷} B, A ⊲ {X}_{K}}{A | \equiv B | \sim X}

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

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

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

\frac{A | \equiv # X, A | \equiv B | \sim X}{A | \equiv B | \equiv X}

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

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

\frac{A | \equiv B | \Rightarrow X, A | \equiv B | \equiv X}{A | \equiv X}

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

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

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

\frac{A | \equiv X, A | \equiv Y}{A | \equiv (X, Y)}

\frac{A | \equiv (X, Y)}{A | \equiv X}

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

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

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

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

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

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

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

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

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

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

A ⟶ B : {A, K_{a b}}_{K_{b s}}

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

A ⟶ B : {A \overset{K_{a b}}{⟷} B}_{K_{b s}}

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

B ⊲ {A \overset{K_{a b}}{⟷} B}_{K_{b s}}

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

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

[a s s u m p t i o n s] S_{1} [a s s e r t i o n 1] \dots [a s s e r t i o n (n - 1)] S_{n} [c o n c l u s i o n s]

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

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

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

A | \equiv A \overset{K}{⟷} B

и

B | \equiv A \overset{K}{⟷} B

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

A | \equiv B | \equiv A \overset{K}{⟷} B

и

B | \equiv A | \equiv A \overset{K}{⟷} B

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

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

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

A \to S : A, {T_{A}, K_{a b}, B}_{K_{a s}}

S \to B : {T_{S}, K_{a b}, A}_{K_{b s}}

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

A \to S : {T_{A}, A \overset{K_{a b}}{⟷} B}_{K_{a s}}

S \to B : {T_{S}, A | \equiv A \overset{K_{a b}}{⟷} B}_{K_{b s}}

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

A | \equiv A \overset{K_{a s}}{⟷} S

S | \equiv A \overset{K_{a s}}{⟷} S

B | \equiv B \overset{K_{b s}}{⟷} S

S | \equiv B \overset{K_{b s}}{⟷} S

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

S | \equiv # T_{A}

B | \equiv # T_{S}

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

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

B | \equiv A | \Rightarrow (A \overset{K_{a b}}{⟷} B)

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

B | \equiv S | \Rightarrow (A | \equiv A \overset{K_{a b}}{⟷} B)

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

A | \equiv (A \overset{K_{a b}}{⟷} B)

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

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

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

Следовательно, $S | \equiv A | \equiv (A \overset{K_{a b}}{⟷} B)$ .

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

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

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

B | \equiv (A \overset{K_{a b}}{⟷} B)

B | \equiv A | \equiv (A \overset{K_{a b}}{⟷} B)

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

A | \equiv B | \equiv (A \overset{K_{a b}}{⟷} B)

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

Критика

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

Примечания

Шаблон:Примечания

Литература

Шаблон:Статья

Шаблон:Статья

Шаблон:Книга

Шаблон:Книга

Шаблон:Книга Шаблон:Wayback

Шаблон:Книга

Ссылки

UT Austin CS course material on BAN logic (PDF) Шаблон:Wayback
Логика аутентификации (зеркало), первоисточник Шаблон:Iw, Шаблон:Iw, and Roger Needham.
Источник: The Burrows-Abadi-Needham logic
BAN logic in context, from UT Austin CS (PDF) Шаблон:Wayback

↑ Н. Смарт, «Криптография», 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.
↑ ^6,0 ^6,1 Н. Смарт, «Криптография», 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.
↑ ^10,0 ^10,1 Boyd,C. and Mao, W. «On a Limitation of BAN Logic»
↑ P.F. Syverson, «The Use of Logic in the Analysis of Cryptographic Protocols»

[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] 6,0 ^6,1 Н. Смарт, «Криптография», 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] 10,0 ^10,1 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]

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

Содержание

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

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

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

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

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

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

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

Критика

Примечания

Литература

Ссылки

Навигация

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

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

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

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

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

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

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

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

Критика

Примечания

Литература

Ссылки

Навигация

Поиск