2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (1185529), страница 53
Текст из файла (страница 53)
квк честные собеседники завершили протокол, н В установил, что его собеседник — А, злоумышленник не должен знать нн Асл — секрещ агента А, нн с«в — секрета вгемса В. Проведем вернфнкацшо протокола с помощью системы Ярсп. Для этого в языке Рюше!ж П построим модель, описывающую действия честных агеева, слелующих правилам протокола; С2 построим недстермнннрованный процесс злоумышлснншш, в котором представлены все перечисленные выше возможные действня; Сз формально с помощью формул ЕТЕ выразим требованна корректности протокола; 25 проверим выполнение требований корректности протокояа у построенной модели, пользуясь системой Ярса. Атакой на протокол в этой постановке будет являться любая последовательшють действий злоумышленннпх нарушающая требовапня корректности протокола, выраженнме формулой ЬТЕ.
Поскольку Зр! л исчерпывающе проверяет вес пугн, которью жжможны в модели, то Ярсп сгенернруст атаку (пайде стн пр Полнь привес ны дш Перси внм сн Испол~ сообсм щего а торых щенке получа его сея гуреев Все 5з Сеть м слыл л~ Модел~ с протг ьсссте нгС пс1 С вьюг зг Сч :1 зч сс С' лось пеоюш )дные он не орма- йства ) дан- юилн ик не ющих гором ениой зтельностн : про. атею (найдет юнггрпример, лля которого не выполняются тргбоеанна коррюггносгн протокола), если такая атака сущестауст. Полный текст программы на Ргопю[а для протокола Нидхэма — Шредера приведен а руководстве по системе Зр[п, приложенном к этой книге. Здесь мы дадим толы)о общую идею этой программы.
Переменные значения, которые могут использоваться а протоколе, представим символьными константами: вкупе ) 1юс, /' тип оообленил */ л11се, гюь, 1пггю!ег, /* ияентиеиквтоуы собеоеяннков */ ры), ртл, рК1, /' публичные юкни собеседников */ поповн, полова, попсе1, /* случайные числа собеседников '/ оь, егг)) ИСПОЛЬЗОВаНИЕМ КОНСтРуКцИИ Сгребет ОнрЕДЕЛИМ СГРУхтУРУ ЗаюнфРОааННЫХ сообщений в сети, состоящих из идентификации посылающего н принимыощего агента, ключе, которым зашифровано сообщение, н двух ланных.
Некоторых элементов в реальном сообщении может и не быть. Например, сообщение типа ! несет только информацию; отправитель, получатель, ключ получателя н секрет отпраюнеля. Сообщение типа 3 не несет отправителя и его секрета. Гупебег нбгурл [лаура Велбег, геле[чек, Кеу, 1пуо1, 1пго2] Все 5 элементов сообщения будут представлены символьными конспнцамн. Сеть моделируется как даа синхронных каны)б разделяемых всеми агенгамн: сплп петногя[2! [О! ог [ исусе, /*мнеьюююеское нмв-номер сооблвнил */ «Ст)рт /' само сообление — структура данных / ) Модель честнмх агензоа Айсе и ВоЬ строится полнощъю в соотаетстющ с протоколом: лог1те ргосгууе А11ое[ ) [ исусе укеу, рююсе) /* пубиичгвж ключ и плюсе партнера */ нсгупг гите) /* выбор ообеоювнид: А и;юет захотеть установить контакт о и ипк 1 */ гг :: реггпегд всепгн) рхеу кеуп /* ию от А бупет нлпрлнпено и */ :: уеггпегА «сепг1) р)юу кеу1 /* лис от А будет направлено 1 / /* посылке первого оообпвнил со своим попсе внбрвюнюу сабаоепнюю */ легногк [0)) [илс1, ногу)ю [А11се, рагспегл, ркеу, псюоед, о ! ) Глене В /* щ»ек попсе ссоеседннка из второго сост»енин, если оно мюа(ромно п(к(нала» к»юс» кеул и соде(»ит ранее пссланннй «опсед */ мсноск пит (»тсз, Васа(; (мса.хе~ кеуюеь(смсампгоз попсел(» рюпае еасалвгозг /' ~юсывм пркнвтозо попсе внсраннсьа ренее сосеседннк( */ пес»жк (0(( оззяз, вссурс (А11се, растласа, р(»у, о, рпсвсе ( (г зтаепзл ойг /* амит А зааериииск успеано */ ( Модель поведения агента (Год также соответствует протоколу и строится аналогично.
й модели злоумышленника опишем все действия, юторые возможны: П кшкдое сообщение, которое, в принципе, мекно шюлать, посылается; (з полученное сообщение, если оно не адресовано злоумышленнику, запомннаегся и патом шккет быть послано без изменения; 0 если сообщение направлено злоумышленнику, ои нз этого сообщения изВлекмт и запоминает м(О информм(ию; (э если данные, необходимые для конструирования любого сообщения, когда-то были получены, Они могут быть испошлованы в операторе посылки (например, в его звщиш). й процесс злоумышленника введем логические переменные, необходимые дня формирования требований к протоюлу, например, параметр 1 клоне попсев станет истинным, если злоумышленник дебетам(ельио получит секрет й.
всвзте ргсссуре 1псюк(м( ( ( Ьоо1 1 алоиз попсеА Га1зе, 1 Юкз» поиав Га1зе( / вначале злоуюаниенник не знает секретов А и В / до / юою полсиуниванив и посьаюк сосбзнний / :: песчана [0( т (з»Ш сиза(-> /* есви подслунал лкоое соосиение / 11 :: 1дсе*серс»1 с(аса( /е либо заимоюет пареказчеюв» данна» '/ :: зщр; / либо нет */ 11( 11 :: овса.кеу зеу1 -> /* если в приннтсм сосбаенки — свой кплч '/ 11 /' то извлекает чувой попсе, если он есть '/ :: дата.пьго1 пайпс»А((паса.зпго2 попсеА->1 клона попова. сюю~ :: сам.1пго1 пспсеи((паса.зпго2 пспсев->1 клона поосев- сапе; :: е1зе -> зщр( гм ш < гы пею Подам Они рз лострО сушсс( 5РИА и контри Пр формы тремя( а с(( тол! КВЦ( Г1 :: е1зе -> я)сьрг /" есю«з прими>си сост)пении — ие сми юзю '/ Гьг /* поюеюет сюю сосеиение' собирая его из позы«нных иусноз ь/ ьь11 /* прсыюнюьзо зм.преет тип соо6ююю */ пез нядз/ /* нелзтзр~иниримнно делеег то ке юю издз и издЗ */ Г)г 11 /* случално зызирает получателя, зыдляая саба за л, В илк 1*/ :: бясл.
зепбес адепсл -> басе. сесе1тег адепте/ басе. сеу рсеупг .../' или выдает себя за В, ипк зл Х, и зыенрпет получ мелек гм >Г /' юяздпют евое поселение дпя посыпяи / :: блсл )лсегсерсебг /* перехзечеююе дпнюю зюет еез иююыеюю «/ зв / ° либо оьюеюет соде)юл«>е юьссзьзюю дью Х */ :: смта. >пео1 адепед) :: з клоня попоек -> беса.ыьгоз попоек/ /*тозидплВ / Г1 оится ю из- /* дю Юнп.з тот */ сю ю р осью я в / з, ко;ылкн 11г пескоск [1)) ')зид, сасрс, беса)/ имые гнет)ь полу- */ ь / (рагвегА армий со рпгпзегВ =цймиА)) Подавляющее число возможных сообщений злоуммшленника некорректны. Они распознмотся агентами А и В, которые не отвечают на них, поэтому построенная программа имеет много блокнрово)с Но нам вюкно проверить, сущсствуез'ли хотя бы один путь, на котором возможна атаке.
Это и лслает Зр!л, проверзя выполнение требованмй корректности просокове и генерируя конзрпример, если он есть. Проверка корректности протокола осуществляется стандартным образом по формальной специфнзацин свойства "атаки нет". Это свойство выражается грена условиями: 0 С! (целостность): "после сессии агент А верит, что его партнер В, если и только если агент В верит, что его партнер А ". Его формельнаа спецификация формулой ).Т)х АС(згппмА сй йс зашиВ ой ~ .,Глаав в Найди 1. л~ 2. Пог мас очи отп 3.
Вг обн щее деи ту . А Пш так< очи 5, Згс ага~ ии 6. !п В реву злоумь чсстиь с поль. (В,Вл наруяо ченноь Оксан! не корр (2 С2 (конфиденциальность): "после того, как агент В завершился и установил, что его партнер — В, агент ! (!п1нк!ег) ие знает секрета Я". Его формальная спецификация: АС (згагнь( о(г дс рагшегА = абел!В ь ) Ьюмя логюеА) (2 СЗ (конфиденциальность): "после та о, шк агант В завершился и установил, что его партнер — В, агент 1 не знает секрсш В", Его формальная спецификация: АО(ялинзВ = од бь рагшегВ абелгА» -4 Ьилгг лолсеб) По этим формальным спецификациям система бр!п находит атаку на протокол (рнс, 8.12), т. е.
последовательшктн соспшний собеседников, нарушающие формальные требования к протоколу. Рне. ЭЛЗ. Агин нв протокол Ннюнма — Шрслсра Итак, ~ поспел к нару зволяе ности являео сообнз Главе В гсгвиО!". Его гстанонльнвя прото~ушаю- Найденная атме слелуюнлш: !. А начинает взаимодейспювать с 1 как с честным партнером. 2. Получив сообщение лмй! от А, 1 посылает свое сообщение лмй! к В, маскируясь под А: он использует лонсеА, полученный от А. Агент В считает, что это сообщение получено ст А, потому что в нем а качестве отправителя стоит А (оно подписано 1, выдающим себа за А ). 3. В посылает сообщение тг82, которое зашифровано ключом А. В зто сообщение включены как лолске, твк и лолсеВ .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
