Ремонт принтеров, сканнеров, факсов и остальной офисной техники


назад Оглавление вперед




[20]

Ek (St (Ra, К А, В), Rb)

(7)Алиса проверяет подпись Трента и свое случайное число. Затем она посылает Бобу второе случайное чи с-ло, шифрованное сеансовым ключом.

(8)Боб расшифровывает свое случайное число и проверяет, что оно не изменилось. Другие протоколы

В литературе описано множество протоколов . Протоколы X.509 рассматриваются в разделе 24.9, Kryp-toKnight - в разделе 24.6, а Шифрованный обмен ключами (Encrypted Key Exchange) - в разделе 22.5.

Другим новым протоколом с открытыми ключами является Kuperee [694]. Ведется работа на протоколами, использующими маяки - заслуживающие доверия узлы сети, которые непрерывно и широковещательно пер е-дают достоверные метки времени [783].

Из приведенных протоколов, как из тех, которые вскрываются, так и из надежных, можно извлечь ряд ва ж-ных уроков:

-Многие протоколы терпят неудачу, так как их разработчики пытались быть слишком умными. Они опт и-мизировали протоколы, убирая важные элементы - имена, случайные числа и т.п. - и пытаясь сделать протоколы как можно более прозрачными [43, 44].

-Оптимизация - эта манящая ловушка - сильно зависит от сделанных предположений. Пример: наличие достоверного времени позволяет вам реализовать многие вещи, невозможные в проти вном случае.

-Выбираемый протокол зависит от архитектуры используемых средств связи. Хотите ли вы минимизир о-вать размер сообщений или их количество? Могут ли сторона взаимодействовать каждый с каждым или круг их общения будет ограничен?

Именно подобные вопросы и привели к созданию формальных методов анализа протоколов .

3.4 Формальный анализ протоколов проверки подлинности и обмена ключами

Проблема выделения безопасного сеансового ключа для пары компьютеров (или людей) в сети настолько фундаментальна, что стала причиной многих исследований . Некоторые исследования заключались в разработке протоколов, подобных рассматриваемым в разделах 3.1, 3.2 и 3.3. Это, в свою очередь, привело к появлению более важной и интересной задачи: формальному анализу протоколов проверки подлинности и обмена ключами. Иногда прорехи в протоколах, кажущихся вполне надежными, обнаруживались спустя много лет п осле их разработки, и разработчикам потребовались средства, позволяющие сразу же проверять безопасность протокола. Хотя большая часть этого инструментария применима и к более общим криптографическим прот о-колам, особое внимание уделялось проверке подлинности и обмену ключами . Существует четыре основных подхода к анализу криптографических протоколов [1045]:

1.Моделирование и проверка работы протокола с использованием языков описания и средств проверки, не разработанных специально для анализа криптографических протоколов.

2.Создание экспертных систем, позволяющих конструктору протокола разрабатывать и исследовать различные сценарии.

3.Выработка требований к семейству протоколов, используя некую логику для анализа понятий "знание" и "доверие".

4.Разработка формальных методов, основанных на записи свойств криптографических систем в алге б-раическом виде.

Полное описание этих четырех подходов и связанных с ними исследований выходит за рамки данной книги. Хорошее введение в эту тему дано в [1047, 1355], я же собираюсь коснуться только основных вопросов.

Первый из подходов пытается доказать правильность протокола, рассматривая его как обычную компьюте р-ную программу. Ряд исследователей представляют протокол как конечный автомат [1449, 1565], другие используют расширения методов исчисления предиката первого порядка [822], а третьи для анализа протоколов используют языки описания [1566]. Однако, доказательство правильности отнюдь не является доказательством безопасности, и этот подход потерпел неудачу при анализе многих "дырявых" протоколов . И хотя его применение поначалу широко изучалось, с ростом популярности третьего из подходов работы в этой области были п е-реориентированы.


Во втором подходе для определения того, может ли протокол перейти в нежелательное состояние (например, потеря ключа), используются экспертные системы. Хотя этот подход дает лучшие результаты при поиске "дыр", он не гарантирует безопасности и не предоставляет методик разработки вскрытий . Он хорош для проверки того, содержит ли протокол конкретную "дыру", но вряд ли способен обнаружить неизвестные "дыры" в протоколе . Примеры такого подхода можно найти в [987,1521], а в [1092] обсуждается экспертная система, разработанная армией США и названная Следователем (Interrogator).

Третий подход гораздо популярнее. Он был впервые введен Майклом Бэрроузом ( Michael Burrows), Мартином Абэди (Martin Abadi) и Роджером Неедхэмом. Они разработали формальную логическую модель для ан а-лиза знания и доверия, названную БАН-логикой [283, 284]. БАН-логика является наиболее широко распространена при анализе протоколов проверки подлинности . Она рассматривает подлинность как функцию от ц е-лостности и новизны, используя логические правила для отслеживания состояния этих атрибутов на протяжении всего протокола. Хотя были предложены различные варианты и расширения, большинство разработчиков пр о-токолов до сих пор обращаются к оригинальной работе.

БАН-логика не предоставляет доказательство безопасности , она может только рассуждать о проверке подлинности. Она является простой, прямолинейной логикой, легкой в применении и полезной при поиске "дыр" . Вот некоторые предложения БАН-логики:

Алиса считает X. (Алиса действует, как если бы X являлось истиной.)

Алиса видит X. (Кто-то послал сообщение, содержащее X, Алисе, которая может прочитать и снова передать X - возможно после дешифрирования.)

Алиса сказала X. (В некоторый момент времени Алиса послала сообщение, которое содержит предложение X. Не известно, как давно было послано сообщение, и было ли оно послано в течении текущего выполнения протокола . Известно, что Алиса считала X, когда говорила X.)

X ново. (X никогда не было послано в сообщении до текущего выполнения протокола .)

И так далее. БАН-логика также предоставляет правила для рассуждения о доверии протоколу . Для доказательства чего-либо в протоколе или для ответа на какие-то вопросы к логическим предложениям о протоколе можно применить эти правила. Например, одним из правил является правило о значении сообщения :

ЕСЛИ Алиса считает, что у Алисы и Боба общий секретный ключ, K, и Алиса видит X, шифрованное K, и Алиса не шифровала X с помощью K, ТО Алиса считает, что Боб сказал X.

Другим является правило подтверждения метки времени :

ЕСЛИ Алиса считает, что X могло быть сказано только недавно, и, что Боб X когда-то сказал X, ТО Алиса считает, что Боб считает X.

БАН-анализ делится на четыре этапа:

(1)Преобразуйте протокол к идеальной форме, используя описанные выше предложения.

(2)Добавьте все предположения о начальном состоянии протокола.

(3)Присоедините логические формулы к предложениям, получая утверждения о состоянии системы после каждого предложения.

(4)Примените логические постулаты к утверждениям и предположениям, чтобы раскрыть состояние доверия участников протокола.

Авторы БАН-логики "рассматривают идеализированные протоколы как более ясные и полные описания, чем традиционные, найденные в литературе..." [283, 284]. Другие исследователи не так оптимистичны и подвергают это действие критике, так как при этом реальный протокол может быть искажен [1161, 1612]. Дальнейшие споры отражены в [221, 1557]. Ряд критиков пытается показать, что БАН-логика может и получить очевидно н е-правильные характеристики протоколов [1161] - см. контрдоводы в [285, 1509] - и что БАН-логика занимается только доверием, а не безопасностью [1509]. Подробное обсуждение приведено в [1488, 706, 1002].

Несмотря на эту критику БАН-логика достигла определенных успехов . Ей удалось обнаружить "дыры" в нескольких протоколах, включая Needham-Schroeder и раннюю черновую версию протокола CCITT X.509 [303]. Она обнаружила избыточность во многих протоколах, включая Yahalom, Needham-Schroeder и Kerberos. Во многих опубликованных работах БАН-логика используется для заявления претензии о безопасности описыва е-мых протоколов [40, 1162, 73].

Были опубликованы и другие логические системы, некоторые из них разрабатывались как расширения БАН-логики [645, 586, 1556, 828], а другие основывались на БАН-логике для исправления ощутимых слабостей [1488, 1002]. Из них наиболее успешной оказалась CNY [645], хотя у нее есть ряд изъянов [40]. В [292,474] к БАН-логике с переменным успехом были добавлены вероятностные доверия . Другие формальные логики описаны в [156, 798,288]. [1514] пытается объединить черты нескольких логик. А в [1124, 1511] представлены логики, в которых доверия изменяются со временем .

Четвертый подход к анализу криптографических протоколов предлагает моделировать протокол как алге б-раическую систему, выразить состояние знания участников о протоколе и затем проанализировать достиж и-


мость определенных состояний. Этот подход пока не привлек столько внимания, как формальная логика, но состояние дел меняется. Он впервые был использован Майклом Мерриттом [1076], который показал, что для анализа криптографических протоколов можно использовать алгебраическую модель . Другие подходы рассмотрены в [473, 1508, 1530, 1531, 1532, 1510, 1612].

Анализатор протоколов Исследовательской лаборатория ВМС (Navy Research Laboratory, NRL), возможно, является наиболее успешным применением этих методов [1512, 823, 1046, 1513]. Он был использован для поиска как новых, так и известных "дыр" во множестве протоколов [1044, 1045, 1047]. Анализатор протоколов определяет следующие действия:

-Принять (Боб, Алиса, M, N). (Боб принимает сообщение Mкак пришедшее от Алисы в течение локального раунда Боба N.)

-Узнать (Ева, M). (Ева узнает M.)

-Послать (Алиса, Боб, Q, M). (Алиса посылает M Бобу в ответ на запрос, Q.)

-Запросить (Боб, Алиса, Q, N). (Боб посылает Q Алисе в течение локального раунда Боба N.) Используя эти действия, можно задать требования . Например:

-Если Боб принял сообщение M от Алисы в какой-то прошедший момент времени, то Ева не знает M в какой-то прошедший момент времени.

-Если Боб принял сообщение M от Алисы в течение локального раунда Боба N, то Алиса послала M Бобу в ответ на запрос Боба в локальном раунде Боба N.

Для анализа Анализатором протоколов NRL исследуемый протокол должен быть описан с помощью прив еденных конструкций. Затем выполняются четыре фазы анализа: определение правил перехода для честных участников, описание операций, возможных и для полностью честных, и для нечестных участников , описание базовых блоков протокола и описание правил преобразования . Смысл всего этого в том, чтобы показать, что да н-ный протокол удовлетворяет необходимым требованиями . Использование инструментов, подобных Анализат ору протоколов NRL, в итоге могло бы привести к созданию протокола, который был бы обоснованно признан безопасным.

Хотя формальные методы в основном применяются к уже существующим протоколам, сегодня есть тенде н-ция использовать их и при проектировании протоколов . Ряд предварительных шагов в этом направлении сделан в [711]. Это же пытается сделать и анализатор протоколов NRL [1512, 222, 1513].

Применение формальных методов к криптографическим протоколам представляет собой качественно новую идею, и трудно обрисовать, к чему может привести ее реализация . С этой точки зрения слабейшим звеном кажется процесс формализации.

3.5 Криптография с несколькими открытыми ключами

Обычная криптография с открытыми ключами использует два ключа. Сообщение, зашифрованное одним ключом, может быть расшифровано другим . Обычно один ключ является закрытым, а другой - открытым . Пусть, один ключ находится у Алисы, а другой - у Боба. Мы хотим реализовать следующую схему: Алиса м о-жет зашифровать сообщение так, что только Боб сможет расшифровать его, а Боб может зашифровать сообщ е-ние так, что только Алиса сможет проч итать его.

Эта концепция была обобщены Конном Бойдом (Conn Boyd) [217]. Представьте себе вариант криптографии с открытыми ключами, использующий три ключа: КА, Кв и Кс, распределение которых показано в 1-й.

Алиса может зашифровать сообщение ключом КА так, что Эллен может расшифровать его, используя ключи Кв и Кс. То же самое, сговорившись, могут сделать Боб и Кэрол. Боб может зашифровать сообщение так, что Фрэнк сможет прочесть его а Кэрол сможет зашифровать сообщение так, что его сможет прочесть Дэйв. Дэйв может зашифровать сообщение ключом КА так, что Эллен сможет прочесть его, ключом Кв так, что его сможет прочесть Фрэнк, или обоими ключами, КА и Кв, так, что сообщение сможет прочесть Кэрол. Аналогично, Эллен может зашифровать сообщение так, что Алиса, или Дэйв, или Фрэнк сможет прочесть его. Все возможные ко м-бинации показаны в , других не существует.

Табл. 3-2.

Распределение ключей в трехключевой системе.

Алиса КА БобКв



[стр.Начало] [стр.1] [стр.2] [стр.3] [стр.4] [стр.5] [стр.6] [стр.7] [стр.8] [стр.9] [стр.10] [стр.11] [стр.12] [стр.13] [стр.14] [стр.15] [стр.16] [стр.17] [стр.18] [стр.19] [стр.20] [стр.21] [стр.22] [стр.23] [стр.24] [стр.25] [стр.26] [стр.27] [стр.28] [стр.29] [стр.30] [стр.31] [стр.32] [стр.33] [стр.34] [стр.35] [стр.36] [стр.37] [стр.38] [стр.39] [стр.40] [стр.41] [стр.42] [стр.43] [стр.44] [стр.45] [стр.46] [стр.47] [стр.48] [стр.49] [стр.50] [стр.51] [стр.52] [стр.53] [стр.54] [стр.55] [стр.56] [стр.57] [стр.58] [стр.59] [стр.60] [стр.61] [стр.62] [стр.63] [стр.64] [стр.65] [стр.66] [стр.67] [стр.68] [стр.69] [стр.70] [стр.71] [стр.72] [стр.73] [стр.74] [стр.75] [стр.76] [стр.77] [стр.78] [стр.79] [стр.80] [стр.81] [стр.82] [стр.83] [стр.84] [стр.85] [стр.86] [стр.87] [стр.88] [стр.89] [стр.90] [стр.91] [стр.92] [стр.93] [стр.94] [стр.95] [стр.96] [стр.97] [стр.98] [стр.99] [стр.100] [стр.101] [стр.102] [стр.103] [стр.104] [стр.105] [стр.106] [стр.107] [стр.108] [стр.109] [стр.110] [стр.111] [стр.112] [стр.113] [стр.114] [стр.115] [стр.116] [стр.117] [стр.118] [стр.119] [стр.120] [стр.121] [стр.122] [стр.123] [стр.124] [стр.125] [стр.126] [стр.127] [стр.128] [стр.129] [стр.130] [стр.131] [стр.132] [стр.133] [стр.134] [стр.135] [стр.136] [стр.137] [стр.138] [стр.139] [стр.140] [стр.141] [стр.142] [стр.143] [стр.144] [стр.145] [стр.146] [стр.147] [стр.148] [стр.149] [стр.150] [стр.151] [стр.152] [стр.153] [стр.154] [стр.155] [стр.156] [стр.157] [стр.158] [стр.159] [стр.160] [стр.161] [стр.162] [стр.163] [стр.164] [стр.165] [стр.166] [стр.167] [стр.168] [стр.169] [стр.170] [стр.171] [стр.172] [стр.173] [стр.174] [стр.175] [стр.176] [стр.177] [стр.178] [стр.179] [стр.180] [стр.181] [стр.182] [стр.183] [стр.184] [стр.185] [стр.186] [стр.187] [стр.188] [стр.189] [стр.190] [стр.191] [стр.192] [стр.193] [стр.194] [стр.195] [стр.196] [стр.197] [стр.198] [стр.199] [стр.200] [стр.201] [стр.202] [стр.203]