Современная криптография - Венбо Мао
ISBN 5-8459-0847-7
Скачать (прямая ссылка):
Несмотря на это, логика BAN, несомненно, является важной вехой. Она породила формальный подход к анализу протоколов аутентификации.
глава 17. Формальные методы анализа протоколов аутентификации 659
17.5 Методы формального доказательства: исследование состояния системы
Другой подход к формальному анализу сложных систем основан на моделировании поведения конечных систем. В этом случае состояния системы выражаются с помощью определенных отношений. Анализ поведения системы, как правило, сводится к исследованию пространства состояний и проверке заданных отношений. Эта методология называется проверкой моделей (model checking).
Проверка моделей должна гарантировать, что либо нежелательные состояния никогда не возникнут, либо в конце концов система будет находиться в требуемом состоянии. В первом случае говорят, что проверка обеспечивает безопасность (safety) системы, а во втором — живучесть (liveness).
По-видимому, для анализа протоколов аутентификации более предпочтительным является первый подход.
17.5.1 Проверка моделей
Проверка модели сводится к следующим действиям.
• Функционирование конечной системы моделируется с помощью конечной системы переходов, переводящей систему из одного состояния в другое в зависимости от происходящих событий. Такие системы называются "системами помеченных переходов" (labeled transition system — LTS).
— Например, машина Тьюринга Div3, описанная в примере 4.1, представляет собой систему LTS, изменяющую свое состояние в зависимости от бита, считанного со входной ленты.
• Каждое состояние системы LTS выражается с помощью логической формулы.
— Например, каждое состояние машины Div3 можно выразить с помощью пропозиционального логического высказывания в множестве {0,1,2}. Эти утверждения имеют следующий смысл: "считанная строка битов представляет собой целое число, сравнимое с нулем, единицей или двойкой по модулю три соответственно".
• Требуемое свойство системы также явно выражается логической формулой.
— Например, целевое состояние машины Div3 можно выразить утверждением "считанная строка битов представляет собой целое число, кратное трем".
• Осуществляется символическое выполнение системы LTS, которое описывается "следом" ("trace")
7г = /oei/гег - -. enfn,
660
Часть V. Методы формального доказательства стойкости1
где /о,..., fn — логические формулы, a ei,..., еп — события.
• Механическая процедура может проверить, является ли целевая формула логическим следствием формулы в "следе".
— Например, при анализе функционирования машины Div3 можно убедиться, что формула "считанная строка битов представляет собой целое число, кратное трем" является логическим следствием любого конеч-J ного "следа".
Следует отметить, что в отличие от доказательства теорем, описываюш| только желательные свойства, при проверке модели результирующая формула может выражать как желательное, так и нежелательное состояние системы. НЦ пример, утверждение
"Злоумышленнику известен новый сеансовый ключ К"
представляет собой формулу, выражающую нежелательное свойство протоколе распределения сеансовых ключей. Если результирующая формула выражает неже! лательное свойство, то проверка модели создает "след", приводящий к явному описанию системной ошибки. Таким образом, проверку моделей можно прими нять для выявления ошибок, скрытых в системе. Как правило, проверку моделе^ при анализе протоколов аутентификации применяют именно для этой цели.
17.5.1.1 Композиция систем при проверке моделей
При разработке сложных систем их, как правило, конструируют из более п(( стых компонентов.
Например, для создания машины Тьюринга, распознающей строки битов, к] ные шести (назовем эту машину Div6), можно просто сконструировать маш распознающую четные числа (под названием Div2), и скомбинировать ее с машЦ ной Div3, выполнив операцию "конъюнктивной композиции" (conjunctive com sition). Заметим, что разработать машины Div2 и Div3 намного проще, чем созд машину Div6 с нуля.
В рамках конъюнктивной композиции машины Div2 и Div3 должны pal тать синхронно, считывая свои входные ленты, на которых записана одна и же информация, и делая очередной ход. Такая машина распознает число, кра^ ное шести, тогда и только тогда, когда обе составляющие ее машины распознав свои входные числа. Очевидно, что метод композиции позволяет правильно ско! струировать машину Div6 (более простой вариант "конъюнктивной композиции1 описывается в разделе 17.5.3).
Рассмотрим "дизъюнктивную композицию", состоящую из машин Div2 и Di\3 Эта машина распознает строки, кратные двум или трем, т.е. числа из последов тельности
0,2,3,4,6,8,9,10,12,14,15,...
3
Глава 17. Формальные методы анализа протоколов аутентификации 661
Термин "дизъюнктивная композиция" означает, что сложная машина должна прекратить работу, если одна из машин Div2 или Div3 примет положительное решение. Очевидно, что, не прибегая к методу дизъюнктивной композиции, разработать машину, функционирующую столь неуклюже, довольно сложно.
Выявление дефектов в протоколах аутентификации с помощью проверки моделей также можно упростить с помощью метода системной композиции.
