Современная криптография - Венбо Мао
ISBN 5-8459-0847-7
Скачать (прямая ссылка):
Протокол 17.5. Второй вариант уточненной спецификации протокола аутентификации с открытым ключом Нидхема-Шредера
ПРЕДВАРИТЕЛЬНЫЕ УСЛОВИЯ И ЦЕЛЬ: те же, что и в протоколе 2.5.
1. Алиса —> Бобу: ^{А'д}^ ,Алиса^
2. Боб-.Алисе: Nb}Ka]k ¦
3. Алиса-* Бобу: {Ns}^] .
L J К д
КА
Атака Лоу для этого варианта также не представляет опасности: теперь Злоумышленник даже не в состоянии запустить протокол связи с Бобом.
17.3 Вычислительные аспекты корректных протоколов — модель Белларе-Роджуэя
В главах 14 и 15 изложены идеи доказуемой стойкости, основанные на вычислительной модели, предложенной в знаменитой работе Голдвассера и Микали [125]. В этой модели секретность (один из нескольких аспектов конфиденциальности) подвергается атаке (одной из многочисленных игровых атак, моделирующих с определенной точностью поведение реальных атакующих алгоритмов, стремящихся взломать схемы шифрования с открытым ключом). Доказательство стойкости схем шифрования с открытым ключом к атакам связано с демонстрацией эффективного преобразования (полиномиальной редукции), сводящего атаку к решению одной из трудноразрешимых задач из теории вычислительной сложности. Невозможность решения такой задачи опровергает существование эффективной атаки, т.е. обнаруживает противоречие.
646
Часть V. Методы формального доказательства стойкости
Следовательно, формальное доказательство стойкости в рамках вычислительной модели состоит из трех этапов.
1. Формальное поведение участников протокола и атакующего алгоритма: моделирование, как правило, осуществляется с помощью атакующей игры, в которой участвуют атакующий алгоритм и объект атаки.
2. Формальное определение стойкости: победа атакующего алгоритма в атакующей игре обычно выражается через (значимую) вероятность и оценку (разумной) временной сложности.
3. Формальная демонстрация существования полиномиальной редукции, сводящей атаку к решению трудноразрешимой задачи, которая, как правило, имеет вид математической теоремы.
Белларе и Роджуэй были первыми исследователями, предложившими вычислительный подход к доказательству стойкости протоколов аутентификации и протоколов согласования аутентифицированных ключей [23]. В своей знаменитой работе они смоделировали атаки на эти протоколы, разработали несколько простых протоколов аутентификации и согласования аутентифицированных ключей, а затем привели доказательство их стойкости. Эти доказательства основаны на редукции атаки к нарушению условия псевдослучайности, т.е. обнаружению отличий между значениями псевдослучайной функции и истинно случайной функции с помощью полиномиального алгоритма распознавания. Иначе говоря, доказательство отрицает существование псевдослучайных функций.
Читатели могут вернуться к разделу 4.7 и проанализировать предположения 4.1 и 4.2. Эти предположения являются основой современной криптографии. Отсюда следует, что результатом редукции должна быть либо ошибка, либо переворот всех основ современной криптографии. Поскольку ошибка более вероятна, редукция приводит к требуемому противоречию.
Мы рассмотрим наиболее простой результат работы Белларе и Роджуэя: доказательство стойкости двусторонней аутентификации сущностей, основанное на использовании общего симметричного ключа [23]. Несмотря на его простоту, этого достаточно для иллюстрации основных принципов, лежащих в основе вычислительной модели.
Описание работы Белларе и Роджуэя, посвященной протоколу аутентификации, состоит из трех этапов. В разделе 17.3.1 описывается формальная модель поведения участников протокола и Злоумышленника. В разделе 17.3.2 приводится формальное определение стойкости протокола взаимной аутентификации сущностей. В разделе 17.3.3 демонстрируется редукционное доказательство стойкости этого протокола.
Глава 17. Формальные методы анализа протоколов аутентификации
647
17.3.1 Формальное моделирование поведения участников протокола
Протоколы, рассмотренные в работе [23], являются двусторонними. Каждый из двух участников протокола моделируется эффективным исполняемым кодом, имеющим входную и выходную информацию. Протокол состоит из сеансов связи между двумя участниками. Однако следует подчеркнуть, что в этих "сеансах связи" участвует Злоумышленник, который может манипулировать значениями, передаваемыми по каналу связи.
Итак, описание абстрактного протокола состоит из двух частей: во-первых, эффективно вычисляемой функции, принадлежащей участнику протокола, и, во-вторых, совокупности связей.
17.3.1.1 Формализация части протокола, выполняемой подлинным участником
С формальной точки зрения абстрактный протокол описывается функцией V, имеющей полиномиальную сложность и следующие аргументы.
\к Параметр безопасности к € N (унарное представление параметра безопасности аргументируется в разделе 4.4.6 и определении 4.7).
г Идентификатор пользователя г € /, выполняющего данную часть протокола. Будем называть этого пользователя "владельцем". Множество / состоит из пользователей, обладающих одним и тем же долговременным ключом.
j Идентификатор партнера, с которым общается владелец; j € /.
