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

Логика Берроуза–Абади–Нидхэма (также известная как логика 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 верит, что key( 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
• Есть несколько других технических постулатов, связанных с составлением сообщений. Например, если P полагает, что Q сказал ⟨ X , Y ⟩ , конкатенацию X и Y , то P также полагает, что Q сказал X , и P также полагает, что Q сказал Y .

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

Очень простой протокол — протокол 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 )

Агент A хочет начать безопасный разговор с 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 AS}

То есть он отправляет выбранный им сеансовый ключ и текущее время на 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 ↔ B )} . (В частности, S полагает, что сообщение не было полностью сфабриковано каким-то злоумышленником.)

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

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

Поскольку 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 верит ключу ( 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 )} , но он больше не может сделать вывод, что t является свежим. Он знает, что A отправил это сообщение в какой-то момент в прошлом (потому что оно зашифровано с помощью K _AS ), но не знает, что это недавнее сообщение, поэтому S не верит, что A обязательно хочет продолжать использовать ключ K _AB . Это напрямую указывает на атаку на протокол: злоумышленник, который может перехватывать сообщения, может угадать один из старых ключей сеанса K _AB . (Это может занять много времени.) Затем злоумышленник воспроизводит старое сообщение { t , key( K _AB , A ↔ B )} , отправляя его S . Если часы не синхронизированы (возможно, как часть той же атаки), S может поверить этому старому сообщению и попросить B снова использовать старый, скомпрометированный ключ.

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

• Берроуз, Майкл ; Абади, Мартин ; Нидхэм, Роджер (1989). «Логика аутентификации». Труды Лондонского королевского общества, серия A. 426 ( 1871): 233. Bibcode : 1989RSPSA.426..233B. CiteSeerX  10.1.1.115.3569 . doi : 10.1098/rspa.1989.0125. S2CID  6937380.
• Источник: Логика Берроуза–Абади–Нидхэма