Интеллектуальные методы анализа протоколов безопасности
Механико-математический факультет

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