УДК 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.

Авторы:

Демидов Александр Владимирович

Орловский государственный университет имени И. С. Тургенева, г. Орел
К.т.н., доцент кафедры информационных систем

Киселев Владимир Евгеньевич

Белгородский государственный национальный исследовательский университет, г. Белгород
Аспирант института ИиЦТ

Список цитируемой литературы:

Последние новости

Случайный материал

  • В статье рассматриваются вопросы эффективной организации мониторинга процессов оказания электронных услуг. В качестве инструмента проведения мониторинга предлагается использовать автоматизированную систему, обеспечивающую адаптивную организацию процессов сбора, хранения и обработки данных. Сформулированы системные и технологические задачи организации мониторинга, раскрыты их сущность и принципы решения.
    Фролов Алексей Иванович, ФГБОУ ВПО «Госуниверситет – УНПК», г. Орел
  • В данной статье рассматриваются подходы к созданию подсистемы стабилизации температуры в барокамере экспериментальной системы контроля качества приборов. Данная подсистема позволяет управлять величиной тока, подаваемого на термоэлектрический модуль, для поддержания воздушной среды управляемого объекта – барокамеры в пределах заданной величины.
    Демина Юлия Александровна, ФГБОУ ВПО «Госуниверситет – УНПК», г. Орел
    Вереницын Андрей Игоревич, ФГБОУ ВПО «Госуниверситет – УНПК», г. Орел
    Демина Елена Григорьевна, ФГБОУ ВПО «Госуниверситет – УНПК», г. Орел
  • В данной статье рассматривается актуальность применения свободного программного обеспечения для оказания электронных услуг населению, а также выявляются проблемы при его внедрении и сопровождении.
    Стычук Алексей Александрович, ФГБОУ ВПО «Госуниверситет – УНПК», г. Орел
    Постников Максим Владимирович, ФГБОУ ВПО «Госуниверситет – УНПК», г. Орел