Помощь в написании студенческих работ
Антистрессовый сервис

Система анализа безопасности и исследования протоколов информационного обмена

ДиссертацияПомощь в написанииУзнать стоимостьмоей работы

Разработанные методы позволили найти несостоятельности в некоторых протоколах, однако до сих пор не было предложено универсального метода анализа, который позволял бы для произвольного протокола получить однозначное заключение о безопасности. Более того, как правило, формальные методы анализа пригодны для работы только с идеализированными ограниченными классами протоколов. Кроме того, исторически… Читать ещё >

Система анализа безопасности и исследования протоколов информационного обмена (реферат, курсовая, диплом, контрольная)

Содержание

  • ГЛАВА 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-е изд. М.: «Издательство Бином», 19 981. 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. В., Молдовян А., Молдовян Н. Безопасность глобальных сетевых технологий. -СПб.: BHV Санкт — Петербург, 20 021.
  21. М.А. Криптографические методы защиты информа|цйи в компьютерных системах и сетях. М.: КУДИЦ-ОБРАЗ, 2001
  22. С. и др. Тестирование программного обеспечения. К.: Издательство «ДиаСофт», 2000
  23. Ю.Г. Теория автоматов. СПб.: Питер, 2002
  24. КоблицН. Курс теории чисел и криптографии. М.: Научное изд-во ТВП, 2001
  25. А., Курдюмов И. и др. Управление проектом по созданию интернет-сайта. М.: Альпина Паблишер, 2001
  26. Д. Разработка Web-приложений с использованием UML— М.: Вильяме, 2001
  27. С. Введение в теорию чисел. Алгоритм RS А. М.: Постмаркет, 2001
  28. В.Б., Алешин С. В., Подколзин A.C. Введение в теорию автоматов. М.: Наука, 1985
  29. Л.Т. Основы кибернетики: В 2-х т. Т.2. Основы кибернетических моделей. М.: Энергия, 1979
  30. К. Применение UML и шаблонов проектирования. М: Издательский дом «Вильяме», 2001I
  31. A.A., Пазизин C.B., Погожин Н. С. Введение в защиту информации в автоматизированных системах. М.: Горячая линия — Телеком, 2001
  32. И.Д., Семьянов П. В., Платонов В. В. Атака через INTERNET. СПб.: «Мир и семья-95», 1997
  33. Д.А. Информационные процессы в компьютерных сетях. Протоколы, стандарты, интерфейсы, модели. М.: КУДИЦ-ОБРАЗ, 2000
  34. A.C. Практический анализ криптографических проток<�Цов. // Информационные технологии, № 9,2003 ' •
  35. A.C. Архитектура сетевого программного комплекса ИКАМ. // Безопасность информационных технологий, № 3,2003
  36. В.И. Элементы криптографии. Основы теории защиты информации. М.: Высш. шк., 1999
  37. Ноден П., Kumme К Алгебраическая алгоритмика. М.: Мир, 1999
  38. В.В., Соловьев Ю. П. Эллиптические функции и алгебраические уравнения. -М.: Изд-во «Факториал», 1997i
  39. Ю.В., Тимофеев П. А., Шаньгин В. Ф. Защита информации в компьютерных системах и сетях. М.: Радио и связь, 1999
  40. В.Ю. Основные графические обозначения предназначенные для объектно-ориентированного проектирования программ и их интерпретация для языка С++. Препринт № 3. М.: НИВЦ МГУ, 1996
  41. Смит Р. Э, Аутентификация: от паролей до открытых ключей. М.: Издательский дом «Вильяме», 2002
  42. Ю.П. Рациональные точки на эллиптических кривых// Соросовский образовательный журнал. 1997. № 10
  43. Ю.П., Садовничий В. А., Шавгулидзе Е. Т., Белокуров В. В. Эллиптические кривые и современные алгоритмы теории чисел. Москва-Ижевск: Институт компьютерных исследований, 2003
  44. В. Криптография и защита сетей: принципы и практика. М.: Издательский дом «Вильяме», 2001 .
  45. Ю.Н., Макаров А. А. Статистический анализ данных на компьютере. М.: ИНФРА, 1998
  46. А.В. Лекции по арифметическим алгоритмам в криптографии. М.: МЦНМО, 2002
  47. A.JI. Современная прикладная криптография. М.: Гелиос АРВ, 2001
  48. . Прикладная криптография. Протоколы, алгоритмы, исходные коды на языке Си. -М.: Издательство ТРИУМФ, 2002i ,
  49. М., Скотт К. UML в кратком изложении. Применение стандартного языка объектного моделирования. М.: Мир, 1999
  50. В.М. Дискретная математика и криптология. М.: ДИАЛОГ-МИФИ, 2003
  51. В.М. Информационная безопасность: Математические основы криптологии. -М.: МИФИ, 1995
  52. С.В. Введение в дискретную математику. М.: Наука, 1979
  53. В.В. Введение в криптографию. М.: МЦНМО «ЧеРо», 1998
  54. Abadi М. Secrecy by typing in security protocols. // Journal of th ACM, 46(5):749−786,1999
  55. Abadi M., Gordon A. A calculus for cryptographic protocols: the spi calculus. // Information and Computation, 148(l):l-70, 1999
  56. 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
  57. 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
  58. Burrows M., Abadi M, Needham R. A Logic of Authentication. // ACM Transactions in Computer Systems, 8(l):18−36, Feb 1990
  59. 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
  60. Diffie W. j Hellman M.E. New Directions in Cryptography // IEEE Transaction on Information Theory. 1976. V. IT-22. № 6. P.644−654.
  61. Do lev D., Yao A. On the security of Public Key Protocols. // IEEE Transaction on Information Theory, 29(2): 198−208, March 1983
  62. 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
  63. 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.
  64. Fabrega F.J., Herzog J., Guttman J, Strand spaces: Why is a security protocol correct? Ini
  65. Proc. IEEE Symposium on Security and Privacy, pages 160−171, 1998. j
  66. 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.
  67. 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.
  68. Hoare G Communicating Sequential Processes. II Prentice-Hall, 1985
  69. Huima A., Efficient infinite-state analysis of security protocols. // Presented at FLOC'99 Workshop on Formal Methods and Security Protocols, 1999! j e
  70. Jakobsson M., MacKenzie P., Garay J. Abuse-Free Optimistic1 Contract Signing. In Proceedings of CRYPTO '99 Springer-Verlag LNCS 1666 1999, pp. 406−416.
  71. Jonson D., Menezes A. Elliptic Curve DSA (ECDSA): An Enhanced DSA // Certicom Corp. White Papers
  72. Kessler K, Wedel G, AUTLOG-An advanced logic of authentication. In Proceedings of the Computer Security Foundations Workshop VII, pages 90−99, 1994,
  73. Klima V., Pokorny O., Rosa T. Attacking RSA-based Sessions in SSL/TLS. // Presented at
  74. CHES2003, September 7−11, Cologne, Germany., i
  75. Lowe G. Breaking and fixing the Needham-Schroeder public-key protocol using FDR. // Software Concepts and Tools, 17:93−102, 1996
  76. Lowe G., Schneider S., Roscoe B. and e.t.c. Modeling and analysis of security protocols. Addison-Wesley Pub Co, 2000, 352 pages.
  77. 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
  78. Meadows C. Open issues in formal methods for cryptographic jpfotocol analysis. // In Proceedings of DISCEX 2000, pages 237−250. IEEE Computer Society Press, 12 000
  79. Meadows C. Analyzing the Needham-Schroeder public-key protocol: A comparison of two approaches. I IESORICS 96, LNCS 1146, pages 351−364, 1996.
  80. Meadows C. Formal verification of cryptographic protocols: a survey. // Advances in Cryptology ASIACRYPT'94 Proceedings in Springer-Verlag, 1995, pages 133−150
  81. Meadows C. The NRL Protocol Analyzer: An Overview. // In Proc. Of the 2nd International Conference on the Practical Application of PROLOG, 1994
  82. Meadows C. Applying Formal Methods to the Analysis of a Key Management Protocol. // Journal of Computer Security, 1:5−53, 1992 I
  83. Mitten J.K., Clark S.C., Freedman S.B. The Interrogator: Protocol Security Analysis. // IEEE Transactions on Software Engineering, SE-13(2), 1987
  84. Milner R., Parrow J., Walker D. A calculus of mobile processes. // Information and Computation, pp. 1−77, 1992
  85. 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
  86. Mitchell J., Shmatikov V., Stem U. Finite-State Analysis of SSL 3.0'. In Proc. 7th USENIX Security Symposium, pages 201−215, 1998
  87. Moore J. H. Protocol failures in cryptosystems. // IEEE Trans. Informal Theory, vol.5 T-76, pp. 594−602, May 1988
  88. 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
  89. 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
  90. Rivest R. L, Shamir A., Adleman L.M. A Method for Obtaining Digital Signatures and Public-Key Cryptosystems // Comm. ACM. 1978. V.21. № 2.
  91. 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.
  92. 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
  93. SchneierB. Security Pitfalls in Cryptography. // Counterpane Systems Press, 1998. http://www.counterpane.com/pitfalls.pdf j ,
  94. Song D. Athena: a New Efficient Automatic Checker for Security Protocol Analysis. // In Proc. 12th IEEE Computer Security Foundations Workshop, pages 192−202,1999.
  95. 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.
  96. 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
  97. 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.
  98. 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
  99. Silverman J, The Arithmetic of Elliptic Curves. Heidelberg etc.: Springer, 1986
  100. Hasse H. Abstrakte Begrundung der konplexen Multiplikation und Riemannsche Vermutung in Funktionenkorpern // Abh. Math. Sem. Humbuxg, 1934. Bd. 10. — s. 325−348.
  101. Schoof R. Elliptic curves over finite fields and computations of square roots mod p. Math.
  102. Сотр., 1985, v. 44, p. 483−494 ji
  103. ГОСТ 28 147–89. Системы обработки информации. Защита криптографическая. Алгоритм криптографического преобразования
  104. ГОСТ Р 34.10−2001. Информационная технология. Криптографическая защита информации. Процессы формирования и проверки электронной цифровой подписи.
  105. ГОСТ Р 34.10−94. Информационная технология. Криптографическая защита информации. Процедуры выработки и проверки электронной цифровой подписи на базе асимметричного криптографического алгоритма1. I
  106. ITU-T Z.100 Specification and Description Language (SDL)
  107. ITU-T Z.109 SDL combined with UML
  108. ITU-T Z.110 Criteria for use of formal description techniques by ITU-T
  109. ITU-T Z.120 Message Sequence Chart (MSC)
Заполнить форму текущей работой