Логика Барроуза – Абади – Нидхема - Burrows–Abadi–Needham logic

Логика Барроуза – Абади – Нидхема (также известный как BAN логика) представляет собой набор правил для определения и анализа протоколов обмена информацией. В частности, логика BAN помогает своим пользователям определить, является ли передаваемая информация надежной, защищенной от подслушивания или и тем, и другим. Логика BAN начинается с предположения, что все обмены информацией происходят на носителях, уязвимых для фальсификации и общественного контроля. Это превратилось в популярную мантру безопасности: «Не доверяйте сети».

Типичная логическая последовательность BAN включает три шага:^[1]

1. Проверка происхождения сообщения
2. Проверка сообщения свежесть
3. Проверка подлинности происхождения.

Логика BAN использует постулаты и определения - как все аксиоматические системы - анализировать аутентификация протоколы. Использование логики BAN часто сопровождает обозначение протокола безопасности формулировка протокола и иногда приводится в бумажных документах.

Тип языка

Логика BAN и логика в одном семействе разрешимый: существует алгоритм, принимающий гипотезы BAN и предполагаемый вывод, и который отвечает, можно ли выводить вывод из гипотез. В предлагаемых алгоритмах используется вариант магические наборы.^[2]

Альтернативы и критика

Логика BAN вдохновила многие другие подобные формализмы, такие как Логика GNY. Некоторые из них пытаются исправить одну слабость логики BAN: отсутствие хорошей семантики с ясным значением с точки зрения знаний и возможных универсумов. Однако, начиная с середины 1990-х, криптопротоколы анализировались в операционных моделях (предполагая совершенную криптографию) с использованием средств проверки моделей, и в протоколах, которые были «проверены» с помощью логики BAN и связанных формализмов, были обнаружены многочисленные ошибки.^{[нужна цитата ]} В некоторых случаях протокол считался безопасным при анализе BAN, но на самом деле небезопасным.^[3] Это привело к отказу от логики семейства BAN в пользу методов доказательства, основанных на стандартных рассуждениях об инвариантности.^{[нужна цитата ]}

Основные правила

Определения и их значение приведены ниже (п и Q сетевые агенты, Икс это сообщение, и K является ключ шифрования ):

• п верит Икс: п действует как если бы Икс верно, и может утверждать Икс в других сообщениях.
• п имеет юрисдикцию над Икс: пубеждения о Икс следует доверять.
• п сказал Икс: Когда-то п переданное (и принятое) сообщение Икс, несмотря на то что п может больше не верить Икс.
• п видит Икс: п получает сообщение Икс, и может читать и повторять Икс.
• {Икс}_K: Икс зашифрован ключом K.
• свежий(Икс): Икс ранее не отправлялся ни в одном сообщении.
• ключ(K, п↔Q): п и Q может общаться с общим ключом K

Смысл этих определений заключен в серии постулатов:

• Если п считает ключ (K, п↔Q), и п видит {Икс}_K, тогда п верит (Q сказал Икс)
• Если п верит (Q сказал Икс) и п считает свежий (Икс), тогда п верит (Q верит Икс).

п должен верить, что Икс здесь свежее. Если Икс не известно, что оно свежее, то это может быть устаревшее сообщение, воспроизведенное злоумышленником.

• Если п верит (Q имеет юрисдикцию над Икс) и п верит (Q верит Икс), тогда п верит Икс
• Есть несколько других технических постулатов, связанных с составом сообщений. Например, если п считает, что Q сказал <Икс, Y>, конкатенация Икс и Y, тогда п также считает, что Q сказал Икс, и п также считает, что Q сказал Y.

Используя эту нотацию, можно формализовать предположения, лежащие в основе протокола аутентификации. Используя постулаты, можно доказать, что определенные агенты верят, что они могут общаться с помощью определенных ключей. Если доказательство не удается, точка отказа обычно предполагает атаку, которая нарушает протокол.

Логический анализ BAN протокола Wide Mouth Frog

Очень простой протокол - Протокол Wide Mouth Frog - позволяет двум агентам, A и B, устанавливать безопасную связь, используя доверенный сервер аутентификации S и синхронизированные часы. Используя стандартные обозначения, протокол можно указать следующим образом:

${\displaystyle A\rightarrow S:A,\{T_{A},K_{ab},B\}_{K_{as}}}$

${\displaystyle S\rightarrow B:\{T_{S},K_{ab},A\}_{K_{bs}}}$

Агенты A и B оснащены ключами K_{так как} и K_bs, соответственно, для безопасного общения с S. Итак, у нас есть предположения:

А считает ключ (K_{так как}, А↔S)

S считает ключ (K_{так как}, А↔S)

B считает ключ (K_bs, B↔S)

S считает ключ (K_bs, B↔S)

Агент А хочет начать безопасный разговор с B. Поэтому он изобретает ключ, K_ab, который он будет использовать для связи с B. А считает, что этот ключ безопасен, поскольку он сам составлял ключ:

А считает ключ (K_ab, А↔B)

B готов принять этот ключ, если уверен, что он пришел из А:

B верит (А имеет юрисдикцию над ключом (K, А↔B))

Более того, B готов доверять S точно передать ключи от А:

B верит (S имеет юрисдикцию над (А считает ключ (K, А↔B)))

То есть, если B считает, что S считает, что А хочет использовать определенный ключ для связи с B, тогда B буду доверять S и верю этому тоже.

Цель - иметь

B считает ключ (K_ab, А↔B)

А читает часы, получая текущее время т, и отправляет следующее сообщение:

1 А→S: {т, ключ(K_ab, А↔B)}_{Kтак как}

То есть он отправляет выбранный сеансовый ключ и текущее время в S, зашифрованный своим частным ключом сервера аутентификации K_{так как}.

С S считает, что ключ (K_{так как}, А↔S), и S видит {т, ключ(K_ab, А↔B)}_{Kтак как}, тогда S заключает, что А на самом деле сказал {т, ключ(K_ab, А↔B)}. (Особенно, S считает, что сообщение не было создано злоумышленником целиком.)

Поскольку часы синхронизированы, мы можем предположить

S считает свежий (т)

С S считает свежий (т) и S верит А сказал {т, ключ(K_ab, А↔B)}, S считает, что А фактически верит этот ключ (K_ab, А↔B). (Особенно, S считает, что сообщение не было воспроизведено каким-то злоумышленником, захватившим его когда-то в прошлом.)

S затем пересылает ключ на B:

2 S→B: {т, А, А считает ключ (K_ab, А↔B)}_Kbs

Поскольку сообщение 2 зашифровано с помощью K_bs, и Bсчитает ключ (K_bs, B↔S), B теперь считает, что Sсказал {т, А, А считает ключ (K_ab, А↔B)}. Поскольку часы синхронизированы, B считает свежий (т) и софреш (А считает ключ (K_ab, А↔B)). Потому что Bсчитает, что Sзаявление свежее, B считает, что S считает, что(А считает ключ (K_ab, А↔B)). Потому что Bсчитает, что S авторитетен в том, что А считает, B считает, что (А считает ключ (K_ab, А↔B)). Потому что Bсчитает, что А является авторитетным в отношении ключей сеанса между А и B, Bсчитает ключ (K_ab, А↔B). B теперь можно связаться Анапрямую, используя K_ab как секретный сеансовый ключ.

Теперь предположим, что мы отказываемся от предположения, что часы синхронизированы. В таком случае, S получает сообщение 1 от А с {т,ключ(K_ab, А↔B)}, но он больше не может сделать вывод, что t свежий. Он знает что А отправил это сообщение на немного время в прошлом (потому что он зашифрован с помощью K_{так как}), но не то, чтобы это недавнее сообщение, поэтому S не верит в это Аобязательно хочет продолжить пользоваться ключомK_ab. Это прямо указывает на атаку на протокол: злоумышленник, который может перехватывать сообщения, может угадать один из старых ключей сеанса. K_ab. (Это может занять много времени.) Затем злоумышленник воспроизводит старую запись {т,ключ(K_ab, А↔B)} сообщение, отправив его S. Если часы не синхронизированы (возможно, как часть той же атаки), S может поверить в это старое сообщение и попросить B снова используйте старый взломанный ключ.

Оригинал Логика аутентификации документ (ссылка на который приведен ниже) содержит этот и многие другие примеры, включая анализ Kerberos протокол рукопожатия и две версии Эндрю Проект Рукопожатие RPC (одно из которых неисправно).

Рекомендации

1. «Курсовые материалы по BAN логике» (PDF). UT Остин CS.
2. Моннио, Дэвид (1999). «Процедуры принятия решений для анализа криптографических протоколов с помощью логики доверия». Материалы 12-го семинара по основам компьютерной безопасности..
3. Бойд, Колин; Мао, Вэньбо (1994). «Об ограничении логики BAN». EUROCRYPT '93 Семинар по теории и применению криптографических методов в достижениях криптологии. Получено 2016-10-12.

дальнейшее чтение

• Берроуз, Майкл; Абади, Мартин; Нидхэм, Роджер. «Логика аутентификации». CiteSeerX  10.1.1.115.3569.
• Источник: Логика Барроуза-Абади-Нидхема