Современная криптография - Венбо Мао
ISBN 5-8459-0847-7
Скачать (прямая ссылка):
• Пользователь видит (sees) сообщение.
• Пользователь создает (utters) сообщение.
• Пользователь верит (believes or provides jurisdiction over) в истинность утверждения.
• Два (или больше) пользователя разделяют (share) общий секрет (сообщение).
• Шифрование сообщения.
• "Свежесть" сообщения.
Глава 17. Формальные методы анализа протоколов аутентификации
657
• Конъюнкция логических утверждений.
• Хороший общий ключ: его не может скомпрометировать Злоумышленник и он всегда остается "свежим".
Эта система аксиом основана на интуитивных представлениях о протоколе аутентификации. Например, требование "свежести" при аутентификации сообщения описывается следующим правилом ("верификация одноразового случайного числа").
Р верит свежий (X) Л Р верит((5 сказал X) (17 4 1
Р верит(<2 верит X) ' ^
Здесь выражение Q верит X означает, что пользователь Q создал сообщение X недавно. Эта аксиома интерпретируется следующим образом: если пользователь Р верит, что сообщение X является "свежим" и создано пользователем Q, то он должен верить и в то, что пользователь Q создал сообщение X недавно.
Анализ протокола с помощью логики BAN начинается с формулировки набора предположений о протоколе. Затем выполняется "идеализация" протокольных сообщений. Она представляет собой процесс преобразования протокольных сообщений в логические формулы. После этого к аксиомам применяются логические формулы, позволяющие установить требуемые свойства, например, качество ключа.
Поскольку логика BAN относится к доказательству теорем, она не содержит механизма, позволяющего выявлять недостатки протоколов. Однако следует отметить, что процесс доказательства можно выполнить в обратном направлении: от желаемой цели — к необходимому набору аксиом. Следовательно, логика BAN может выявить важные предположения, пропущенные при спецификации протокола. Игнорирование необходимых предположений часто ведет к дефектам. Большое количество недостатков множества протоколов аутентификации было раскрыто в работе [61]. Однако для обнаружения скрытых дефектов на основе логики BAN необходимо участие высококвалифицированного эксперта, проницательного и удачливого.
Процедура идеализации протокола может оказаться уязвимой. Протоколы, описанные в литературе, как правило, сводятся к последовательности сообщений, отправленных и полученных пользователями. Чтобы воспользоваться логикой BAN, аналитик должен выразить протокол в виде формул, относящихся к сообщениям, которыми обмениваются пользователи, и допускающих применения аксиом. Например, если Трент посылает сообщение, содержащее ключ Кав, этап передачи сообщения выражается следующим образом.
Гсказал А КАв В.
<->
Это означает, что ключ Кав является качественным. Этот этап идеализации выглядит довольно простым. Однако на самом деле процедура идеализации явля-
658
Часть V. Методы формального доказательства стойкости
ется довольно сложной. Мао обнаружил, что логика BAN допускает применение контекстно-свободных процедур идеализации [183]. Например, этап идеализации, описанный выше, выполнен без учета контекста протокола. Это довольно опасно. Мао утверждает, что идеализация протокола с помощью логики BAN должна быть контекстно-зависимым процессом.
Другим недостатком логики BAN является отсутствие формального определения семантических правил, на которых основана система аксиом. В результате систему для доказательства теорем с помощью логики BAN следует считать некорректной. Кроме того, некоторые аксиомы теряют смысл. Например, в правиле верификации одноразового случайного числа (17.4.1) выражение Q верит X часто содержит ошибку интерпретации (type error) для боыпинства значений А" (одноразового случайного числа): число X, как правило, не является логической формулой даже после идеализации. (В интерпретации правила верификации одноразового случайного числа необходимые исправления уже сделаны.)
Попытки усовершенствовать семантику и обеспечить корректность логики BAN предпринимались в работах [3, 286].
Интересной модификацией логики BAN является логика GNY, разработанная Гонгом (Gong), Нидхемом и Яхаломом (Yahalom) [131], расширенная логика ван Оршота (van Oorschot) [292], а также логика идентификации, предложенная Кайларом (Kailar) [156].
Логика GNY включает в себя понятие распознаваемости, основанное на информации о типе сообщения, предотвращающей ошибки, связанные с неправильной интерпретацией, а также понятие сообщения, принадлежащего пользователю который либо создал, либо распознал его.
Расширенная логика ван Оршота облегчает проверку протокола согласовагаи аутентифицированных ключей в криптографии с открытым ключом. Эта систем-была использована для анализа трех протоколов согласования ключей Диффи Хеллмана, включая протокол STS (протокол 11.6, изученный в разделе 11.6.1). I
Логика Кайлара (Kailar) предназначена для систем электронной коммерции, i Она содержит синтаксические правила, позволяющие обеспечить идентификацию пользователей.
Все эти три модели, как и логика BAN, недостаточны для создания формальной семантической модели.
