3.4 Формальный анализ протоколов проверки подлинности и обмена ключами

Проблема выделения безопасного сеансового ключа для пары компьютеров (или людей) в сети настолько фундаментальна, что стала причиной многих исследований. Некоторые исследования заключались в разработке протоколов, подобных рассматриваемым в разделах 3.1, 3.2 и 3.3. Это, в свою очередь, привело к появлению более важной и интересной задачи: формальному анализу протоколов проверки подлинности и обмена ключами. Иногда прорехи в протоколах, кажущихся вполне надежными, обнаруживались спустя много лет после их разработки, и разработчикам потребовались средства, позволяющие сразу же проверять безопасность протокола. Хотя большая часть этого инструментария применима и к более общим криптографическим протоколам, особое внимание уделялось проверке подлинности и обмену ключами. Существует четыре основных подхода к анализу криптографических протоколов [1045]:

1. Моделирование и проверка работы протокола с использованием языков описания и средств проверки, не разработанных специально для анализа криптографических протоколов.

2. Создание экспертных систем, позволяющих конструктору протокола разрабатывать и исследовать различные сценарии.

3. Выработка требований к семейству протоколов, используя некую логику для анализа понятий "знание" и "доверие".

4. Разработка формальных методов, основанных на записи свойств криптографических систем в алгебраическом виде.

Полное описание этих четырех подходов и связанных с ними исследований выходит за рамки данной книги. Хорошее введение в эту тему дано в [1047, 1355], я же собираюсь коснуться только основных вопросов.

Первый из подходов пытается доказать правильность протокола, рассматривая его как обычную компьютерную программу. Ряд исследователей представляют протокол как конечный автомат [1449, 1565], другие используют расширения методов исчисления предиката первого порядка [822], а третьи для анализа протоколов используют языки описания [1566]. Однако, доказательство правильности отнюдь не является доказательством безопасности, и этот подход потерпел неудачу при анализе многих "дырявых" протоколов. И хотя его применение поначалу широко изучалось, с ростом популярности третьего из подходов работы в этой области были переориентированы.

Во втором подходе для определения того, может ли протокол перейти в нежелательное состояние (например, потеря ключа), используются экспертные системы. Хотя этот подход дает лучшие результаты при поиске "дыр", он не гарантирует безопасности и не предоставляет методик разработки вскрытий. Он хорош для проверки того, содержит ли протокол конкретную "дыру", но вряд ли способен обнаружить неизвестные "дыры" в протоколе. Примеры такого подхода можно найти в [987, 1521], а в [1092] обсуждается экспертная система, разработанная армией США и названная Следователем (Interrogator).

Третий подход гораздо популярнее. Он был впервые введен Майклом Бэрроузом (Michael Burrows), Мартином Абэди (Martin Abadi) и Роджером Неедхэмом. Они разработали формальную логическую модель для анализа знания и доверия, названную БАН-логикой [283, 284]. БАН-логика является наиболее широко распространена при анализе протоколов проверки подлинности. Она рассматривает подлинность как функцию от целостности и новизны, используя логические правила для отслеживания состояния этих атрибутов на протяжении всего протокола. Хотя были предложены различные варианты и расширения, большинство разработчиков протоколов до сих пор обращаются к оригинальной работе.

БАН-логика не предоставляет доказательство безопасности, она может только рассуждать о проверке подлинности. Она является простой, прямолинейной логикой, легкой в применении и полезной при поиске "дыр". Вот некоторые предложения БАН-логики:

Алиса считает X. (Алиса действует, как если бы X являлось истиной.)

Алиса видит X. (Кто-то послал сообщение, содержащее X, Алисе, которая может прочитать и снова передать X - возможно после дешифрирования.)

Алиса сказала X. (В некоторый момент времени Алиса послала сообщение, которое содержит предложение X. Не известно, как давно было послано сообщение, и было ли оно послано в течение текущего исполнения протокола. Известно, что Алиса считала X, когда говорила X.)

X ново. (X никогда не было послано в сообщении до текущего выполнения протокола.)

И так далее. БАН-логика также предоставляет правила для рассуждения о доверии протоколу. Для доказательства чего-либо в протоколе или для ответа на какие-то вопросы к логическим предложениям о протоколе можно применить эти правила. Например, одним из правил является правило о значении сообщения:

ЕСЛИ Алиса считает, что у Алисы и Боба общий секретный ключ, K, и Алиса видит Х, шифрованное K, и Алиса не шифровала X с помощью K, ТО Алиса считает, что Боб сказал X.

Другим является правило подтверждения метки времени:

ЕСЛИ Алиса считает, что X могло быть сказано только недавно, и, что Боб X когда-то сказал X, ТО Алиса считает, что Боб считает X.

БАН-анализ делится на четыре этапа:

1. Преобразуйте протокол к идеальной форме, используя описанные выше предложения.

2. Добавьте все предположения о начальном состоянии протокола.

3. Присоедините логические формулы к предложениям, получая утверждения о состоянии системы после каждого предложения.

4. Примените логические постулаты к утверждениям и предположениям, чтобы раскрыть состояние доверия участников протокола.

Авторы БАН-логики "рассматривают идеализированные протоколы как более ясные и полные описания, чем традиционные, найденные в литературе..." [283, 284]. Другие исследователи не так оптимистичны и подвергают это действие критике, так как при этом реальный протокол может быть искажен [1161, 1612]. Дальнейшие споры отражены в [221, 1557]. Ряд критиков пытается показать, что БАН-логика может и получить очевидно неправильные характеристики протоколов [1161] - см. контрдоводы в [285, 1509] - и что БАН-логика занимается только доверием, а не безопасностью [1509]. Подробное обсуждение приведено в [1488, 706, 1002].

Несмотря на эту критику БАН-логика достигла определенных успехов. Ей удалось обнаружить "дыры" в нескольких протоколах, включая Needham-Schroeder и раннюю черновую версию протокола CCITT X.509 [303]. Она обнаружила избыточность во многих протоколах, включая Yahalom, Needham-Schroeder и Kerberos. Во многих опубликованных работах БАН-логика используется для заявления претензии о безопасности описываемых протоколов [40, 1162, 73].

Были опубликованы и другие логические системы, некоторые из них разрабатывались как расширения БАН-логики [645, 586, 1556, 828], а другие основывались на БАН-логике для исправления ощутимых слабостей [1488, 1002]. Из них наиболее успешной оказалась CNY [645], хотя у нее есть ряд изъянов [40]. В [292,474] к БАН-логике с переменным успехом были добавлены вероятностные доверия. Другие формальные логики описаны в [156, 798,288]. [1514] пытается объединить черты нескольких логик. А в [1124, 1511] представлены логики, в которых доверия изменяются со временем.

Четвертый подход к анализу криптографических протоколов предлагает моделировать протокол как алгебраическую систему, выразить состояние знания участников о протоколе и затем проанализировать достижимость определенных состояний. Этот подход пока не привлек столько внимания, как формальная логика, но состояние дел меняется. Он впервые был использован Майклом Мерриттом [1076], который показал, что для анализа криптографических протоколов можно использовать алгебраическую модель. Другие подходы рассмотрены в [473, 1508, 1530, 1531, 1532, 1510, 1612].

Анализатор протоколов Исследовательской лаборатория ВМС (Navy Research Laboratory, NRL), возможно, является наиболее успешным применением этих методов [1512, 823, 1046, 1513]. Он был использован для поиска как новых, так и известных "дыр" во множестве протоколов [1044, 1045, 1047]. Анализатор протоколов определяет следующие действия:

• Принять (Боб, Алиса, M, N). (Боб принимает сообщение M как пришедшее от Алисы в течение локального раунда Боба N.)

• Узнать (Ева, M). (Ева узнает M.)

• Послать (Алиса, Боб, Q, M). (Алиса посылает M Бобу в ответ на запрос, Q.)

• Запросить (Боб, Алиса, Q, N). (Боб посылает Q Алисе в течение локального раунда Боба N.)

Используя эти действия, можно задать требования. Например:

• Если Боб принял сообщение M от Алисы в какой-то прошедший момент времени, то Ева не знает M в какой-то прошедший момент времени.

• Если Боб принял сообщение M от Алисы в течение локального раунда Боба N, то Алиса послала M Бобу в ответ на запрос Боба в локальном раунде Боба N.

Для анализа Анализатором протоколов NRL исследуемый протокол должен быть описан с помощью приведенных конструкций. Затем выполняются четыре фазы анализа: определение правил перехода для честных участников, описание операций, возможных и для полностью честных, и для нечестных участников, описание базовых блоков протокола и описание правил преобразования. Смысл всего этого в том, чтобы показать, что данный протокол удовлетворяет необходимым требованиями. Использование инструментов, подобных Анализатору протоколов NRL, в итоге могло бы привести к созданию протокола, который был бы обоснованно признан безопасным.

Хотя формальные методы в основном применяются к уже существующим протоколам, сегодня есть тенденция использовать их и при проектировании протоколов. Ряд предварительных шагов в этом направлении сделан в [711]. Это же пытается сделать и анализатор протоколов NRL [1512, 222, 1513].

Применение формальных методов к криптографическим протоколам представляет собой качественно новую идею, и трудно обрисовать, к чему может привести ее реализация. С этой точки зрения слабейшим звеном кажется процесс формализации.