УДК 004.054
В рамках данной работы проведен обзор актуальных программных инструментов формального анализа протоколов аутентификации и авторизации. Рассмотрены такие программные средства, как AVISPA, ProVerif, Tamarin Prover и Scyther, а также их применимость и производительность для оценки безопасности протоколов аутентификации и авторизации. На основании анализа исследований сделан вывод об отсутствии универсального инструмента верификации протоколов, и выдвинута гипотеза о возможности повышении уровня достоверности оценки безопасности протоколов аутентификации и авторизации распределенных систем путем применения БАН-логики. Исследование выполнено при финансовой поддержке РФФИ в рамках научного проекта No 18-37-00430.
In the given article, was conducted an overview of the current software tools for formal analysis of authentication and authorization protocols. There are considered such software tools as AVISPA, ProVerif, Tamarin Prover and Scyther as well as their applicability and performance for assessing the security of authentication and authorization protocols. Based on the analysis studies concluded that there is no universal protocol verification tool and the hypothesis of the possible increase of reliability level of the safety assessment of distributed systems authentication and authentication protocols by applying BAN-logic raised. The research was sponsored by RFBR, research project number No 18-37-00430.