Современная криптография - Венбо Мао
ISBN 5-8459-0847-7
Скачать (прямая ссылка):
Действительно, поиск ошибок в протоколах аутентификации представляет собой процесс проверки системы, которая всегда крупнее, чем системы, имитирующие отдельные части протокола. В лучшем случае, спецификация протокола только описывает законные действия пользователей. Однако удачная атака всегда описывает поведение более крупной системы, в которой Злоумышленник согласовывает свое поведение с законными пользователями (т.е. обманывает их или незаметно раскрывает секреты).
Следовательно, при анализе протоколов аутентификации с помощью проверки модели необходимо моделировать не только действия законных пользователей, но и типичное поведение Злоумышленника. Каждый из этих компонентов протокола является системой LTS. Эти компоненты объединяются в более сложные системы, а затем подвергаются проверке. Операция композиции в ходе проверки моделей часто моделирует асинхронную связь между компонентами системы. Термин "асинхронный" означает, что составная система может выполнять операции в зависимости от действий подсистем. Он описывает ситуацию, в которой поведение Злоумышленника может не зависеть от действий законных пользователей.
В начале раздела мы подчеркнули, что проверка моделей предназначена для анализа конечных систем. При анализе протоколов аутентификации это значит, что Злоумышленник должен быть полиномиально ограниченным: действия, связанные с неограниченной вычислительной мощностью, не рассматриваются.
При проверке моделей часто возникает проблема "комбинаторного взрыва": система отображается в крупную систему LTS, имеющую слишком большое количество состояний, для обработки которых имеющихся вычислительных ресурсов недостаточно. Эта проблема имеет особенно острый характер при анализе крупного программного или аппаратного обеспечения. Такие системы имеют огромное пространство состояний. К счастью, при разумном предположении, что Злоумышленник является полиномиально ограниченным, большинство протоколов аутентификации можно смоделировать с помощью относительно небольших LTS-систем. Следовательно, проверка моделей особенно эффективна при анализе протоколов аутентификации.
Рассмотрим два метода проверки моделей, применяемых при анализе протоколов аутентификации.
662 Часть V. Методы формального доказательства стойкости
17.5.2 NLR-анализатор протоколов
Мидоуз разработал программу, написанную на языке ПРОЛОГ, под названием ] NRL-анализатор протоколов [194]. Здесь аббревиатура NRL означает Naval Research Laboratory of the United States of America (Исследовательская лаборатория J военно-морского флота США).
Как и другие средства для анализа протоколов аутентификации, NRL-анали- I затор протоколов основан на модели Долева-Яо [101] (см. раздел 2.3). Итак, Злоумышленник может контролировать обмен сообщениями в сети, перехватывать их, читать, модифицировать или уничтожать, выполнять преобразование перехваченных сообщений (например, владея правильными ключами, он может выполнять шифрование или расшифровку) и пересылать их другим участникам протокола, маскируясь законным пользователем. Однако вычислительные возможности Злоумышленника полиномиально ограничены. Следовательно, существует определенное множество "слов", которые остаются неизвестными как в начале выполнения протокола, так и после его завершения, если протокол оказался стойким. Эти слова могут быть секретными сообщениями или криптографическими ключами, которые защищаются протоколом. Назовем эти слова "запретными" (forbidden words).
NRL-анализатор протоколов использует метод проверки моделей и являет- 1 ся системой перезаписи термов (term-rewriting system). Он основан на модифицированной модели Долева-Яо, имеющей название "модель перезаписи термов Долева-Яо". Будем считать, что Злоумышленник может манипулировать этой системой. Если целью Злоумышленника является распознавание запретных слов, задача доказательства стойкости протокола формулируется следующим образом: запретные слова должны остаться запретными. И наоборот, доказательство уязвимости протокола означает, что в итоге запретные слова становятся известными Злоумышленнику.
В NRL-анализаторе протоколы моделируются с помощью глобальной конеч- Щ ной системы. Эта система состоит из нескольких локальных подсистем и содержит определенную информацию о состояниях, доступную для Злоумышленника. Каждая локальная подсистема описывает функционирование законного участника протокола. Такой способ конструирования системы следует стандартной методологии создания сложных систем из более простых компонентов (раздел 17.5.1.1).
Включение Злоумышленника в глобальную систему моделирует способ, кото- 9 рым он получает информацию в результате выполнения протокола. Целью Злоумышленника является генерация "запретных" слов путем перевода законных пользователей в определенное нежелательное состояние, противоречащее прото- I колу. Такое состояние называется "опасным". Если протокол содержит ошибку, \ пользователь может оказаться в опасном состоянии. В модели перезаписи термов опасное состояние эквивалентно возникновению последовательности термов, де-
