Русская Википедия:Логика Бэрроуза — Абади — Нидхэма

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

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

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

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

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

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

<math>P | \equiv X</math> означает, что <math>P</math> верит в высказывание <math>X</math>. Это значит, что <math>P</math> станет действовать так, как будто <math>X</math> — истинная информация.
<math>P \vartriangleleft X</math> подразумевает, что <math>P</math> видит <math>X</math>, то есть <math>P</math> принял сообщение, в котором содержится <math>X</math>. То есть <math>P</math> может прочитать и воспроизвести (возможно, после процедуры расшифрования) сообщение <math>X</math>.
<math>P | \sim X</math> означает, что <math>P</math> однажды высказал <math>X</math>, то есть в какой-то момент времени <math>P</math> послал сообщение, содержащее <math>X</math>.
<math>P | \Rightarrow X</math> означает, что <math>X</math> входит в юрисдикцию <math>P</math> (или <math>P</math> имеет юрисдикцию над <math>X</math>), то есть <math>P</math> обладает авторитетом по вопросу относительно <math>X</math>.
<math>\# X</math> означает, что высказывание <math>X</math> получено недавно. То есть сообщение <math>X</math> не было послано когда-то в прошлом (до момента запуска протокола).
<math>P \stackrel{k}{ \longleftrightarrow } Q</math> означает, что <math>P</math> и <math>Q</math> используют для общения разделенный ключ <math>k</math>.
<math>\lbrace X \rbrace_k</math> подразумевает, что данные <math>X</math> зашифрованы ключом <math>k</math>.

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

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

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

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

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

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

<math> \dfrac{A | \equiv A \stackrel{K}{ \longleftrightarrow } B , A \vartriangleleft \lbrace X \rbrace_K}{A | \equiv B | \sim X} </math>

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

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

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

<math> \dfrac{A | \equiv \# X , A | \equiv B | \sim X}{A | \equiv B | \equiv X} </math>

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

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

<math> \dfrac{A | \equiv B | \Rightarrow X , A | \equiv B | \equiv X}{A | \equiv X} </math>

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

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

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

<math>\dfrac{A | \equiv X, A | \equiv Y}{A | \equiv (X,Y)} </math>

<math>\dfrac{A | \equiv (X,Y)}{A | \equiv X} </math>

<math>\dfrac{A | \equiv B | \equiv (X,Y)}{A | \equiv B | \equiv X} </math>

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

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

<math>\dfrac{A | \equiv B | \sim (X,Y)}{A | \equiv B | \sim X} </math>

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

<math>\dfrac{A | \equiv \# X}{A | \equiv \# (X,Y)}</math>

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

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

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

Поясним смысл данной процедуры. Первый шаг носит название идеализации и состоит в следующем: каждый шаг протокола, записанный в виде <math>P \longrightarrow Q: message</math>, преобразуется в набор логических утверждений, касающихся передающей и принимающей стороны. Пусть, например, один из шагов протокола выглядит следующим образом:

<math>A \longrightarrow B: \lbrace A,K_{ab} \rbrace_{K_{bs}}</math>

Это сообщение говорит участнику <math>B</math> (обладающему ключом <math>K_{bs}</math>), что ключ <math>K_{ab}</math> должен быть использован для сообщения с <math>A</math>. Соответствующая логическая формула для данного сообщения имеет вид:

<math>A \longrightarrow B: \lbrace A\stackrel{K_{ab}}{ \longleftrightarrow } B\rbrace_{K_{bs}}</math>

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

<math>B \vartriangleleft \lbrace A\stackrel{K_{ab}}{ \longleftrightarrow } B\rbrace_{K_{bs}}</math>

то есть <math>B</math> видит данное сообщение и в дальнейшем будет действовать в соответствии с ним.

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

<math>[assumptions]S_1[assertion1]\cdots[assertion(n-1)]S_n[conclusions]</math>

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

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

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

<math>A| \equiv A \stackrel{K}{\longleftrightarrow} B</math> и <math>B| \equiv A \stackrel{K}{\longleftrightarrow} B</math>

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

<math>A | \equiv B | \equiv A \stackrel{K}{\longleftrightarrow} B</math> и <math>B | \equiv A | \equiv A \stackrel{K}{\longleftrightarrow} B</math>

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

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

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

<math>A \rightarrow S: A,\{T_A, K_{ab}, B\}_{K_{as}}</math>

<math>S \rightarrow B: \{T_S, K_{ab}, A\}_{K_{bs}}</math>

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

<math>A \rightarrow S: \{T_A, A \stackrel{K_{ab}}{\longleftrightarrow} B \}_{K_{as}}</math>

<math>S \rightarrow B: \{T_S, A | \equiv A \stackrel{K_{ab}}{\longleftrightarrow} B \}_{K_{bs}}</math>

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

<math> A | \equiv A \stackrel{K_{as}}{\longleftrightarrow} S </math>

<math> S | \equiv A \stackrel{K_{as}}{\longleftrightarrow} S </math>

<math> B | \equiv B \stackrel{K_{bs}}{\longleftrightarrow} S </math>

<math> S | \equiv B \stackrel{K_{bs}}{\longleftrightarrow} S </math>

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

<math> S | \equiv \#T_A </math>

<math> B | \equiv \#T_S </math>

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

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

<math> B | \equiv A | \Rightarrow (A \stackrel{K_{ab}}{\longleftrightarrow} B)</math>

<math>B</math> доверяет <math>S</math> передать ключ от <math>A</math>:

<math> B | \equiv S | \Rightarrow (A | \equiv A \stackrel{K_{ab}}{\longleftrightarrow} B)</math>

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

<math> A | \equiv (A \stackrel{K_{ab}}{\longleftrightarrow} B)</math>

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

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

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

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

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

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

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

<math> B | \equiv (A \stackrel{K_{ab}}{\longleftrightarrow} B)</math>

<math> B | \equiv A | \equiv (A \stackrel{K_{ab}}{\longleftrightarrow} B)</math>

С учетом исходного предположения о том, что <math> A | \equiv (A \stackrel{K_{ab}}{\longleftrightarrow} B)</math>, получаем, что анализируемый протокол обоснован. Единственное, чего нельзя утверждать:

<math> A | \equiv B | \equiv (A \stackrel{K_{ab}}{\longleftrightarrow} B)</math>

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

Критика

Наибольшей критике подвергается процесс идеализации, поскольку идеализованный протокол может некорректно отражать свой реальный аналог.^[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]

Партнерские ресурсы
Криптовалюты	Обмен криптовалют - www.bestchange.ru Криптовалютная биржа CoinEx Криптовалютная биржа Binance HIVE OS - операционная система для майнинга e4pool - Мультивалютный пул для майнинга.
Магазины	AliExpress — глобальная виртуальная (в Интернете) торговая площадка, предоставляющая возможность покупать товары производителей из КНР; computeruniverse.net - Интернет-магазин компьютеров(Промо код 5 Евро на первую покупку:FWWC3ZKQ);
Хостинг	DigitalOcean - американский провайдер облачных инфраструктур, с главным офисом в Нью-Йорке и с центрами обработки данных по всему миру;
Разное	Викиум - Онлайн-тренажер для мозга Like Центр - Центр поддержки и развития предпринимательства. Gamersbay - лучший магазин по бустингу для World of Warcraft. Ноотропы OmniMind N°1 - Усиливает мозговую активность. Повышает мотивацию. Улучшает память. Санкт-Петербургская школа телевидения - это федеральная сеть образовательных центров, которая имеет филиалы в 37 городах России. Lingualeo.com — интерактивный онлайн-сервис для изучения и практики английского языка в увлекательной игровой форме. Junyschool (Джунискул) – международная школа программирования и дизайна для детей и подростков от 5 до 17 лет, где ученики осваивают компьютерную грамотность, развивают алгоритмическое и креативное мышление, изучают основы программирования и компьютерной графики, создают собственные проекты: игры, сайты, программы, приложения, анимации, 3D-модели, монтируют видео. Умназия - Интерактивные онлайн-курсы и тренажеры для развития мышления детей 6-13 лет SkillBox - это один из лидеров российского рынка онлайн-образования. Среди партнеров Skillbox ведущий разработчик сервисного дизайна AIC, медиа-компания Yoola, первое и самое крупное русскоязычное аналитическое агентство Tagline, онлайн-школа дизайна и иллюстрации Bang! Bang! Education, оператор PR-рынка PACO, студия рисования Draw&Go, агентство performance-маркетинга Ingate, scrum-студия Sibirix, имидж-лаборатория Персона. «Нетология» — это университет по подготовке и дополнительному обучению специалистов в области интернет-маркетинга, управления проектами и продуктами, дизайна, Data Science и разработки. В рамках Нетологии студенты получают ценные теоретические знания от лучших экспертов Рунета, выполняют практические задания на отработку полученных навыков, общаются с экспертами и единомышленниками. Познакомиться со всеми продуктами подробнее можно на сайте https://netology.ru, линейка курсов и профессий постоянно обновляется. StudyBay Brazil – это онлайн биржа для португалоговорящих студентов и авторов! Студент получает уникальную работу любого уровня сложности и больше свободного времени, в то время как у автора появляется дополнительный заработок и бесценный опыт. Автор24 — самая большая в России площадка по написанию учебных работ: контрольные и курсовые работы, дипломы, рефераты, решение задач, отчеты по практике, а так же любой другой вид работы. Сервис сотрудничает с более 70 000 авторов. Более 1 000 000 работ уже выполнено. StudyBay – это онлайн биржа для англоязычных студентов и авторов! Студент получает уникальную работу любого уровня сложности и больше свободного времени, в то время как у автора появляется дополнительный заработок и бесценный опыт.