Моделирование свойств безопасности аутентификации криптографических протоколов с использованием средств формальной верификации SPIN

Резюме: Для оценки качества и безопасности криптографических протоколов применяют различные инструменты формальной верификации, к наиболее известным, относят Scyther tool, Avispa, ProVerif. Существующие формальные верификаторы могут проверять протокол на уязвимость к атакам на секретность и аутентификацию, так как это самые распространенные атаки на протоколы. Однако, этого недостаточно для полноценного анализа безопасности протокола. В статье, предлагается использовать проверку на моделях с применением линейной темпоральной логики LTL с помощью инструмента SPIN. Данный инструмент, в отличие от перечисленных выше формальных верификаторов, не создан для конкретного применения в контексте криптографических протоколов, однако, он обладает очень широким спектром возможности. В частности, для каждого свойства безопасности можно описать поведение злоумышленника и осуществить проверку на устойчивость модели протокола к различным его атакам. Цель данной работы – описание разработанной методики верификации безопасности свойств аутентификации с помощью верификатора SPIN. В работе описана проверка свойств аутентификации криптографических протоколов. Для проверки конкретного свойства моделируется некое поведение злоумышленника, которое нарушает штатное исполнение протокола. В случае, если злоумышленнику удается нарушить штатное исполнение, но на выбранной стороне протокол корректно завершается, то это свидетельствует о невыполнении свойства безопасности. В качестве примера был выбран протокол Kerberos.

Ключевые слова: Верификация; криптографические протоколы; SPIN; аутентификация; свойства безопасности.

Perevyshina E.A, Babenko L.K.

Modeling security properties of authentication of cryptographic protocols using spin formal verification

Summary: To assess the quality and security of cryptographic protocols, we use various formal verification tools, such as Scyther tool, Avispa, ProVerif. these formal verifiers can check the protocol for vulnerability to attacks on secrecy and authentication, as these are the most prevalent attacks on protocols. However, this is not enough to fully analyze the security of the protocol. In this article, we will use linear temporal logic (LTL) model checking with SPIN. This tool, unlike the formal verifiers listed above, is not designed for a specific application in the context of cryptographic protocols; however, it has a very wide range of possibilities. In particular, for each security property, it is possible to describe the behavior of an attacker and test for the stability of the protocol model to its various attacks. The purpose of this work is to describe the developed methodology for verifying the security of authentication properties using the SPIN verifier.

doi 10.34219/2078-8320-2020-11-3-21-25