Анализ криптографических протоколов
АНАЛИЗ КРИПТОГРАФИЧЕСКИХ ПРОТОКОЛОВ
По материалам зарубежной печати рассматривается методика разработки, спецификации и логического анализа криптографических протоколов. Методика позволяет обнаруживать дефекты, порожденные нечеткостью целей участников протокола и логическими ошибками. Возможен анализ безопасности криптографических протоколов против атак, если в число участников протокола включить противника с соответствующей стратегией поведения в протоколе.
1. Типичный протокол предполагает 2 - 3 участников. Пусть это будут пользователи А, В и сервер S. Один из них, например, А, является инициатором запуска протокола. На основании информации, имеющейся у него в памяти, А генерирует информацию для передачи, выполняет над ней некоторую последовательность действий, формирует сообщение и передает его В или S в зависимости от данного протокола.
Пользователь В (сервер S), получив сообщение от А, выполняет над ним соответствующую последовательность действий, регистрирует в своей памяти выделенную информацию. На этом завершается 1-ый шаг протокола, а роль инициатора передается В (S).
Аналогично, пользователь В на основании информации, имеющейся теперь в его памяти, генерирует информацию для передачи, формирует сообщение и передает его А или S в зависимости от данного протокола. После приема сообщения, его обработки и регистрации выделенной информации в памяти получателя завершается 2-ой шаг протокола, и т.д.
Каждый участник по протоколу имеет свою цель, выражающуюся в получении определенной информации. Протокол завершается, когда каждый из участников достигает своей цели. В противном случае протокол обрывается.
2. Для формального описания и анализа протоколов такого типа предлагается модель системы с конечным числом состояний и дискретным временем, измеряемым шагами протокола [1]. Состояние системы
В качестве примера рассмотрим протокол доставки сервером S
ключа Kab пользователям А и В. Начальным состоянием пользователя А является ключ Kas для связи А с S, начальным состоянием пользователя В является ключ Kbs
для связи В с S, начальным состоянием сервера S являются ключи Kas и Kbs для связи S c А
и В. Целью пользователей А и В в протоколе является получение ключа Kab; целью сервера S является генерация ключа Kab и передача его безопасным способом пользователям А и В по открытому каналу связи.
Предполагается, что каждый участник протокола имеет справочник адресов, который также входит в состав начального состояния участника.
1-ый шаг: Пользователь А формирует запрос [А
¦ В], шифрует его на ключе Kas и посылает S сообщение [A ¦ S ¦ Kas {A
¦ B}] ; состояние
А изменяется на
¦ В ], Kas
{А ¦ В }}. Сервер S по адресам А, S в сообщении извлекает Kas
и расшифровывает запрос; состояние S изменяется на
Kas, Kbs , [А ¦ В ], Kas {А ¦ В }}. Состояние В изменяется на
¦ Kas {А
¦ В }]}.
2-ой шаг: Сервер S генерирует ключ Kab
, шифрует его на ключах Kas, Kbs и посылает сообщения [S ¦ A
¦ Kas { Kab
}] и [S ¦ B
¦ Kbs { Kab
}] для А и В; состояние S изменяется на
К полученной информации относится также информация, не адресованная данному участнику протокола, но переданная по открытому каналу связи.
Пользователь А по адресам S, A
сообщения извлекает ключ Kas и расшифровывает ключ Kab; состояние А изменяется на
[S¦A¦Kas{Kab}] , [S¦B¦Kbs{Kab}]}
Пользователь В по адресам S, В
сообщения извлекает ключ Kbs и расшифровывает ключ Kab
; состояние В изменяется на
Цели участников протокола достигнуты; протокол завершается. Анализируя состояния участников протокола, можно убедиться, что ключ Kab известен только А, В и S, если ключ Kas
известен только А и S, а ключ Kbs известен только В и S.
3. До сих пор предполагалось, что участники протокола честно выполняют протокол (нарушителей нет), а противник пассивен, т.е. он только перехватывает все сообщения в канале связи, пытаясь извлечь из них максимум информации, но не вмешиваясь в протокол. Такой противник является четвертым неявным участником протокола, состояние которого также должно учитываться и анализироваться с точки зрения безопасности протокола.
Если же противник активен, то он становится четвертым несанкционированным участником протокола, скрытым для санкционированных участников А, В и S. Такой противник не обязан соблюдать протокол. Он должен только поддерживать видимость нормального хода протокола. Противник Е в протоколе может попеременно играть роль А, В
и S (соответствующие обозначения: Ea, Eb, Es). Он может подставлять вместо сообщений, передаваемых санкционированными участниками, сообщения, переданные в предыдущих запусках протокола, в текущем запуске, или, наконец, он может инициировать от имени А
или В новый запуск протокола до окончания текущего и воспользоваться сообщениями этого параллельного протокола. Еще более сильным противником является такой, который обладает ключом (ключами), действующим или выведенным из действия, причем участники протокола об этом могут не знать, по крайней мере, в течение некоторого времени.
Чтобы иметь возможность анализировать криптографические протоколы с точки зрения безопасности в условиях активных действий противника, понятие состояния участника протокола приходится расширить, дополнив множество сообщений, записанных в его памяти, множеством доверий, т.е. высказываний, выражающих доверие к корреспондентам, к их правам, к наличию у них определенных данных, к ключам и к “свежести” полученных данных, т.е. что эти данные генерированы в ходе текущего протокола и не были использованы ранее.
Множество доверий также состоит из высказываний, заложенных предварительно, и высказываний, полученных в процессе протокола к данному шагу. Последние получаются по правилам вывода, имеющим вид: С1 С2 ... Сn / D, где С1, С2, ..., Сn - условия, D - вывод. Если высказывания С1, С2, ..., Сn находятся во множестве доверий, то высказывание D включается во множестве доверий.
С точки зрения математической логики множество доверий Фa
пользователя А является множеством метасообщений, т.е. множеством высказываний о сообщениях множества
В приведенном выше примере множество доверий Фa
может состоять из высказываний, выражающих доверие к ключу Kas, к серверу S, к его праву генерировать и распределять ключи. Во множестве Фa может не быть высказываний, выражающих доверие к В, к его ключу Kbs, к “свежести” полученного сообщения [S¦A¦Kas{Kab}], поскольку оно могло быть подменено противником на ранее переданное, а отсюда недоверие к ключу Kab. Таким образом, протокол, рассмотренный в примере, не позволяет А и В убедиться ни в “свежести” выделенного ключа Kab, ни в том, что он у них одинаков, а позволяет лишь утверждать, что этот ключ генерирован S, да и то при условии, что до настоящего времени ключи Kas и Kbs
не были скомпрометированы, а ключ Kab содержит достаточно избыточности для практически достоверного опознания его как ключа, а не “шума”, полученного операцией расшифрования.
В процессе протокола число сообщений в состояниях (
случайное число (“нонс”) Na. Сервер отвечает сообщением, шифрованным на ключе Kas, в которое включается Na. Пользователь А может убедиться в “свежести” полученного сообщения, сравнивая хранимое значение Na с полученным, после чего число стирается, а в Ф записывается высказывание: “сообщение ... свежее”. Во множестве доверий Ф могут находиться высказывания вида: “верю ... до тех пор, пока не получу сообщение типа ...”. При получении сообщения такого типа данное высказывание удаляется из Ф. Так, например, доверие к ключу сохраняется до тех пор, пока не поступает сообщение о его компрометации или окончании срока действия.
В качестве множества правил вывода предлагается взять логику BAN [2] с некоторыми модификациями, изложенными в [3].
4. Недостатки протокола, приведенного в примере, можно исправить следующим образом:
Пользователь А формирует запрос ключа для А и В, генерирует нонс Na и все это отправляет серверу S
в шифрованном виде на ключе Kas.
Сервер S генерирует ключ Kab и мог бы послать его отдельно А и В. Однако с целью снижения нагрузки на сервер, S формирует сообщение для А и включает его в сообщение для В, чтобы тот переслал его А. В сообщении для А
содержится нонс Na и ключ Kab, шифрованные на ключе Kas. В сообщении для В также содержится ключ Kab, но шифрованный на ключе Kbs.
Пользователь В вскрывает на ключе Kbs
ключ Kab и сообщение для А, шифрованное на ключе Kas. Чтобы убедиться в “свежести” полученного ключа Kab, оставляя сообщение для А шифрованным только на ключе Kas.
Пользователь А вскрывает сначала свое сообщение на ключе Kas и извлекает Kab и нонс, который сравнивает с Na, чтобы убедиться в “свежести полученного ключа Kab. Далее он вскрывает нонс Nb на ключе Kab и возвращает Nb пользователю В
в перешифрованном виде на ключе Kab.
Пользователь В вскрывает нонс на ключе Kab
и сравнивает его с Nb, тем самым убеждаясь через А в “свежести” ключа Kab, а также в том, что у А этот ключ такой же.
Полная спецификация протокола может быть получена с помощью методики, основные идеи которой изложены в п.п. 1 - 3; при этом построение протокола идет одновременно с анализом на предмет наличия скрытых недостатков.
Если требуется проверить работу протокола в присутствии активного противника с заданной стратегией поведения, то включив противника четвертым участником протокола. можно анализировать безопасность протокола против данной атаки.
5. Как сообщается в [3], на основе логики BAN создана программа “PROLOG”, позволяющая вести логический анализ криптографического протокола после некоторой его идеализации, что является недостатком. В заключении работы [1] выражается намерение создать программу для разработки спецификации и анализа криптографических протоколов по методике, основные идеи которой популярно изложены в п.п. 1 ¸ 3 настоящей статьи. Обе программы явились бы удобным инструментом для разработки и анализа протоколов.
Литература
1. Rubin, Honeyman “Nonmonotonic cryptographic protocols”. Proc.Comp.Sec.Found. Workshop, VII, 1994.
2. Burrows, Abadi, Needham “A logic of authentication”. Report 39, Digital Systems Research Center, California, 1989
3. Kessler, Wedel “ AUTLOG - An advanced logic of authentication” Proc.Comp.Sec.Found. Workshop, VII, 1994.
