Современная криптография - Венбо Мао
ISBN 5-8459-0847-7
Скачать (прямая ссылка):
Глава 17. Формальные методы анализа протоколов аутентификации 663
монстрирующей, что некоторое слово, которое должно быть недоступным Злоумышленнику ("запретным"), становится ему известным.
В NRL-анализаторе протокола определяется набор правил перехода из одного состояния в другое. При определенных условиях правило перехода может "сработать" ("fired").
Для того чтобы правило сработало, должны выполняться два условия.
1. Злоумышленнику приписываются определенные слова.
2. Соответствующие локальные состояния оказываются связанными с определенными значениями.
После применения правила происходит следующее.
1. Законный пользователь выводит определенные слова, которые, таким образом, становятся известными Злоумышленнику.
2. Соответствующие локальные состояния оказываются связанными с новыми значениями.
Слова, связанные с правилом, подчиняются правилам перезаписи термов. Обычно в системе существуют три правила, выражающие понятие равенства, а также тот факт, что шифрование и расшифровка являются обратными функциями. Эти правила выглядят следующим образом.
encrypt(.X, decrypt(A',y)) -»• У
decrypt(.X, encrypt(X, У)) -> Y
id_check(X, X) -* ДА Чтобы выполнить анализ, пользователь посылает NRL-анализатору запрос о состоянии с помощью слов, известных Злоумышленнику (т.е. описание опасного состояния). Затем NRL-анализатор протокола выполняет обратный поиск, пытаясь обнаружить исходное состояние глобальной системы. Для этого программа, написанная на ПРОЛОГЕ, пытается применить к текущему состоянию правую часть правила перезаписи термов и свести ее к левой части, которая описывает предыдущее состояние. Если исходное состояние обнаружено, система действительно является нестойкой, в противном случае выполняется попытка доказать, что исходное состояние недостижимо. Для этого программа пытается показать, что любое состояние, из которого можно перейти в указанное состояние, также является недостижимым. Эта разновидность поиска часто приводит к возникновению бесконечного следа, в котором для того, чтобы Злоумышленник распознал слово А, необходимо, чтобы он узнал слово В, а для этого он должен узнать слово С, и т.д. Анализатор обладает определенными возможностями, позволяющими пользователю доказать лемму о недостижимости определенного класса состояний. Цель этой процедуры — уменьшить пространство состояний так, чтобы стал возможным исчерпывающий поиск, позволяющий определить стойкость протокола.
664
Часть V. Методы формального доказательства стойкости
Следует отметить, что основной алгоритм, использованный в NRL-анализато-ре, решает задачу о достижимости определенного состояния. Хорошо известно, что такой алгоритм может оказаться бесконечным. Следовательно, необходимо ограничить количество рекурсивных вызовов некоторых проверяющих процедур. Работа с NRL-анализатором требует от пользователя большой аккуратности при кодировании правил перехода и описании опасного состояния. Кроме того, NRL-анализатор особенно эффективен при проверке протоколов согласования ключей.
NRL-анализатор использовался для проверки большого количества протоколов аутентификации и успешно обнаружил их заранее известные дефекты. В частности, с его помощью были проанализированы протокол аутентификации с открытым ключом Нидхема-Шредера (протокол 2.5) [193] (в этой работе Мидоуз сравнил результаты анализа протокола с помощью NRL-анализатора и метода Лоу, основанного на применении модели FDR [181]), "протокол избирательного вещания" ("selective broadcast protocol"), предложенный Симмонсом (Simmons) [192, 274], протокол Татебаяши-Мацузаки-Ньюмана (Tatebayashi-Matsuzaki-Newman) [160], протокол IKE (Internet Key Exchange, см. раздел 12.2.3) [135,195] и протоколы безопасных электронных транзакций (Secure Electronic Transaction — SET) [196, 259].
17.5.3 Метод CSP
Аббревиатура CSP означает Communicating Sequential Processes (многостадийные процессы передачи информации) и предложена в работе Хоара (Ноаге) [137]. Позднее, уточнив семантику, это название заменили на TCSP (Theoretical CSP — теоретические многостадийные процессы передачи информации) [60]. В конце концов, в работе [138] исследователи вернулись к исходному названию — CSP.
Аббревиатура CSP означает целое семейство систем, называемое алгеброй процессов (process algebra). Это семейство основано на алгебраическом подходе к построению абстрактных вычислительных структур (см. главу 5). Поскольку CSP — это алгебра, она представляет собой язык термов (terms), для которых определены операции (operations). Эти операции подчиняются аксиоме замыкания, т.е. термы CSP образуют множество, замкнутое относительно указанных операций (см. определения 5.1, 5.12 и 5.13 в главе 5). Каждая операция имеет определенный смысл, согласованный со смыслом термов. Множество операций в алгебре CSP будет описано позднее.
17.5.3.1 Действия и события
В алгебре CSP система описывается в терминах действий, которые она может выполнять. Действием (action) называется конечная последовательность событий, возникающих последовательно. В частности, действие может описываться последовательностью нулевой длины, которая означает отсутствие каких-либо действий. Множество всех возможных событий (зафиксированных перед началом
