WikiSort.ru - Не сортированное

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

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

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

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

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

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

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

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

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]

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

Рассмотрим простой протокол аутентификации — протокол широкоротой лягушки — который позволяет двум сторонам, ${\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 (December 1989). “A Logic of Authentication”. Systems Research Center of Digital Equipment Corporation in Palo Alto. 426: 44–54. Используется устаревший параметр |month= (справка)

• Monniaux, D. (1999). “Decision procedures for the analysis of cryptographic protocols by logics of belief”. Computer Security Foundations Workshop, 1999. Proceedings of the 12th IEEE: 44–54.

• Boyd, Colin; Mao, Wenbo. On a Limitation of BAN Logic // Advances in Cryptology — EUROCRYPT ’93 / Helleseth, Tor. — Springer Berlin / Heidelberg, 1994. — P. 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. — ISBN 0-47111-709-9.

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

Ссылки

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