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

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

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

Проверка происхождения сообщения
Проверка актуальности сообщения
Проверка достоверности происхождения.

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

Тип языка

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

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

Логика BAN вдохновила множество других подобных формализмов, таких как логика GNY . Некоторые из них пытаются исправить одну слабость логики БАН: отсутствие хорошей семантики с ясным значением с точки зрения знаний и возможных вселенных. Однако, начиная с середины 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 верит свежему ( X ), то P верит ( Q верит X ).

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

Если P считает ( Q обладает юрисдикцией над X ) и P считает ( Q считает X ), то P считает X
Есть еще несколько технических постулатов, касающихся композиции сообщений. Например, если P считает, что Q сказал ⟨ X , Y ⟩ , конкатенацию X и Y , то P также считает, что сказал X , и P также считает, что Q сказал Y. Q

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

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

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

А → S : А , Т _А , CAB , B } _{CAS _{}

S → B : { T _S , K _AB , A} _{K _BS}

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

А Ключ KAS ₎ , A ↔ S верит (

S считает ключом KAS ₎ , A ↔ S (

B считает ключом ( K _BS , B ↔ S )

S считает ключом( K _BS , B ↔ S )

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

А верит в ( KAB _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 считает ключом KAB _A , B ↔ ( )

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

1 А → S : { т , ключ ( K _AB , А ↔ 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 ↔ Б )} . (В частности, С. полагает, что сообщение не было сфабриковано каким-то злоумышленником.)

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

С считает свежим( т )

Поскольку S верит в свежесть( 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 , и 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 считает, ключ( KAB _что , A ↔ B ) ). Поскольку B считает, что S авторитетен в отношении того, во что верит A , B считает, что ( A считает, что ключ ( K _AB , A ↔ B ) ). Поскольку B считает, что A является авторитетным в отношении сеансовых ключей между и B , B верит в key( KAB _, A A ↔ B ) . Теперь B может связаться с A напрямую, используя K _AB в качестве секретного сеансового ключа.

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

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

Ссылки

^ «Курсовый материал по логике БАН» (PDF) . UT Остин CS.
^ Моннио, Дэвид (1999). «Процедуры принятия решений для анализа криптографических протоколов с помощью логики доверия» . Материалы 12-го семинара IEEE по основам компьютерной безопасности . стр. 44–54. дои : 10.1109/CSFW.1999.779761 . ISBN 0-7695-0201-6 . S2CID 11283134 .
^ Бойд, Колин; Мао, Вэньбо (1994). «Об ограничении логики БАН» . Семинар EUROCRYPT '93 по теории и применению криптографических методов на основе достижений криптологии : 240–247. ISBN 9783540576006 . Проверено 12 октября 2016 г.

Дальнейшее чтение

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

[1] «Курсовый материал по логике БАН» (PDF) . UT Остин CS.

[2] Моннио, Дэвид (1999). «Процедуры принятия решений для анализа криптографических протоколов с помощью логики доверия» . Материалы 12-го семинара IEEE по основам компьютерной безопасности . стр. 44–54. дои : 10.1109/CSFW.1999.779761 . ISBN 0-7695-0201-6 . S2CID 11283134 .

[3] Бойд, Колин; Мао, Вэньбо (1994). «Об ограничении логики БАН» . Семинар EUROCRYPT '93 по теории и применению криптографических методов на основе достижений криптологии : 240–247. ISBN 9783540576006 . Проверено 12 октября 2016 г.

[1]

[2]

[3]