Обозначения и сокращения 5
Введение 6
1 Обзор основных свойств безопасности криптографических
протоколов 7
1.1 Понятие криптографического протокола 7
1.2 Свойства, характеризующие безопасность протоколов 12
1.3 Разбор свойств безопасности криптографических протоколов . 13
2 Обзор методов анализа уязвимостей криптографических протоколов . . 18
2.1 Алгебраические свойства, анализируемые при проверке
корректности криптографических протоколов 18
2.2 Проверка корректности криптографических протоколов с
использованием формальных методов анализа 20
3 Обзор средств автоматизированного анализа протоколов 25
3.1 Значение автоматизированного анализа протоколов 25
3.2 AVISPA 25
3.3 Scyther 26
3.4 ProVerif. 28
3.5 Isabelle 28
3.6 SPIN 29
4 Обзор языка спецификации протоколов высокого уровня HLPSL 32
4.1 Понятие ролей и переходов 32
4.2 Синтаксис языка HLPSL 42
5 Разработка лабораторного стенда для проведения лабораторного
практикума 44
6 Реализация лабораторного практикума для средств AVISPA и SPAN .. 45
6.1 Ознакомление с языком описания криптографических
протоколов HLSPL и инструментом анализа протоколов AVISPA 45
6.2 Реализация протокола обеспечения конфиденциальности и целостности передачи сообщения между двумя участниками на языке
HLPSL и проверка его корректности 51
6.3 Реализация протокола явного ключевого аутентифицированного обмена с использованием языка спецификации протоколов высокого
уровня HLPSL и инструмента анализа протоколов AVISPA 58
Заключение 69
Список использованных источников 71
В сфере безопасности информационных технологий для безопасной передачи сообщений по большей части используются технологии криптографии. Процесс зашифрования, передачи, дешифрования
регламентируется особым порядком действий - протоколом. Развитие современных технологий не обошло стороной и криптографию: протоколы, считавшиеся надежными в течения десятилетий, обнаруживают свою неработоспособность в определенных условиях. Это возникло благодаря формализации и автоматизации средств анализа протоколов.
Студентам, обучающимся по специальности 10.03.05 «Информационная безопасность автоматизированных систем» необходимо получить знания и выработать практические навыки по применению средств автоматизированного анализа криптографических протоколов, так как установление причин уязвимостей и изучение атак на криптографические протоколы, которые реализуются благодаря им - отличная база для создания защищенных протоколов. Это позволит избегать прошлые ошибки и синтезировать надежные, относительно предыдущих, протоколы. Таким образом, тема выпускной квалификационной работы является актуальной.
В процессе выполнения задания на дипломное проектирование были
решены следующие задачи:
произведен обзор основных требований к безопасности
криптографических протоколов;
произведен обзор основных методов анализа криптографических
протоколов;
произведен обзор ряда средств автоматизированного анализа
криптографических протоколов;
разработан лабораторный стенд для проведения лабораторного
практикума;
разработан лабораторный практикум для практического закрепления
навыков работы со средством автоматизированного анализа
криптографических протоколов;
разработаны рекомендации для проведения лабораторного
практикума.
В результате разработан лабораторный практикум для применения
процедур управления сертификатами ключей проверки электронной подписи,
включающий лабораторный стенд, рекомендации для проведения практикума и
комплект заданий.
В разработанном практикуме рассмотрены следующие вопросы:
ознакомление со средством автоматизированного анализа
криптографических протоколов;
реализация протокола обеспечения конфиденциальности и
целостности передачи сообщения между двумя участниками на языке HLPSL и
проверка его корректности;
реализация протокола явного ключевого аутентифицированного
обмена.
70
Лабораторный стенд содержит виртуальную машину с установленной
операционной системой Ubuntu 10, средством автоматизированного анализа
криптографических протоколов AVISPA и аниматором протоколов
безопасности для данного средства SPAN.
Таким образом, цель ВКР достигнута, требования технического задания
на выпускную квалификационную работу выполнены в полном объеме.
