Аннотация:
Протоколы аутентификации — это распределенные алгоритмы, предназначенные для обеспечения аутентификации агентов и передачи конфиденциальной информации (криптографических ключей и т.п.) в небезопасной среде. Они используются, например, в электронных платежах, электронных процедурах голосования, системах доступа к базам данных, и т.д. Учитывая большой финансовый и социальный ущерб в случае неправильной работы таких протоколов, необходимо использовать математические методы для обоснования их корректности и безопасности. В настоящей работе вводится новая математическая модель таких протоколов аутентификации, позволяющая описывать как сами протоколы, так и их свойства. Показывается, как на базе данной модели можно решать задачи верификации протоколов аутентификации.