Войти
Логика Берроуза – Абади – Нидхема (также известна как логика BAN ) - это набор правил для определения и анализа протоколов обмена информацией. В частности, логика BAN помогает своим пользователям определить, является ли передаваемая информация надежной, защищенной от подслушивания или и тем, и другим. Логика BAN начинается с предположения, что все обмены информацией происходят на носителях, уязвимых для фальсификации и общественного контроля. Это превратилось в популярную мантру безопасности: «Не доверяйте сети».
Типичная логическая последовательность BAN включает три этапа:
Логика BAN использует постулирует и определения - как и все аксиоматические системы - для анализа аутентификации протоколов. Использование логики BAN часто сопровождает формулировку протокола нотация протокола безопасности и иногда приводится в документах.
логика BAN и логики в одном семействе разрешимы : существует алгоритм, принимающий гипотезы BAN и предполагаемый вывод, и который отвечает, можно ли выводить вывод из гипотезы. Предлагаемые алгоритмы используют вариант магических наборов.
Логика BAN вдохновила многие другие подобные формализмы, такие как. Некоторые из них пытаются исправить одну слабость логики BAN: отсутствие хорошей семантики с ясным значением с точки зрения знаний и возможных универсумов. Однако, начиная с середины 1990-х, криптопротоколы анализировались в операционных моделях (предполагая совершенную криптографию) с использованием средств проверки моделей, и в протоколах, которые были «проверены» с помощью логики BAN и связанных формализмов, были обнаружены многочисленные ошибки. В некоторых случаях протокол считался безопасным при анализе BAN, но на самом деле небезопасным. Это привело к отказу от логики семейства BAN в пользу методов доказательства, основанных на стандартных рассуждениях об инвариантности.
Определения и их значения приведены ниже (P и Q - сетевые агенты, X - сообщение, а K - ключ шифрования ):
Смысл этих определений зафиксирован в серии постулатов :
P должен верить, что X здесь свежий. Если известно, что X не является свежим, это может быть устаревшее сообщение, воспроизведенное злоумышленником.
Используя эту нотацию, предположения, лежащие в основе аутентификации протокол можно формализовать. Используя постулаты, можно доказать, что определенные агенты верят, что могут общаться с помощью определенных ключей. Если доказательство не удается, точка отказа обычно предполагает атаку, которая компрометирует протокол.
Очень простой протокол - Wide Mouth Frog протокол - позволяет двум агентам, A и B, устанавливать безопасную связь, используя доверенный сервер аутентификации, S, и синхронизированные часы повсюду. Используя стандартные обозначения, протокол может быть определен следующим образом:
Агенты A и B снабжены ключами K as и K bs соответственно для безопасного взаимодействия с S. Итак, мы имеют предположения:
Агент A хочет инициировать безопасный диалог с B. Поэтому он изобретает ключ, K ab, который будет использовать для связи с B. A считает этот ключ безопасным, поскольку он сам составлял ключ:
B готов принять этот ключ, если он уверен, что он пришел от A:
Более того, B готов доверять S, чтобы точно передать ключи от A:
То есть, если B считает, что S считает, что A хочет использовать определенный ключ для связи с B, то B будет доверять S и тоже верить ему.
Цель состоит в том, чтобы
A считывал часы, получая текущее время t, и отправлял следующее сообщение :
То есть, он отправляет свой выбранный сеансовый ключ и текущее время на S, зашифрованный его секретный ключ сервера аутентификации K as.
Поскольку S считает, что ключ (K as, A↔S), а S видит {t, key (K ab, A↔B)} Kas, тогда S заключает, что A действительно сказал {t, key (K ab, A↔B)}. (В частности, S считает, что сообщение не было полностью создано каким-то злоумышленником.)
Так как часы синхронизированы, мы можем предположить, что
Поскольку S верит fresh (t), а S верит, что A сказал {t, key (K ab, A↔B)}, S считает, что A действительно верит, что ключ (K ab, A↔ Б). (В частности, S считает, что сообщение не было воспроизведено каким-то злоумышленником, захватившим его в какой-то момент в прошлом.)
S затем перенаправляет ключ на B:
Поскольку сообщение 2 зашифровано с помощью K bs, а B верит в ключ (K bs, B↔S), B теперь считает, что S сказал {t, A, A верит ключу (K ab, A↔B)}. Поскольку часы синхронизированы, B считает свежий (t) и такой свежий (A считает ключ (K ab, A↔B)). Поскольку B считает, что утверждение S свежее, B считает, что S считает, что (A верит ключу (K ab, A↔B)). Поскольку B считает, что S авторитетен в отношении того, во что верит A, B считает, что (A верит ключу (K ab, A↔B)). Поскольку B считает, что A является авторитетным в отношении ключей сеанса между A и B, B считает ключ (K ab, A↔B). Теперь B может связаться с A напрямую, используя K ab в качестве секретного сеансового ключа.
Теперь предположим, что мы отказались от предположения, что часы синхронизированы. В этом случае S получает сообщение 1 от A с {t, key (K ab, A↔B)}, но он больше не может заключить, что t свежий. Он знает, что A отправил это сообщение когда-то в прошлом (потому что оно зашифровано с помощью K как), но не то, что это недавнее сообщение, поэтому S не считает, что A обязательно хочет продолжить используйте клавишу K ab. Это прямо указывает на атаку на протокол: злоумышленник, который может перехватывать сообщения, может угадать один из старых ключей сеанса K ab. (Это может занять много времени.) Затем злоумышленник воспроизводит старое сообщение {t, key (K ab, A↔B)}, отправляя его на S. Если часы не синхронизированы (возможно, как часть той же атаки), S может поверить этому старому сообщению и потребовать от B использовать старый скомпрометированный ключ снова.
Исходный документ по логике аутентификации (ссылка ниже) содержит этот пример и многие другие, включая анализ протокола подтверждения Kerberos и две версии Andrew Project Рукопожатие RPC (одно из которых неисправно).
| journal =()