19-08-2023
Логика Бэрроуза — Абади — Нидхэма (англ. Burrows-Abadi-Needham logic) или БАН-логика (англ. BAN logic) — набор правил, используемый для определения и анализа протоколов обмена информацией. В частности, БАН-логика помогает своим пользователям, определить является ли информация, участвующая в обмене подлинной, защищённой от прослушивания и т. д. Первое, о чём говорит БАН-логика — это то, что конфиденциальность и подлинность информации, передаваемой в любой среде (будь то медный провод, оптоволокно или воздух), находятся под угрозой. Это утверждение выливается в популярную мантру информационной безопасности «Не доверяйте сети». Обычная последовательность БАН-логики состоит из трёх шагов:
Для анализа протоколов аутентификации БАН-логика, как и все описания протоколов защиты информации.
BAN логика и логики её семейства являются разрешимыми: существует алгоритм, проверяющий правильность выводов, сделанных с помощью BAN логики из гипотез. BAN логика является основой других формальных систем, некоторые из них пытаются устранить слабое место BAN логики: отсутствие хороших, понятных семантик.
Основные правила и их следствия приведены ниже (P и Q — клиенты сети, X — передаваемое сообщение, K — ключ шифрования):
Суть этих определений можно понять из следующих логических выражений: Если P доверяет key(K, P↔Q), и P видит {X}K, тогда P доверяет (Q сказал X). Если P доверяет (Q сказал X) и P доверяет fresh(X), тогда P доверяет (Q доверяет X). Здесь P должен доверять тому, что Х свежее, иначе X может быть старым сообщением, повторённым атакующей стороной.
Если P доверяет (Q имеет права на X) и P доверяет (Q доверяет X), тогда P доверяет X. Также существует ещё несколько технических утверждений, используемых для работы с композицией сообщений. Например, если P доверяет тому, что Q доверяет <X,Y> (конкатенации X и Y), тогда P доверяет тому, что Q сказал X и Q сказал Y. Используя эту нотацию, можно формализовать описания протоколов аутентификации. Также с помощью этих утверждений можно проверить, что данные клиенты доверяют использованию данных ключей для связи.
Очень простой протокол аутентификации — «протокол Лягушки» — позволяет двум агентам, A и B, установить защищённое соединение, используя сервер S, которому они оба доверяют, и синхронизированные часы. Используя стандартную нотацию, протокол может быть записан следующим образом:
Агенты A и B обладают ключами Kas и Kbs соответственно, для защищённой связи с сервером S. Из этого можно сделать следующие выводы:
Агент A хочет начать защищённую переписку с агентом B. Для этого он генерирует ключ Kas, для связи с B. A считает этот ключ безопасным, так он сам его сгенерировал: A доверяет key(Kas, A↔S)
B готов использовать этот ключ, пока он уверен, что этот ключ пришёл от A: B доверяет (A имеет права на key(K, A↔B))
Более того, B готов доверять тому, что S будет безошибочно передавать ключи от A: B доверяет (S имеет права на (A believes key(K, A↔B)))
Это значит, что если B доверяет тому, что S доверяет тому, что A хочет использовать собственный ключ для связи с B, будет доверять S и полагаться на него. Цель получить B доверяет key(Kab, A↔B)
А получает текущее время t с часов, и посылает следующее сообщение: 1 A->S: {t, key(Kab, A↔B)}Kas
Это значит, что он посылает сессионный ключ и текущее время на сервер S, шифруя их своим ключом аутентификации на сервере S — Kas. Как только S доверяет fresh(t) и S доверяет (A сказал {t, key(Kab, A↔B)}), S доверяет тому, что A доверяет тому, что key(Kab, A↔B). (В частности, S доверяет тому, что сообщение не является повтором атакующей стороны, перехватившей его в прошлом). После этого S отправляет ключ B: 2 S->B: {t, A, A доверяет key(Kab, A↔B)}Kbs Так как сообщение 2 зашифровано ключом Kbs, и B доверяет key(Kbs, B↔S), B теперь доверяет тому, что S сказал {t, A, A доверяет key(Kab, A↔B)}. Так как часы синхронизированы, B доверяет fresh(t), и следовательно доверяет fresh(A доверяет key(Kab, A↔B)). Из того, что B доверяет тому что утверждения S свежие, B доверяет тому, что S доверяет (A доверяет key(Kab, A↔B)). Так как B доверяет тому, что S знает о том, чему доверяет A, B доверяет (A доверяет key(Kab, A↔B)). Из того, что B доверяет тому, что A осведомлен о сессионных ключах между A и B, B доверяет key(Kab, A↔B). Теперь B может общаться с A напрямую, используя Kab как секретный сессионный ключ. Теперь давайте отбросим предположение о том, что часы синхронизированы. В таком случае S получает сообщение 1 от A с {t, key(Kab, A↔B)}, но он не может больше полагать, что оно свежее. B знает, что именно A отправил это сообщение когда то в прошлом (так как оно зашифровано ключом Kas) но не то, что оно последнее, следовательно S не доверяет тому, что A непременно хочет продолжать использовать ключ Kab. Это и есть возможность совершить атаку на протокол: атакующая сторона, которая может перехватить сообщение, может также угадать один из старых сессионных ключей Kab. (процесс угадываения может отнять много времени.) Далее злоумышленник повторяет сообщение {t, key(Kaи, A↔B)}, посылая его на сервер S. Если часы не синхронизированы (это может быть частью такой атаки), S может поверить этому старому сообщению и посчитать, что B использует старый скомпрометированный ключ снова. В приведённом ниже исходном документе «Logic of authentication» (ссылка ниже), приведён анализ протокола Kerberos и двух версий протокола Andrew Project RPC (один из них некорректный).
Логика Бэрроуза — Абади — Нидхэма.