Программное средство логической проверки корректности криптографических протоколов распределения ключей на основе BAN-логики

Введение. Криптографические протоколы играют значимую роль в защите информации. В разное время было создано большое количество криптографических протоколов различного назначения. Фактически протокол представляет собой список сообщений, которыми должны обменяться участники протокола. Несмотря на кажущуюся простоту, проблема оценки уровня безопасности протоколов является очень сложной. Так многие протоколы, считавшиеся надёжными долгое время, спустя десятки лет демонстрировали свою уязвимость в результате атак [1, 2]. Если определять криптографический протокол более строго, то это — распределённый алгоритм последовательности шагов, точно специфицирующих действия, которые требуются от участников для решения некоторой криптографической задачи [1,3].

Для исследования уровня безопасности, который может обеспечить как уже существующий, так и только разрабатываемый протокол, используют специализированные формальные методы. Среди математических аппаратов, используемых для решения задачи формального анализа протокола, важную роль играют различные логики, среди которых наибольшее распространение получили логики доверия. В работе [4] была предложена BAN-логика, которая стала основой для разработки ряда других логик. Данная логика является первой попыткой построения формального языка для описания исходных предположений, правил вывода и конечных целей анализа безопасности. BAN-логика, как и её расширения, позволяют проводить анализ протокола вручную, однако это достаточно трудоёмко и чревато ошибками. Целесообразным представляется использовать автоматизированные системы анализа, но в настоящее время подобных программ в свободном доступе нет. Программные средства (ПС), реализующие анализ протоколов методами BAN-логики, могут быть полезны и для тестирования работоспособности и безопасности криптографических протоколов обмена ключами, и для учебных целей, так как изучение любых логик доверия базируется на владении навыками анализа методами BAN-логики.

Постановка задачи. Создать ПС BanAnalyzer, автоматизирующее процесс анализа криптографических протоколов методами BAN-логики. Входные и выходные данные программного средст- ва должны быть максимально приближены по своему формату к идеализированным протоколам, предлагаемым создателями BAN-логики в оригинальной работе [4].

Для выполнения задачи кратко опишем идеи, лежащие в основе BAN-логики, и сконструируем алгоритмы работы ПС и опишем идею его создания. Затем рассмотрим пример анализа протокола с использованием ПС BanAnalyzer и исследуем корректность результатов его работы. Основные положения BAN-логики. Данная логика используется для анализа протоколов распределения ключей [4—6]. Основная идея BAN-логики состоит в отслеживании восприятия сторонами поступающей информации, а именно: какие данные они принимают на веру, какие данные им точно известны и какие могут быть выведены логическим путём из достоверных для них фактов. Так, для каждого шага протокола методами BAN-логики формируется список утверждений о безопасности протокола, которым доверяют участники протокола.

При использовании BAN-логики не моделируются ни различие между простым просмотром сообщения и пониманием его, ни пересмотр доверий, ни знание. Все эти аспекты адресуются к неформальному отображению спецификации протокола в спецификацию BAN-логики, которое авторы [4] называют идеализацией. Таким образом, анализу протокола предшествует его идеализация, которая производится человеком самостоятельно согласно описанию протокола. Идеализированные протоколы считаются более ясными и обладающими более полной спецификацией, чем традиционные описания. В терминах BAN-логики протокол рассматривается на абстрактном уровне, следовательно, ошибки конкретной реализации, такие как тупики или неправильное использование криптосистемы, при анализе не обнаруживаются. Методами BAN-логики анализируется непосредственно криптографический протокол и его логика, а используемые в нём криптографические методы считаются стойкими.

Перечислим объекты, которые различают в BAN-логике, и укажем их обозначения. Участники протокола обычно обозначаются А, В, 8; общие ключи шифрования, применяемые при симметричной криптографии, обозначаются К_АВ, Kas и K_BS, где индексы в обозначении указывают на участников, использующих данных ключи; открытые ключи, используемые при асимметричной криптографии, обозначаются К_А, K_s и К_в (где А, В, 8— участники, которым принадлежат данные открытые ключи), связанные с ними секретные ключи обозначаются Кд¹, Ks""¹ и К_в^-1 соответственно; Мд, N_B, N_s — специальные числовые значения (нонсы, метки времени); X, Y— общее обозначение для формул и утверждений.

Единственная используемая логическая операция в BAN-логике — конъюнкция обозначается запятой. Свойства ассоциативности и коммутативности считаются доказанными.

Укажем базовую систему обозначений, принятую в BAN-логике.

Р |= X — участник протокола Р верит (believes) утверждению X; далее участник Р будет действовать, считая, что утверждение X верно.

Р < X — участник Р видит (sees) утверждение X; участник Р получил от кого-то утверждение Хи может его прочитать и повторить.

Р |~ X — участник Р однажды заявил (once said) утверждение X, и в тот момент Р верил утверждению X, однако время этого высказывания неизвестно.

Р |^ X — Р обладает полномочиями (jurisdiction) над X; т. е. участник Р является автором утверждения X и верит в него. Эта конструкция часто обозначает, что пользователь имеет права на создание ключей.

• #(Х^ — утверждение ^является свежим (fresh). Под термином «свежий» понимается, что утверждение X сгенерировано в текущем сеансе связи и не было послано до начала работы протокола. к

Р <^Q — участники Р и Q могут использовать общий ключ К для установления связи. Предполагается, что ключ К достаточно стоек и не может быть взломан кем-либо из посторонних, если это не предусмотрено протоколом.

К

• -^Р — Р имеет открытый ключ К (public key), а также согласованный с ним качественный секретный ключ /С¹, никому не известный, кроме Рили участника, которому он доверяет.

P«Q — утверждение ^является секретом, известным только участникам Ри Q, и они могут использовать Хдля доказательства своей аутентичности один другому.

^Х^_к — данные Xзашифрованы с использованием ключа К. Шифрование считается надёжным.

^ — конкатенация утверждения Хи секрета Y. Секрет /полностью идентифицирует объект, заявивший утверждение X.

При анализе протоколов аутентификации различают два времени: прошлое и настоящее. Настоящее время начинается со старта данного сеанса работы протокола. Все сообщения, посланные до этого, считаются старыми сообщениями, и в ходе работы протокола необходимо предотвращать возможность появления таких сообщений. Все веры, принятые в настоящем, неизменны на протяжении всего сеанса работы протокола, однако те веры, которые были приняты в прошлом, не обязательно должны быть переведены в настоящее. Такое простое разделение времени на прошлое и настоящее является достаточным для использования в ВАМ-логике.

Ниже укажем наиболее важные правила вывода BAN-логики, используемые для получения новых утверждений и доверий участников протокола. В постулатах используем запись вида

А, В

С '

что означает, что так как утверждения А и В верны, то верно и утверждение С.

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

PNQ^P,P<^K

P\=Q\~X   '

P\^Q,P

P\=Q\~X

PNQoP.P^ P\=Q\~X    "

Дадим эквивалентную словесную формулировку первому из этих выражений: из предположений о том, что Р верит в совместное с Q использование ключа К, и Р видит сообщение X, зашифро- ванное ключом К, делаем вывод: Р верит, что Q в какой-то момент высказал X Заметим, что здесь неявно предполагается, что сам Р никогда не высказывал X.

Правило проверки нонсов:

PN#W,PNQ\~X P\-Q\-X

• т. е. если Р верит, в свежесть сообщения Хи верит, что Q когда-то высказал X, то он верит в то, что Q по-прежнему доверяет X.

Правило полномочий:

P|=Q|^2G^MM

Р |=Х говорит, что вера Рв полномочия Q относительно Хи вера Qb X, влекут за собой веру Рв X.

Как уже было сказано, перед непосредственным анализом протокола его необходимо представить в идеализированной форме. Для этого нужно записать шаги протокола в терминах BAN-логики. Обычно в литературе каждый шаг протокола записывается в виде символьной строки:

Р -^Q\ сообщение.

Такая запись означает, что участник Р посылает сообщение участнику Q, a Q получает это сообщение. Сообщение представляет собой строчку, содержащую различные данные. Сообщение в идеализированном протоколе — это формула. Например, в описании протокола может быть такая символьная запись:

^еЩА, к,л которая означает, что В получил сообщение от А. Сообщение зашифровано ключом KBS связи участника В и доверенного сервера S и содержит имя участника протокола А, а также ключ КАВ для связи участников А и В. Этот шаг может быть идеализирован как:

^АВ

в<\а^в что означает, что участник В принял сообщение и может действовать дальше на основе полученных данных. В идеализированной форме опускаются части сообщений, которые не способствуют получению новых формул. Например, можно опустить сообщения, используемые как рекомендации о необходимости инициализации связи, то есть, как будто участники действуют спонтанно. Идеализированные протоколы не включают открытый текст как часть сообщения, так как эти части могут быть подделаны.

Идеализированные протоколы считаются более ясными и более законченными спецификациями, чем традиционные описания, используемые в литературе, поэтому авторы BAN-логики рекомендуют использовать идеализированные формы при изобретении и описании протоколов. Получение практического вида протокола из идеализированной формы, хотя и не совсем тривиально, но менее трудоёмко и менее подвержено ошибкам, чем однозначное понимание специфических неформальных записей протоколов. К сожалению, идеализация протокола производится человеком самостоятельно, этот этап нельзя автоматизировать, и, следовательно, при его выполнении возможны ошибки. К тому же не существует строгого алгоритма записи протокола в идеализированной форме. Более того, в ряде случаев идеализация одного и того же шага протокола может быть выполнена различными способами.

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

Для протоколов передачи ключей минимальными целями являются:

А\=А^В, В\=А^В

• т. е. оба участника верят в то, что у них есть общий ключ К для связи. Однако можно потребО' вать от протокола большего, например уверенности участников в свежести ключа:

Д|=#| А^В\,В\=*\ А^В а также уверенности каждого из них в том, что другой участник также верит в этот ключ

А\=В\=А^В,В\=А\=А^В.

Такие утверждения называют подтверждением приёма ключа. Т. е. в результате работы протокола А будет уверен в знании В о том, что он разделяет секретный ключ с А, а В будет верить в то, что А знает об их общем ключе. В случае использования асимметричной криптографии цели анализа протокола формируются аналогичными утверждениями.

Пример анализа протокола методами BAN-логики. Рассмотрим хорошо известный протокол Керберос [2, 3], разработанный как часть проекта Project Athena корпорацией МГГ. Протокол позволяет двум участникам, используя доверенный сервер аутентификации, получить общий ключ. Напомним, что протокол состоит из 4 шагов. На первом участник А посылает серверу 8 сообщение, указывая участника В, с которым хочет установить общий ключ; на втором шаге сервер 5отправляет А новый ключ К_АВ, зашифрованный ранее установленным между >4 и 5общим ключом K_As, а также К_АВ, зашифрованный общим между В и 8 ключом K_Bs- В своё сообщение 8 добавляет временные метки для подтверждения свежести ключа; на следующем шаге участник А пересылает участнику В сообщение из двух частей: ключ К_АВ, зашифрованный K_Bs, а так же ключ К_АВ, зашифрованный этим же ключом. В своё сообщение А добавляет временные метки; на последнем шаге участник В пересылает А сообщение со своей временной меткой, закрытое новым общим ключом К_АВ. В традиционной символьной записи шаги этого протокола выглядят следующим образом:

Шаг1\А^8'\А,В^

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

Шаг2\А

Шаг 3: В

Шаг

^АВ

В табл, указаны первоначальные доверия участников, необходимые для начала работы протокола.

Доверия участников протокола Керберос (в терминах BAN-логики)

Доверия	Значение
КА5	А верит, что между А и Sустановлен общий ключ для симметричного шифрования Kas
КВ5 В\=В^5	вверит, что между в и Sустановлен общий ключ для симметричного шифрования Kbs
А И S о Кдв	А доверяет серверу аутентификации S генерацию симметричного ключа Кдв
B\=So Кдв	в доверяет серверу аутентификации генерацию симметричного ключа Кдв
а\=#т5	А верит в то, что временная вставка Ts, созданная S, актуальна (доказывает свежесть сообщения от S)
в\=#т5	вверит в то, что временная вставка Ts, созданная S, актуальна (доказывает свежесть сообщения от S)
А\=#ТВ	А верит в то, что временная вставка В актуальна (доказывает свежесть сообщения от в)
вмтд	В верит в то, что временная вставка А актуальна (доказывает свежесть сообщения от А)

Проанализируем шаги протокола последовательно один за другим, по возможности применяя к ним все основные правила BAN-логики. Запишем основные значимые этапы анализа. На втором шаге, применяя правило значения сообщений (1) получаем:

Из правила проверки коксов (2) получаем

Применение правила проверки полномочий (3) даёт нам следующий результат:

Таким образом, в результате шага 2 протокола участник А доверяет полученному от S ключу для связи А и В.

Последовательно применяя (1), (2) и (3) к шагу 3 протокола получаем

К АВ

К,

Результат анализа шага 4 протокола даёт формулу:

^АВ

Таким образом, анализ BAN-логикой показал, что выполнение протокола Керберос обеспечивает достижение всех целей симметричного протокола обмена ключами без использования дополнительных доверий. Ещё раз подчеркнём, что использованная логика не показывает уязвимостей протокола, связанных со слабостью процедур шифрования и ошибками реализации. По результатам анализа мы получили знание о логической корректности протокола.

Алгоритмическое конструирование ПС. Алгоритмы работы программы условно можно разделить на четыре части: алгоритмы, реализующие взаимодействие с пользователем; алгоритм разбора введённого пользователем текста описания протокола на утверждения ВАМ-логики; алгоритм анализа протокола и алгоритм формирования выходных данных.

Алгоритм разбора пользовательского ввода на утверждения ВАМ-логики получает на вход текст описания протокола. Текст может содержать шаги протокола, принятые доверия и комментарии к описанию. Комментарии из дальнейшего анализа исключаются как незначимые для анализа протокола. Выделить их в описании достаточно просто по служебному символу «#», предваряющему текст комментария. Шаги протокола отличаются от доверий тем, что их запись начинается с номера. Затем в строках, содержащих шаги и доверия, выделяем имена участников, ключевые слова (believes, sees, said, controls) и т. д. Алгоритмом по мере работы заполняются списки шагов, доверий и сообщений об ошибках — эти три списка считаются выходными данными этого алгоритма.

S believes Kab

A believes Kas

S believes Kas

A believes S controls Kab A believes fresh(Ts)

В believes Kbs

S believes Kbs

В believes S controls Kab

В believes fresh(Ts)

В believes fresh(Ta) 2 A sees (Ts, Kab)Kas

• 3 В sees (Ts, Kab)Kbs #3 В sees (Ta)Kab

• #4 A sees (Ta+l)Kab

Рис. 1. Основное окно ПС BanAnalyzer и полный текст описания исследуемого протокола Керберос

Наиболее трудоёмким является алгоритм проведения анализа. Он различается для симметричных и асимметричных криптографических протоколов. Оба варианта алгоритма включа-

И ют в себя как составную часть алгоритм поиска по довериям и результатам. Результат работы алгоритма поиска указывает, известно ли уже данное утверждение и чем оно является — первоначальным доверием или результатом анализа. Анализ каждого из шагов протокола проходит через три стадии, на каждой из которых последовательно применяются основные правила BAN-логики: проверка значений сообщений, проверка нонсов и проверка полномочий, при необходимости к основным правилам добавляется ещё ряд стандартных правил BAN-логики, не описанных в данной работе.

Выходные данные представляются в виде текстового файла, который формируется в следующем порядке: сначала к выходному тексту добавляем все распознанные шаги протокола в естественном порядке, затем добавляем все распознанные доверия протокола, после этого дописываем все полученные результаты анализа протокола в порядке их получения, в заключение вносим в результирующий файл информацию о всех неиспользованных довериях протокола, записи о правилах BAN-логики, применённых к каждому из шагов протокола, записи об ошибках во время распознавания шагов и доверий протокола.

Программное конструирование анализатора BAN-логики BanAnalyzer. Для реализации программного средства был использован высокоуровневый язык программирования C++ в совокупности с бесплатным фреймворком Qt4. Архитектурный каркас данного ПС реализует шаблон проектирования MVC («модель — представление — контроллер»). Это подразумевает, что модели данных приложения, пользовательский интерфейс и основная логика работы приложения разделены на три слабосвязных компонента так, что модификация одного из компонентов оказывает минимальное воздействие на остальные.

Роль обязательной для C++ функции main() в разработанном ПС заключается в создании главного окна приложения и запуска цикла обработки событий. Модель архитектуры MVC реализована в модуле models, представленном файлами models.h и models.срр. Основой программы является класс Expression, представляющий в программе выражения BAN-логики. Класс Exression имеет три поля: строковое поле who; поле type, принимающее одно из четырёх возможных значений: BELIEVES, CONTROLS, SAID, SEES, и поле what, являющееся объектом класса Subject, определённого в этом же модуле. Класс Expression имеет два конструктора; метод toQString, возвращающий строковое представление выражения, и статический метод stringlsType(QString), возвращающий значение «истина», если параметр функции является допустимым значением для поля type, и «ложь» в противном случае. Класс BanAnalyzer, унаследованный от QMainWindow, — основная составная часть представлений модели MVC. Важнейшими методами класса являются следующие. Input_parsing() реализует разбор пользовательского ввода на выражения BAN-логики, создание объектов класса Expression и добавление их к собственному объекту класса BanControl. On_pushButton_clicked() — обработчик события нажатия на кнопку «Расчёт», запускает метод input_parsing(), затем метод контроллера для процедуры анализа, после чего формирует окончательный вывод результата. Обработчики нажатия на кнопки конструктора описаний, добавляют соответствующие им слова в поле для ввода в текущую позицию курсора. Обработчики вызовов меню. Класс HelpDialog, унаследованный от QDialog, реализует диалоговое окно помощи. Основными функциональными компонентами являются следующие. Метод showHelp(QString) позволяет отображать текстовое содержание файла с именем, указанным в параметре на поле вывода диалогового окна. Обработчики нажатий на кнопки диалога вызывают метод showhelp, передавая ему различные имена файлов, в которых хранятся соответствующие справочные тексты. Класс BanControl — контроллер программы по архитек-12

Steps:

О A SEES (TS, KABjKAS

• 1    В SEES (IS, KABJKBS

• 2    В SEES (ТА КАВ)КАВ

• 3    A SEES (ТВ, КАВ)КАВ

Trusts:

О A BELIEVES KAS

• 1    A BELIEVES S CONTROLS KAB

• 2    A BELIEVES FRESH(TS)

• 3    В BELIEVES KBS

• 4    В BELIEVES S CONTROLS KAB

• 5    В BELIEVES FRESH(TS)

• 6    В BELIEVES FRESH(TA)

• 7    A BELIEVES FRESH(TB)

• 8    В BELIEVES FRESH (TA)

Results:

A BELIEVES S SAID TS, KAB

A BELIEVES S BELIEVES TS

A BELIEVES S BELIEVES KAB

A BELIEVES KAB

В BELIEVES S SAID TS, KAB

В BELIEVES S BELIEVES TS

В BELIEVES S BELIEVES KAB

В BELIEVES KAB

В BELIEVES A SAID TA, KAB

В BELIEVES A BELIEVES TA

B BELIEVES A BELIEVES KAB

A BELIEVES В SAID ТВ, KAB

A BELIEVES Б BELIEVES ТВ

A BELIEVES В BELIEVES KAB

Additional info:

trust 8 is unused I

Step 0 fully resolved

Step 1 fully resolved

Step 2 nonce-verification resolved

Step 3 nonce-verification resolved

Рис. 2. Результат автоматизированного анализа протокола Керберос

туре MVC, инкапсулирует в себе динамические списки шагов (steps), доверий (trusts) и результатов (results) протокола, список строк со сведениями об ошибках (messages) и некоторую служебную информацию, в том числе сведения об использовании шагов (массив steps_analisys) и доверий (массив trust_using). Алгоритм процедуры анализа протокола BAN-логикой выполняется в теле метода calculating().

В левой части рис. 1 приведён скриншот основного окна ПС BanAnalyzer, содержащий описание протокола Керберос и результаты его анализа. В программе для записи шагов протоколов и доверий участников использованы обозначения BAN-логики, предложенные разработчиками BAN-логики. Кнопки Believes, Controls, Said, Sees, Fresh используются для вставки соответствующих кванторов при формировании описания протокола.

Пример проведения анализа протокола с использованием ПС BanAnalyzer. На правой части рис. 1 представлено полное описание протокола Керберос, введённое в программу для анализа. Результат анализа протокола Керберос с помощью построенного ПС представлен на рис. 2. Напомним, что по результатам ручного анализа протокол Керберос обеспечил достижение четырёх целей симметричного протокола обмена ключами, в результате автоматизированного анализа достигнуты те же цели. Итоговые результаты на рис. 2 подчёркнуты.

Исследование работоспособности ПС BanAnalyzer. Для испытания качества разработанного ПС были подготовлены идеализированные описания ряда из четырнадцати хорошо известных протоколов (Керберос, асимметричного и симметричного протоколов Нидхема — Шрёдера, Ньюмана — Стабблайна, By — Лама, Деннин га — Сакко, Отвея — Рииса, Andrew RPC Handshake, DASS, BAN-Yahalom, Station-to-station, EKE, SPX, «Широкоротая лягушка» [2, 6, 7]). Для каждого из этих протоколов был проведён анализ «вручную» и подготовлен список известных из литературы возможных атак. В ходе испытаний проводился автоматизированный анализ с помощью разработанного ПС и затем сравнивались результаты автоматизированного, ручного анализа и известных уязвимостей. Проведённые испытания показали, что реализованное ПС BanAnalyzer корректно выполняет формальный анализ криптографических протоколов распределения ключей методами BAN-логики и может быть использовано как для изучения уже существующих протоколов, так и в процессе разработки новых протоколов для предотвращения их возможных уязвимостей.

Заключение. В работе построено автоматизированное ПС, позволяющее проводить формальную проверку логической корректности криптографических протоколов распределения ключей на основе использования BAN-логики. Проведённые исследования показали корректность его 13

работы. В настоящее время построенное ПС доступно во внутренней сети ФГБОУ ВПО «ДГТУ» для использования студентами специальности 090103 «Компьютерная безопасность» в рамках изучения дисциплины «Криптографические протоколы» [5].

В качестве дальнейшего направления работы представляется интересным построить программные реализации для других логик доверия, например, AUTLOG (V. Kessler, G. Wedel), логики объяснений (R. Kaylar), RV-логики (D. Kindred), GNY (L. Gong, R. Needham, R. Yahalom), BGNY/HOL, SvO (R Syverson), что позволит легко анализировать протоколы этими методами, а также проводить сравнительный анализ как различных протоколов, так и результатов анализа одного и того же протокола различными логиками. Считаем важной задачей организацию свободного доступа к разработанной программе и её исходным кодам через Интернет для всех заинтересованных в использовании, изучении, а также дальнейшей разработке.