Содержание к диссертации
Введение
ГЛАВА I. Задача обеспечения безопасности протоколов информационного обмена 10
1.1 Общесистемные вопросы организации информационного обмена 10
1.1.1 Протоколы информационного обмена 11
1.1.2 Средства моделирования информационных процессов 12
1.1.3 Криптографические методы, используемые в ПИО . 16
1.2 Современные требования безопасности протоколов , 22
1.3 Несостоятельности протоколов 25
1.4 Обзор существующих методов анализа протоколов 29
1.4.1 Модель Долева-Яу 30
1.4.2 BAN - логика 31
1.4.3 STC-исчислєниє 36
1.4.4 Анализ протоколов с использованием алгебры CSP 39
1.5 Ограничения формальных методов анализа 43
1.6 Постановка задачи 45
1.7 Выводы 47
ГЛАВА II. Теоретические основы разработки математического обеспечения системы 49
2.1 Метод организации математических преобразований 50
2.1.1 Алгоритмы преобразований над данными 50
2.1.2 Преобразования в группах точек эллиптической кривой 52
2.2 Представление протоколов , 57
2.2.1 Вербальное описание 58
2.2.2 Нотация для представления протоколов 59
2.2.3 Автоматное представление протоколов 66
2.3 Выводы 73
ГЛАВА III. Проектирование системы 76
3.1 Общие требования к системе 74
3.2 Метод анализа протоколов 79
3.3 Архитектура системы , 81
3.4 Определение функциональных возможностей S3
3.4.1 Функциональность подсистемы управления сообщениями 86
3.4.2 Функциональность подсистемы эмуляции атак 90
3.4.3 Функциональность подсистемы мониторинга 92
3.4.4 Функциональность подсистемы администрирования , 94
3.4.5 Функциональность подсистемы математических преобразований 95
3.5 Модель данных 98
3.5.1 Концептуальная модель данных информационного обмена 99
3.5.2 Концептуальная модель данных для эмуляции атак 102
3.6 Выводы 106
ГЛАВА IV. Сетевой программный комплекс "ИКАМ" и его использование 107
4.1 Технологические аспекты реализации сетевого ПК "ИКАМ" 107
4.2 Режимы использования 110
4.2.1 Анализ протоколов 110
4.2.2 Анализ протокола "слепой" подписи для эллиптических кривых 111
4.2.3 Анализ протокола Нидхема-Шредера в двух параллельных сессиях 116
4.2.4 Экспериментальное исследование протоколов , 119
4.2.5 Дистанционное обучение 123
4.2.6 Итерационный подход к проектированию протоколов , 124
4.3 Инсталляция сетевого ПК "ИКАМ" 127
4.3.1 Состав 127
4.3.2 Инсталляция 128
4.3.3 Результаты эксплуатации 130
4.4 Выводы 131
Заключение 132
Литература 135
Приложения 144
- Средства моделирования информационных процессов
- Преобразования в группах точек эллиптической кривой
- Функциональность подсистемы математических преобразований
- Анализ протокола Нидхема-Шредера в двух параллельных сессиях
Введение к работе
В современном мире значительный объем коммерческой, личной и прочей
информации передается через открытые глобальные и локальные сети. Бурный рост
исследований в области информационных и сетевых технологий в последней четверти
прошлого века привел к развитию направления связанного с разработкой протоколов
информационного обмена (ПИО). Важной является задача исследования и определения
безопасности современных протоколов, а также разработка новых безопасных протоколов.
Потребность в доказательстве безопасности ПИО является особенно актуальной в связи с
развитием современных направлений электронного бизнеса и электронного
документооборота. Задача привлечения новых клиентов и поставщиков услуг во многом
зависит от безопасности ПИО, используемых в системах злеіаронной коммерции, а такнсе от
возможности реализации различных бизнес-процессов. Организация электронных
коммуникаций и транзакций решается в рамках выполнения ПИО, которые в процессе
информационного обмена используют различные математические и криптографические
алгоритмы преобразования данных. Примерами таких протоколов могут служить, например,
протоколы электронных платежей, передача электронных документов, имеющих
юридическую силу, электронный арбитраж спорных ситуаций и тому подобное. Стойкость
используемых криптографических алгоритмов является необходимым, но отнюдь не
достаточным условием для обеспечения безопасности протокола в целом. Протокол может
быть непригодным к использованию и без непосредственной атаки на используемые в нем
криптографические алгоритмы. В таких случаях говорят о несостоятельности протокола [95].
Безопасным будем называть протокол, в котором отсутствуют несостоятельности.
Несостоятельности можно рассматривать как логические ошибки в протоколе, которые
потенциально позволяют причинить ущерб абонентам, участвующим в процессе
информационного обмена. Анализ безопасности ПИО состоит в обнаружении возможных
несостоятельностей в протоколах. Несостоятельности в протоколах иногда могут возникать из-за некорректного применения заведомо стойких криптографических алгоритмов. Вопросы, связанные с определением стойкости существующих криптографических алгоритмов, разработкой новых алгоритмов и методов их криптоанализа, находятся вне рамок анализа безопасности протоколов и научного исследования данной диссертационной работы. В области исследования работы находятся вопросы разработки метода для выявления несостоятельностей в протоколах, представляющих угрозу безопасности.
Открытая сетевая инфраструктура, в частности глобальная сеть Интернет, может потенциально рассматриваться абонентами информационного обмена, как недружелюбная. Под этим понимается, что каналы передачи сообщений могут контролироваться злоумышленниками, в роли которых могут выстулать, например, недобросовестные конкуренты, недоброжелатели, хакеры и тому подобный круг лиц. В общем случае можно предполагать, что злоумышленник может полностью контролировать все каналы связи, то есть осуществлять перехват, блокировку и внедрение любых сообщений. Кроме того, абоненты вовсе не обязаны доверять друг другу. Тем не менее, несмотря на все эти неблагоприятные допущения, ПИО должны быть такими, чтобы обеспечивать невозможность причинения злоумышленниками какого-либо ущерба абонентам.
К настоящему времени получили развитие математические методы формального
анализа безопасности протоколов. Основу таких методов составляют процедуры
формального описания протокола с последующей верификацией работы модели протокола.
Разработанные методы позволили найти несостоятельности в некоторых протоколах, однако
до сих пор не было предложено универсального метода анализа, который позволял бы для
произвольного протокола получить однозначное заключение о безопасности. Более того, как
правило, формальные методы анализа пригодны для работы только с идеализированными
ограниченными классами протоколов. Кроме того, исторически так сложилось, что
большинство существующих методов формального анализа ориентированы только на
доказательство традиционных требований безопасности: секретности и аутентичности.
Однако на практике появляется все больше протоколов с другими, новыми требованиями
безопасности. В большей степени это связано с развитием электронной коммерции. Так,
например, появились требования честности, анонимности, неопровержимости и другие,
присущие протоколам электронного заключения контрактов и платежей. Кроме того, как
показывает реальная практика, обнаружение несостоятельностей в протоколах может
происходить и происходит спустя длительное время после опубликования, разработки и
внедрения протоколов. В некоторых случаях оказывается, что новые несостоятельности и
угрозы безопасности обнаруживаются в протоколах, которые ранее уже подвергались
анализу с использованием одного или нескольких методов. Например, несостоятельность
связанная с выполнением протокола Нидхема-Шредера в двух параллельных сессиях, была
продемонстрирована спустя семнадцать лет, после опубликования протокола [83, 96]. Совсем
недавно была показа принципиальная возможность успешной атаки на протоколы SSL/TLS,
несостоятельность которых связана с анализом времени отклика сервера в случае
некорректной реализации протоколов. Между опубликованием протокола SSL и
обнаружением несостоятельности в этом случае прошло порядка девяти лет [81]. Следует
заметить, что протоколы Нидхема-Шредера и SSL/TLS неоднократно подвергались анализу
безопасности, но указанных несостоятельностей в свое время обнаружено не было. Эти и
другие проблемы формальных методов не позволяют говорить о существовании приемлемого
решении задачи анализа безопасности протоколов.
В работе выполнение и анализ ПИО предлагается осуществлять в специальной
исследовательской среде информационного обмена (ИСИО), которая создается и управляется
с помощью вычислительной системы. ИСИО строится на базе существующей глобальной
сетевой инфраструктуры. Работа и выполнение ПИО происходит в реальном сетевом режиме.
Должна быть обеспечена возможность анализа максимально широкого класса протоколов
без изменений в математическом, программном и информационном обеспечении системы.
Объединение пользователей для работы по выбранному протоколу будем называть сессией протокола. Должна быть обеспечена возможность одновременного выполнения различных сессий одного или нескольких протоколов. Для анализа безопасности и поиска ьозможных несостоятельностей, в системе необходимо предусмотреть механизм для осуществления эмуляции атак на выполняемые протоколы. Система автоматически должна корректировать выполнение протокола в соответствии с установками, определяющими условия атаки. При эмуляции атак нет необходимости осуществлять действительный перехват и анализ сетевого трафика. Система должна автоматически копировать, блокировать и заменять нужные сообщения. При анализе протоколов следует учитывать свойства алгебраических операций, использующихся в алгоритмах математических преобразования и корректность их применения. В системе абонентам должна быть предоставлена возможность для выполнения требуемых математических преобразований и вычислений.
Целью диссертационной работы явилась: создание математического, программного и информационного обеспечения системы и разработка сетевого программного комплекса для моделирования выполнения протоколов и эмуляции атак; разработка архитектуры вычислительной системы; разработка нового метода анализа безопасности ПИО.
Основными направлениями научного исследования являются вопросы создания
моделей ПИО и разработки программного комплекса для моделирования выполнения и
анализа безопасности ПИО в ИСИО, созданной на базе существующей глобальной сетевой
инфраструктуры Интернет. В область исследования данной работы также входят вопросы
автоматизации процессов анализа безопасности протоколов, анализ использования
математических алгоритмов и преобразований данных в ПИО и автоматизация расчетов в
процессе выполнения ПИО в ИСИО, и разработка интерфейсов взаимодействия человека с
ЭВМ в рамках системы. Направление исследований связано с созданием способа
обнаружения несостоятельностей в разрабатываемых ПИО на этапе их проектирования, либо
в уже существующих ПИО, что позволит сокращать сроки анализа протоколов и
соответственно сокращать сроки модификации и внедрения информационных систем, использующих ПИО.
В результате проделанной работы был предложен новый метод анализа ПИО, основанный на информационном моделировании выполнения ПИО в ИСИО и эмуляции атак на них. Была разработана архитектура вычислительной системы, предназначенной для создания ИСИО с целью анализа и исследования протоколов. Было создано математическое и программное обеспечение сетевого программного комплекса. Обеспечивается возможность одновременной организации работ по произвольным ПИО в реальном сетевом режиме с поддержкой удаленной связи абонентов и подсистем через Интернет. Результаты диссертационной работы внедрены в учебный процесс. Разработанный программный комплекс используется в качестве лабораторного практикума, для анализа широкого спектра ПИО, включая протоколы передачи электронных документов, заверенных электронной цифровой подписью (ЭЦП), финансовые протоколы электронных платежей с помощью цифровых денег, протоколы разделения информации между абонентами сети и другие.
Данная работа состоит из четырех глав и двух приложений. В первой главе ставится задача анализа безопасности ПИО и определяется место работы в общей схеме процессов информационного обмена. Во второй главе излагаются теоретические основы для разработки математического обеспечения системы и рассматриваются алгоритмы преобразования данных и криптографических алгоритмов с целью их классификации и разложения на элементарные алгебраические операции для автоматизации расчетов в процессе анализа ПИО. В третьей главе предлагается метод анализа безопасности ПИО, описывается архитектура и информационное обеспечение вычислительной системы анализа и исследования ПИО. Четвертая глава посвящена разработке и эксплуатации сетевого ПК. В приложении приведены физические модели данных информационного обмена и эмуляции атак, а также элементы пользовательского интерфейса системы.
Средства моделирования информационных процессов
Процессы информационного обмена являются сложными динамическими процессами, для моделирования которых существуют различные подходы. Одним из таких подходов является использование унифицированного языка моделирования (Unified Modeling Language, UML). Исторически UML появился в 90-х годах прошлого века как результат синтеза ряда существовавших на тот момент нотаций и методологий объектно-ориентированного проектирования программных систем, в первую нотаций Booch, ОМТ (Object Modeling Technique) и OOSE (Object-Oriented Software Engineering), Впоследствии спецификации UML были развиты и сертифицированы усилиями специально созданных рабочих групп [9]. На сегодняшний день этот язык является признанным промышленным стандартом в области моделирования систем. Возможности UML и методологии его применения практически полностью охватывают все этапы жизненного цикла проекта, начиная от создания концепции проекта, определения функциональности и заканчивая вопросами инсталляции и сопровождения конечного продукта [8, 9]. Хотя первоначально UML создавался для моделирования программных систем, внутренние возможности и потенциал данного языка позволяют успешно использовать его для описания и моделирования в других предметных областях. В этой связи привлекательной возможностью UML является понятие "стереотипов", позволяющих фактически расширять существующие элементы нотации или вводить в язык новые понятия присущие выбранной предметной области. Отличным примером является работа [26], в которой предложено расширение стандартного варианта UML с целью проектирования именно WEB-приложений, описания структуры страниц сайта и переходов между ними. В арсенале возможностей UML имеются средства для моделирования динамического взаимодействия между различными объектами или частями системы. Для этого в языке определено порядка пяти типов диаграмм для построения соответствующих моделей; диаграммы использования (прецедентов), последовательности, кооперации, состояний и деятельности. Диаграммы использования [use-case) могут применяться для иллюстрации взаимодействия человека и вычислительной системы, а также для функциональной декомпозиции системы на различные подсистемы, С точки зрения вопросов информационного взаимодействия наибольший интерес, безусловно, представляют три типа диаграмм - это диаграммы последовательности {sequence), диаграммы состояний (state) и диаграммы деятельности (activity) [9, 46, 57]. Диаграммы последовательности используются для моделирования взаимодействия объектов во времени. Основное внимание при этом уделяется временной упорядоченности событий. На таких диаграммах изображаются множества объектов и посланные или принятые ими сообщения. Диаграммы последовательности полезны также для представления параллельных процессов. Диаграммы состояний исторически являются непосредственным развитием применения теории автоматов [23]. В своей основе они показывают некоторый автомат, содержащий состояния, переходы, события и действия. Диаграммы состояний используются в основном для моделирования поведения объектов. Диаграммы деятельности могут описывать один или несколько параллельно выполняющихся процессов. В отличие от диаграмм последовательности и обычных блок схем, диаграммы деятельности оставляют возможность варьировать порядок выполнения конкретных действий. Подобный тип диаграмм полезен для моделирования бизнес-процессов, параллельного проектирования, графиков работ и многих других задач, Специфичным для диаграмм деятельности является понятие синхронизации между параллельно вьшолняюпщмися процессами. Важно, что некоторые действия могут начаться, только когда будут закончены другие [30, 57]. Таким образом, в UML есть возможности для применения его к предметной области протоколов информационного обмена. Кроме того, описываемые ;с помощью UML модели динамического взаимодействия могут быть интерпретированы как протоколы информационного обмена. Аналогичный круг вопросов связан с созданием и исследованием сетевых протоколов и стандартов взаимодействия в компьютерных сетях. Например, при описании процедурных характеристик, протоколов синхронного дуплексного управления, последовательности передачи сообщений при установлении и разрыве связи и многих других информационных процессах [34], Можно описывать протоколы информационного обмена с помощью языка спецификаций и описаний (Specification and Description Language, SDL), принятого в качестве международного стандарта ITU Z.100 [114]. В своей основе SDL относится к разряду конечно-автоматных языков. Язык SDL предназначен для создания спецификаций и описаний систем реального времени, в том числе и телекоммуникационных протоколов обмена данными. Спецификация системы означает задание требований к системе, а описание системы соответствует ее реализации. Язык SDL обладает достаточно широкими возможностями по степени детализации представления систем. Одна из основных возможностей стандарта ГГО-Т 2.100 заключается в создании полностью формальных и однозначных моделей систем. Критерии и требования по использованию формальных описаний, включая язык SDL, приведены в стандарте ITU Z.110 [116]. Кроме того, возможно совместное моделирование и описание систем с использованием языков UML и SDL. Стандарт ITU Z.109 [115] описывает подмножества элементов XJML и способы их однозначного преобразования в представления с помощью языка SDL. Кроме того, большой интерес представляет стандарт ITU Z.120 [117], описывающий диаграммы последовательности сообщений (Message Sequence Chart, MSC) для представления систем и процессов, взаимодействующих посредством передачи сообщений. Наглядность, интуитивность и широта возможностей делают это представление достаточно привлекательным для описаний ПИО, а также более широкого класса протоколов электронной коммерции и электронного документооборота.
Преобразования в группах точек эллиптической кривой
Несмотря на то, что формальные методы анализа позволяют найти несостоятельности во многих протоколах, до сих пор не было предложено универсального метода доказательства безопасности (или небезопасности) произвольного ПИО. На сегодняшний день имеется целый ряд открытых вопросов и нерешенных проблем, связанных с доказательством безопасности произвольных ПИО,
Исторически так сложилось, что большинство разрабатываемых методов ориентированы только на протоколы аутентификации, хотя реальный круг прикладных задач, в которых используются самые различные ПИО, очень широк. Таким образом, фактически за рамками возможностей анализа остаются большинство требований безопасности ПИО. В первую очередь это связано с трудностью формализации таких требований и ограниченностью используемых моделей.
Часто формальные модели описывают идеализированные варианты протоколов. В таких условиях, формальный анализ возможен только для узкого класса протоколов. Попытки отказаться от ограничений накладываемых на протокол, приводят к неразрешимости доказательства его безопасности. Ярким примером является сложность доказательства безопасности ПИО, при условии организации произвольного количества параллельных сессий этого протокола. Большинство формальных методов не могут использоваться для непосредственного анализа расширяемых протоколов {open-ended protocols). Под расширяемыми протоколами первого класса будем понимать протоколы, которые допускают обмен сообщениями с произвольной структурой данных. К расширяемым протоколам второго класса отнесем те, которые подразумевают участие произвольного количества абонентов. Специфическими являются проблемы, связанные с необходимостью учета возможности использования злоумышленником сообщений (или их частей), полученных в рамках одного протокола, в другом протоколе. Решение таких задач напрямую зависит от предположений о потенциальных возможностях злоумышленника. Кроме того, многие реальные коммерческие протоколы являются очень объемными и сложными. Как отмечают, например, авторы подхода к анализу безопасности протоколов с использованием алгебры CSP, из-за сложности реальных протоколов их непосредственный анализ становится крайне затруднительным или вообще невозможным по причине стремительного увеличения количества возможных состояний протокола и передаваемых сообщений. Другой проблемой, присущей многим формальным методам, является их слишком высокий уровень абстракции при рассмотрении конкретного протокола. Очень часто используемые криптографические преобразования представляются в качестве "черных ящиков" (black box). Между тем очень многие атаки на протоколы, особенно на те из них, которые используют криптографические алгоритмы с открытыми ключами, зависят непосредственно от выбранных преобразований. Еще одним фактором, влияющим на эффективность формальных методов, является выбор начальных допущений и ограничений. В данном случае экспертное мнение и опыт могут являться определяющими. Однако, как это было показано при рассмотрении методов BAN-логЕки, часто именно используемые допущения играют ключевую роль в общей эффективности анализа. В случае, принудительного введения необоснованного допущения, даже хорошая методика анализа не даст результата, как это случилось, когда BAN-анализ не нашел несостоятельностей в протоколе Нидхема-Шредера. Таким образом, фактор экспертного решения является достаточно сильным при формализации протоколов и заданий условий их выполнения. На основе имеющегося описания или спецификации ПИО, осуществить моделирование вьшолнения протокола и эмуляцию атак на него с целью анализа безопасности и определения возможных несостоятельностей. Для решения этой задачи необходимо: 1. Подготовить описание протокола с использованием специальной нотации. На этапе формализации следует определить классы используемых криптографических і алгоритмов. В зависимости от этого протокол анализируется с учетом или без учета свойств используемых математических операций. 2. Использовать формализованное описание протокола для организации процесса его вьшолнения в исследовательской среде информационного обмена, создаваемой с помощью вычислительной системы. Проверить корректность действий абонентов. 3. Одновременно с моделированием вьшолнения протокола, организовать процесс анализа, его безопасности, путем эмуляции атак с заданными свойствами. Обеспечить автоматизированное получение необходимых для анализа данных, в соответствии с предполагаемыми возможностями злоумышленника. В рамках первого пункта необходимо выделить основные этапы протокола: генерацию первоначальных параметров, подготовку сообщений для передачи, передачу сообщений между абонентами, обработку получаемых данных. Этап генерация параметров подразумевает в частности возможность генерации параметров и ключей для криптографических алгоритмов, которые впоследствии могут быть использованы для подготовки сообщений или для обработки полученных данных. На этапе формализации протокола необходимо принять решение о том, следует ли учитывать при выполнении и анализе протокола свойства математических операций, используемых в криптографических алгоритмах. Как правило, внутренняя структура симметричных алгоритмов F_1(j8r,.F(lir,M)) = М , в которых один и тот же параметр К, используется всеми абонентами, не влияет на безопасность протокола. В противоположность этому, внутренняя структура асимметричных алгоритмов F(K"1,F(K,M)) = М, в которых используются связанные параметры К и 1С , может служить причиной появления несостоятельностей протокола и непосредственно влияет на его безопасность. Размер чисел, используемых для вычисления, не имеет значения. Если это необходимо для выполнения или анализа протокола, то в формализованной записи протокола должны быть отражены действия абонентов на уровне использования математических операций в процессах обработки данных.
Функциональность подсистемы математических преобразований
Также необходимо определить список ролей, присущий каждому протоколу. Кроме того, имеется специфика в случае использования системы для практического изучения протоколов и проведения лабораторных работ. В этом случае администратор должен настроить систему таким образом, чтобы студенты могли организовывать сессии только для изучения протоколов, предусмотренных учебным планом. Регистрация пользователей в системе происходит без участия администратора. Пользователь самостоятельно указывает свой логин, пароль и прочие регистрационные данные в начале работы с системой. В дальнейшем, администратор должен иметь возможность блокировать/разблокировать пользователей, то есть запрещать или разрешать им дальнейшую работу с системой. Управление сессиями заключается в возможности изменения статуса сессий. Таким образом, администратор может принудительно закрыть доступные или активные сессии. Эта потребность возникает из-за того, что сессии могут быть созданы, но не закрыты их создателями по причине разрыва и невозможности восстановления связи между компьютером пользователя и сервером системы.
Подсистема математических преобразований используется абонентами и злоумышленниками для осуществления необходимых вычислений (рис. 3,11). Наличие данной подсистемы позволяет реализовывать криптографические алгоритмы с учетом их структуры и специфики, то есть криптографические алгоритмы не рассматриваются как "черный ящик". Такая возможность системы позволяет эмулировать атаки на протоколы, связанные со свойствами используемых операций. I Кроме того, ПМП поддерживает два математических аппарата для реализации математических преобразований: методы модулярной алгебры и операции в конечных полях вычисления в группах точек эллиптической кривой Использование двух указанных математических аппаратов позволяет реапизовывать современные алгоритмы с открытыми ключами. Практически любой криптографический алгоритм с открытыми ключами можно представить как последовательность применения базовых операций и вспомогательных алгоритмов для генерации необходимых параметров алгоритма и собственно операций зашифрования и расшифрования. Кроме того, часто для ускорения и упрощения процессов работы над протоколом можно использовать автоматически сгенерированные параметры распространенных криптографических схем. Текущая версия сетевого программного 1 , комплекса поддерживает автоматическую и полуавтоматическую генерацию параметров для криптографических алгоритмов RSA и электронной цифровой подписи Эль-Гамаля. Выбор данных схем для реализации был обусловлен их широкой известностью и распространенностью. Анализ протоколов в системе не требует использования криптографических ключей и других значений, обеспечивающих действительную стойкость используемых алгоритмов. Основная задача ПМП состоит в предоставлении возможности выполнения определенных математических преобразований, не важно над числами какого размера. По этой причине ПМП использует числа небольшого размера. Так, например, максимально возможный размер ключа шифрования для алгоритма RSA составляет всего девять цифр (36 бит). Максимальное значение используемых для вычисления чисел ограничено значением 2 147 483 647, что соответствует целочисленному типу данных int в языке программирования C++. Кроме того, использование чисел небольшого размера позволяет упростить непосредственную реализацию алгоритмов за счет использования стандартных типов данных, предусмотренных в выбранном языке программирования. Это в свою очередь позволяет сократить сроки разработки. В таблице 3.1 приведены все основные характеристики по размерам чисел, Максимальный размер ключей в схеме Эль-Гамаля (бит/цифр) 32/4 деление двух чисел по модулю; возведение в степень по модулю; вычисление квадратного корня из числа; сложение двух точек эллиптической кривой; вычитание двух точек эллиптической кривой; умножение точки на заданное число. Кроме того, определены следующие вспомогательные алгоритмы: перевод строки символов в числовую форму; обратный перевод числа в строку символов; расширенный алгоритм Евклида; вычисление хэш-значения от заданного числа (алгоритм Флетчера); генерация случайного простого числа; просмотр таблицы простых чисел; генерация эллиптической кривой; ( поиск точек эллиптической кривой; [ определение ранга эллиптической кривой; определение ранга точки на эллиптической кривой; вычисление мультипликативного обратного элемента по модулю; перевод строки в массив точек на эллиптической кривой; обратный перевод массива точек эллиптической кривой в строку; разложение числа на множители.
Анализ протокола Нидхема-Шредера в двух параллельных сессиях
Проведен анализ и определены современные требования безопасности протоколов информационного обмена, использующихся в системах электронного документооборота и электронной коммерции. Систематизированы причины появления несостоятельностей в протоколах, представляющих угрозы информационной безопасности протоколов и информационных систем.
Проведен критический анализ существующих теоретико-автоматных и теоретико-алгебраических методов и логических исчислений, использующихся для доказательства безопасности протоколов. Показаны ограничения существующих методов формального анализа протоколов и обозначена область применимости таких методов. Поставлена задача разработки нового метода для анализа безопасности протоколов и автоматизированной человеко-машинной системы для осуществления анализа протоколов и их экспериментального исследования в условиях создаваемой исследовательской среды информационного обмена.
Часто в существующих методах формального анализа безопасности, протоколы представляются в идеализированном виде, при котором не рассматривается внутренняя структура используемых криптографических алгоритмов и математических преобразований, что приводит к принципиальной невозможности определения несостоятельностей, связанных со свойствами используемых алгебраических операций, В; .работе протоколы рассматриваются с учетом внутренней структуры алгоритмов. Была разработана оригинальная нотация для детализированного представления протоколов и математическое обеспечение системы, позволяющее учитывать используемые алгебраические операции в процессе анализа протоколов и соответственно определять связанные с этим несостоятельности. В качестве базового аппарата математических преобразований, в системе был выбран аппарат эллиптических кривых, определенных в конечном поле, что обусловлено его перспективностью в разработке современных прокотолов. 4. Предложен класс расширенных конечных автоматов Мили, предназначенный для создания моделей протоколов информационного обмена. Состояния автомата рассматриваются как знания абонентов на определенный момент времени, переходы между состояниями соответствуют процессам обработки данных или передачи сообщений. Автоматные модели используются для обеспечения корректности вложения протоколов в систему и автоматической верификации процессов выполнения протоколов.
Разработан новый метод анализа безопасности протоколов информационного обмена, основанный на оценке результатов выполнения и автоматизированной эмуляции атак на протоколы, с целью обнаружения возможных несостоятельностей, представляющих угрозу информационной безопасности. Преимущества нового метода по сравнению с существующими формальными методами заключаются в возможности анализа: менее идеализированных вариантов протоколов; расширяемых протоколов; протоколов с учетом их выполнения в параллельных сессиях. Ограничения разработанного метода связаны с уменьшением степени автоматизации анализа.
Разработана архитектура человеко-машинной системы, предназначенной для создания и управления исследовательской средой информационного обмена, в рамках которой происходит анализ протоколов. Разработаны модели данных, для обеспечения процессов информационного обмена и автоматизированной эмуляции атак на протоколы в создаваемой исследовательской среде.
На основе разработанной архитектуры и определенных функциональных требований был создан сетевой ПК "ИКАМ", с помощью которого стало возможным создание исследовательской среды информационного обмена на базе существующей инфраструктуры сетей Интернет/Интранет. Программное обеспечение сетевого ПК предоставляет интерфейсы для взаимодействия пользователей между собой и с информационной системой, в процессе анализа и исследования протоколов. Сетевой ПК "ИКАМ" поддерживает четыре режима работы: анализ безопасности протоколов; экспериментальное исследование протоколов; дистанционное обучение через Интернет; итерационный процесс синтеза-анализа протоколов.
Результаты работы внедрены в учебный процесс высших учебных заведений. Были подтверждены несостоятельности ряда протоколов и показана возможная несостоятельность протокола электронных платежей, связанная с выбором параметров в используемых алгоритмах. За время эксплуатации разработанного сетевого ПК было организовано более 500 сессий для 12 различных протоколов. В работе приняло участие около 150 пользователей. 9. Использование разработанной системы и метода анализа безопасности протоколов, позволяет существенно сокращать сроки выполнения экспериментального исследования и анализа протоколов, в первую очередь за счет достаточной универсальности созданного математического и программного обеспечения и отсутствия необходимости вносить в него изменения, в случае вложения в систему нового протокола.
