В мобильной распределённой кибер-физической системе эта задача осложняется рядом специфических факторов, связанных, в том числе с неконтролируемым доступом к беспроводной среде передачи данных и ограничениями на применение «тяжёлой» криптографии. В работе исследуется предложенный автором облегчённый протокол взаимной аутентификации мобильных агентов, а также проводится формализованная проверка выполнения требований по безопасности, предъявляемых к этому протоколу. Результаты исследования подтверждают корректность предлагаемого протокола с учётом ограничений по ресурсоёмкости и целесообразность применения инструментального средства формализованного доказательства корректности параллельных процедур с использованием технологии верификации моделей (Model Checking).

Чан З., Ле З. (науч. рук. Комаров И.И.) Верификация безопасности протокола аутентификации типа «запрос – ответ» с помощью инструмента AVISPA // Сборник тезисов докладов конгресса молодых ученых. Электронное издание. – СПб: Университет ИТМО, [2021]. URL: https://kmu.itmo.ru/digests/article/6241