Современная криптография - Венбо Мао
ISBN 5-8459-0847-7
Скачать (прямая ссылка):
К Долговременный симметричный ключ (т.е. секретная входная информация). В двустороннем протоколе симметричный ключ К принадлежит как владельцу, так и его партнеру.
conv Предыдущие сообщения — conv (от англ.: conversation — прим. ред.), представляющие собой строку битов. Эта строка увеличивается по мере выполнения протокола, причем новая строка приписывается к старой.
г Случайный аргумент владельца — читатель может считать число г одноразовым случайным числом, генерируемым владельцем.
Поскольку V(lk,i,j, К, conv,г) имеет полиномиальную сложность, зависящую от размера аргументов (отметим, что размер параметра к равен lfc), можно считать, что аргументы К и г имеют размер к, а размер аргументов г, j и conv полиномиально зависит от параметра к.
648
Часть V. Методы формального доказательства стойкости
Значениями функции г, j, К, conv, г) являются три числа.
т Следующее сообщение, подлежащее отправке, — т Е {0,1}* U {"сообщений нет"}. Это — открытое сообщение, подлежащее отправке адресату через открытую сеть.
6 Решение пользователя — 5 Е {Принять, Отказать, Не принимать решения}. Пользователь решает, принять или отвергнуть идентификатор партнера по переговорам, либо не принимать решения вообще. Принятие идентификатора, как правило, откладывается до завершения протокола, а отклонить его можно в любой момент. Если пользователь принимает какое-либо определенное решение, значение 6 больше не изменяется.
а Закрытый результат, вычисленный владельцем, — о. Е {0,1}* U {"результата нет"}. Читатели могут считать, что закрытым результатом, вычисленным владельцем при благоприятном исходе протокола, является согласованный сеансовый ключ.
Анализ показывает, что в формальную модель Белларе-Роджуэя входят важные компоненты протоколов аутентификации сущностей: криптографические операции, идентификаторы участников, идентификаторы "свежести" и сообщения. (Смысл этих компонентов описан в разделе 11.4.)
Иногда абстрактный протокол аутентификации сущностей, принадлежащих множеству 1, обозначается как Р(1к,1).
Для любой пары i,jEl (т.е. для любых двух участников протокола, обладающих одним и тем же долговременным симметричным ключом) и для числа s Е N обозначим через Yitj игрока г, пытающегося аутентифицировать игрока j в ходе сеанса с меткой s. Эта попытка может инициироваться игроком г, а может быть и ответом на сообщение, полученное от пользователя j. Фактически мы всегда будем интерпретировать эту попытку как ответ на запрос оракулу, посланный Злоумышлеником. Для этого необходимо формализовать понятие обмена информацией.
17.3.1.2 Формализация обмена информацией
Белларе и Роджуэй в своей работе следовали идее Долева и Яо [101] (см. раздел 2.3): Злоумышленник, т.е. атакующий алгоритм, контролирует всю сеть связи.
Злоумышленнику, контролирующему сеть, могут быть известны последовательности игроков Yllj и i для любой пары г, j ЕI (т.е. для любых двух пользователей, обладающих общим долговременным симметричным ключом), даже если он не вычисляет их сам. Однако, будучи активным атакующим алгоритмом, Злоумышленник может делать намного больше, чем просто пассивно наблюдать за сообщениями. Он может организовывать сколько угодно сеансов связи и убеж-
Глава 17. Формальные методы анализа протоколов аутентификации
649
дать любого пользователя (например, г) начать протокол, считая Злоумышленника другим подлинным пользователем (например, j).
Поскольку Злоумышленник является мощным и активным атакующим алгоритмом, он может использовать игроков ГТ^- и П^(*13 Е I,s,tE М) в качестве оракулов, представляющих собой черные ящики. Это значит, что Злоумышленник может послать запрос оракулу Ц? -, передавая пользователю г аргументы (i,j,s,conv). Аналогичным образом Злоумышленник может послать запрос оракулу П$г Когда Злоумышленник посылает запрос оракулу ГЦ;?» используя аргументы (i,j,s,conv), пользователь г добавляет к ним собственный секретный ключ К, случайное число г и вычисляет функцию \~\s(lk,i,j, К,conv,г). После этого пользователь г" отсылает в сеть результат тп (если он существует) или строку "сообщений нет", а также решение 8, сохраняя у себя закрытый компонент результата а. Все результаты, посланные пользователем в сеть, оказываются в распоряжении Злоумышленника и могут быть использованы для организации атаки.
В модели Долева-Яо любой запрос считается пришедшим от Злоумышленника, пока оракул не примет положительного решения.
Не ограничивая общности, можно считать, что среди злоумышленников всегда есть относительно безопасный противник, называемый "безвредным". Он просто выбирает пары оракулов ГТ^- и П^г> а затем перехватывает и точно передает сообщения, которыми они обмениваются, начиная с оракула ГТ? .. Другими словами, первый запрос безвредного противника выглядит так: (г, j, s,"") (здесь символы ""
(г)
обозначают пустую строку). В ответ Злоумышленник получает сообщение тп\ . Второй запрос выглядит следующим образом: (j, г, t, тп^). В ответ противник по-лучает сообщение тщ' и так далее, пока оба оракула не примут положительное решение и не прекратят свою работу. Таким образом, безвредный противник играет роль проводника, связывающего между собой пользователей г и j. Позднее мы убедимся, что в доказуемо стойком протоколе Злоумышленник, стремящийся пройти аутентификацию, вынужден играть роль безвредного противника.
