Логика Бэрроуза

Логика Бэрроуза — Абади — Нидхэма (англ. 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-логики

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)}$

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

С практической точки зрения, анализ протокола осуществляется следующим образом:^{[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$

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

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

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

$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$ получил нужный ключ.

Критика

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

Примечания

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.
6. ↑ Н. Смарт, "Криптография", p. 177.
7. ↑ M. Burrows, M. Abadi, R. Needham, "A Logic of Authentication", p. 13.
8. ↑ Н. Смарт, "Криптография", p. 177.
9. ↑ Н. Смарт, "Криптография", p. 169-170.
10. ↑ D.M. Nessett, "A Critique of the Burrows, Abadi, and Needham Logic", pp. 35-38.
11. ↑ Boyd,C. and Mao, W. "On a Limitation of BAN Logic"
12. ↑ Boyd,C. and Mao, W. "On a Limitation of BAN Logic"
13. ↑ P.F. Syverson, "The Use of Logic in the Analysis of Cryptographic Protocols"

Литература

• 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.

• 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.

• 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)
• Логика аутентификации (зеркало), первоисточник Burrows, Abadi, and Needham.
• Источник: The Burrows-Abadi-Needham logic
• BAN logic in context, from UT Austin CS (PDF)