МОДЕЛЬ  НАРУШИТЕЛЯ  ДЛЯ  ФОРМАЛЬНОЙ  ВЕРИФИКАЦИИ  КРИПТОГРАФИЧЕСКИХ  ПРОТОКОЛОВ  АУТЕНТИФИКАЦИИ

Борхаленко  Вадим  Анатольевич

аспирант  кафедры  экономики  в  энергетике  и  промышленности  Национального  исследовательского  университета  «Московский  Энергетический  Институт»,  РФ,  г.  Москва

E-mail: 

THE  INTRUDER  MODEL  FOR  CRYPTOGRAPHIC  PROTOCOLS  FORMAL  VERIFICATION

Borkhalenko  Vadim

postgraduate  of  Economics  of  Power  Engineering  and  Industry,  National  Research  University  “Moscow  Power  Engineering  Institute”,  Russia,  Moscow

АННОТАЦИЯ

В  данной  работе  рассматривается  расширенная  модель  нарушителя  Долева-Яо  с  использованием  тактик  известных  атак.  С  помощью  аппарата  автомата  Бюхи  приводится  короткое  математическое  описание  данной  модели.  Приведен  пример  использования  данной  модели  нарушителя  для  верификации  свойств  безопасности  протокола  SSL  c  помощью  метода  model  checking.

ABSTRACT

In  this  article  the  expanded  Dolev-Yao  model  of  intruder  is  described.  For  short  mathematical  description  of  this  model  we  use  the  Buchi  automata  tool.  The  application  of  the  intruder  model  is  used  in  example  of  the  security  properties  verification  of  the  SSL-protocol  based  on  model  checking  method.

Ключевые  слова:  модель  Долева-Яо;  математическое  моделирование;  model  checking;  криптографические  протоколы.

Keywords:  Dolev-Yao  model;  mathematical  modeling;  model  checking;  cryptographic  protocols.

1.  Введение

Метод  верификации  на  моделях  (model  checking)  [2,  с.  35,  3,  с.  41,  6,  с.  1,  7,  с.  198]  заключается  в  проверке  того,  что  на  проверяемой  формальной  модели  системы  заданная  спецификация  выполняется  на  всех  вычислениях.  В  данной  работе  метод  model  checking  используется  для  верификации  протокола  SSL  [5,  с.  97],  применяемого,  в  частности,  в  системах  безопасных  электронных  платежей.  Каждый  из  участников  данного  протокола  рассматривается  как  параллельный  взаимодействующий  процесс.  Однако  для  данной  статьи  основной  интерес  представляет  предлагаемая  модель  процесса,  описывающего  поведение  нарушителя.  Многие  инструментальные  средства  верификации  протоколов  используют  модель  Долево-Яо  для  выявления  возможных  уязвимостей  [3,  с.  24,  4,  с.  61].  Целью  нарушителя,  описываемого  в  данной  модели,  является  обнаружение  секрета  в  передаваемом  сообщении  или  создание  сообщений,  благодаря  которым  легальные  участники  протокола  могут  принять  злоумышленника  за  легального  пользователя,  т.  е.  олицетворение  участника  протокола.  Однако  возможны  и  другие  тактики,  с  помощью  которых  осуществляются  успешные  атаки  на  протоколы,  например  атака  повтора  [1,  с.  100].  Целью  данной  работы  является  создание  расширенной  модели  Долева-Яо,  использующей  тактику  атаки  повтора  и  DoS-атаки,  и  формализация  данной  модели  с  помощью  автоматов  Бюхи  для  последующей  верификации  криптографических  протоколов.  Рассмотрим  модель  угроз  Долева-Яо  и  предлагаемую  реализацию  ее  расширения.

2.  Модель  угроз  Долева-Яо 

Рассмотрим  модель  угроз  злоумышленника  в  компьютерной  сети,  предложенную  Долевым  и  Яо.

Предполагается,  что  злоумышленник  обладает  следующими  возможностями  [4,  с.  61]:

·     Может  перехватывать  любое  сообщение,  передаваемое  по  сети.

·     Является  законным  пользователем  сети  и  имеет  право  устанавливать  соединение  с  любым  другим  пользователем.

·     Может  посылать  сообщения  всем  пользователям  от  имени  любого  пользователя.

Однако  в  модели  есть  и  ограничения  на  возможности  нарушителя:

·     Злоумышленник  не  может  угадать  нонс  (выбранное  участником  протокола  случайное  число).

·     Не  имея  соответствующего  ключа,  не  может  расшифровать  зашифрованное  сообщение.

·     Не  может  сгенерировать  закрытый  ключ  участника  по  его  открытому  ключу.

·     Контролируя  средства  связи,  злоумышленник,  тем  не  менее,  не  может  получить  доступ  к  закрытым,  внутренним  ресурсам,  например,  к  памяти  или  жёсткому  диску  пользователя.

Однако  данных  предположений  недостаточно.  Например,  нарушитель  может  хранить  перехваченные  сообщения  и  вставлять  их  при  попытке  установления  нового  защищенного  соединения,  также  нарушителю  может  быть  известен  протокол  установления  защищенного  соединения  и  известны  тактики  совершения  различных  атак.  Модель  нарушителя,  предлагаемая  автором,  заключается  в  том,  что  злоумышленник  может  стохастически  выбирать  любую  тактику  атаки,  использовать  шаг,  подразумеваемый  данной  атакой,  а  после  совершенного  действия  может  заново  выбрать  тактику  атаки  и  использовать  действие,  описываемое  уже  новой  атакой,  что  приведет  к  комбинации  атак. 

3.  Формальная  модель  нарушителя

Опишем  и  формализуем  тактики  атак,  используемые  злоумышленником:

·                        Атака  «человек  посередине»  (Man  in  the  middle,  MIM-атака)  —  термин  в  криптографии,  обозначающий  ситуацию,  когда  атакующий  способен  читать  и  видоизменять  по  своей  воле  сообщения,  которыми  обмениваются  корреспонденты,  причём  ни  один  из  последних  не  может  догадаться  о  его  присутствии  в  канале.  Представим  упрощенную  и  укороченную  (в  коде  автора  она  более  подробна)  формальную  модель  данной  тактики  атаки  с  помощью  следующего  автомата  Бюхи  (рис.  1).

Рисунок  1.  Автоматная  модель  MIM-атаки

·     Атака  повтора  (replay  attack)  —  в  этой  атаке  противник  полностью  или  фрагментарно  записывает  сеанс  протокола  и  повторно  применяет  эти  сообщения  в  более  поздние  моменты  времени  или  в  следующем  сеансе,  т.  е.  «повторяет»  (отсюда  название  «replay»)  сеанс  или  его  часть  в  некоторый  более  поздний  момент  времени.  Заметим,  что  многие  часто  используемые  атаки  являются  частными  случаями  атаки  повтора,  например,  атака  типа  отражения  (reflection  attack).  На  рис.  2  приведен  упрощенный  автомат  Бюхи,  описывающий  данную  атаку.

Рисунок  2.  Автоматная  модель  Replay-атаки

·     DoS-атака,  целью  которой  является  переполнение  каналов  связи  ложными  сообщениями,  которые  препятствуют  легальным  участника  протокола  установить  или  поддерживать  защищенное  соединение  (рис.  3).

Рисунок  3.  Автоматная  модель  DoS-атаки

Нарушитель  может  комбинировать  данные  атаки  и  на  основе  их  тактик  получать  новые  виды  атак,  например,  атаку  параллельного  сеанса.  Объединением  данных  автоматов  и  является  автомат,  описывающий  модель  нарушителя.  Однако,  так  как  целью  DoS-атаки  является  переполнение  каналов  связи,  ее  стоит  рассматривать  отдельно,  чтобы  возможно  было  рассмотреть  комбинацию  «осмысленных»  тактик.

4.  Пример  проверки  спецификаций  для  протокола  SSL

Рассмотрим  две  спецификации,  описанные  с  помощью  аппарата  логики  LTL  [2,  с.  41,  7,  с.  198],  проверяемые  на  протоколе  SSL.  Первая  определяет  классическое  свойство  безопасности,  описывающее  невозможность  знания  перехватчиком  нонсов  обоих  участников  и  секретной  последовательности  PreMaster:

Инструментальное  средство  SPIN  показало,  что  данное  свойство  выполняется  на  всех  вычислениях  системы  (рис.  4).

Рисунок  4.  Результат  проверки  свойства  безопасности

Второе  свойство  описывает  стабильность  установленного  SSL-соединения,  его  можно  еще  назвать  свойством  живости  [2,  с.  227].  Если  клиент  отправил  сообщение,  то  сервер  обязательно  его  получит:

G ((Client==Send->F(Server==Receive))  &  F(Client==Send))

Атомарный  предикат  Client==Send  означает,  что  клиент  отправил  сообщение  в  защищенном  сеансе,  Server==Receive  означает,  что  сервер  получил  сообщение  в  защищенном  сеансе.  Однако  данное  свойство  нарушается  с  помощью  атаки  повтора,  и  защищенное  соединение  может  быть  разорвано.  Укажем  трассу,  которая  приводит  к  разрыву  соединения  (рис.  5).

Рисунок  5.  Нарушение  свойства  живости

При  использовании  нарушителем  DoS-атаки  все  процессы,  описывающие  участников  протокола,  блокируются,  и  все  вышеуказанные  свойства  не  выполняются,  как  это  видно  на  рис.  6.

Рисунок  6.  Результат  выполнения  DoS-атаки

5.  Выводы

Разработанная  автором  формальная  модель  нарушителя  эффективно  зарекомендовала  себя,  как  расширение  модели  Долева-Яо.  Данная  модель  может  использоваться  на  этапе  проектирования  протоколов  аутентификации  для  формальной  верификации  модели  протокола.  В  дальнейшем  целью  автора  является  исследовать  протоколы  электронной  коммерции,  используя  приведенную  модель,  а  также  формализовать  данную  модель  нарушителя  с  помощью  временных  сетей  Петри.

Список  литературы:

1.Давыдов  А.Н.  Атаки  на  протоколы  установления  ключа.  //  Труды  научно-технической  конференции  Безопасность  информационных  технологий.  Пенза,  2004.  —  С.  99—104.

2.Карпов  Ю.Г.  Верификация  параллельных  и  распределенных  систем.  СПб.:  БХВ-Петербург,  2010.  —  552  c.

3.Косачёв  А.С.,  Пономарёва  В.Н.  Анализ  подходов  к  верификации  функций  безопасности  и  мобильности.  ИСП  РАН,  2004.  —  101  c.

4.Мао  В.  Современная  Криптография:  теория  и  практика:  пер.  с  англ.  М.:  Издательский  дом  “Вильямс”,  2005.  —  763  c.

5.Нестеров  С.А.  Информационная  безопасность  и  защита  информации.  СПб.:  Изд-во  Политехн.  Ун-та,  2009.  —  125  c.

6.Powell  J.D.  Model  Checking  for  Software  Security  Properties.  [Электронный  ресурс]  —  Режим  доступа.  —  URL:  http://trs-new.jpl.nasa.gov/dspace/bitstream/2014/7143/1/03-0769.pdf  (дата  обращения:  04.01.2015).

7.Maggi  P.,  Sisto  R.  Using  Spin  to  Verify  Security  Properties  of  Cryptographic  Protocols.  Lecture  Notes  in  Computer  Science,  2002.  —  210  с.