2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (1185529), страница 54
Текст из файла (страница 54)
1 перехалгываст зто сообщение. Поскольку оно закодировано открытым ключом А, 1 не может декодировать это сообщение сам, н поэтому престо пересылает его агенту А. 4. Получив сообщение ли82, А видит в ием евой лолсеА, считает, что все закончилось успешно, н пссылщт лмВЗ своему партнеру — агенту 1, считая, что он установил связь с Г . 5. Это сообщение закодировано ключом для 1 и содержит лоисеВ.
Поэтому агент 1 молит его декодировать, получив. в дополнение к лолсеА, также и лолсеВ. б. Г насылает в своем сообщении лм83 этот иолсеВ агап!у В, который тоже удовлетворен н успешно завершается, счигяя, что нм установлена связь с А. В результате этой атаки Воб думает, что он говорит с АЬсе. а он говорит со злоумышленником (рнс. 8.(3), а сам злоумышленник имеет секрстм обоих честных собеседников, А и В. Теперь злоумышленник может разговаривать с пользователем В под видом пользователя А. Итак, прн анализе протокола Нидхзма — Шредера найдена атака, т.
е, тамм последомпельиость действий одного из субъектов обмена, которая приводит к нарушению свойств корректности протокола. Анализ найденных атак позволяет изменить криптографический протокол так, чтобы свойства корректности удовлепюрялись. Например, одной из причин возможной атаки здесь являкюя то, что агент 1 может от своего имени послать полученное ст В сообщение мг82, лкресованное агенту А. Если в этом сообщении потрсбо.
вать идентификации отправителя (т.е. если вид этого сообщения станет (В,Ь ю Ьгл)р„), то верификатор не находит возможной атаки: агент А обнаружит по содеряшмому этого сообщения, что хотя он говорит с Г, в полученном от Г зашифрованном сообщении стоит не его имя. Очевидно, что в общем случае алгоритм верифшшцин может н не выявить некорректность криптографического протокола, если модевь этого протокола глава в прош снеге меня Одни ция к гоксл возик !папаш вилы пгютс если ~ в.в. 8.6. Заключение Вери~ другг деляг тулы слишком грубая. Модель криптографических средств зашиты информации должна летально и полно описывать, какой информацией владеет на кшкдом возможном шаге функционирования системы кмкдый субьект распределенной системы, а это не всегда легко сделшь. Кроме того, часто является трудным делом формально вырвзпть такие свойства криптографических протоколов, квя секрспвють, конфнденциаяьность, анонимность и т.
п. йсЬ Рис. ЗЛЗ. ВоЬ лумает, что он говорят с Айсг„ а в яейсшвтекьноспг ои говорят с Ьшмгсг Метод шобе! сЬесЫой попользуется не только для верификации систем абрабогкн данных — программ и аппаратуры. В этой главе приведены примеры яншь некоторых нз задач, которые могут быль решены с помощью этой техники. В последние годы этот метод стал широко применяться в разработке алгоритмов планирования при анализе веб-документов, анализе бизнеспроцессов и протоколов электронной коммерции, в искусственном интеллекте.
В 2000 г. состоаюв уже пятый Международный семинар по шоде1 сЬесЫпй н Искусственному интеллекту (МоСЬАп Ч). Любая поисковая система выласт сотни ссылок на сочетания слов пюре! сйесЫпй со словами: вссем сшито! ро1Ыу, вГогЫ ФЫе зуеЬ, меЬ мят1сш, меЬ врр1юабопв, зузгешз Ью1ойу, пвпомсЬио1ойу. Публикуются работы по применению этого метода для пресбрпимания графов, анализа учебных планов, анализа ХМ! документов, Суще сгся ~ Очем для и лиэи правя злект Испо ется параз ложе~ полы шеки темш ры ср кав н иайтг ется ~ !179ф Вики проверки непротиворечивости семантических ограничений в текетвк, енелиш систем пршшпзвленгш знаний, анализе коммуникации ипгеляектувльных агентов и т. д.
и т. п. манин шелом делен. ~ труд- Одним нз ванных приложений мвюда проверки модели является аерифика. ция криптографических протоколов. Для проверки правильности таких про. токолов с помощью воде! сйесйшй обычно строится модель протажша и всех возмохпкюэпй, доступных злоумышленнику, а в качестве спецификации правильной работы формулируется утверждение, что требованиа корректности протокола не нарушаются.
Система верификации тогда сгенерирует шпху, если она возможна в этом протоколе. 8.6. Замечания гмеры й тех,ботке хвате юапй а вмзссем э)ою. г пре- Существует множество работ, в которых процедуру воде! сйесЫпй преллиастся испольэовать для верификации бизнес-процессов, например, [15 Ц, [40]. Очень похшкие идеи лежат в основе исполшоввння алгоритма тоде! сйесйшй для анализа диаграмм а«тившкти ОМЕ [49].
В отличие от юыка АшЬег, язык диаграмм активностей 0М$ стандартизнрован [122]. Близким к этому направлению являсзся быстро развивающаяся область верификации протоколов электронной коммерции с гюмощью пик[в! сйесЬ[пй (например, [7]). Использование любе! сйесипй для решение проблем шшннровання обсуждается ао многих публикациах. В искусственном инэеллекге сформировшшсь паршгигма "рйглл!пй аз яшгЫ с)мс)зпй" [59]. Введение в это направление изложено в [23), эта работа пспольэшшна в разделе 7.2. В [18] прелложено использовать темпоршьную логику для управления процессом поиска при решении звлач планирования: в этой работе демонстрируется, квк с помощью темпоральной логики махно формализовать специфические знания структуры среды поиска.
Описание подходов к проблемам планирования в мИре блоков можно найти в [137). Статью в Википслии о Кигвйских кольцах можно найти по ссылке [! 9Ц. Стариннав задача фермер-волк-коза-капуста описывается во многих сборниках логических задач, ее обсуждение можно найти в [179].
Логическая головоломка о миссионерах и каннибалах описана в статье Википедии [180]. Верификация криптографических протоколов с помощью шоде1 сЬесЫпй н других подходов к верифнкасшн параллельных систем превратилвоь в сч дельную ветвь криптшшвлиза. Изяоженный здесь материал опирается на ре. зультаты нз [100], [115], [84] н [106), В.7. Задачи а главе 6 8.В Выразим в СТ(.
и проверьте лля задачи волк-коза-юшуста следукяцее: существует решение задачи, которое удоввегворяст ограничениям (т. е. что все переправятсв, но при этом коза не останется без присмотра с виком, а капуста — с козой), в также и дополнительным условиям: а) если коза переедет на ту сторону, она там навсегда н останется; б) волк может остаться наедине с капустой (без фермера и без козы) иа этом берегу реки; в) при любом вариыпе решения задачи фермер данкен будет хоть раз переенкать реку обратно не один. 8.2.
Какие свойства в задаче волк-коза-капуста вырююиот формулы: АР~ ~КХС 1 иЧ с~хМ С[мЦ(АР ю)1 АС ~~ аэ Р-эг~ АР~У ] ерс(А) 83. С помощью системы бр!и решите головслом«у о лягушках, которые хотат по камням пересечь ручей (см. (196)). Три зеленых лягушки сидят на трех камнях слева и хотят перебратьсз слева направо, три красных лягушки сидят на трех камнях справа и хотят перебраться справа ивлево, между ними один свободный камень. Найти последовательность действий лягушек, после которой все валеные лягушки окажутся справа, а в:е красные — слева. Ограничения иа движения лягушек а) они могут прыгать только в том направлении, куда они глядят: лягушки слева могут прыгать только к правому берегу, лягушки справа — только к левому берегу; б) лягушки могут прыгать лабо на своболный камень перед собой, либо на свободный камень, перепрыгнув через одну ллПлнку лругого паста перел собой.
8.4. Одна из пшоваломок о пермпэвае звучит так. Муж с женой и двумв детьми хотят переправиться через реку. Единственный способ перепльпь сев взять . зать т зи сеь .юмку 8.5. Рэ помоч зать э праву'. Аб. С ху) кием э ровать берегу 8.7. П точно виде и ио, пуч Помес этой г тольке предиг душем р, ств ным). Поско: кой ае верши верши П стр ЭРЭ :. что ом, а ~) на : хогрех чдят дин сго- иче- лки ~ько Проблема поиска Гвмильтоновв пути яаляемя НР-полной. Сведение этой проблемы к проверке истинности НТ( формулы говорит о том, чго сжикносзь алгоритма проверки модели шш (,Т формулы ввляетса )ЧР-полной проблемой.
э на .рсл взять лодку у рыбака, находящегося на этом берегу. Но лодка макет выдер. жать только одного взрослого илн двух детей, которые умеют грести. Может лн семья переплыть реку на этой яодке и вернуп се рыбаку? Решите головоломку с помощью системы бргп. 8,5. Еще одна головоломка о переправе. Два маиьчика с лодкой согласились помочь трем солдатам переплыть реку.
Их лодка так мала, что может видар. жать либо одного солдата, либо двух мальчиков. Как распланировать переправу? Решите головоломку с помощью системы бр)п. 8.6. Один нз вариантов головоломки о переправе через реку относят к ХИ веку. Задача соспхгг в переправе трех пар эселнг-иеееста с использованием лодки, которы мсжет выдержать только двоих. Чтобы не компрометировать невесту, она не должна оказаться с чужим женихом в лодке либо на берегу, если своего жениха нет рядом. 8.7. Проблема поиска в ~рафе гамильтонова пуси, т.е.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
