Cryptographic protocols are the core of any protected system. With the help of them, data are transmitted that need protection from third parties. The paper examines the features of analyzing the security of cryptographic pro-tocols using various modern veri cation tools. Basic veri cation goals, such as party authentication, data con dentiality, integrity control, have been set. A simpli ed cryptographic protocol of electronic voting based on blind intermediaries is described. Presentday e ective means of veri cation of Avispa, SPIN are presented. The voting protocol in the CAS + language is described in the Avispa tool, the veri cation objectives in the form of data secrecy and authentication of the parties are indicated, the scheme of the transmitted data is shown in the presence of an attacker. The protocol of voting in the language Promela in the tool SPIN is described, veri cation objectives in the form of authentication and veri cation of the correct completion of the protocol are established in the presence of an active attack by the attacker. The analysis of the protocol's safety with the help of the given means of veri cation was carried out. The possibilities and limitations of each tool are shown when verifying compliance with veri cation objectives. Recommendations on the use of each of the means are given.
The security of secure systems directly depends on the quality of the cryptographic protocols used in them. Various veri ers are used to analyze the security of protocols. In this paper, the most popular veri er Avispa [Avi06], speci cally designed for security analysis of cryptographic protocols, and the more versatile tool SPIN [Ben08] are considered. However, it is not always possible to produce a full analysis of the protocol using one of the veri ers provided. Each of the presented tools has its own peculiarities and is used depending on the chosen veri cation objectives. Thus, the goal of this paper is to identify the features of the protocol safety analysis using the veri cation tools provided and to make recommendations on the use of each of them. Copyright c by the paper's authors. Copying permitted for private and academic purposes.
When analyzing the security of cryptographic protocols, the use of the Dolev-Yao threat model is assumed [Dol83]. This involves the presence of an attacker who can monitor the data transfer between the parties, block it, intercept and modify all messages. The protocol must be resistant to this kind of attacker and ensure the secrecy, authenticity and integrity of the data. Thus, the goals of veri cation of the security of cryptographic protocols are:
2. Integrity of transmitted data 3. Authentication of the parties
The purpose of the con dentiality of the transmitted data is set so that the attacker can not know the contents of the transmitted data between the legal parties. To achieve these goals, asymmetric and symmetric encryption is used, depending on the type of data. Typically, asymmetric ciphers are used to transfer a small amount of data, such as keys for other ciphers, identi ers, random numbers, since asymmetric encryption is limited by the smallest bit of the cipher itself. Symmetric ciphers are used to encrypt a large amount of data, but unlike asymmetric ciphers using a public key for encryption and secret for decryption, a common secret key is used. This makes it necessary to use a pre-shared secret encryption key, or to generate it using the protocols for generating a common session key, such as Di e-Hellman.
The purpose of the integrity of the transmitted data is to ensure that the attacker can not modify the data transmitted between the legal parties. If an integrity violation is detected, either a repeated data request or the end of the current session is performed. To ensure the integrity of the data, the authentication codes of the MAC message, which are one of the symmetric cipher encryption modes, HMAC (hash-based message authentication code), the mechanism for exchanging data using a private key and hash functions, signature with a secret key and signature veri cation with using the public key of the asymmetric cipher.
The purpose of party authentication is to ensure that the parties are con dent that they are interacting in the current session that the messages contain data of the present time and the parties are sure that they communicate with each other. To ensure authentication, a request-response scheme can be used in which one side sends a random number to the other party and the other party in the response message sends the same number or some function performed on this number and which the original side knows. One of the types of authentication attacks is replay-attack [Syv94]. It consists in reusing the previously transmitted legal message. To prevent this, you can use both random numbers in conjunction with the regeneration of the session interaction keys at the beginning of each session, and the use of timestamps in the message. 3
As a protocol for veri cation, a simpli ed e-voting protocol is used, the extended version of which is used in the electronic voting system based on blind intermediaries [Bab17].Any connection between the client and the component begins with the initialization of the session key. All transmitted data between the parties is encrypted with a symmetric AES cipher, in the CBC mode with 128 bits IV (initialization vector) and HMAC-SHA256 256 bits with a 128 bit key for integrity checking control. The key of the session is the combination of [key, IV, HMAC key], its total length is 512 bits. The session key is generated using the Di e-Hellman protocol on elliptical curves using ephemeral keys and signing the secret parts.
(1) A -> B: \Hello" (2) B -> A: DHB, SignBsk(DHB), B Certi cate (3) A: veri es the certi cate and signature (4) A -> B: DHA (5) Both parties generate a key k for symmetric encryption
It is important that two components authenticate each other, so both of them make the secret part signatures. When connecting to the user, it is important only to authenticate the server, so the signature is required only from the server. Denote ECDHE (A, B) = k as generating the session key k via the Di e-Hellman protocol between parties A and B. When voting, the following protocol is used, based on the principle of blind intermediaries [Bab17], simpli ed scheme of which shown in Figure 1. It provides the ability to authenticate the user on his personal data while preserving the anonymity of the vote. E-voting protocol: (1) ECDHE (V, AS) = vas; (2) ECDHE (V, VS) = vvs; (3) ECDHE (AS, VS) = asvs; (4) AS-> V: Evas(Nas), HMAC1 (5) VS-> V: Evvs(Nb,Nvs), HMAC2 (6) VS -> AS: Easvs(Nasvs), HMAC3 (7) V -> AS: Evas (Nas, authData, Evvs(Nvs, vote), HMAC4), HMAC5 (8) AS-> VS: Easvs (Nasvs, Evvs(Nvs, vote), HMAC4)), HMAC6
Nb is N blinded (number of blinding), a non-random random number, which is regenerated each time. It is introduced in order to add some data before the semantic random number for making full search more complicated (in particular, it is necessary to select two encryption keys for message 7 in order to nd authData). Session keys are generated by (1)-(3). Randomly generated random numbers are sent as shown in (4)-(6) to authenticate the parties and to enhance the sparseness of subsequent data in the message when CBC encryption mode is applied. HMAC-SHA256 with a 128-bit key is used for integrity monitoring of all transmitted messages. The message (7) uses the principle of blind intermediaries [Bab17]. The voter encrypts his vote vote on the session key with VS, applies his personal data to the ciphertext, and encrypts it on the session key with AS. AS hashes the sent personal data, searches for the hash in the database and, and, if detected, redirects the message to the VS component. VS memorizes the vote. 4
Avispa is a tool for automated security analysis of cryptographic protocols [Avi06]. With the help of Avispa, in the context of the developed protocols, it is possible to verify: the authentication of the parties, the secrecy of data and protection against replay attacks. The possibility of veri cation of integrity when using the HMAC mechanism is not provided. The protocol will be analyzed after the phase of development of the common session key between the parties. The protocol will be described in the CAS + [Sai11] language, then translated using the Avispa translator into HLPSL [Ohe05]. The instrument allows veri cation in one of 4 modes: OFMC [Bas05], ATSE [Tur06], SATMC [Arm04], TA4SP [Glo06]. The CAS + language is quite simple and allows you to quickly describe your protocol. However, Avispa works with the HLPSL language, which is more complicated. When translating a description to CAS + in HLPSL, errors may occur that need to be corrected manually. The description of the protocol in CAS + is given below. 1 p r o t o c o l EVoting ; 2 i d e n t i f i e r s 3 V, AS , VS : u s e r ; 4 Nas , Nvs , Nasvs , AuthData , Vote : number ; 5 Kvas , Kvvs , Kasvs : s y m m e t r i c k e y ; 6 7 m e s s a g e s 8 1 . VS > V
: fNvsgKvvs
In the area (2) - (5) are indicated the role sides, encryption keys, data. In the area (7) - (12) is described the
transfer of messages between roles, what data is transmitted and on which key are encrypted. In the area (14)
(
Thus, the Avispa tool allows you to check the protocol for attacks on privacy and authentication, including the presence of replay-attack. The description of the protocols can be performed in a very simple CAS + language, but it still requires translation into HLPSL, which is more complicated. To detect attacks, you must manually assign scan targets for each element of the cryptographic protocol, such as a random number or a transmitted identi er. This tool can be used for initial analysis of the cryptographic protocol and allows to detect typical attacks with the subsequent study of the graphical representation of the data transmitted between the parties. 5
SPIN (Simple Promela Interpreter) [Hol03] is a formal veri er for multithreaded systems, using model checking and linear temporal logic. To be able to verify, it is necessary to describe your model in the special language Promela (PROcess MEta LAnguage), set the veri cation variables that must change depending on the progress of the model execution, specify the veri cation objectives using the LTL formula associated with the veri cation variables. The main structural units for modeling are the channels, processes, data transferred and the LTL formula.
LTL [Ger95] is an extended condition in which, in addition to the classical operators, and, or, time operators are not added. Thus, it is possible to make a more extensive condition for testing the model, which will take into account di erent points in time. The complete list of operators is given below.
Unlike other tools, SPIN has not been sharpened for security analysis of cryptographic protocols. There are no concepts of encryption, roles, knowledge of a certain role. Processes are the main units of interaction. It is processes that can be considered roles. Processes can interact through channels into which one process can put information, and the other can take. Thus, to verify the security of the protocols, you rst need to model your protocol, the cryptographic functions used in it. Since this tool is not tied to any context of checks, it is possible to create your own more extensive checks. For example, you can check the values of HMAC, which in other tools is not possible, conduct an active attack on the substitution of data and look at the change in the course of the protocol. It is also possible to check various situations of non-public execution of the protocol, for example, if the message integrity is violated, check the session break or reconnect. A simpli ed e-voting protocol has been simulated to detect authentication attacks and verify that the connection is complete when an authentication random number is substituted. The description of the protocol in the Promela language is given below. mtype Nasvs , authData , Nvs , Vote , Nb , NasRet ; / mtype Nas ; / Know / / mtype Vote , NvsRet , NasvsRet ; / mtype Nasvs , Nvs , Nb ; / Know /
/ vas ? NasRet , authData , Nvs , Vote , 0 ; atomic f Get1 ( NasRet , Nas ) ; i f : : NasRet == Nas > a s v s ! Nasvs , Nvs , Vote , 0 ; : : e l s e f i
The line (1) denotes the types of data used. In the lines (3) - (6), a macro is de ned, which are located at
the message transfer points to verify the correctness of the authentication. In the lines (8) - (10) the channels
for interaction of the sides are indicated. 3 channels for interaction of V-VS, AS-VS, V-AS are de ned. In line
(12), the error ag is shown. Further, a process is de ned that can be considered as roles for the client, the
authentication server, and the voting server. In each of the processes, the original knowledge of the party, the
order and the data itself transferred between the parties are described and a macro is also speci ed to verify
the correctness of the returned random number Nas. Also, after the macros, the checks of the returned random
numbers are indicated. If the veri cation fails, the protocol is terminated. The following describes an attacker
who replaces the value of Nas to commit an attack on the authentication of the parties. In lines (74) - (82), the
starting point init is speci ed, in which the processes are indicated. The line (84) speci es the macro for the LTL
formula, which is the error ag. In lines (86) - (
However, this is laborious process, since it is necessary to correctly create the model, including the model of the attacker, to identify the critical locations of the model in which it is necessary to verify certain requirements and compile an LTL formula according to which the model will be veri ed. Also, after veri cation, it is necessary to correctly interpret the graphical results to determine the errors. This tool can be used for the nal analysis of the cryptographic protocol, allows to detect atypical errors according to the established requirements. 6
In the course of the work, the veri ers Avispa, SPIN were considered. Basic veri cation goals, such as party authentication, data con dentiality, integrity control, have been set. A simpli ed cryptographic protocol of electronic voting based on blind intermediaries is described. The means of veri cation of Avispa, SPIN are described. The analysis of the protocol's safety with the help of the given means of veri cation was carried out. It is established that for the primary and rapid analysis for the presence of attacks on authentication and secrecy, the Avispa tool is suitable. It allows you to simply describe the protocol in a special language and verify the cryptographic protocols. For the nal analysis of the protocol, the SPIN tool can be used, with the help of which, according to the established checking rules and the created protocol model, it is possible to check more exact requirements, for example, the case of a correct completion of the protocol, after an attack by the intruder. Acknowledgements The work was supported by the Ministry of Education and Science of the Russian Federation, grant No 2.6264.2017/8.9. [Avi06] The AVISPA team. The High Level Protocol Speci cation Language. http://www.avispa-project.org/, 2006. [Ben08] M. Ben-Ari. Principles of Spin. Springer, Verlag, 2008. [Dol83] D. Dolev, A. C. Yao. On the security of public key protocols. IEEE Transactions on Information Theory, 1983. IT-29: 198{208, doi:10.1109/tit.1983.1056650