BAN-логика

BAN-логика

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

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

Для анализа протоколов аутентификации BAN логика, как и все формальные теории, использует аксиомы и определения. BAN логика часто сопровождает формальные описания протоколов защиты информации.

Тип языка и альтернативы

BAN логика и логики её семейства являются разрешимыми: существует алгоритм, проверяющий правильность выводов, сделанных с помощью BAN логики из гипотез. BAN логика является основой других формальных систем, некоторые из них пытаются устранить слабое место 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 не отправлялось ни в одном сообщении.
• key(K, P↔Q): P и Q могут связываться с помощью ключа 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. Используя эту нотацию, можно формализовать описания протоколов аутентификации. Также с помощью этих утверждений можно проверить, что данные клиенты доверяют использованию данных ключей для связи.

Анализ «протокола Лягушки» с помощью BAN-логики

Очень простой протокол аутентификации — «протокол Лягушки» — позволяет двум агентам, A и B, установить защищённое соединение, используя сервер S, которому они оба доверяют, и синхронизированные часы. Используя стандартную нотацию, протокол может быть записан следующим образом:

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

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

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

A доверяет key(K_as, A↔S)

S доверяет key(K_as, A↔S)

B доверяет key(K_bs, B↔S)

S доверяет key(K_bs, B↔S)

Агент A хочет начать защищённую переписку с агентом B. Для этого он генерирует ключ K_as, для связи с B. A считает этот ключ безопасным, так он сам его сгенерировал: A доверяет key(K_as, 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(K_ab, A↔B)

А получает текущее время t с часов, и посылает следующее сообщение: 1 A->S: {t, key(K_ab, A↔B)}K_as

Это значит, что он посылает сессионный ключ и текущее время на сервер S, шифруя их своим ключом аутентификации на сервере S — K_as. Как только S доверяет fresh(t) и S доверяет (A сказал {t, key(K_ab, A↔B)}), S доверяет тому, что A доверяет тому, что key(K_ab, A↔B). (В частности, S доверяет тому, что сообщение не является повтором атакующей стороны, перехватившей его в прошлом). После этого S отправляет ключ B: 2 S->B: {t, A, A доверяет key(K_ab, A↔B)}K_bs Так как сообщение 2 зашифровано ключом K_bs, и B доверяет key(K_bs, B↔S), B теперь доверяет тому, что S сказал {t, A, A доверяет key(K_ab, A↔B)}. Так как часы синхронизированы, B доверяет fresh(t), и следовательно доверяет fresh(A доверяет key(K_ab, A↔B)). Из того, что B доверяет тому что утверждения S свежие, B доверяет тому, что S доверяет (A доверяет key(K_ab, A↔B)). Так как B доверяет тому, что S знает о том, чему доверяет A, B доверяет (A доверяет key(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)}, но он не может больше полагать, что оно свежее. B знает, что именно A отправил это сообщение когда то в прошлом (так как оно зашифровано ключом K_as) но не то, что оно последнее, следовательно S не доверяет тому, что A непременно хочет продолжать использовать ключ K_ab. Это и есть возможность совершить атаку на протокол: атакующая сторона, которая может перехватить сообщение, может также угадать один из старых сессионных ключей K_ab. (процесс угадываения может отнять много времени.) Далее злоумышленник повторяет сообщение {t, key(K_aи, A↔B)}, посылая его на сервер S. Если часы не синхронизированы (это может быть частью такой атаки), S может поверить этому старому сообщению и посчитать, что B использует старый скомпрометированный ключ снова. В приведённом ниже исходном документе «Logic of authentication» (ссылка ниже), приведён анализ протокола Kerberos и двух версий протокола RPC (один из них некорректный).

Литература

• David Monniaux, Decision Procedures for the Analysis of Cryptographic Protocols by Logics of Belief, in Proceedings of The 12th Computer Security Foundations Workshop, 1999. (Online).

Ссылки

• UT Austin CS course material on BAN logic (PDF)
• Логика аутентификации (зеркало), первоисточник Burrows, Abadi, and Needham.
• Источник: The Burrows-Abadi-Needham logic
• BAN logic in context, from UT Austin CS (PDF)

Связать^?