УДК 004.054
В рамках данной статьи проведен обзор наиболее используемых подходов для формального анализа криптографических протоколов и программных инструментов, реализованных на основе данных подходов. В статье рассмотрены такие подходы, как проверка модели, доказательство теорем и логика доверия, приведен перечень известных инструментов автоматизации анализа криптографических протоколов в рамках каждого подхода. На основании проведенных исследований сделан вывод об отсутствии универсального средства верификации протоколов и актуальности использования БАН-логики для формального анализа протоколов аутентификации. Исследование выполнено при финансовой поддержке РФФИ в рамках научного проекта No 18-37-00430.
In the given article, are reviewed the most used approaches for formal cryptographic protocols analysis and software tools implemented on these approaches basis. The article considers such approaches as model checking, theorem proving and the logic for trust, and a list of known tools for automating cryptographic protocols analysis within each approach basis.Based on conducted research was concluded that there is no universal protocol verification tool and the relevance of using BAN-logic for formal authentication protocols analysis. The research was sponsored by RFBR, research project number No 18-37-00430.