Страница курса: https://lk.msu.ru/course/view?...

В курсе сначала будут изложены примеры протоколов безопасности, предназначенные для решения различных задач, связанных с обработкой информации в условиях присутствия в среде выполнения протоколов активного противника. Это протоколы электронной торговли, протоколы аутентификации, протоколы голосования, и др. Затем будет подробно описана введенная автором процессная модель протоколов безопасности. Для данной модели будут сформулированы и доказаны математические утверждения, на базе которых можно решать задачи формальной верификации протоколов безопасности. В практических занятиях, относящихся к данному курсу, будет изучаться система дедуктивной верификации Isabelle. Дедуктивная верификация связана с построением математических доказательств теорем о том, что анализируемые протоколы безопасности обладают заданными свойствами. Задачи построения математических доказательств формальных утверждений относятся к классическим задачам искусственного интеллекта — автоматизации логических рассуждений. В курсе будут излагаться логические формализмы, связанные с проведением интеллектуальных рассуждений о правильности протоколов, и будут даны различные иллюстрации проведения интеллектуальных рассуждений для различных классов программ и протоколов, в том числе для параллельных и распределенных программ и криптографических протоколов. Анализ моделей программ (model checking) связан с другими подходами — построением диаграмм переходов программ (моделей Крипке), которые представляют собой большие графы и во многих случаях требуют для своего анализа с приемлемой сложности упрощения до компактных вероятностных автоматных моделей. В курсе будет дано введение в вероятностные автоматные модели. Также в курсе будут изложены методы моделирования и верификации протоколов безопасной передачи данных через ненадёжную среду.

Список всех тем лекций

Лекция 1. Понятие протокола безопасности.
Криптографический протокол, основные понятия Задача проверки подлинности, протокол Нидхэма-Шредера Примеры протоколов безопасности

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

Лекция 3. Протоколы электронного голосования.
Принцип работы слепой подписи Анонс семинара к курсу Циклический протокол голосования Протокол с защитой от мошенничества ЦИК

Лекция 4. Протоколы электронных платежей.
Протоколы электронных платежей Протокол Диффи-Хеллмана Протокол Station-To-Station Протоколы квантовой передачи ключей

Лекция 5. Теория процессов. Примеры верификации свойств процессов.
Протоколы передачи ключей по квантовому каналу Протокол и его процессы Система из параллельно выполняемых процессов Интеллектуальный анализ протокола

Лекция 6. Верификация протокола с чередованием битов.
Протокол передачи данных в одном направлении Проверка свойств рассмотренного протокола

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

Лекция 8. Протоколы безопасности на вероятностном уровне.
Протокол передачи данных через небезопасную среду Вероятностная система переходов Язык описания свойств протоколов PCTL

Лекция 9. Алгоритмы вычисления значений формул.
Повторение Вычисление формул в протоколе PCTL Общие модели сложных устройств Описание формул в протоколе CTL Вычисление формул в протоколе CTL

Лекция 10. Протокол аутентификации Yahalom.
Протокол Yahalom Формальная модель сеанса протокола Проверка ожидаемых от протокола свойств

Лекция 11. Задача двух миллионеров, протоколы с нулевым разглашением (изоморфизм графов, доказательство знания гамильтонова цикла в графе), протокол подписания контракта.