WikiDer > Логика Барроуза – Абади – Нидхема

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

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

А считает ключ (Kтак как, АS)
S считает ключ (Kтак как, АS)
B считает ключ (Kbs, BS)
S считает ключ (Kbs, BS)

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

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

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

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

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

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

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

Цель - иметь

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

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

1 АS: {т, ключ(Kab, АB)}Kтак как

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

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

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

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

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

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

2 SB: {т, А, А считает ключ (Kab, АB)}Kbs

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

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

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

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

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

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