IX Международная студенческая научная конференция Студенческий научный форум - 2017

Данная статья посвящена анализу подходов к верификации протоколов безопасности.

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

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

• Подмена- попытка подменить одного пользователя другим. Нарушитель, выступая от имени одной из сторон и полностью имитируя ее действия, получает в ответ сообщения определенного формата, необходимые для подделки отдельных шагов протокола.

• Повторное навязывание сообщения- повторное использование ранее переданного в текущем или предыдущем сеансе сообщения или какой-либо его части в текущем сеансе протокола.

• Отражение- атака, связанная с обратной передачей отправителю ранее переданных им сообщений.

• Задержка передачи сообщения- перехват противником сообщения и навязывание его в более поздний момент времени.

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

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

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

• Использование противником своих средств в качестве телекоммуникационной структуры - атака, при которой в протоколе идентификации между участниками А и В противник С входит в телекоммуникационный канал и становится его частью при реализации протокола между участниками А и В.

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

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

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

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

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

1. Программный продукт AVISPA появился в начале осени 2005 года. Разработка дан­ного средства проводилась в рамках единого европейского проекта, в котором участво­вали LORIA-INRIA (Франция), ЕТН Цюрих (Швейцария), университет г. Генуя (Ита­лия), Siemens AG (Германия).

Архитектура AVISPA допускает анализ протокола одним из четырех выходных модулей (TA4SP, SATMC, OFMC, CL-At.Se). Спецификация протокола, основанная на ролевом представлении, записывается на языке высокого уровня HLPSL, а затем транслируется во внутренний язык IE. Проверяемые свойства записываются в терми­нах темпоральной логики. Модуль TA4SP реализует технику, основанную на построе­нии древовидных автоматов и развитую для систем автоматического доказательства. Строится верхняя аппроксимация древовидного автомата, реализующего систему пе­реписывания термов, которая описывает максимальные знания нарушителя. Исследо­вание свойства конфиденциальности теперь сводится к проверке наличия в этом мно­жестве терма, содержащего секрет. Модули SATMC, OFMC, CL-AtSe осуществляют верификацию методом проверки на модели (model checking). Протокол представляется как бесконечная система переходов, а задача верификации сводится к проверке выполнимости формулы, решения которой соответствуют атакам на протокол. Для сведения к конечному случаю применяются разные подходы. В модуле SATMC ис­пользуются методы, разработанные в рамках теории решения задач планирования, в модуле OFMC — символический метод, позволяющий группировать различные со­стояния в бесконечные классы, а в CL-AtSe — применяется техника, основанная на построении ограничений.

1. Scyther создан в ЕТН (Цюрих). Верифицирует ограниченное и неограниченное число сеан­сов протокола. Использует символический анализ в сочетании с обратным поиском, ос­нованный на частично упорядоченных шаблонах. Scyther не требует задания сценария атаки. Он требует только задания параметров, ограничивающих либо максимальное число запусков, либо пространства перебираемых траекторий. В первом случае всегда дает результат и показывает найденные траектории атаки. Во втором случае заверше­ние не гарантировано. В качестве ответа возможна одна из трех ситуаций: установлено, что проверяемое свойство выполнено; свойство не выполнено, так как найдена атака; свойство может быть корректно для заданного пространства траекторий.

2. ProVerif разработан в рамках проекта, финансируемого INRIA (Франция). Анализирует неограниченное число сеансов протокола с использованием верхней аппроксимации и представления протокола с помощью хорновских выражений. ProVerif предлагает два тина входных файлов: хорновские выражения и подмножество Pi-исчисления. При использовании Pi-исчислеиия ProVerif основывается на описании множества процес­сов, каждый из которых может выполняться неограниченное число раз. На выходе возможны четыре ситуации: свойство не выполнено; доказано, что свойство выполне­но; свойство не может быть доказано, так как есть пример атаки (могут быть найдены ложные атаки); работа не завершается.

3. Isabelle - средство для автоматизированного логического вывода, основанное на логике предикатов первого порядка. При использовании Isabelle разработчик протокола должен построить логическую теорию и доказать в ее рамках различные утверждения. В силу теоретических ограничений данного подхода автоматическое доказательство невозможно. Однако отдельные фрагменты логического вывода можно выполнить автоматически. Основная трудность состоит в том, что пока определенное утверждение не доказано, нельзя сказать определенно, почему оно не доказано: потому, что оно не выводимо (и можно вывести его отрицание); или же потому, что еще не найден подходящий вывод. Это означает, что эффективность работы с Isabelle во многом зависит от начальных предположений, которые разработчик протокола делает на основании опыта и интуиции.

4. SPIN, Murphi – универсальные средства проверки на моделях. Для верификации протоколов безопасности с использованием SPIN и Murphi необходимо:

• представить поведение участников протокола в виде, внешне напоминающем фрагмент программы на языке С (со специальными конструкциями, задающими обмен данными между участниками);

• аналогичным образом специфицировать поведение злоумышленника (в том числе перехват сообщений и генерацию новых сообщений на основе того, что уже известно злоумышленнику);

• описать критерии безопасности с использованием темпоральной логики (в терминах переменных, представляющих состояние/знание участников протокола и/или злоумышленника). В силу того, что в Murphi и SPIN не представлена специфика верификации протоколов безопасности, описания получаются громоздкими.

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

• уровень автоматизации (чем больше степень автоматизации, тем лучше);

• простоту модели (ошибки возможны не только в протоколе, но и в его формальной модели, и вероятность таких ошибок возрастает с усложнением модели);

• гибкость в смысле выразительных свойств модели (чем меньше ограничений на моделируемые свойства, тем лучше);

• ограничения на модель в теоретико-вычислительном смысле (чем более сложные конфигурации можно промоделировать, тем лучше);

• ложные срабатывания при определении уязвимостей протокола (лучший вариант — без ложных срабатываний, приемлемый вариант - с небольшой вероятностью ложного обнаружения возможной атаки);

• извлечение алгоритма атаки (с точки зрения проектирования протокола возможность узнать способ использования уязвимости протокола предпочтительнее по сравнению с индикацией наличия уязвимости);

• наличие сообщества исследователей и/или разработчиков, ис- пользующих данное средство верификации (его наличие косвенным образом свидетельствует о достаточной выразительности средства и привлекательности для решения реальных задач) [3].

Сводная оценка средств верификации представлены в таблице 1.

Таблица 1 – Сводная оценка средств верификации

Из таблицы видно, что ни одно из средств верификации протоколов безопасности не обладает идеальным набором свойств. Это значит, что ни одному из них нельзя отдать предпочтение как “лучшему” средству верификации.

Библиографический список

1. Давыдов А.Н. Формальнвй анализ криптографических протоколов: методы, основанные на моделях конечных автоматов. Том 6. С.28-31. Секция-9: Аутентификация: парольная, биометрическая, криптографическая Пенза-2005.

2. А.В. Черемушкин «Автоматизированные средства анализа протоколов».

3. А.В. Черемушкин «Криптографические протоколы: основные свойства и уязвимости».

4. Котенко И.В., Резник С.А., Шоров А.В. Верификация протоколов безопасности на основе комбинированного использования существующих методов и средств.

Код для цитирования: Скопировать