Современная криптография - Венбо Мао
ISBN 5-8459-0847-7
Скачать (прямая ссылка):
Другая точка зрения, символическая, была изложена в разделах 17.4 и 17.5. Она основана на простом, но эффективном использовании формальных языков. Вернемся еще раз к доказательству стойкости шифрования. Символисты считают, что секретность — это сложность восстановления исходного текста с помощью аксиом следования, перечисленных на рис. 17.2. Механическое применение этих* аксиом основывается либо на методах автоматического доказательства теорем, либо на приемах исследования состояния систем.
Эти две точки зрения возникли в разных научных сообществах, между которыми долгое время существовала пропасть. Символическая точка зрения привлекательна своей простотой, однако иногда эта простота оказывается обманчивой и приводит к неверным результатам. Например, некоторые символисты считают, что цифровая подпись и шифрование с помощью одной и то же пары секретных и открытых ключей аннулируют друг друга, приводя в пример некоторые учеб/ ные криптографические алгоритмы. Намного чаще символисты рассматривают
Глава 17. Формальные методы анализа протоколов аутентификации 671
шифрование как детерминированную функцию, побуждая инженеров применять учебные алгоритмы шифрования.
Абади и Роджуэй взяли на себя труд уничтожить пропасть между вычислительной и символической точками зрения [2]. Они считают, что эти точки зрения должны не соревноваться, а дополнять друг друга. Абади и Роджуэй разработали следующие принципы.
• Взаимодействие между вычислительной и символической теориями должно укрепить основы формальной криптологии и выявить неявные предположения, скрытые в формальных методах. Оно должно сделать доказательства стойкости протоколов более убедительными, явно сформулировав требования к реализации криптографических операций.
• Для описания постоянно усложняющихся систем необходимо применять формальные методы вычислительной криптологии. Символический подход также основан на формальных принципах и даже допускает автоматическое доказательство. Кроме того, некоторые символические подходы точно описывают определенные наивные, но важные интуитивные предположения, принятые в криптографии. Эти интуитивные подходы следует укрепить методами вычислительной криптологии.
Работа Абади и Роджуэя посвящена вычислительному обоснованию символического подхода к шифрованию. Они стремились показать, что символическая и вычислительная точки зрения являются "почти гомоморфными". Во-первых, с вычислительной точки зрения два неразличимых зашифрованных текста считаются эквивалентными. Во-вторых, с символической точки зрения эквивалентными считаются два зашифрованных текста, смысл которых невозможно выяснить с помощью аксиом следования. Таким образом, из эквивалентности зашифрованных текстов с символической точки зрения следует их неразличимость с вычислительной точки зрения. Итак, вычислительную точку зрения на стойкость можно считать формальным базисом символической теории.
В работе Абади и Роджуэя были заложены основы для дальнейшего формального доказательства стойкости других криптографических примитивов, таких как цифровые подписи, функции хэширования, а также протоколы аутентификации или распределения аутентифицированных ключей.
17.7 Резюме
В этой главе рассмотрены протоколы аутентификации, имеющие большое прикладное значение. На этот раз изучались формальные доказательства их стойкости.
Сначала была обоснована необходимость уточнения метода, позволяющего создавать спецификации протокола. Было указано, что неточности общепринятого
672
Часть V. Методы формального доказательства стойкости
метода спецификации протоколов приводят к ошибкам и неправильному использованию криптографических средств в протоколах аутентификации. Затем был предложен уточненный метод спецификации протоколов и приведено несколько примеров, демонстрирующих его эффективность.
В главе описана методология формального анализа стойкости протоколов, как с вычислительной, так и символической точки зрения.
Обе теории имеют свои преимущества и недостатки. В главе указаны попытки согласовать их между собой, предпринятые в последнее время.
Формальный анализ протоколов аутентификации все еще остается на ранней стадии развития. Таким образом, материал, изложенный в этой главе, нельзя считать окончательным решением проблемы.
Упражнения
17.1. Для создания рандомизированных зашифрованных текстов широко исполь-« зуется режим СВС. Обеспечивает ли он секретность с прикладной точки зрения?
Подсказка: позволяет ли режим СВС предотвратить активную атаку?
17.2. В главе 2 описан процесс уточнения протоколов аутентификации "атака-i исправление". Позволяет ли этот процесс создавать стойкие протоколы^ Если нет, то почему?
17.3. Примените метод уточнения спецификаций обменов сообщениями в рам* ках протокола Kerberos (раздел 12.4.2). Укажите правильные спецификации^ необходимые для аутентификации.
Подсказка: еще раз прочтите раздел 12.4.3.
17.4. Неправильное применение криптографических средств — распространенная ошибка, возникающая при разработке протоколов аутентификации и прото! колов обмена аутентифицированными ключами. В чем именно проявляется эта ошибка?
