Введение
Логика Бэрроуза–Абади–Нидэма (также известная как логика BAN) — это набор правил для определения и анализа протоколов обмена информацией. В частности, логика BAN помогает пользователям определить, является ли обменянная информация достоверной, защищена ли она от перехвата, или и то, и другое. Логика BAN исходит из предположения, что все обмены информацией происходят в среде, уязвимой для подмены и публичного наблюдения. Это привело к появлению популярного принципа безопасности: "Не доверяй сети". Типичная последовательность действий в логике BAN включает три шага:
1. Проверка подлинности источника сообщения.
2. Проверка актуальности сообщения.
3. Проверка достоверности источника.
Verification of message origin
Verification of message freshness
Verification of the origin's trustworthiness. BAN logic uses postulates and definitions – like all axiomatic systems – to analyze authentication protocols. Use of the BAN logic often accompanies a security protocol notation formulation of a protocol and is sometimes given in papers.
Логика BAN использует постулаты и определения – как и любая аксиоматическая система – для анализа протоколов аутентификации. Применение логики BAN часто сопровождается формальным описанием протокола безопасности и иногда приводится в научных публикациях.
Verification of message origin
Verification of message freshness
Verification of the origin's trustworthiness. BAN logic uses postulates and definitions – like all axiomatic systems – to analyze authentication protocols. Use of the BAN logic often accompanies a security protocol notation formulation of a protocol and is sometimes given in papers.
Тип языка
Логика BAN и логики того же семейства являются разрешимыми: существует алгоритм, который, получив гипотезы BAN и предполагаемое заключение, определяет, выводимо ли заключение из гипотез. Предлагаемые алгоритмы используют вариант магических множеств.
Альтернативы и критика
Логика BAN вдохновила множество других подобных формализмов, таких как логика GNY. Некоторые из них пытаются устранить один из недостатков логики BAN: отсутствие надлежащей семантики с чётким смыслом в терминах знаний и возможных миров. Однако, начиная с середины 1990-х годов, криптопротоколы стали анализировать в операционных моделях (исходя из предположения о совершенной криптографии) с использованием средств проверки моделей, и в протоколах, которые были "проверены" с помощью логики BAN и связанных формализмов, было обнаружено множество ошибок. В некоторых случаях протокол признавался безопасным на основе анализа BAN, но фактически оказывался уязвимым. Это привело к отказу от логик семейства BAN в пользу методов доказательства, основанных на стандартном инвариантном анализе.