Постулаты BAN-логики



         

Постулаты BAN-логики


При анализе протоколов аутентификации следует различать два времени: прошлое и настоящее. Настоящее время начинается на старте работы изучаемого протокола. Все убеждения, имеющие место в настоящем, являются неизменными до завершения выполнения протокола; кроме того, допускается, что когда пользователь P заявляет X, то он действительно доверяет X.

Зашифрованное сообщение представляется как логическое утверждение, зашифрованное на ключе шифрования. Шифрованное сообщение не может быть расшифровано пользователем, не имеющим ключа. Ключ не может быть получен из шифрованного сообщения. Каждое шифрованное сообщение содержит избыточность достаточную, чтобы пользователь, расшифровывающий данное сообщение, имел возможность проверить, что он использовал правильный ключ. Кроме того, сообщения содержат информацию, необходимую пользователю, чтобы обнаружить и проигнорировать его собственные сообщения.

Правила значения сообщения имеют отношение к интерпретации сообщений. Два первых правила позволяют интерпретировать шифрованные сообщения, а третье правило позволяет интерпретировать сообщения с секретами. Они все объясняют процесс получения доверия о происхождении сообщений.

Для общих ключей формула выглядит следующим образом:

.

Если пользователь P верит, что ключ K есть только у него и Q, и получает сообщение X, шифрованное на ключе K, то P верит, что это Q прислал сообщение X. Чтобы данное правило имело смысл, необходимо гарантировать, что пользователь P не послал сообщение X сам себе.

Для общих секретов формула выглядит следующим образом:

.

Если пользователь P верит, что секрет Y есть только у него и у пользователя Q, и получает

, то P верит, что это пользователь Q прислал X.

Правило проверки нонсов:

.

Если пользователь P верит, что сообщение X является свежим и что его отправил пользователь Q, то P верит, что Q доверяет X. Для простоты, X должно быть открытым текстом и не должно включать никаких шифрованных подстрок.

Правило полномочий указывает, что если P верит, что Q создал утверждение X, и P доверяет Q, то P убеждён в истинности X:




Содержание    Вперед