Научная литература
booksshare.net -> Добавить материал -> Криптография -> Венбо Мао -> "Современная криптография" -> 271

Современная криптография - Венбо Мао

Венбо Мао Современная криптография. Под редакцией Клюшиной Д.А. — М. : Издательский дом Вильямс, 2005. — 768 c.
ISBN 5-8459-0847-7
Скачать (прямая ссылка): sovremennaya_kriptografiya.djvu
Предыдущая << 1 .. 265 266 267 268 269 270 < 271 > 272 273 274 275 276 277 .. 311 >> Следующая

Создав машины Div2 и Div3 с помошью операций алгебры CSP, машину Div6 можно создать механически.
Пример 17.2. CSP-спецификация машины Div2
Div2 d= Ro; R0 d= (0 До) ? (1 Дх) ? ({} STOP); Ri = (0- Д0)П(1-Д1); ?
Теперь машину Div6 легко создать, механически применив операцию "параллельность".
668
Часть V. Методы формального доказательства стойкости!
Пример 17.3. CSP-спецификация машины Div6
Div6 def Div2 ll Div3 = Ro || So;
Ro II So def (0- Ro\ |So)c(l ^Ri\ |Si)i
Ri II Si def (0-> Ro\ |S2)n(l -+Ri | |So);
Ro 11 s2 def (0- Ro\ |Si)D(l |S2);
Ri II So def (0-> Ro\ |S0)D(1 -*Ri \Si);
Ro II Si def (0- Ro\ |S2)D(1 ^Ri\ \So);
Ri II s2 def Co- Ro\ -Ri \S2);
STOP II STOP = STOP. В примере спецификация
STOP || STOP = STOP
представляет собой "аксиому поглощения" (поглощается операция ||).
Механически созданная машина Div6 действительно правильно реализует ал горитм (читатели могут убедиться в этом самостоятельно). Механическая моделЛ использующая метод FDR, подтверждает, что процесс Div6 уточняет процесс Dhl и процессы Div2. Отсюда следует, что процесс Div6 действительно реализует ука| занный алгоритм.
Аналогично на основе машин Div2 и Div3 можно создать машину, распознаю; щую целые числа, кратные двум или трем. Эту механическую композицию можн| создать, заменяя операцию "чередование" операцией "параллельность" каждЫ| раз, когда объединяемые термы обозначают одно и то же действие, и примени "аксиому блокировки".
STOPIP = STOP || Р = РрТОР = Р || STOP = STOP.
Машина, полученная в результате такой композиции, довольно велика (име^ много состояний), поэтому мы не приводим ее спецификацию.
17.5.3.6 Анализ стойкости протоколов
Операция композиции в алгебре CSP делает ее особенно полезной для моде^ лирования и описания поведения параллельных систем и средств связи. Имен™ это обстоятельство побудило некоторых исследователей утверждать, что алгебра CSP позволяет анализировать протоколы аутентификации [249, 250, 253]. Кроме того, существует модель FDR [248], которая используется в сочетании с алгеброй CSP для уточнения процессов. С помощью этой модели Лоу обнаружил скрытую ошибку в протоколе аутентификации Нидхема-Шредера [181].
Глава 17. Формальные методы анализа протоколов аутентификации
669
При анализе конфиденциальности сообщений отношение "следования" I h т позволяет указать, как извлечь информацию из доступных данных. Аксиомы следования, описывающие извлечение информации, перечислены на рис. 17.2.
Пусть J — исходная информация.
• Если т е /, то / Ь т.
• Если J Ь т и J С Г, то Г Ь т.
• Если / I- mi и / Ь тг, то /1- (mi, m2) (спаривание).
• Если / Ь (т^тг), то / Ь mi и IV- т2 (проекция).
• Если Л-ти/Ь-АГе/С, то/Ь- {т}к (шифрование).
• Если J Ь {т}к и IЬ К~х е /С, то J Ь т (расшифровка).
Рис. 17.2. Аксиомы следствия CSP
Например,
и но
{{ШК2}Кз,К3)\-Кг{шшъ).
Аксиомы следования интуитивно описывают, как Злоумышленник извлекает информацию. Пытаясь скрытно взломать протокол, Злоумышленник может использовать исходную информацию, которой он владеет, и некоторые протокольные сообщения, перехваченные в сети. Кстати, множество /, в принципе, является бесконечным. Однако в реальности для данного протокола множество I можно сузить до конечного множества "интересной" информации. Более того, исследователи пользуются тем, что на самом деле им не обязательно конструировать множество I. Достаточно проверить условие т е I для некоторого конечного набора сообщений.
Подводя итоги, укажем, что в рамках алгебры CSP применение механических средств является важным элементом анализа функционирования систем. Эти механические средства применяют набор интуитивно определенных правил. Например, при конструировании системы из небольших компонентов с помощью операции композиции можно создать более крупные системы, применяя семантические правила, перечисленные на рис. 17.1. В процессе уточнения процессов механические средства позволяют применить процедуру уточнения (раздел 17.5.3.4) и аксиомы следования (рис. 17.2).
670 Часть V. Методы формального доказательства стойкости
Синтаксис CSP, учитывающий линии связи между компонентами системы, не очень удобен для человека, зато вполне пригоден для реализации с помощью механических средств. (Следует отметить, что механическое конструирование машины Div6 с помощью операции композиции, описанное в примере 17.3, являете^ лаконичным (succinct), поскольку в нем отсутствует какой бы то ни было обмен, информацией между машинами Div2 и Div3.)
Поскольку протоколы аутентификации включают в себя обмен информацией между несколькими пользователями, большинству читателей, не являющимся специалистами в области формальных методов, может показаться, что модель CSP не пригодна для их анализа. Доказательство обратного утверждения приведено в работе Райана (Rayan) и Шнайдера (Schneider) [250].
17.6 Согласование двух точек зрения на
формальное доказательство стойкости
В главе 14 приведены две разные точки зрения на доказательство стойкости.
Одна из них, вычислительная, описана в главе 14 и в разделе 17.3. Она основана на подробной вычислительной модели. Рассмотрим в качестве примера стойкость шифрования. Вычислительная модель рассматривает секретность как. сложность распознавания исходного текста. Иначе говоря, атакующий алгоритм, имеющий в своем распоряжении два исходных текста и зашифрованный текст одного из них, не должен догадываться, какой именно исходный текст был зашифрован. Доказательство секретности обычно проводится с помощью сведения к противоречию, причем противоречием является решение одной из трудноразреи шимых задач из теории вычислительной сложности.
Предыдущая << 1 .. 265 266 267 268 269 270 < 271 > 272 273 274 275 276 277 .. 311 >> Следующая

Реклама

c1c0fc952cf0704ad12d6af2ad3bf47e03017fed

Есть, чем поделиться? Отправьте
материал
нам
Авторские права © 2009 BooksShare.
Все права защищены.
Rambler's Top100

c1c0fc952cf0704ad12d6af2ad3bf47e03017fed