Современная криптография - Венбо Мао
ISBN 5-8459-0847-7
Скачать (прямая ссылка):
Благодаря природе связи доказать стойкость протокола аутентификации намного сложнее, чем стойкость криптографического алгоритма. Подход Белларе и Роджуэя был шагом в правильном направлении. Их идеи в настоящее время развиваются многими последователями.
17.4 Доказательство корректности протоколов с помощью символических манипуляций 1
Доказательство корректности протоколов с помощью символических манипу-| ляций основано на формальных методах исследований, принятых в компьютерных науках. В этих случаях стойкость демонстрируется с помощью операций над абстрактными символами. В одних работах для анализа стойкости используются формальные логические системы, а в других — автоматизированные средства для доказательства математических теорем, возвращающее результат ДА/НЕТ.
Глава 17. Формальные методы анализа протоколов аутентификации
655
17.4.1 Доказательство теорем
Подход, основанный на доказательстве теорем, состоит в следующем.
• Определяется множество алгебраических или логических символов, использующихся для описания поведения системы или утверждений, которые могут быть как предпосылками (известными формулами), так и следствиями (результатами вывода).
• Постулируется набор аксиом, устанавливающих правила вывода формул.
• Поведение системы описывается в виде набора доказываемых теорем.
• В доказательстве теорем используются предпосылки и аксиомы, а также ранее доказанные теоремы.
Иногда процесс доказательства можно автоматизировать с помощью определенных правил применения аксиом и теорем. Как правило, для автоматизации доказательства применяются правила подстановки термов (term rewriting rules). Например, широко известно, что любое булевское выражение можно механически переписать в "конъюнктивной нормальной форме" (conjunctive normal form — CNF). Однако в большинстве случаев автоматизированное доказательство теорем является слишком долгим и утомительным. Хорошо известно, что длина автоматизированного доказательства может оказаться неполиномиально ограниченной величиной, зависящей от размера доказываемой формулы (понятие неполиномиально ограниченной величины введено в разделе 4.6).
Несмотря на то что автоматизированные доказательства теорем часто оказываются слишком длинными, этот метод нашел широкое применение при исследовании систем, поведение которых невозможно описать с помощью конечной структуры (например, системы с бесконечным пространством состояний). Примером такого доказательства является метод математической индукции. Однако для получения короткого доказательства необходимо вмешательство человека.
Необходимым свойством алгебраического доказательства теоремы является аксиоматическая система, сохраняющая так называемое свойство конгруэнтности (congruence property). Это свойство является обобщением понятия сравнимости между целыми числами, определенного в разделе 4.3.2.5, на произвольные алгебраические структуры. Бинарное отношение R, определенное в алгебраической структуре, называется конгруэнтностью, если для любой бинарной операции о над элементами этой структуры из условий
R(x, и) и R(y, v)
следует утверждение
R{x о у, и о v).
Конгруэнтность иногда называют также свойством подстановки или замены (sub-stitutability). В таком случае один компонент системы можно заменить другим,
656
Часть V. Методы формального доказательства стойкости
не нарушая согласованности между элементами системы. Без этого автоматизированное доказательство теорем становится необоснованным. По этой причине свойство подстановки часто называют свойством семантической непротиворечивости (soundness) системы для доказательства теорем. Семантически противоречивое доказательство теорем лишено смысла, поскольку может привести к ложному утверждению, например, к абсурдному выводу "1 = 2".
Полнота (completeness) системы для доказательства теорем зависит от того, обладает ли выбранная система аксиом свойством семантической истинности. Если система для доказательства теорем является полной, любое семантически истинное утверждение должно быть доказуемым, т.е. должна существовать последовательность применения аксиом, демонстрирующая синтаксическую истинность утверждения. Полнота системы желательна, но, как правило, автоматизированные системы доказательства теорем ею не обладают.
Целью доказательства теоремы является демонстрация требуемых свойств системы или обнаружение ошибок. Именно поэтому нежелательное свойство нельзя сформулировать в виде теоремы. Несмотря на это, невозможность доказать требуемое свойство при доказательстве теоремы часто приводит к выявлению скрытых ошибок.
Протоколы аутентификации представляют собой чрезвычайно уязвимые системы. Как правило, невозможно сначала разработать неуязвимый протокол, а потом формально доказать его стойкость с помощью доказательства теоремы. Следовательно, этот подход необходимо применять уже на этапе разработки протокола.
17.4.2 Логика аутентификации
Одной из первых попыток формализации понятия корректности протокола была "логика аутентификации", предложенная Барроузом (Burrous), Абади и Нид-хемом и получившая сокращенное название логики BAN [61]. Логику BAN можно рассматривать как один из возможных способов доказательства теорем. Она представляет собой набор логических формул, моделирующих следующие действия участников протокола на основе интуитивных рассуждений. Формулы состоят из следующих выражений и компонентов.
