Из Википедии, бесплатной энциклопедии
  (Перенаправлено из логики Берроуза-Абади-Нидхэма )
Перейти к навигации Перейти к поиску

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

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

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

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

Тип языка [ править ]

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

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

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

Основные правила [ править ]

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

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

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

  • Если P считает ключ ( K , P ↔ Q ), а P видит { X } K , то P считает ( Q сказал X )
  • Если P верит ( Q сказал X ), а P верит fresh ( X ), то P верит ( Q верит X ).

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

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

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

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

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

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

A верит ключу ( K as , A ↔ S )
S считает ключ ( K as , A ↔ S )
B считает ключ ( K bs , B ↔ S )
S считает ключ ( K bs , B ↔ S )

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

A верит ключу ( K ab , A ↔ B )

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

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

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

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

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

Цель состоит в том, чтобы иметь

B считает ключ ( K ab , A ↔ B )

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

1 A → S : { t , key ( K ab , A ↔ B )} K как

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

Поскольку S считает, что key ( K as , A ↔ S ), а S видит { t , key ( K ab , A ↔ B )} K as , то S заключает, что A действительно сказал { t , key ( K ab , A ↔ Б )}. (В частности, S считает, что сообщение не было создано злоумышленником целиком.)

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

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

Поскольку S верит fresh ( t ), а S верит, что A сказал { t , key ( K ab , A ↔ B )}, S считает, что A действительно верит этому ключу ( K ab , A ↔ B ). (В частности, S считает, что сообщение не было воспроизведено каким-либо злоумышленником, захватившим его в какой-то момент в прошлом.)

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

2 S → B : { t , A , A считает ключ ( K ab , A ↔ B )} K bs

Поскольку сообщение 2 зашифровано с K BS , и Б считает , ключевые ( K BS , B ↔ S ), Б теперь считает , что S говорит , { т , , считает , ключ ( K AB , ↔ B )}. Поскольку часы синхронизированы, B считает fresh ( t ) и таким новым ( A считает key ( K ab , A ↔ B )). Поскольку B считает, что Sутверждение свежее, B считает, что S считает, что ( A верит key ( K ab , A ↔ B )). Поскольку B считает, что S авторитетен в отношении того, во что верит A , B считает, что ( A верит ключу ( K ab , A ↔ B )). Поскольку B считает, что A является авторитетным в отношении ключей сеанса между A и B , B полагает, что key ( K ab, A ↔ B ). Теперь B может связаться с A напрямую, используя K ab в качестве секретного сеансового ключа.

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

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

Ссылки [ править ]

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

Дальнейшее чтение [ править ]