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

На правах рукописи

МИХАЙЛОВ АЛЕКСАНДР СЕРГЕЕВИЧ

СИСТЕМА АНАЛИЗА БЕЗОПАСНОСТИ И ИССЛЕДОВАНИЯ ПРОТОКОЛОВ ИНФОРМАЦИОННОГО ОБМЕНА

05.13.11 - математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей.

05.13.19 - методы и системы защиты информации, информационная безопасность

АВТОРЕФЕРАТ

диссертации на соискание ученой степени кандидата технических наук

Москва 2005

Работа выполнена в Московском инженерно-физическом институте (государственном университете).

Научный руководитель:

кандидат технических наук, доцент Ерохин Евгений Алексеевич

Официальные оппоненты:

доктор технических наук, профессор Пятибратов Александр Петрович

кандидат технических наук, Васильев Валерий Николаевич

Ведущая организация: Московский государственный индустриальный университет (МГИУ)

Защита состоится « ¡6 » 2005 г. в № Ч. м. на

заседании диссертационного'совета Д 212.130.03 в МИФИ по адресу: 115409, Москва, Каширское шоссе, д.31, тел. (095)323-91-67.

С диссертацией можно ознакомиться в библиотеке МИФИ.

Автореферат разослан

«1о»

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

Ученый секретарь диссертационного совета Д 212.130.03 д.т.н., профессор

В.Э. Вольфенгаген

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ

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

Актуальность темы.

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

Цель работы.

Основными задачами диссертационной работы являются:

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

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

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

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

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

Разработка архитектуры, математического и информационного обеспечения системы, предназначенной для управления исследовательской средой информационного обмена (ИСИО), в рамках которой осуществляются процессы выполнения протоколов и эмуляции атак. Создание программного обеспечения сетевого программного комплекса с целью экспериментального исследования и анализа безопасности протоколов.

Применение разработанного метода для исследования широкого спектра прикладных протоколов информационного обмена.

Научная новизна.

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

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

Предложен новый метод анализа безопасности ПИО, основанный на определении возможных несостоятельностей, в процессе выполнения протоколов и эмуляции атак на них, с заданными свойствами.

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

Практическая значимость.

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

Разработан сетевой программный комплекс (ПК) "ИКАМ", использующийся для организации ИСИО на базе имеющейся сетевой инфраструктуры. Использование разработанного сетевого программного

4

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

Разработанный сетевой ПК "ИКАМ" внедрен в учебный процесс в высших учебных заведениях, обеспечивает полностью удаленный режим работы пользователей через сеть Интернет и используется для выполнения, контроля и организации работ в рамках концепции дистанционного образования.

Основные результаты, выносимые на защиту.

Главным итогом диссертационной работы является создание системы для экспериментального исследования протоколов и реализации разработанного метода для анализа безопасности протоколов. На защиту выносятся:

- систематизация современных требований безопасности ПИО;

- результаты критического анализа существующих методов определения безопасности протоколов;

- методика детализированного и автоматного представления протоколов в системе;

- архитектура, математическое и информационное обеспечение системы;

- метод анализа безопасности протоколов;

- сетевой ПК "ИКАМ", успешная эксплуатация которого подтверждается актами о внедрении и результатами анкетирования специалистов;

- экспериментальные результаты анализа протоколов.

Внедрение результатов.

Результаты работы внедрены в учебный процесс и успешно эксплуатируются в следующих высших учебных заведениях:

в Московском инженерно-физическом институте (МИФИ) на кафедре кибернетики для подготовки специалистов по сетевым и информационным технологиям;

в Московском государственном университете экономики, статистики и информатики (МЭСИ) на факультете магистерской подготовки для подготовки специалистов по информационному менеджменту. Разработанный сетевой ПК "ИКАМ" используются в научном исследовании в области анализа безопасности современных протоколов электронной коммерции и информационного обмена в сетях.

Апробация работы.

Основные положения работы докладывались и обсуждались на Научных сессиях МИФИ (г. Москва, 2001-2004 гг.), научно-практических конференциях "Реинжиниринг бизнес-процессов на основе современных информационных технологий" (г. Москва, 2001-2002, 2004 гг.), XI международном научно-техническом семинаре "Современные технологии в задачах управления, автоматики и обработки информации" (г. Алушта, 2002 г.), научно-практическая конференция "Проблемы защиты кредитно-учетных организаций от мошенничества и недобросовестной конкуренции" (г. Москва, 2004 г.).

Публикации.

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

Структура и объем работы.

Диссертация состоит из введения, четырех глав, заключения, списка литературы и двух приложений. Общий объем 155 с, из них основного текста 134 с, список литературы из 117 наименований, 38 рисунков и 14 таблиц.

СОДЕРЖАНИЕ РАБОТЫ

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

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

6

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

Проблема анализа безопасности протоколов была впервые четко обозначена в начале 80-х годов прошлого века в работах Д. Долева и А. Яу, сформулировавших основные условия относительно выполнения протоколов в недружелюбной сетевой среде и возможностей злоумышленника. За прошедший период был предложен ряд методов для анализа безопасности ПИО. В ходе выполнения работы был сделан критический анализ ранних теоретико-автоматных методов, логических исчислений (BAN-, GNY-, AT- и SVO-лотики) и современных теоретико-алгебраических методов (CSP-алгебра, Лт-исчисление и его расширения), предлагавшихся для решения проблемы определения безопасности протоколов. Существующие методы были апробированы на большом количестве протоколов и позволили найти ряд новых несостоятельностей. Однако до сих пор не было предложено общепризнанного и достаточно универсального метода доказательства безопасности произвольного протокола. Проведенный критический анализ показал область

применимости существующих методов и ряд ограничений в их использовании. Исторически так сложилось, что существующие методы позволяют проверять выполнение только свойств секретности и аутентичности, в то время как современные протоколы должны обеспечивать выполнение гораздо большего количества различных требований безопасности. При использовании существующих методов рассматриваются идеализированные модели протоколов, на которые часто накладываются строгие ограничения по возможному формату сообщений и последовательности их передачи. Алгоритмы математических преобразований представляются в виде "черных ящиков", то есть внутренняя структура таких алгоритма, используемые алгебраические операции и их свойства не принимаются в расчет. При анализе идеализированных моделей протоколов учитывается только внешний интерфейс используемых алгоритмов, определяющийся набором и форматом входных и выходных значений. В тоже время, показано, что целый ряд несостоятельностей зависит именно от свойств используемых алгебраических операций в процессе преобразования данных. Сложность представляет анализ расширяемых протоколов, в которых заранее не известно количество абонентов и/или формат передаваемых сообщений. Часто невозможным становится анализ при условии, что злоумышленник может одновременно принимать участие в выполнении одного или

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

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

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

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

следующее уравнение эллиптической кривой: у1 = х3 +ах + Ь, где а,Ь,х,у е Рр,

р - характеристика конечного поля Ж, причем 3 И 4а3 + 2762 Ф 0. Выбор указанного математического аппарата обусловлен перспективностью его применения при разработке современных и будущих протоколов и систем, использующих криптографические технологии. В целом аппарат преобразований в группах точек эллиптической кривой обеспечивает большую стойкость алгоритмов, а значит и более долгосрочное хранение данных, являющихся результатом соответствующих криптографических преобразований, по сравнению с более традиционным аппаратом преобразований в мультипликативных группах, элементами которых являются целые числа. Выбор базового вида уравнения эллиптической кривой связан с утверждением этого уравнения в отечественном стандарте ГОСТ Р 34.10-2001, описывающем процессы формирования и проверки электронной цифровой подписи. Указанный стандарт является одним из ключевых для разработки безопасных ПИО в системах электронной коммерции и электронного документооборота.

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

автоматов Мили, где конечное непустое множество состояний; 5„с5-конечное непустое множество начальных состояний; X - конечное непустое множество входных значений; У- конечное непустое множество выходных значений; единичное множество синхронизирующих

значений; функция переходов и функция

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

условия ожидания абонентом некоторого сообщения и

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

В работе предлагается архитектура системы, предназначенной для создания и управления ИСИО, в рамках которой осуществляется выполнение протоколов и эмуляция атак на них. Для обеспечения процессов моделирования предложены две концептуальные модели

данных: модель информационного обмена (рис. 1) и модель эмуляции атак (рис.2).

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

Рис. 1 Модель данных информационного обмена

Для авторизации в системе определено несколько групп пользователей: абоненты, наблюдатели и администраторы. Абонентом является пользователь системы, который участвует в работе над протоколом, то есть в процессах выполнения протокола и эмуляции атак на него. В системе организуется ролевая работа над протоколом. Каждый абонент участвует в работе в выбранной роле.

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

Сессией будем называть объединение абонентов для работы над конкретным протоколом. В системе может одновременно выполняться несколько сессий одного и того же или нескольких протоколов. Каждый абонент может принимать участие в работе только одной сессии. Каждый пользователь может являться абонентом различных сессий.

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

В модели данных эмуляции атак введены следующие основные сущности: канал, цель, атак, тип атаки и потенциал злоумышленника.

В системе возможны три типа цели для атак: атаки на абонента, атаки на канал и атаки на сессию. Цель атаки определяется конкретный выбор объекта атаки.

Рис. 2 Модель данных эмуляции атак

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

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

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

Предложенный в работе метод анализа безопасности ПИО, состоит из следующих этапов:

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

11

реинжиниринга распределенных систем с целью восстановления реализованных в них протоколов.

2. На основании первичного описания протокола, подготавливается его унифицированное представление с помощью предложенной в работе нотации. На основании подготовленного унифицированного представления протокола принимаются следующие решения:

- выделяются роли абонентов;

- определяется последовательность передачи сообщений;

- определяются действия абонентов по подготовке и обработке сообщений;

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

3. Создается автоматная модель протокола с помощью предложенного в работе РКА. На основании созданной формальной модели происходит вложение протокола в систему. На этапе вложения определяется новый экземпляр сущности Протокол и связанный с ним список ролей.

4. В системе в рамках ИСИО создается новая сессия анализируемого протокола. Пользователи системы выбирают роли легальных абонентов и подключаются к сессии.

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

6. В системе осуществляется моделирование выполнения протокола. Легальные абоненты обмениваются сообщениями в соответствии с определенным представлением протокола. Контроль взаимодействия абонентов осуществляется на основе соответствия с формальной автоматной моделью протокола.

7. В системе автоматически происходит эмуляция атак на анализируемый протокол в соответствии с заданными условиями атаки и потенциалом злоумышленника. Если на некоторых этапах выполнения протокола требуется вмешательство нелегальных абонентов, то система приостанавливает выполнение протокола до принятия решения такими абонентами.

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

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

Архитектура системы (рис. 3) включает в себя следующий набор компонентов: подсистему управления сообщениями (ПУС), подсистему

эмуляции атак (ПЭА), подсистему математических преобразований (ПМП), подсистему администрирования (ПА) и подсистему мониторинга (ПМ).

Рис. 3 Архитектура системы

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

- специализированный вычислитель с поддержкой операций в мультипликативных группах;

- специализированный вычислитель с поддержкой операций в группах течек эллиптической кривой, определенной в конечном поле.

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

Максимальное число для математических операций 2 147 483 647

Максимальный размер модуля эллиптической кривой (бит/цифр) 32/4

Максимальное значение модуля эллиптической кривой 1200

Интервал доступных для просмотра простых чисел 2 - 2437

Максимальный размер хэш-значения (бит/цифр) 24/3

Интервал хэш-значений 0-255

Максимальное входное значение для алгоритма хэширования 36 893 488 147 419 103 231

Максимальный размер ключей в схеме RSA (бит/цифр) 72/9

Максимальный размер ключей в схеме Эль-Гамаля (бит/цифр) 32/4

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

На основе предложенной архитектуры было разработано математическое и программное обеспечение сетевого программного комплекса (ПК) "ИКАМ". ИСИО создается на базе существующей глобальной сетевой инфраструктуры Интернет. Разработанный сетевой ПК поддерживает следующие основные режимы работы:

- анализ безопасности протоколов;

- экспериментальное исследование протоколов;

- дистанционное обучение;

- итерационный процесс синтеза-анализа протоколов.

Результаты работы внедрены в учебный процесс высших учебных заведений и используются для подготовки специалистов в области информационных и сетевых технологий. За время эксплуатации сетевого ПК "ИКАМ", в своей работе его использовали около 150 пользователей, было организовано более 500 сессий для 12 различных ПИО. В таблице 2 приведена статистика использования сетевого ПК "ИКАМ" для экспериментального выполнения протоколов.

Таблица 2. Результаты выполнения протоколов

№ Наименование протокола Кол-во абонентов Среднее время выполнения (мин)

1 Передача конфиденциальных подписанных сообщений 3 40

2 Диалоговая передача сообщений Месси-Омуры 2 26

3 Разделение информации между абонентами сети 9 37

4 Электронные платежи с помощью цифровых денег 3 42

5 ЭЦП на основе схемы Эль-Гамаля 2 20

6 ЭЦП на основе стандарта ГОСТ Р 34.10-2001 2 35

7 ЭЦП на основе стандарта ИСО 9796 3 32

8 Распределение ключей Диффи-Хеллмана (ИСО 11770-3) 3 22

9 Распределение ключей МКВ (ИСО 11770-3) 3 31

10 Взаимная аутентификация Нидхема-Шредера 3 28

11 Исследование операций в конечных полях 2 38

12 Исследование операций в группах точек эллиптической кривой 2 41

ОСНОВНЫЕ РЕЗУЛЬТАТЫ РАБОТЫ

В процессе разработки и исследования системы были получены следующие теоретические и практические результаты:

1. Проанализированы требования безопасности современных ПИО, использующихся в системах электронного документооборота и электронной коммерции. Систематизированы современные требования безопасности протоколов и причины появления несостоятельностей в протоколах.

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

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

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

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

6. Разработана архитектура, математическое и информационное обеспечение вычислительной системы, предназначенной для создания и управления ИСИО, в рамках которой происходит анализ протоколов. Разработаны модели данных, обеспечивающие выполнение процессов информационного обмена и эмуляции атак на протоколы.

7. На основе разработанных методов и архитектуры был создан сетевой программный комплекс "ИКАМ". Разработанный сетевой ПК реализован по технологии клиент-сервер для создания ИСИО на базе глобальной сетевой инфраструктуры Интернет. С использованием разработанного сетевого ПК возможно проводить анализ новых протоколов без внесения изменений в программное, математическое и информационное обеспечение. Сетевой ПК

15

"ИКАМ" поддерживает четыре режима работы: анализ безопасности протоколов; экспериментальное исследование протоколов; дистанционное обучение через Интернет; итерационный процесс синтеза-анализа протоколов.

9. Результаты работы внедрены в учебный процесс высших учебных заведений. Были подтверждены несостоятельности ряда протоколов и показана возможная несостоятельность протокола электронных платежей, связанная с выбором параметров в используемых математических алгоритмах преобразования данных. За время эксплуатации разработанного сетевого ПК было организовано более 500 сессий для 12 различных протоколов. В работе приняло участие около 150 пользователей.

Основные результаты диссертации опубликованы в следующих работах:

1. Михайлов А.С., Левина Е.В., Анализ протокола Нидхема-Шредера с использованием ИКАМ. // Научная сессия МИФИ-2004. Сборник научных трудов. - М.: МИФИ, 2004

2. Михайлов А.С. Архитектура сетевого программного комплекса ИКАМ. // Безопасность информационных технологий, №3,2003

3. Михайлов А.С. Практический анализ криптографических протоколов. // Информационные технологии, №9,2003

4. Гайдюкова А.В., Михайлов А.С. Изучение информационного обмена в сетях. Лабораторный практикум. // Научная сессия МИФИ-2003. Сборник научных трудов. В 14 томах. Т.2. Программное обеспечение. Информационные технологии. М.: МИФИ, 2003

5. Гайдюкова А.В., Михайлов А.С. Автоматизация изучения протоколов информационного обмена. // Сборник научных трудов XI международного научно -технического семинара: Современные технологии в задачах управления, автоматики и обработки информации. - М.: МГАПИ, 2002

6. Ерохин ЕА., Михайлов А.С. Протоколы информационного обмена. Лабораторный практикум по курсу "Информационный обмен в сетях". - М.: МИФИ, 2002

7. Михайлов А.С. Автоматизация исследования протоколов информационного обмена. // 6-я Российская научно-практическая конференция "Реинжиниринг бизнес-процессов на основе современных информационных технологий. Системы управления знаниями": Сборник научных трудов / Моск. госуд. ун-т, экономики, статистики и информатики. - М., 2002

8. Михайлов А.С, Шаповалова А.В. Разработка подсистемы криптографических преобразований, интегрированной в WEB приложение. // Научная сессия МИФИ-2002. Сборник научных трудов. В 14 томах. Т.2.Программное обеспечение. Информационные технологии. - М.: МИФИ, 2002

9. Михайлов А.С. Способ построения среды информационного обмена для исследования криптографических протоколов. // 5-я Российская научно-практическая конференция "Реинжиниринг бизнес-процессов на основе современных информационных технологий" (РБП-2001). Сборник трудов. - М.: 2001

10. Ерохин ЕА., Михайлов А.С. Один подход к вопросу автоматизации проектирования криптографических протоколов. // Научная сессия МИФИ-2001. Сборник научных трудов. В 14 томах. Т.2. Информатика. Информационные технологии. Сетевые технологии. - М.: МИФИ, 2001

22МДР20о{ ÍJjg

Подписано в печать 10.12.2004 Тираж 120 экз. V

\ ! * /

ВВЕДЕНИЕ.

ГЛАВА I. ЗАДАЧА ОБЕСПЕЧЕНИЯ БЕЗОПАСНОСТИ ПРОТОКОЛОВ

ИНФОРМАЦИОННОГО ОБМЕНА.

1.1 Общесистемные вопросы организации информационного обмена.

1.1.1 Протоколы информационного обмена.

1.1.2 Средства моделирования информационных процессов.

1.1.3 Криптографические методы, используемые в ПИО.

1.2 Современные требования безопасности протоколов.

1.3 Несостоятельности протоколов.

1.4 Обзор существующих методов анализа протоколов.

1.4.1 Модель Долева-Яу.

1.4.2 ВАК-логика.

1.4.3 Бя-исчисление.

1.4.4 Анализ протоколов с использованием алгебры СвР.

1.5 Ограничения формальных методов анализа.

1.6 Постановка задачи.

1.7 Выводы.

ГЛАВА II. ТЕОРЕТИЧЕСКИЕ ОСНОВЫ РАЗРАБОТКИ МАТЕМАТИЧЕСКОГО

ОБЕСПЕЧЕНИЯ СИСТЕМЫ.

2.1 Метод организации математических преобразований.

2.1.1 Алгоритмы преобразований над данными.

2.1.2 Преобразования в группах точек эллиптической кривой.

2.2 Представление протоколов.

2.2.1 Вербальное описание.

2.2.2 Нотация для представления протоколов.

2.2.3 Автоматное представление протоколов.

2.3 Выводы.

ГЛАВА III. ПРОЕКТИРОВАНИЕ СИСТЕМЫ.

3.1 Общие требования к системе.

3.2 Метод анализа протоколов.

3.3 Архитектура системы.

3.4 Определение функциональных возможностей.

3.4.1 Функциональность подсистемы управления сообщениями.

3.4.2 Функциональность подсистемы эмуляции атак.

3.4.3 Функциональность подсистемы мониторинга

3.4.4 Функциональность подсистемы администрирования.

3.4.5 Функциональность подсистемы математических преобразований.

3.5 Модель данных.

3.5.1 Концептуальная модель данных информационного обмена.

3.5.2 Концептуальная модель данных для эмуляции атак.

3.6 Выводы.

ГЛАВА IV. СЕТЕВОЙ ПРОГРАММНЫЙ КОМПЛЕКС "ИКАМ"

И ЕГО ИСПОЛЬЗОВАНИЕ.

4.1 Технологические аспекты реализации сетевого ПК "ИКАМ".

4.2 Режимы использования

4.2.1 Анализ протоколов.

4.2.2 Анализ протокола "слепой" подписи для эллиптических кривых.

4.2.3 Анализ протокола Нидхема-Шредера в двух параллельных сессиях.

4.2.4 Экспериментальное исследование протоколов.

4.2.5 Дистанционное обучение.

4.2.6 Итерационный подход к проектированию протоколов.

4.3 Инсталляция сетевого ПК "ИКАМ".

4.3.1 Состав.

4.3.2 Инсталляция.

4.3.3 Результаты эксплуатации.

4.4 Выводы.

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

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

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

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

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

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

Разработанные методы позволили найти несостоятельности в некоторых протоколах, однако до сих пор не было предложено универсального метода анализа, который позволял бы для произвольного протокола получить однозначное заключение о безопасности. Более того, как правило, формальные методы анализа пригодны для работы только с идеализированными ограниченными классами протоколов. Кроме того, исторически так сложилось, что большинство существующих методов формального анализа ориентированы только на 6 доказательство традиционных требований безопасности: секретности и аутентичности. Однако на практике появляется все больше протоколов с другими, новыми требованиями безопасности. В большей степени это связано с развитием электронной коммерции. Так, например, появились требования честности, анонимности, неопровержимости и другие, присущие протоколам электронного заключения контрактов и платежей. Кроме того, как показывает реальная практика, обнаружение несостоятельностей в протоколах может происходить и происходит спустя длительное время после опубликования, разработки и внедрения протоколов. В некоторых случаях оказывается, что новые несостоятельности и угрозы безопасности обнаруживаются в протоколах, которые ранее уже подвергались анализу с использованием одного или нескольких методов. Например, несостоятельность связанная с выполнением протокола Нидхема-Шредера в двух параллельных сессиях, была продемонстрирована спустя семнадцать лет, после опубликования протокола [83, 96]. Совсем недавно была показа принципиальная возможность успешной атаки на протоколы SSL/TLS, несостоятельность которых связана с анализом времени отклика сервера в случае некорректной реализации протоколов. Между опубликованием протокола SSL и обнаружением несостоятельности в этом случае прошло порядка девяти лет [81]. Следует заметить, что протоколы Нидхема-Шредера и SSL/TLS неоднократно подвергались анализу безопасности, но указанных несостоятельностей в свое время обнаружено не было. Эти и другие проблемы формальных методов не позволяют говорить о существовании приемлемого решении задачи анализа безопасности протоколов.

В работе выполнение и анализ ПИО предлагается осуществлять в специальной исследовательской среде информационного обмена (ИСИО), которая создается и управляется с помощью вычислительной системы. ИСИО строится на базе существующей глобальной сетевой инфраструктуры. Работа и выполнение ПИО происходит в реальном сетевом режиме. Должна быть обеспечена возможность анализа максимально широкого класса протоколов без изменений в математическом, программном и информационном обеспечении системы. 7

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

Целью диссертационной работы явилась: создание математического, программного и информационного обеспечения системы и разработка сетевого программного комплекса для моделирования выполнения протоколов и эмуляции атак; разработка архитектуры вычислительной системы; разработка нового метода анализа безопасности ПИО.

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

ЭВМ в рамках системы. Направление исследований связано с созданием способа обнаружения несостоятельностей в разрабатываемых ПИО на этапе их проектирования, либо в уже существующих ПИО, что позволит сокращать сроки анализа протоколов и 8 соответственно сокращать сроки модификации и внедрения информационных систем, использующих ПИО.

В результате проделанной работы был предложен новый метод анализа ПИО, основанный на информационном моделировании выполнения ПИО в ИСИО и эмуляции атак на них. Была разработана архитектура вычислительной системы, предназначенной для создания ИСИО с целью анализа и исследования протоколов. Было создано математическое и программное обеспечение сетевого программного комплекса. Обеспечивается возможность одновременной организации работ по произвольным ПИО в реальном сетевом режиме с поддержкой удаленной связи абонентов и подсистем через Интернет. Результаты диссертационной работы внедрены в учебный процесс. Разработанный программный комплекс используется в качестве лабораторного практикума, для анализа широкого спектра ПИО, включая протоколы передачи электронных документов, заверенных электронной цифровой подписью (ЭЦП), финансовые протоколы электронных платежей с помощью цифровых денег, протоколы разделения информации между абонентами сети и другие.

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

8. Результаты работы внедрены в учебный процесс высших учебных заведений. Были подтверждены несостоятельности ряда протоколов и показана возможная несостоятельность протокола электронных платежей, связанная с выбором параметров в используемых алгоритмах. За время эксплуатации разработанного сетевого ПК было организовано более 500 сессий для 12 различных протоколов. В работе приняло участие около 150 пользователей.

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

Заключение

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

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

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

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

I I I

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

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

6. Разработана архитектура человеко-машинной системы, предназначенной для создания

I : и управления исследовательской средой информационного обмана, в рамках которой

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

7. На основе разработанной архитектуры и определенных функциональных требований был создан сетевой ПК "ИКАМ", с помощью которого стало возможным создание исследовательской среды информационного обмена на базе существующей инфраструктуры сетей Интернет/Интранет. Программное обеспечение сетевого ПК предоставляет интерфейсы

133 для взаимодействия пользователей между собой и с информационнЬй системой, в процессе анализа и исследования протоколов. Сетевой ПК "ИКАМ" поддерживает четыре режима работы: анализ безопасности протоколов; экспериментальное исследование протоколов; дистанционное обучение через Интернет; итерационный процесс синтеза-анализа протоколов.

1. АкритасА. Основы компьютерной алгебры с приложениями. М.: Мир, 1994.

2. Анин Б. Защита компьютерной информации, СПб.: BHV - Санкт-Петербург, 2000

3. Анохин М.И., Варновский Н.П., Сидельников В.М., Ященко, В.В. Криптография в банковском деле. -М.: МИФИ, 1997 I ;

4. Афонина C.B. Электронные деньги. СПб.: Питер, 2001

5. Бабенко и др. Новые технологии электронного бизнеса и безопасности. М.: Радио и связь, 2001

6. Бек К. Экстремальное программирование. СПб.: Питер, 2002

7. Брауэр В. Введение в теорию конечных автоматов. М.: Радио и связь, 1987

8. Буч Г. Объектно-ориентированный анализ и проектирование с примерами приложений на С++, 2-е изд. М.: "Издательство Бином", 19981.i

9. Буч Г., Рамбо Д, Якобсон А. Унифицированный процесс разработки программного обеспечения. СПб.: Питер, 2002.

10. Варфоломеев A.A., Жуков А.Е., Мельников А.Б„ Устюжин Д.Д. Блочные криптосистемы. Основные свойства и методы анализа стойкости. — М.: МИФИ, 1998

11. Василенко О.Н. Теоретико-числовые алгоритмы в криптографии. М.: МЦНМО, 2003

12. Верещагин Н.К., Шень А. Лекции по математической логики и теории алгоритмов. Часть 2. Языки и исчисления. М.: МЦНМО, 2002

13. Виноградов И.М. Основы теории чисел. М.: Наука, 1972

14. Галочкин А.И., Нестеренко Ю.В., Шидловский А.Б. Введение в Теорию чисел. М.: МГУ, 1984

15. Гашков С.Б., Чубариков В.Н, Арифметика. Алгоритмы. Сложность вычислений. М.:1. Наука, 1996

16. Глухое М.М., Нечаев A.A., Елизаров В.П. Алгебра: Учебник для вузов: В 2 т.: Т. 1. М.: Гелиос АРВ, 2003

17. Домашев A.B., Попов О.В., Правиков Д.И., Прокофьев И.В., Щербаков А.Ю.

18. Программирование алгоритмов защиты информации. М.: "Нолидж'1 2000

19. Ерохин Е.А., Михайлов A.C. Протоколы информационного ; обмена. Лабораторный практикум по курсу "Информационный обмен в сетях". М.: МИФИ, 2002

20. Ерохин Е.А., Михайлов A.C. Один подход к вопросу автоматизации проектирования криптографических протоколов. // Научная сессия МИФИ-2001. Сборник научных трудов. В 14 томах. Т.2. Информатика. Информационные технологии. Сетевые технологии. М.: МИФИ, 2001

21. Зима В., Молдовян А., Молдовян Н. Безопасность глобальных сетевых технологий. -СПб.: BHV Санкт - Петербург, 20021..

22. Иванов М.А. Криптографические методы защиты информа|цйи в компьютерных системах и сетях. М.: КУДИЦ-ОБРАЗ, 2001

23. Канер С. и др. Тестирование программного обеспечения. К.: Издательство "ДиаСофт", 2000

24. Карпов Ю.Г. Теория автоматов. СПб.: Питер, 2002

25. КоблицН. Курс теории чисел и криптографии. М.: Научное изд-во ТВП, 2001

26. Ковалев А., Курдюмов И. и др. Управление проектом по созданию интернет-сайта. М.: Альпина Паблишер, 2001

27. Коналлен Д. Разработка Web-приложений с использованием UML; М.: Вильяме, 2001

28. Коутинхо С. Введение в теорию чисел. Алгоритм RS А. М.: Постмаркет, 2001

29. Кудрявцев В.Б., Алешин С.В., Подколзин A.C. Введение в теорию автоматов. М.: Наука, 1985

30. Кузин Л.Т. Основы кибернетики: В 2-х т. Т.2. Основы кибернетических моделей. М.: Энергия, 1979

31. Ларман К. Применение UML и шаблонов проектирования. М,: Издательский дом "Вильяме", 2001I

32. Малюк A.A., Пазизин C.B., Погожин Н.С. Введение в защиту информации в автоматизированных системах. М.: Горячая линия - Телеком, 2001

33. Медведовский И.Д., Семьянов П.В., Платонов В.В. Атака через INTERNET. СПб.: "Мир и семья-95", 1997

34. Мельников Д.А. Информационные процессы в компьютерных сетях. Протоколы, стандарты, интерфейсы, модели. М.: КУДИЦ-ОБРАЗ, 2000

35. Михайлов A.C. Практический анализ криптографических проток<Цов. // Информационные технологии, №9,2003 ' •

36. Михайлов A.C. Архитектура сетевого программного комплекса ИКАМ. // Безопасность информационных технологий, №3,2003

37. Михайлов A.C., Гайдюкова A.B. Изучение информационного обмена в сетях. Лабораторный практикум. // Научная сессия МИФИ-2003. Сборник научных трудов. В 14 томах. Т.2. Программное обеспечение. Информационные технологии. М.: МИФИ, 2003

38. Михайлов A.C., Левина Е.В. Анализ протокола Нидхема-Шредера с использованием ИКАМ. // Научная сессия МИФИ-2004. Сборник научных трудов. М.: МИФИ, 2004

39. Нечаев В.И. Элементы криптографии. Основы теории защиты информации. М.: Высш. шк., 1999

40. Ноден П., Kumme К Алгебраическая алгоритмика. М.: Мир, 1999

41. Прасолов В.В., Соловьев Ю.П. Эллиптические функции и алгебраические уравнения. -М.: Изд-во "Факториал", 1997i

42. Романец Ю.В., Тимофеев П.А., Шаньгин В.Ф. Защита информации в компьютерных системах и сетях. М.: Радио и связь, 1999

43. Романов В.Ю. Основные графические обозначения предназначенные для объектно-ориентированного проектирования программ и их интерпретация для языка С++. Препринт №3. М.: НИВЦ МГУ, 1996

44. Смит Р.Э, Аутентификация: от паролей до открытых ключей. М.: Издательский дом "Вильяме", 2002

45. Соловьев Ю.П. Рациональные точки на эллиптических кривых// Соросовский образовательный журнал. 1997. № 10

46. Соловьев Ю.П., Садовничий В.А., Шавгулидзе Е.Т., Белокуров В.В. Эллиптические кривые и современные алгоритмы теории чисел. Москва-Ижевск: Институт компьютерных исследований, 2003

47. Столлингс В. Криптография и защита сетей: принципы и практика. М.: Издательский дом "Вильяме", 2001 .

48. Тюрин Ю.Н., Макаров А. А. Статистический анализ данных на компьютере. М.: ИНФРА, 1998

49. Черемушкин А.В. Лекции по арифметическим алгоритмам в криптографии. М.: МЦНМО, 2002

50. Чмора A.JI. Современная прикладная криптография. М.: Гелиос АРВ, 2001

51. Шнайер Б. Прикладная криптография. Протоколы, алгоритмы, исходные коды на языке Си. -М.: Издательство ТРИУМФ, 2002i ,

52. Фаулер М., Скотт К. UML в кратком изложении. Применение стандартного языка объектного моделирования. М.: Мир, 1999

53. Фомичев В.М. Дискретная математика и криптология. М.: ДИАЛОГ-МИФИ, 2003

54. Фомичев В.М. Информационная безопасность: Математические основы криптологии. -М.: МИФИ, 1995

55. Яблонский С.В. Введение в дискретную математику. М.: Наука, 1979

56. Ященко В.В. Введение в криптографию. М.: МЦНМО «ЧеРо», 1998

57. Abadi М. Secrecy by typing in security protocols. // Journal of th ACM, 46(5):749-786,1999

58. Abadi M., Gordon A. A calculus for cryptographic protocols: the spi calculus. // Information and Computation, 148(l):l-70, 1999

59. Abadi M., Fiore M. Computing symbolic models for verifying cryptographic protocols. // In 14th IEEE Computer Security Foundations Workshop, pp. 160-173. IEEE Computer Society, 2001

60. Bleichenbacher D. A Chosen Cipertext Attack against Protocols based on the RSA Encryption Standard PKCS #1. Proc. In CRYPTO'98, LNCS 1462, pages 1-12. Spring-Verlag, Berlin, 1998

61. Burrows M., Abadi M, Needham R. A Logic of Authentication. // ACM Transactions in Computer Systems, 8(l):18-36, Feb 1990

62. Comon H., Shmatikov V. Is it possible to decide whether a cryptographic protocol is secure or not? // Journal of Telecommunications and Information Technology, vol. A, 2002, pages 5-15

63. Diffie W.j Hellman M.E. New Directions in Cryptography // IEEE Transaction on Information Theory. 1976. V.IT-22. № 6. P.644-654.

64. Do lev D., Yao A. On the security of Public Key Protocols. // IEEE Transaction on Information Theory, 29(2): 198-208, March 1983

65. Durgiv N., Lincoln P., Mitchell J., ScedrovA. Undecidability of bounded security protocols. // In Proceedings "Workshop on formal methods in security protocols". The 1999 Federated Logic Conference (FLoC'99), Trento, Italy, July, 1999

66. ElGamal T. A. Public-Key Cryptosystem and a Signature Scheme Based on Discrete Logarithms // IEEE Transaction on Information Theory. 1985. V.31. № 4. P.569-472.

67. Fabrega F.J., Herzog J., Guttman J, Strand spaces: Why is a security protocol correct? Ini

68. Proc. IEEE Symposium on Security and Privacy, pages 160-171, 1998. j

69. Gong L.y Needham R., Yahalom R, Reasoning about belief in cryptographic protocols. In IEEE Symposium on Research in Security and Privacy, pages 234-248, Oakland, California, May 1990. IEEE Computer Society Press.

70. Gordon A., Jeffrey A. Authentication by typing in security protocols. II In 14th IEEE Computer Security Foundations Workshop (CSFW 2001), pages 145-159, Cape Breton, June 11-13, 2001.

71. Hoare G Communicating Sequential Processes. II Prentice-Hall, 1985

72. Huima A., Efficient infinite-state analysis of security protocols. // Presented at FLOC'99 Workshop on Formal Methods and Security Protocols, 1999 !j e

73. Jakobsson M., MacKenzie P., Garay J. Abuse-Free Optimistic1 Contract Signing. In Proceedings of CRYPTO '99 Springer-Verlag LNCS 1666 1999, pp. 406-416.

74. Jonson D., Menezes A. Elliptic Curve DSA (ECDSA): An Enhanced DSA // Certicom Corp. White Papers

75. Kessler K, Wedel G, AUTLOG-An advanced logic of authentication. In Proceedings of the Computer Security Foundations Workshop VII, pages 90-99, 1994,

76. Klima V., Pokorny O., Rosa T. Attacking RSA-based Sessions in SSL/TLS. // Presented at

77. CHES2003, September 7-11, Cologne, Germany . ,i

78. Lowe G. Breaking and fixing the Needham-Schroeder public-key protocol using FDR. // Software Concepts and Tools, 17:93-102, 1996

79. Lowe G., Schneider S., Roscoe B. and e.t.c. Modeling and analysis of security protocols. Addison-Wesley Pub Co, 2000, 352 pages.

80. Meadows C. Formal Methods for Cryptographic Protocol Analysis: Emerging Issues and Trends. // IEEE Journal on Selected Areas in Communication, Vol. 21, No. 1, pp. 44-54, January 2003

81. Meadows C. Open issues in formal methods for cryptographic jpfotocol analysis. // In Proceedings of DISCEX 2000, pages 237-250. IEEE Computer Society Press,12000

82. Meadows C. Analyzing the Needham-Schroeder public-key protocol: A comparison of two approaches. I IESORICS 96, LNCS 1146, pages 351-364, 1996.

83. Meadows C. Formal verification of cryptographic protocols: a survey. // Advances in Cryptology ASIACRYPT'94 Proceedings in Springer-Verlag, 1995, pages 133-150

84. Meadows C. The NRL Protocol Analyzer: An Overview. // In Proc. Of the 2nd International Conference on the Practical Application of PROLOG, 1994

85. Meadows C. Applying Formal Methods to the Analysis of a Key Management Protocol. // Journal of Computer Security, 1:5-53, 1992 I

86. Mitten J.K., Clark S.C., Freedman S.B. The Interrogator: Protocol Security Analysis. // IEEE Transactions on Software Engineering, SE-13(2), 1987

87. Milner R., Parrow J., Walker D. A calculus of mobile processes. // Information and Computation, pp. 1-77, 1992

88. Mitchell J., Mitchell M., Stern U. Automated Analysis of Cryptographic Protocols using Murphi. // In Proc. Of he 1997 IEEE Symposium on Security and Privacy, pages 141-151. IEEE Computer Society Press, 1997 ii

89. Mitchell J., Shmatikov V., Stem U. Finite-State Analysis of SSL 3.0'. In Proc. 7th USENIX Security Symposium, pages 201-215, 1998

90. Moore J. H. Protocol failures in cryptosystems. // IEEE Trans. Informal Theory, vol.5 T-76, pp. 594-602, May 1988

91. Needham R.M., Schroeder M.D. Using encryption for authentication in Large Networks of Computers. // Communications of the ACM, 21(12):993-999, Dec. 1978

92. Paulson L.C. Inductive analysis of the Internet protocol TLS. // ACM Transactions on Information and System Security (TISSEC), Volume 2, Issue 3, 1999, pp. 332-351

93. Rivest R.L, Shamir A., Adleman L.M. A Method for Obtaining Digital Signatures and Public-Key Cryptosystems // Comm. ACM. 1978. V.21. № 2.

94. Roscoe A.W. Modeling and verifying key-exchange protocols using CSP and FDR. // In 8th IEEE Computer Security Foundation Workshop, pp. 98-107. IEEE Computer Society, 1995.

95. Rusinowitch M., Turuani M. Protocol insecurity with finite number of session is NP-complete. // In 14th IEEE Computer Security Foundations Workshop, pp. 174-190. IEEE Computer Society, 2001

96. SchneierB. Security Pitfalls in Cryptography. // Counterpane Systems Press, 1998. http://www.counterpane.com/pitfalls.pdf j ,

97. Song D. Athena: a New Efficient Automatic Checker for Security Protocol Analysis. // In Proc. 12th IEEE Computer Security Foundations Workshop, pages 192-202,1999.

98. Song D., Berezin S., Perrig A. Athena: a novel approach to efficient automatic security protocol analysis. // Journal of Computer Security, 9(l):47-74,2001.

99. Tang L. Verifiable Transaction Atomicity for Electronic Payment Protocols. // In Proc. of the 16th International Conference on Distributed Computing Systems (ICDCS'96), Hong Kong, 1996, pp. 261-269

100. Wagner D., Schneier В. Analysis of the SSL 3.0 Protocol. // The Second USENIX Workshop on Electronic Commerce Proceedings, USENIX Press, November 1996, pp. 129-40.

101. Wang W., HidvegiZ., Bailey A. D., Whinston A. B. E-Process Design and Assurance Using Model Checking. // IEEE Computer Vol. 33, No 10, 2000, pp. 48-53

102. Silverman J, The Arithmetic of Elliptic Curves. Heidelberg etc.: Springer, 1986

103. Hasse H. Abstrakte Begründung der konplexen Multiplikation und Riemannsche Vermutung in Funktionenkörpern // Abh. Math. Sem. Humbuxg, 1934. Bd. 10. - s. 325-348.

104. Schoof R. Elliptic curves over finite fields and computations of square roots mod p. Math.

105. Сотр., 1985, v. 44, p. 483-494 ji

106. ГОСТ 28147-89. Системы обработки информации. Защита криптографическая. Алгоритм криптографического преобразования

107. ГОСТ Р 34.10-2001. Информационная технология. Криптографическая защита информации. Процессы формирования и проверки электронной цифровой подписи.

108. ГОСТ Р 34.10-94. Информационная технология. Криптографическая защита информации. Процедуры выработки и проверки электронной цифровой подписи на базе асимметричного криптографического алгоритма1.I

109. ITU-T Z.100 Specification and Description Language (SDL)

110. ITU-T Z.109 SDL combined with UML

111. ITU-T Z.110 Criteria for use of formal description techniques by ITU-T

112. ITU-T Z.120 Message Sequence Chart (MSC)