Formal Verification of Cryptographic Protocols: A Survey

1995 ◽  
Author(s):  
Catherine A. Meadows
Keyword(s):  
Formal Verification ◽  
Cryptographic Protocols

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

2020 ◽  
pp. 21-25
Author(s):  
E.A. Perevyshina ◽  
L.K. Babenko
Keyword(s):  
Model Checking ◽  
Formal Verification ◽  
Temporal Logic ◽  
Cryptographic Protocols ◽  
Wide Range ◽  
Security Properties ◽  
Verification Tools ◽  
The Stability ◽  
Security Property ◽  
Ltl Model Checking

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.

scholarly journals Optimization of ProVerif programs for AKE-protocols

2021 ◽  
Vol 33 (5) ◽  
pp. 105-116
Author(s):  
Evgenii Maksimovich Vinarskii ◽  
Alexey Vasilyevich Demakov
Keyword(s):  
Formal Verification ◽  
Formal Methods ◽  
Distinctive Feature ◽  
Formal Specification ◽  
Cryptographic Protocols ◽  
Experimental Results ◽  
Automatic Verification ◽  
Cryptographic Protocol ◽  
Encryption Scheme ◽  
Program Model

Cryptographic protocols are used to establish a secure connection between “honest” agents who communicate strictly in accordance with the rules of the protocol. In order to make sure that the designed cryptographic protocol is cryptographically strong, various software tools are usually used. However, an adequate specification of a cryptographic protocol is usually presented as a set of requirements for the sequences of transmitted messages, including the format of such messages. The fulfillment of all these requirements leads to the fact that the formal specification for a real cryptographic protocol becomes cumbersome, as a result of which it is difficult to analyze it by formal methods. One of such rapidly developing tools for formal verification of cryptographic protocols is ProVerif. A distinctive feature of the ProVerif tool is that with large protocols, it often fails to analyze them, i.e. it can neither prove the security of the protocol nor refute it. In such cases, they resort either to the approximation of the problem, or to equivalent transformations of the program model in the ProVerif language, simplifying the ProVerif model. In this article, we propose a way to simplify the ProVerif specifications for AKE protocols using the El Gamal encryption scheme. Namely, we suggest equivalent transformations that allow us to construct a ProVerif specification that simplifies the analysis of the specification for the ProVerif tool. Experimental results for the Needham-Schroeder and Yahalom cryptoprotocols show that such an approach can be promising for automatic verification of real protocols.

EXPLOITING SYMMETRIES FOR TESTING EQUIVALENCE VERIFICATION IN THE SPI CALCULUS

2006 ◽  
Vol 17 (04) ◽  
pp. 815-832
Author(s):  
IVAN CIBRARIO BERTOLOTTI ◽  
LUCA DURANTE ◽  
RICCARDO SISTO ◽  
ADRIANO VALENZANO
Keyword(s):  
Formal Verification ◽  
Cryptographic Protocols ◽  
Transition System ◽  
Experimental Results ◽  
Verification Problem ◽  
Security Properties ◽  
Universal Quantification ◽  
Equivalence Verification ◽  
Testing Equivalence ◽  
Labelled Transition System

Testing equivalence is a quite powerful way of expressing security properties of cryptographic protocols, but its formal verification is a difficult task, because it is based on universal quantification over contexts. A technique based on state exploration to address this verification problem has previously been presented; it relies on an environment-sensitive labelled transition system (ES-LTS) and on symbolic term representation. This paper shows that such a technique can be enhanced by exploiting symmetries found in the ES-LTS structure. Experimental results show that the proposed enhancement can substantially reduce the size of the ES-LTS and that the technique as a whole compares favorably with respect to related work.

An approach to the formal verification of the two-party cryptographic protocols

1999 ◽  
Vol 33 (4) ◽  
pp. 48-51 ◽  
Author(s):  
Yuqing Zhang ◽  
Jihong Li ◽  
Guozhen Xiao
Keyword(s):  
Formal Verification ◽  
Cryptographic Protocols
Sign in / Sign up

Export Citation Format

Share Document