Введение 4
1 Обзор методов анализа уязвимостей криптографических протоколов 5
1.1 Понятие криптографического протокола, виды
криптографических протоколов, свойства безопасности 5
1.2 Атаки на криптографические протоколы 8
1.3 Классификация методов анализа уязвимостей
криптографических протоколов 10
2 Обзор средств анализа уязвимостей криптографических
протоколов 14
3 Разработка протоколов с уязвимостями 22
3.1 Разработка протокола односторонней аутентификации со
внесением уязвимости в виде отсутствия защиты от атак повтора 22
3.2 Разработка протокола взаимной аутентификации со внесением
уязвимостей в виде отсутствия защиты от атак повтора и отсутствия контроля целостности потока сообщений 29
3.3 Разработка протокола передачи данных с обеспечением свойства
конфиденциальности со внесением уязвимостей в виде отсутствия защиты от атак повтора и отсутствия контроля целостности сообщений 40
3.4 Разработка протокола передачи данных с обеспечением свойства неотказуемости со внесением уязвимостей в виде отсутствия защиты от атак повтора, отсутствия контроля целостности потока сообщений, вычисления цифровой подписи не от всех полей сообщения, а также отсутствия
аутентификации одного из участников протокола 47
4 Разработка виртуального стенда для проведения лабораторного
практикума 60
5 Разработка рекомендаций по проведению лабораторного практикума...63
5.1 Разработка методики проведения практикума 63
5.2 Разработка руководства пользователя 65
6 Вредные психофизиологические факторы, влияющие на органы зрения специалиста по защите информации. Методы и средства физической культуры,
снижающие их воздействие 88
Заключение 91
Список используемых источников 92
При подготовке специалистов по информационной безопасности автоматизированных систем предусмотрено изучение дисциплины «Криптографические протоколы», в которой у студентов формируется компетенция ПК-3 «способность проводить анализ защищенности автоматизированных систем». При освоении данной компетенции студенты должны знать основные уязвимости криптографических протоколов и уметь проводить анализ их защищенности.
На сегодняшний момент для анализа защищенности криптографических протоколов применяются различные средства автоматизированного анализа, поэтому в рамках изучения дисциплины на практических занятиях студенты должны получить навыки работы с современными средствами анализа уязвимостей. Одним из таких средств является Tamarin Prover. Данное программное средство является одним из новейших инструментов для символьного моделирования и анализа криптографических протоколов. Сочетание автоматизированного и интерактивного режима построения доказательств позволит студентам наиболее детально понять процесс анализа уязвимостей.
Таким образом, разработка практикума по анализу уязвимостей криптографических протоколов с использованием Tamarin Prover является актуальной.
В ходе выполнения выпускной квалификационной работы был произведен анализ методов анализа уязвимостей криптографических протоколов. Был рассмотрен ряд средств анализа уязвимостей криптографических протоколов, при этом было произведено сравнение указанных средств по разработанным критериям. Затем был изучен синтаксис языка Tamarin, а также были получены навыки работы с Tamarin prover.
В результате был разработан лабораторный стенд, содержащий компоненты, необходимые для проведения лабораторного практикума. Был разработан ряд протоколов со внесенными уязвимостями, их формальное описание и описание в нотации Tamarin. Была разработана методика проведения практикума. Было оформлено руководство пользователя Tamarin prover, содержащее в себе синтаксис используемого языка, инструкцию по поиску уязвимостей с помощью Tamarin prover и пример такого поиска.
Таким образом, задание на выпускную квалификационную работу выполнено в полном объеме.
Лабораторный практикум, разработка которого осуществлялась в ходе выпускной квалификационной работы, был внедрен для использования на кафедре «Информационная безопасность систем и технологий».
