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

Материал из Википедии — свободной энциклопедии
Перейти к: навигация, поиск

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

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

Критика[править | править исходный текст]

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

Примечания[править | править исходный текст]

  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. 1 2 Н. Смарт, "Криптография", 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.
  10. 1 2 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"

Литература[править | править исходный текст]

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

Ссылки[править | править исходный текст]