Кафедра «Кибернетика» Дипломная работа по направлению «Прикладная математика и информатика» на тему: Разработка инструментального средства автоматизированного анализа протоколов на основе расширения SPI- исчисления 2009 МОСКОВСКИЙ ИНЖЕНЕРНО-ФИЗИЧЕСКИЙ ИНСТИТУТ (ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТ) студент:Селезнёв Сергей Сергеевич руководитель:Михайлов Александр Сергеевич

Кафедра «Кибернетика» Методы анализа протоколов 2 Метод проверки Ограничения участников протокола Вычисли- тельная сложность анализа Сложность разработки модели Теоретико-доказательный подход нетнизкаявысокая LTSестьзаметнаянизкая SPI: Проверка тестовой эквивалентности естьзаметнаянизкая SPI: TypeCheckingнетнизкаяневысокая

Кафедра «Кибернетика» Анализатор STA 3 val inA = a'1!(N'A,A)^+kI >> a'2?(N'A,x'NI)^+kA >> a'3!(x'NI)^+kI >> stop & a1!(NA,A)^+kB >> a2?(NA,xNB)^+kA >> a3!(xNB)^+kB >> stop;

Кафедра «Кибернетика» Проект AVISPA-SPAN 4

Кафедра «Кибернетика» Синтаксис представления протокола Ограниченность протокола/злоумышленника Пользовательский интерфейс Базовая ОС - Linux Недостатки имеющихся анализаторов ПИО 5

Кафедра «Кибернетика» Текст протокола: SPI-исчисление Метод анализа: проверка типов typeChecking Свойства безопасности: аутентичность сущности, сообщения Результат анализа: обнаружены или нет уязвимости « Янус »: формальный анализ протокола 6

Кафедра «Кибернетика» Синтаксис представления протокола - SPI 7 Операция SPIСмысл операции out M N отправка inp M (x:T) приём repeat inp M (x:T) повторяющийся приём split M is (x:T,y:U) разделение пары match M is (N,y:T) сравнение пары case M is inl (x:T) P is inr (y:U) Q выбор из объединения decrypt M is {x:T} N симметричное зашифрование decrypt M is {|x:T|} N1 асимметричное зашифрование check M is N проверка метки времени new (x:T) создание имени P | Qкомпозиция stop бездействие

Кафедра «Кибернетика» Добавление к протоколу специальных операций К протоколам добавляется спецификация проверя- емого свойства и формализованный комментарий, показывающий, как именно достигается это свойство. Эти сведения представляются в виде специальных операций и типов данных. Они не нужны во время выполнения протокола, но позволяют провести его формальный анализ. Вычисление эффекта протокола Эффект протокола – множество, описывающее усло- вия, при которых в протоколе будет выполняться специ- фицированное свойство. Метод анализа TypeChecking 8

Кафедра «Кибернетика» Анализ модели протокола Нидхема - Шредера 9

Кафедра «Кибернетика» Сложность моделей протокола и злоумышленника неограничены В отличие от средств, основанных на model checking Легко подготовить модель протокола Модель протокола Нидхема-Шредера: 400 строк в CSP, 50 строк в SPI Графический интерфейс, ОС Windows Большинство аналогичных средств работает под Linux и ориентированы на командную строку Выводы : преимущества анализатора « Янус » 10

Кафедра «Кибернетика» Апробация работы 11 Селезнев С.С. «Янус»- анализатор протоколов информационного обмена. // Научная сессия МИФИ XII Московская международная телекоммуникационная конференция студентов и молодых ученых Молодежь и наука. В 2-х частях. Ч. 2. – М.: МИФИ, стр Селезнев С.С. О подходе к анализу протоколов с использованием расширенного SPI-исчисления. // Научная сессия МИФИ Сборник научных трудов. В 15 томах. Т.11. Технологии разработки программных систем. Информационные технологии. – М.: МИФИ, стр. 138 – Михайлов А.С., Ильичева Н.В., Селезнев С.С. Моделирование и анализ протоколов информационного обмена // Научная сессия МИФИ Аннотации докладов. В 3-х томах. Т.3. – М.: МИФИ, стр Seleznev S.S., Mikhaylov A.S. The security protocols analyzer using extensions of SPI-calculus. // In Proc. of SYRCoSE 2008, vol. 1, 2008, pp

Кафедра «Кибернетика» Спасибо за внимание! Вопросы?