Вопрос или проблема
Читая о протоколах аутентификации, я увидел на Википедии о логике Бурроуса-Абади-Нидхэма:
В некоторых случаях протокол считался безопасным по анализу BAN, но на самом деле был небезопасен.[3] Это привело к отказу от логик семейства BAN в пользу методов доказательства, основанных на стандартном рассуждении о инварианте.[citation needed]
Затем в этой статье Сиверсона я вижу:
В ответ на это разнообразие Сиверсон и ван Оорсхот разработали логику SVO, которая была предназначена для объединения вышеперечисленных предшественников [SvO94, SvO96]
Это довольно технический материал — существует ли более простое объяснение того, как логика SVO улучшает BAN? Я также задаюсь вопросом, в какой степени логика, основанная на BAN, действительно “отказана” в компьютерной безопасности.
Как логика SVO улучшает BAN?
SVO изменяет различные аспекты BAN, такие как нотация, аксиомы и этапы анализа. Расширенная нотация и аксиомы делают логику SVO более выразительной. Привожу два примера, где SVO является сильнее чем BAN.
1. Инвалидация небезопасных протоколов
Нотация SVO включает в себя следующее в дополнение к нотации BAN:
- P имеет X
Теперь рассмотрим протокол Нессета.
В упомянутой вами статье говорится:
SVO содержит как отрицание, так и возможность выражать владение. Она может выразить, кому не следует получать ключи в протоколе Нессета.
Точнее, если мы не хотим, чтобы противник имел ключи, мы должны предполагать:
Мы знаем, что предположение выше неверно. На самом деле, абсолютно противоположное верно. Если мы предполагаем противника Долева-Йао, мы можем вывести следующее:
С помощью приведенного выше вывода мы можем использовать SVO, чтобы доказать, что протокол небезопасен. Мы не могли бы сделать это с использованием логики BAN.
2. Валидация протоколов на основе Диффи-Хеллмана
SVO имеет Аксиому Соглашения о Ключах.
Эта аксиома делает логику SVO подходящей для анализа протоколов обмена ключами на основе Диффи-Хеллмана. Мы не можем применять BAN для таких протоколов.
В какой степени логика, основанная на BAN, отвергнута в компьютерной безопасности?
Логика BAN не отвергнута. Исследователи все еще используют ее для проверки определенных протоколов. Вы можете найти недавние статьи с ее использованием на Google Schoolar.
Ответ или решение
Различия между логикой SVO и логикой BAN: детальный обзор
Когда речь идет о логических системах для анализа протоколов аутентификации, логика Burrows-Abadi-Needham (BAN) и логика Syverson-van Oorschot (SVO) занимают центральное место. В этом обзоре мы рассмотрим ключевые отличия между этими двумя логическими системами, подчеркнув, как SVO улучшает и развивает идеи, заложенные в BAN.
Как логика SVO улучшает логику BAN?
Логика SVO вобрала в себя множество улучшений и изменений по сравнению с BAN, включая расширения в нотации, аксиомах и анализе шагов. Вот два важных аспекта, в которых SVO является сильнее чем BAN:
1. Опровержение ненадежных протоколов
Логика SVO вводит дополнительные нотации, которые отсутствуют в BAN. Например, SVO позволяет выразить следующее:
- P имеет X
- ¬φ (не φ, т.е., логическая отрицание)
Это позволяет более точно формулировать предположения о том, кто не должен иметь доступ к ключам в определенных протоколах. Рассмотрим протокол Nessett:
- (A \rightarrow B : (nA, k{AB})_{k_A^{-1}})
- (B \rightarrow A : (nB){k_{AB}})
Согласно логике SVO, можно выразить, что злоумышленник не должен иметь доступ к секретному ключу (k_{AB}) с помощью формулы:
[
¬(E \text{ имеет } k_{AB})
]
Тем не менее, предполагая наличие противника в модели Долева-Яо (Dolev-Yao), можно показать, что на самом деле злоумышленник может получить доступ к этому ключу. SVO позволяет произвести вывод о том, что протокол Nessett является ненадежным, в то время как логика BAN не предоставляет таких возможностей.
2. Проверка протоколов на основе Диффи-Хеллмана
Логика SVO вводит новую аксиому, называемую Аксисом Соглашения по Ключу:
[
(PK_\delta(P, kP) \wedge PK\delta(Q, kQ)) \rightarrow P \underset{F{0(k_P, k_Q)}}{\leftrightarrow} Q
]
Эта аксиома делает SVO подходящей для анализа протоколов обмена ключами на основе метода Диффи-Хеллмана. В логике BAN такая возможность отсутствует, что ограничивает её применимость в современных протоколах.
Насколько широко логика BAN всё еще используется в компьютерной безопасности?
Несмотря на критику и появление новых логик, BAN не была полностью abandoned (брошена) в области компьютерной безопасности. Многие исследователи продолжают применять BAN для проверки определенных протоколов. Например, поиск недавних публикаций, основанных на логике BAN, может быть осуществлён через Google Scholar. Это говорит о том, что, хотя SVO и предлагает улучшения, логика BAN все еще актуальна для некоторых специфических задач.
Заключение
Итак, различия между логикой SVO и логикой BAN можно описать как улучшение выразительности, возможность анализа ненадежных протоколов и проверку систем на основе современных методов обмена ключами. Логика SVO предоставляет более мощные инструменты и возможности для анализа современных протоколов аутентификации, тогда как BAN продолжает сохранять свою актуальность в определённых контекстах.
Использование этих логик требует глубокого понимания теоретических основ и практических применений, чтобы обеспечить надежную защиту цифровых систем.