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

Компьютеры - Логика Бэрроуза-Абади-Нидхэма - Тип языка и альтернативы

BAN логика и логики её семейства являются разрешимыми: существует алгоритм, проверяющий правильность выводов, сделанных с помощью BAN логики из гипотез. BAN логика является основой других формальных систем, некоторые из них пытаются устранить слабое место BAN логики: отсутствие хороших, понятных семантик.

Основные правила

Основные правила и их следствия приведены ниже:

• 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 не отправлялось ни в одном сообщении.
• key: P и Q могут связываться с помощью ключа K.

Суть этих определений можно понять из следующих логических выражений: Если P доверяет key, и P видит {X}_K, тогда P доверяет. Если P доверяет и P доверяет fresh, тогда P доверяет. Здесь P должен доверять тому, что Х свежее, иначе X может быть старым сообщением, повторённым атакующей стороной.

Если P доверяет и P доверяет, тогда P доверяет X. Также существует ещё несколько технических утверждений, используемых для работы с композицией сообщений. Например, если P доверяет тому, что Q доверяет <X,Y>, тогда P доверяет тому, что Q сказал X и Q сказал Y. Используя эту нотацию, можно формализовать описания протоколов аутентификации. Также с помощью этих утверждений можно проверить, что данные клиенты доверяют использованию данных ключей для связи.