Современная криптография - Венбо Мао
ISBN 5-8459-0847-7
Скачать (прямая ссылка):
Глава 17. Формальные методы анализа протоколов аутентификации
665
анализа) называется алфавитом процесса (alphabet of a process) и обозначается символом Е. Итак, для любого действия выполняется условие а € ?*. Например, алфавитом процесса может служить множество Е = {0,1}, а действием, выполняемым таким процессом, может являться битовая строка, обладающая определенным свойством.
При моделировании протоколов или систем связи с помощью алгебры CSP действие представляет собой отдельное сообщение или последовательность сообщений. Если М и N — последовательности сообщений, то M.N — также последовательность сообщений. Иногда при записи последовательности сообщений символ "." пропускается.
17.5.3.2 Процессы
Процессы являются компонентами системы. Они представляют собой сущности, описываемые алгеброй CSP в терминах возможных действий, которые они могут выполнять. Основные процессы алгебры CSP и их смысл указаны на рис. 17.1.
• STOP ("отсутствие действий" — бездействие).
• а —> Р("префикс:" сущность выполняет действие а, а затем функционирует, как пользователь Р).
• POQ ("детерминированный выбор": сущность ведет себя как пользователь Р или Q в зависимости от внешнего события).
• PUQ ("недетерминированный выбор": сущность ведет себя как пользователь Р или Q по непонятным причинам).
• /а ("сокрытие:" не обращать внимание на действие а).
• рХ.Р{х) ("рекурсия": повторить действия пользователя Р над переменной X, т.е. рХ.Р(х) =f Р(рХ.Р(х))).
• Р || Q ("параллельность:" пользователи Р и Q одновременно выполняют одно и то же действие).
• РIQ ("чередование:" пользователи Р и Q не обязаны выполнять одно и то же действие).
Рис. 17.1. Язык CSP
Основные операции, перечисленные на рис. 17.1, представляют собой строительные конструкции процессов в алгебре CSP, предназначенные для моделирования и описания функционирования конечной системы. Эти конструкции и семан-
666
Часть V. Методы формального доказательства стойкости
тика операций делают язык CSP достаточно мощным для того, чтобы описывать сложные конечные системы.
Например, машину Тьюринга Div3 из примера 4.1, представляющую собой конечную систему, можно точно описать в виде процесса CSP. В этом описании используются только "префикс", "детерминированный выбор" и "рекурсия".
Пример 17.1. CSP-спецификация машины Тьюринга Div3
Div3 =f So;
So = (0 So) ? (1 -+ Sx) ? ({} STOP); 5id= (0^S2)D(1-+S0); 52^(0^5!) D(1^S2);
Процесс Div3 рекурсивно определен с помощью многих подпроцессов. Все подпроцессы, за исключением операции STOP, реагируют на события из множества ? = {О, I}1. Операция STOP реагирует на пустое действие, прекращая работу машины. Легко убедиться, что машина Div3 функционирует следующим образом:
Div3 = а -» STOP для всех а е DIV3 U {}.
17.5.3.3 "Следы"
Процесс Р представляет собой множество последовательностей возможных событий traces(P). К этому множеству относится также пустой "след" {} и последовательность 1001 (возможный "след" машины Div3).
Операция "." над двумя множествами "следов" ТиТ' определена следуюшим образом.
Т.Т' = {tr.tr' \treTAtr'eГ'} , где операция конкатенации "." определена в разделе 17.5.3.1.
17.5.3.4 Анализ процессов
Процесс Р соответствует языку L (например, его спецификации), если все его "следы" являются частью языка L.
Psat L traces(P) С L.
Процесс Р уточняет процесс Q, если traces(P) С traees(Q). Значит, если процесс Q соответствует языку L (т.е. Q sat L), то процесс Р также соответствует ему.
'Напомним, что в разделе 17.5.3.1 при записи атомарного сообщения {е} скобки пропущены. Все подпроцессы, за исключением операции STOP, реагируют на атомарные события {0} и {1} из алфавита Е*. Процесс So реагирует также на пустое действие {}, которое прекращает работу машины Div3.
Глава 17. Формальные методы анализа протоколов аутентификации
667
Например, справедливо утверждение Div3 satDIV3 U {}, поскольку выполняется условие traces{Div3} = DIV3 U {}. Более того, процесс Div3 уточняет процесс, обрабатывающий все битовые строки. Естественно, процесс STOP уточняет процесс Div3 (вообще говоря, процесс STOP уточняет любой процесс). Немного позднее мы опишем нетривиальный процесс, уточняющий процесс Div3.
Подход, основанный на проверке моделей, позволяет механически проверять отношения между конечными процессами, используя метод уточнения расхождений (Failures Divergences Refinement — FDR), разработанный компанией Formal Systems (Europe) Ltd. Детали этого метода можно найти на Web-странице http: //www. f sel. com/index. html.
17.5.3.5 Композиция систем в алгебре CSP
В разделе 17.5.1.1 указывалось, что композиция систем играет чрезвычайно важную роль в проверке моделей. В алгебре CSP композиция систем достигается с помощью операций "параллельность" и "чередование".
Рассмотрим пример, демонстрирующий эффективность композиции систем в алгебре CSP. В разделе 17.5.1.1 был предложен метод реализации машины Div6, распознающей целые числа, кратные шести. Этот метод рассматривает машину Div6 как совокупность машин Div2 и Div3, обрабатывающих одну и ту же строку. Хотя этот метод достаточно прост, он представляет собой лишь абстрактную идею и не позволяет конкретизировать конструкцию машину Div6.
