2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (1185529), страница 52
Текст из файла (страница 52)
п. Однако в значительно большей степени криптографические протоколы нуждакгтл в проверке их основных функций — обеспечения конфиденциальности (неагпиожности получения информации посторонним) и аутечггичностн (подлинно. сгн авторстве) лри передаче информации по сети. Несмотря на относительную простоту криптографических протоколов, многие из прелложенных в атой области решений оказались некорректными, что объясняется трудностью анализа всех вариантов развития событий в системе. в которой параллельно действуют как участники обмена информацией, тмг и злоумышлеи.
мики. Атака на криптографический протокол — зто возможньм действия нечестных пользователей сети (злоумышленников, швцбегя), направленные на нарушение требований безопасности протокола Верификация такого протокола соегоит в выявлении всех возможных атак определенного типа, для чего необходимо построить формальную модель действий честных субъектов обмена и всех возможных действий потенциальных злоумышленников. Если проблему удастся свести к анализу системы с конечным числом состояний, в требования безопасности протокола вырюнть с помощью логической формулы, то ляя верификации мгскно использовать резработанные процедуры тоде! свес(г(пй, результатом работы которых будет либо гарантия того, что атака невозможна, либо копгрпример — найленная атака на протокол, т.
е. последовательность действий злоумышленнют, на шпорой требмзання корректности протокола не выполюются, Гневе В котла ~ шзъ д( может се креп Мы рм Шреде атяры, ауюнт~ проток Предпс  — В публнч могут ~ ника, н нне дее юл сас (рнс. 8. 1. Айсе будуа напал нъ щи Протекал Нндзэвш — Шрбдера. Мы выполннм здесь впаяю на отсутствие атак ювестного крнптографнческого протокола Нидхзма — Шредера. Задачей этого протокола является абеспеченне взанмной аутентификации объектов в компьютерной асти.
Роджер Нндхэм и Михаэль Шредер в 197й году ((120)) впервые предложили механнзм решення проблемы аугентифнкации в сети, который базнруется на использовании так называемого "шифрования с открьпым ключом". Только через 17 лет после опублнковання этого протока. ла с помощью верификации была обнаружена атака на зтат протокол.
Протокол был модифицирован, н в настоящее время на основе модифицированного протокола Нндхэма — Шредера построена шнроко известная система аутентификации Кегбтог (катарах названа именем Церберв, пса нз греческой мнфологнн, охранявшего ворота в ад). Аугентнфнкацня (англ. ангйелг(сшюп), это падтегрждеине лодлнияасти— проверка сеотвагствня субъекта тому, за кого он себя выдаст. Протокол вушнтнфнкацни решает следующую задачу. Имекюя открытав компьютерная сеть, в углах которой находятся субъекты обмена (собеседннкн). Необходнмо абеспечнть взаимную аугентнфнквцню сабеседннков. Как убедить удаленного собеседннка, что ты — это ты7 Как самому убедиться в том, что твой удаленный сабааедннк — мменно тот, за кого он себя выдввг7 Очевидно, что собеаедннка можно считать вутенгнфнцнрованным, если он продемонстрнровал зланве некоторого сек)мягц известного только гму.
Принципиальным момешом протокола Нндхэма — Шредера вшшется удо. стоверенне в том, что собеседник действительно знает свой личный секрет. Ясно, что посылка агентом авоето секрета через сеть беасмысленна: сеть не защищена, н любой злоумышленник может перехватить секрет н затем вальзоваться нм под видом этого агента. Протокол Нидхэма — Шредера решшт проблему аутентнфнкацнн на основе непользования так называемых публичных н аея)мтных ключей. Кшкдый агент Я в сети обладшт публичным (опсрытым) ключом РК(Я) н секретным ключом ВК(Я).
Публичный ключ РК(Я) агента Я вЂ” это метод шифрования информации. Он известен всем другим собеседникам в сети, и кюкдый из ннх может с помощью этого ключа зашифровать посылаемое по сегн сообщение лля Я. Секретный ключ ВК(Я) знает только сам владелец Я этого ключа: только он макет дешифровать любое сообщение, зашифрованное его публичным ключом. Протокол аутентнфнкацнн Нндхэма — Шредера использует для ндентнфикацнн удаленного собеседннка Я знание нм его секретного ткача ВК(Я), нлн, что то вш, возмшкность дешнфрованюз нм соабщення, зашифрованного публичным ключом РК(Я) . Протокол Нндхэма — Шредера швволяет двум нн- рлаеа В отокол перизя голи мо ждитьбя вы- ши он О КИУ.
Я УДО- жкрст. ить не ~ ПОЛЬ- ХИОЯЕ икаый етным рроваэый из сооб- ЭТОГО кйика- И или, О публи ин- Гтсгвие Г. Заяа- объек73 году галии в ьания с ЗОТОКОПро оан ного аугенОй Мн- котла не встречавшинся удаленным собеседникам ие тпько идентифицировать друг прута в сети, но н обменаться им секрепюй информацией, которая может быть использована этими ссбеседникаин дла генерации их общего секретного ключа для последующего сеанса связи, закрытого От других.
Мы рассмотрим здесь несколько упрощенный окрылит протокола Нидхэма— Шредера„отличающийся от оригинального тем, что все собеседники помшп оглкрьплые ключи друг друга, а не обращаются эа ними к открьпому серверу аутентификации, как это сделано в протоколе КегЬеюз. Это не изменяет суть протокола, но чуп упрощает модель.
Предположим, что сушествуег несколько субтжктов (например, А — Айса.  — ВоЬ и др.)„у каждого из которых есгь свой известный всем другин его публичный ключ и известный только ему свой секретный ключ. Субъекты могут передавать сообщения, зашифрованные публичным ключом собеседника, но только сам собеседник может своим секретныи ключом зто сообщение дешифровать. Инициатором обмена будем считать субъевтА!!Ое. Протокол состоит из посылок по несекретному канаяу следующих трех сообщений (рис, К10).
Рнс. $ЛВ. Схема лретоюла аугентифншцин Нилхэма — Шредера 1. АВсе генерирует случайное число(поясе) ЬГГ ()Ä— первая половина ее будущего общего "секрвш" с ВоЬ, жэторый дпа иаделшоети будет потом использован только один раэ), шифрует сообщшше (А,ДГ„), публичным Глвеа В ключом РК(В) агенш В, н посылает по сети шифрованное сообщение (А,М„)рх!в). Здесь 'А — идентификация отправителя. Получить это сообщение может любой, но дешифровано оно может быль только агентом В. 2. Дешифрошш зто гзюбщение, ВоЬ генерирует свое случайное непредсказуемое число !понсе) ЬГв (вторую половину их будущего общего с Айса "секрета"), шифрует сообщение (Ьг,,дгл), публичным ключом РКг,А), принадлежащим Адсе, и посылвет в сеть шифрованное сообщение ()тл,дгл)ря!,) . В этом сообщении кРоме полее Уя (тот секРет агента А, котормй В прочитал нз полученного им сообщения) прис)чствуст и попсе Лгл — вторая часть их общего секрета.
Поскольку сообщение змпнфровано публичным ключом РК(А), то только А!)се может дешифровать зто сообщение. 3. АВсе получает сообщение (Ьгя,дгл) „„и дешифрует его. Наличие Ул в этом сообщении убеждает Абае, что код получен именно от ВоЬ— только он мог дешифровать первое сообщение. Она принимает пару (КюЬГв) как их общий секрет и уверена, что установила связь именно с В. Айсе отсылает ВоЬ сообщение (Ыв)ря!в) с его секРетом Фв, зашифровав его публичным ключом РК(В), чтобы подтвердить прием второго сообщения. 4. ВоЬ принимает сообщение (Ьгя)ря!л) и дешифрует его.
Наличие в нем ЬГв убеждает ВоЬ, по сообщение прислала АВсе — только она могла дешнфроппь второе сообщение с его, ВоЬ, секретом ЬГв. Поэтому ВоЬ таске принимает пару (ьгл,ьге), как их общий секрет, и уверен, что он установил свюь именно с А. Таким образом,' хотя асс сообщения посылаются по несекретному каналу, каждый собеседник, и А, и В, пролемонстрировал своему партнеру знание своих секретных ключей, и поэтому аутентифицированы друг другом: А убежден, чю его собеседник В, а В убежден, что его собеседник А. Кроме того, пара случайных чисел (Ьг„,Ул) известна только этим двум собеседникам (поекольку этн значения посылались голыш зашифрованнымн), н зта пара теперь может быть нспошловюм юш генерации по извсспюму нм обоим алгоритму нового секретшно ключа лля шкрьпого сеанса нх приватной беседы.
Предш вы ши и ннкг нас ем ложею нс мол иия дл Атака общем умыпп нс мол атаку г как и з Злоуьи лозтои г)туся Наша. лений, пел инне о сом В. кскв- Айсс .'(А), нние аА, юлсе ь это ~Ь— пару енно 1пасаег ето- югла ВсЬ о он пара еды. дэлу, ание с А роме днн- Предполшкнм, что компьютеры агентов зшцнщены от вторжешш, а цримгпивы шифрования являются стойкими (т. е. шифрование является абсолкнимм, и никто, кроне владельца секретного ключа, не может дешифровюь посланное ему сообщение, зашифрованное его публичныы ключом). В зпег предположениях протокол выпшдит совершенно безупречно: ведь злоумышленник нс может нмнтиромпь такой обмен, т.
к. не макет дешифровать ни сообщения дня А, нисообгценнядля В. Атака иа протокол Нплзэма — Шредера. Будем считать, что в обмене сообщениями кроме Айте и ВоЬ присутствует еще один собеседник, злоумышленник (1п3пкЬг), который не знает секретных ключей собеседников и нс может получить доступ к данным в их компыстерах, но пытщтся провести атаку на протокол с помощью всех других доступных средспч имея такой же, как н все участники, доступ к каналам связи и зная сам протокол (рис. ЗА)). Злоумышленник выступает перед другнмн агапами честнмм собеседшшом, поэтому с ним, как и с другнмн честными участниками обмена, н А н В могут устанавянмпь кощв$сГы. Рнс, ЗЛ1.
Агапы прстонма ау~епшфаишаи Наша задаче — найти атаку на протокол не путем общих логических рассуди лений, а использовать спшдартпмй подход к асрифнкаянн параллельных систем с помощью сисгсмы верификации Зрю, которая проанализирует вы- Глава В чнслення прн воск действиях злоумышлснннкв, ему доступных, н сама выберет ту последовательность действий злоумышленника, которые прнвсдуг к нарушению требований секретности протокояа. Иными словами, система верификация сгенернруст атаки на протокол, если онн существуют.
Будем счнтать, что злоумышленник может выполнять следующие очевидные действия, возможные прн работе с незащпщеннымн каналамн связи: бз перехватывать сообщення, посланные по каналу; Бз псюылать сообщення, которые он мог перехватить ранее ~щеке если он нс нмеег ключа для нх дешнфровання); сэ сощаавть собственные сообщения, используя пзшстную ему информацию, н посылать нх, маскируясь под любого нз агентов в сети.
Может лн злсумыпшенннк, выполняя такие действия, провести ваку на этот протокол2 Как уже говорилось, атака — это действия, нарушмощне свойства корректности крнптопротокола. Неформально требования корректности данного протокола можно выразпь так: Сг «елаешлослв: когда квжлый нз вгеспов, А н В, успешно завершпя обмен сообщениями, то А верит, чпгего собеседник В млада и шолько тогда, когда В верпт, что его собеседннк А; С2 колфндел«иальлосвм: после того.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
