И.В. Шошмина, Ю.Г. Карпов - Введение в язык Promela и систему комплексной верификации Spin (1161239), страница 11
Текст из файла (страница 11)
Сторона A генерирует свое случайное число, оно является ее частью их общегосекрета. Сторона В генерирует в ответ свое число. В результате работы протокола каждаясторона должна быть уверена в своем партнере и должна узнать его часть секрета.Полный вариант алгоритма построения доверительных отношений предполагает, что припостроении отношений публичные ключи партнеров не хранятся на каждой стороне, за ниминадо обращаться к серверу.
Без потери общности будем считать, что каждый участник знаетпубличные ключи всех возможных партнеров. Сокращенный алгоритм Нидхама-Шредератаков:Сообщение 1. Сторона А отправляет стороне В сообщение 1, в зашифрованной частикоторого передает свой идентификатор и nonceA. Сообщение шифруется открытым ключомB.Сообщение 2. Сторона В, получив сообщение 1, расшифровывает его, проверяетсоответствует идентификатор отправителя в зашифрованной части с идентификаторомоткрытой части письма. Если соответствие есть, то сторона В уверена в своем партнере иотправляет сообщение 2, зашифровав публичным ключом А два секрета: nonceA и nonceB.Сообщение 3. Сторона А, получив сообщение 2, расшифровывает его, находит в сообщениисвой nonceA, что убеждает ее, что отправителем является В, поскольку только В могпрочитать зашифрованное сообщение 1.
Теперь сторона А знает полный секрет, онаподтверждает этот факт, посылая стороне В ее часть секрета nonceB в зашифрованной частисообщения 3. Сторона В, получив сообщение 3, уверена, что во-первых, ее партнер – А, вовторых, А знает полный секрет.Спустя почти 20 лет использования алгоритма, в 1995 году Лоуве (Lowe) описал модельалгоритма на CSP и верифицировал его при помощи верификатора FDR [4].Он ввел в процесс обмена сообщениями третью сторону – злоумышленника (intruder),поведение которого не подчинялось определенном алгоритму. Злоумышленник можетвыполнять несколько действий с сообщениями:1. прослушивать сообщения, идущие по каналу,2.
сохранять схваченные сообщения; если сообщения предназначались ему, то онрасшифровывает скрытую часть, иначе, хранит в том виде, в котором ее получил,473. генерировать сообщения на основе имеющейся информации,4. отправлять свои сообщения в сеть.Введения злоумышленника с заданным поведением оказалось достаточным для того, чтобыобнаружить криптографическую атаку в алгоритме Нидхама-Шредера.Описание модели на языке PromelaСмоделируем протокол Нидхама-Шредера на языке Promela и попытаемся обнаружить атаку,найденную Лоуве, средствами Spin.В модели присутствуют три участника Alice (сторона А), Bob (сторона В) и Intruder(злоумышленник), которым поставим в соответствие три одноименных процесса.
Будеммоделировать некорректное поведение алгоритма, поэтому считаем, что все сообщения всети проходят через злоумышленника. Для обмена сообщениями между процессами введемтри рандеву-канала: fakedA и fakedB (испорченные), intercepted (прослушиваемый).Записывая сообщение в intercepted канал, Alice или Bob не знают, что сообщение будетперехвачено. Прочитывая сообщение из своего испорченного канала fakedA, Alice непредполагает, что сообщение было испорчено (аналогичная ситуация для Bob).
Intruderчитает сообщение из канала intercepted, записывает сообщение в канал fakedA или вканал fakedB в зависимости от того, кому предназначается сообщение. Используется лишьодин тип сообщения msg./* Читающий из faked канала не подозревает, что сообщение было испорчено */chan fakedA = [0] of {mtype, mesCrypt};chan fakedB = [0] of {mtype, mesCrypt};/* Пишущий в intercepted канал не знает, что сообщение будет прочитано */chan intercepted = [0] of {mtype, mesCrypt};Структура сообщения сложная и состоит из нескольких частей, для того чтобы ее описатьвведены данные такого типа:typedef mesCrypt {/* открытая часть сообщения */mtype s,/* отправитель *//* получатель */r,nummsg,/* номер сообщения */key,/* публичный ключ, которым зашифровано сообщение *//* зашифрованная часть сообщения */d1,/* здесь может быть идентификатор или nonce */d2};Кроме того, в перечислимых типах еще введены идентификаторы процесса, публичныеключи, случайные числа каждой стороны и состояния участников.mtype={msg,alice, bob, intruder,pkA, pkB, pkI,nonceA, nonceB, nonceI,ok, err};/* тип сообщения/* идентификаторы участников/* публичные ключи участников/* случайные числа участников*/*/*/*/Введем некоторые ограничения в модели для уменьшения числа возможных состоянийсистемы:48•инициирует начало обмена сообщениями Alice,•Intruder прослушивает сообщения от Alice и Bob, потому он знает ихидентификаторы изначально,•Intruder хранит лишь последнее прослушиваемое сообщение,•получив сообщение, Intruder обязательно отправляет сообщение (прослушанноеили сохраненное) в сеть,•в случае если Alice или Bob получают сообщение, не соответствующее ожидаемомупо любому из признаков (согласно действующему алгоритму), то процесс прекращаетработу.Получаемые из своих каналов данные, Alice и Bob хранят в переменной data описанноговыше типа mesCrypt.
Опишем лишь одну из проверок, которую проходит получаемоесообщение на честной стороне. Например, первое сообщение получает Bobif:: (data.r == bob) &&/* Bob ли получатель сообщения ? *//* Можно ли расшифровать сообщение */(data.key == pkB) &&/* Можно ли доверять отправителю ? */(data.s == data.d1) &&(data.nummsg == 1)->/* Правильный ли № сообщения ? */partnerB = data.s;pnonce = data.d2;:: else -> goto stopB;fi;Он проверяет, является ли он получателем сообщения, проверяет номер сообщения (должноприйти первое сообщение), проверяет, что информация зашифрована его ключом. Если всетак, Bob может расшифровать сообщение.
Затем Bob проверяет, что идентификаторотправителя в открытой части сообщения соответствует идентификатору в зашифрованнойчасти сообщения. Он запоминает партнера и его часть секрета, только если все эти проверкипройдены, иначе он останавливает работу. Совершенно очевидно, что при таком количествеусловий большинство попыток злоумышленника вторгнуться во взаимодействие Alice иBob, закончатся безуспешно. Нас, однако, интересует другое: существуют ли успешныепопытки вторжения. Оказывается, что такие возможности существуют, и они могут бытьСГЕНЕРИРОВАНЫ системой верификации точно так же, как было сгенерировано решение взадаче “фермер, волк, коза, капуста“.Intruder использует две переменные типа mesCrypt – переменную data для полученияданных из канала, а другую fake для генерации своего сообщения на основе имеющейсяинформации.
Злоумышленник не подвергает приходящие сообщения никаким проверкам,кроме одной: в случае, если зашифрованные данные зашифрованы его ключом (data.key== pkI), то он может расшифровать закрытую часть сообщения и узнать ее содержимое(значимые величины nonceA и nonceB). Остальные действия Intruder’а связаны ссоставлением своего сообщения, которое он отправит в сеть.active proctype Intruder() {/* … */end: doсообщения/* бесконечный цикл, в котором читаемиз канала intercepted */:: intercepted ? msg(data) ->if/* осуществляем проверку данных data */:: (data.key == pkI) -> /* если можем расшифровать секретную часть,49то извлекаем оттуда информацию в открытомвидеtrue;*/if:: (data.d1 == nonceA || data.d2 == nonceA) -> knowNA =/* возможно нам попался nonceA, зафиксируем, что мы его знаем knowNA=1 *//* аналогично для nonceB *//* … */fi;:: else -> skip;/* иначе: ничего не делаем */fi;/* построение испорченного сообщения fake */if/* недетерминировано выбираем отправителя *//* если отправитель Alice */:: fake.s = alice ->/* то получатель Bob */fake.r = bob; fake.key = pkB;/* аналогично для Bob и самого злоумышленника*/fi;/* поскольку злоумышленник не знает правила построения сообщенияон помещает в часть сообщения d1 любую известную емуоткрытую информацию */if:: fake.d1 = alice;:: fake.d1 = bob;:: fake.d1 = intruder;:: fake.d1 = nonceI;:: (knowNA) -> fake.d1 = nonceA;:: (knowNB) -> fake.d1 = nonceB;fi;/* аналогично он поступает и с частью d2 *//* … *//* злоумышленник может вставить неизвестную зашифрованную часть изтолько что полученного сообщения */if:: (data.key != pkI) ->fake.key = data.key;fake.d1 = data.d1;fake.d2 = data.d2;:: else -> skip;fi;/* выбираем номер сообщения *//* … *//* отправляем сообщение или полученное, или свое созданноев канал, предназначая его либо Alice, либо Bob */if:: (data.r == alice) ->fakedA ! msg(data); /* повторяем полученное сообщение Alice*/:: (data.r == bob) ->fakedB ! msg(data); /* повторяем полученное сообщение Bob *//* аналогично для испорченного сообщения *//* … */fi;50od;}Код алгоритма Нидхама-Шредера на языке Promela/* Протокол Нидхама-Шредера *//* Три участника: Alice, Bob, и Intruder, которые обмениваются сообщениями другс другом по сети*/mtype = {msg, alice, bob, intruder, pkA, pkB, pkI,nonceA, nonceB, nonceI, ok, err};/* По сети передается сообщение( отправитель, получатель, №, зашифрованные данные (случайные числа или ID) )*/typedef mesCrypt {/* сообщение */mtype s, r, nummsg,/* открытая часть */key, d1, d2;/* зашифрованная часть */};/* Читающий из faked канала не подозревает, что сообщение было испорчено */chan fakedA = [0] of {mtype, mesCrypt};chan fakedB = [0] of {mtype, mesCrypt};/* Пишущий в intercepted канал не знает, что сообщение будет прочитано */chan intercepted = [0] of {mtype, mesCrypt};/* Переменные, используемые в LTL формулах */mtype partnerA, partnerB;mtype statusA, statusB;/* Переменные отражают знание посторонним секретных частей общего ключа */bool knowNA, knowNB;/* Честный инициатор процесса обмена */active proctype Alice() {mtype pkey, pnonce;mesCrypt data;statusA = err;if /* недетерминировано выбирает партнера */:: partnerA = bob; pkey = pkB;:: partnerA = intruder; pkey = pkI;fi;/* конструируется сообщение № 1 и отправляется */d_step {data.s = alice;data.r = partnerA;data.nummsg = 1;data.key = pkey;data.d1 = alice;data.d2 = nonceA;}intercepted ! msg(data);/* ожидает сообщения № 2 и расшифровывает его */fakedA ? msg(data);51end_errA:/* проверяет, что сообщение предназначалось именно ему ичто отправитель его партнер,иначе останавливает процедуру обмена.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
