Интернет магазин китайских планшетных компьютеров

Компьютеры - Логика Бэрроуза-Абади-Нидхэма - Анализ «протокола Лягушки» с помощью BAN-логики

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

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

A доверяет key

S доверяет key

B доверяет key

S доверяет key

Агент A хочет начать защищённую переписку с агентом B. Для этого он генерирует ключ K_as, для связи с B. A считает этот ключ безопасным, так он сам его сгенерировал: A доверяет key

B готов использовать этот ключ, пока он уверен, что этот ключ пришёл от A: B доверяет)

Более того, B готов доверять тому, что S будет безошибочно передавать ключи от A: B доверяет))

Это значит, что если B доверяет тому, что S доверяет тому, что A хочет использовать собственный ключ для связи с B, будет доверять S и полагаться на него. Цель получить B доверяет key

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

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