Постулаты BAN-логики
При анализе протоколов аутентификации следует различать два времени: прошлое и настоящее. Настоящее время начинается на старте работы изучаемого протокола. Все убеждения, имеющие место в настоящем, являются неизменными до завершения выполнения протокола; кроме того, допускается, что когда пользователь P заявляет X, то он действительно доверяет X.
Зашифрованное сообщение представляется как логическое утверждение, зашифрованное на ключе шифрования. Шифрованное сообщение не может быть расшифровано пользователем, не имеющим ключа. Ключ не может быть получен из шифрованного сообщения. Каждое шифрованное сообщение содержит избыточность достаточную, чтобы пользователь, расшифровывающий данное сообщение, имел возможность проверить, что он использовал правильный ключ. Кроме того, сообщения содержат информацию, необходимую пользователю, чтобы обнаружить и проигнорировать его собственные сообщения.
Правила значения сообщения имеют отношение к интерпретации сообщений. Два первых правила позволяют интерпретировать шифрованные сообщения, а третье правило позволяет интерпретировать сообщения с секретами. Они все объясняют процесс получения доверия о происхождении сообщений.
Для общих ключей формула выглядит следующим образом:
Если пользователь P верит, что ключ K есть только у него и Q, и получает сообщение X, шифрованное на ключе K, то P верит, что это Q прислал сообщение X. Чтобы данное правило имело смысл, необходимо гарантировать, что пользователь P не послал сообщение X сам себе.
Для общих секретов формула выглядит следующим образом:
Если пользователь P верит, что секрет Y есть только у него и у пользователя Q, и получает
Правило проверки нонсов:
Если пользователь P верит, что сообщение X является свежим и что его отправил пользователь Q, то P верит, что Q доверяет X. Для простоты, X должно быть открытым текстом и не должно включать никаких шифрованных подстрок.
Правило полномочий указывает, что если P верит, что Q создал утверждение X, и P доверяет Q, то P убеждён в истинности X:
Неизбежным свойством оператора доверия является то, что пользователь P верит ряду утверждений тогда и только тогда, когда он верит каждому отдельному утверждению. Это обосновывает следующие правила:
Другие аналогичные правила могут быть введены при необходимости.
Если пользователь получает сообщение, то он также получает все поля данного сообщения, если он знает необходимые ключи:
Предполагается, что пользователь P не послал сообщение X сам себе.
Если одна часть формулы является свежей, то целая формула тоже является свежей:
Можно написать и другие аналогичные правила. Например, можно показать, что если утверждение X является свежим, то
Для добавления понятия «хэш-функция» в BAN-логику вводится символ H для представления хэш-функций. Правило получения атрибутов авторства сообщения X из сообщения H(X) будет следующим:
