This paper presents a new mathematical model, and based on it a new automatic approach for verication of security protocols. This model contains a representation of the actions executed during the realization of the protocol, and the representation of changes of knowledge states of honest users and an Intruder. These possibilities are given to us by the formal denition (also shown in the article) of the runs representing the execution of protocols in real, open computer networks. Our model uses a simple and intuitive idea of chains of states for which the concept of protocol's properties verication has been given. This idea has been implemented, and the results presented in this article are compared with the results obtained by the use of the best verication tools.
Security protocols are a key point of safety in computer systems. In the open computer networks, especially in the systems which fulll the aims of the public key infrastructure, these concurrent algorithms are often applied during an exchange of information for, generally speaking, assuring a sucient level of security of data transmitted over networks and electronic transactions. The mutual authentication of communicating parties (users, servers) or a new session key distribution is mostly a principal task. Basically, they are most often used as vital elements of large systems, such as widely used communication protocols. Vital examples of such systems are Kerberos, SSL/TLS and Zfone. However in literature and applications, errors in the protocol’s design can be found. That is why the methods of specifying and verifying their properties are developed to nd faults which allow unwanted behavior and can lower the security level or even question it completely.
For automatic or semi-automatic verication systems of protocols, not only modeling protocol’s executions are required, but also modeling of the user’s knowledge gained during the system performance. The full and formal description of the protocol is needed as a base for a formal verication. However, the Common Language does not fulll this requirement. Hence, specifying of the internal and external protocol’s actions are required. The methodology suggested in the following sections of this paper fullls this requirement.
The same as communicating protocols there are several approaches to
verifying of time (in)dependent security protocols. We can verify the protocols
using the deductive methods (e.g., theorem proving) or algorithmic methods. The
deductive methods have been exploited in many verication systems such as:
Isabelle, TAPS, PVS, and NRL [
Intuitively, the model checking of a security protocol consists of checking if a model of the protocol accepts an execution that represents an attack upon the protocol. In comparison with the standard model checking methods for communicating protocols or for distributed systems, the main trouble is the need to model both the intruder who is responsible for generating attacks as well as changes of knowledge (about keys, nonces, etc.) of the participants.
We can dene the properties expressing correctness of security protocols as
reachability properties or in linear (branching) time temporal logic. Following the
early achievements in model checking of cryptographic protocols by the teams of
E. Clarke, C. Meadows, G. Lowe, or D. Bolignano, there has been the
state-ofthe-art verication system AVISPA [
On the other hand, verication systems for distributed and real time systems
such as SMV, Spin, KRONOS, UppAal [
In this paper we present a new idea of verication of security protocols by
using the chains for modeling separately the steps of many dierent executions
of the protocol. Thanks to that we get a very distributed representation of the
protocol executions, which is important for an ecient model checking. For the
above we use a syntax and semantics of security protocols introduced in paper
[
In the following, a method is given for representing the executions of a
security protocol (within a computational structure for a bounded number of
sessions) by the chains of states and it shows how the attacks on authentication
and security can be found.Our model allows for specication and verication
of untimed cryptographic protocols realizing the well-known challenge-response
idea. The Needham-Schroeder public key protocol [
Our model of the Intruder’s behavior follows the well known Dolev-Yao model
[
The rest of the paper is organized as follows. In the second section we show the NSPK protocol as the basic example of protocols. In the third section we introduce a formal language that allows you to intuitively describe in detail the steps of security protocols. In the next section we present a new, simple, mathematical model representing executions of protocol’s steps (introducing the Intruder). Finally, we show the experimental results for a few protocols. 2
The Needham Schroeder Public Key Protocol If we want to understand the problems of design and the practical use of protocols in this section, there is one example of them presented: the Needham Schroeder Public Key Authentication Protocol (NSPK). The protocol is written in the so called Common Language a protocol’s specication language widely used in the literature. Unfortunately, as we can see, this language does not fully describe the protocol. A scheme of sending messages during the protocol’s execution and constructing the messages is presented, i.e., the external actions of the protocol. The description of the internal actions and the other conditions of the protocol’s execution is usually written in a natural language.
Now, we show one of the protocols proposed in [
The user A initiates the protocol. The objective, which should be achieved after the protocol’s execution, is a mutual authentication of the parties A and B, i.e., the mutual conrmation of their identities. The notation A ! B : X means that the message X is transmitted from A to B. In our approach it is often assumed that sending information implies its receipt by the receiver. The notation X Y means concatenation of X and Y .
Example 1. The paper [
NBiKA ; 3 A ! B : hNBiKB : In the rst step of the protocol, the user A generates its random number NA and sends it together with its identier i(A) to B, encrypting everything with the public key belonging to B. In the second step, B generates its own number NB and encrypts it together with the obtained number NA with A’s public key.
Then, B sends the so prepared ciphertext to A, which can decrypt it, A compares the number received from B with its nonce NA and at this moment A acknowledges B to be authenticated, since B sent to A the nonce NA. A encrypts this number with B’s public key and sends it to B. B decrypts the ciphertext (only it is able to do that) and compares the number sent by A with its own NB. At this moment A is authenticated by B. Due to the structure of transferring the data used in the protocol and properties of the asymmetric cryptography, the users A and B should be sure of their identity after executing the protocol.
A very interesting and instructive history of this protocol has been shown
and used in practice in its original version for 17 years. However, in 1995 it
turned out that the protocol can be broken. Gavin Lowe presented an attack
upon the protocol in [
A security protocol can be described intuitively without a formal denition. There is one of the common methods to write such a protocol in the so-called (2) (3) Common Language, in which there are external protocol’s actions and this is the scheme of sending messages. Unfortunately this is not a complete description of the protocol, since it is necessary to add the information about the internal actions such as generating new condential information or the process of the message encryption/decryption. A formal denition which provides all the information about the protocol can be found in the papers [1820]. In these works the protocol is dened as an abstract object (algorithm) and is diered from the execution. The executions of the protocol are certain substitutions of the abstract protocol in a dened structure which reects the actual work of the network [1820]. Note that in such approach we can also consider the execution, which cannot be done alone (see Example 3). Such execution is treated as the hypothetical execution that may be made as parts of the interleaves of several executions which are assembled as the attack. In this paper we use intuitively described executions of the protocol as these substitutions.
Example 3. We consider previously discussed Needham Schroeder protocol. Below there are two dierent hypothetical executions. In the rst one, the honest users B and A communicate with each other. In the second: the user A communicates with the Intruder who impersonates the user B. Such behavior of the Intruder is marked by (B).
Note that the second execution cannot be done alone. However, it can be considered as a potential part of the interleave of several executions are assembled as the attack (see Example 2).
13 = B ! A : hNB i(B)iKA ; 23 = A ! B : hNB NAiKB ; 33 = B ! A : hNAiKA ; 14 = A ! (B) : hNA i(A)iKB ; 24 = (B) ! A : hNA N iKA ; 34 = A ! (B) : hN iKB : The basic notations used in the following part of the paper are given below. We begin with dening the following sets:
P = fP1; P2; : : : ; PnP g - a set of the honest participants in the network, P = f ; (P1); (P2); : : : ; (PnP )g - a set of the dishonest participants containing the Intruder and the Intruder impersonating the participant Pi for 1 i nP , I = fi(P1); : : : ; i(PnP ); i g - a set of the identiers of the participants in the network, K = SnP
i=1fKPi ; KPi1g [ fK ; K 1g - a set of the public and private cryptographic keys (already existing or possible to be generated) of the participants, N = SiN=P1fNP1i ; : : : ; NPkiN g [ fN 1; : : : ; N kN g - a set of the nonces1.
By the set of letters L we mean the smallest set fullling the following conditions:
L, 1 As before, we assume that NP and KN are some xed natural numbers. For simplicity, we take the same number of nonces for each user.
The same as in the papers [
In this way we can describe any number of executions of the tested protocol.
During the verication the considered space is limited to two honest users and
the Intruder (more information can be obtained in [
The intuition of the following denition is as follows: constructed runs correspond with dierent true interleaves of the protocol. Due to the fact that in reality, the ability to execute the steps of the protocol is dependent on the knowledge of the individual members in order to dene the conditions which enable to construct the necessary runs, the knowledge of the users will be needed during the execution of the protocol.
Consider the following nite sequence of the execution of the protocol’s steps: R = ki11 ; ki22 ; ki33 ; : : : ; kiss , where in denoting a step the superscript indicates the number of execution, and the subscript indicates the number of the step in the given execution.
Example 5. If we consider the two dierent executions of the same protocol, wRh=ich 11c;ons21i;st 12o;f t31h;re22e; st32e.pOs,bse11r;ve21t;ha31t ainndsuch12;se22q;ue32n,cetsheitpisosnseibcelesssaerqyuteonckeeeips: the chronology of the execution of each step, i.e., no step of the execution can be found in the sequence before the preceding step in the protocol. For each such sequence R we dene the set sequence of the knowledge of users who take part in the executions which constitute the R. The initiators of given steps are denoted by Send( ), and the recipients of the information sent during the step’s execution by Rec( ). Denote by U the set of all the users involved in the steps which constitute the sequence R.
We have: U = Sj=1;:::;sfSend( kijj )g [ Sj=1;:::;sfRec( kijj )g. Assume that each user has a basic knowledge and it means that the user knows his own encryption keys (public and private), user IDs and public keys of the users.
In the following denition we will use the operator ,2 that means to acquire the knowledge of the encrypted messages. This acquisition is of course dependent on the possession of the appropriate encryption keys.
Next denition models the knowledge of the users during the execution of the protocol’s steps, taking into account the increase of the knowledge through the messages and their contents (if the user has the appropriate encryption keys for the decryption) and the generated information. Dened sequences are the ascending sequences.
Consider any j = 1; : : : s 1 for any sequence R = ki11 ; ki22 ; ki33 ; : : : ; kiss . For every user p 2 P we have Knowp1 = SnP
s=1fi(Ps); KPs g [ f ; K ; Kp 1g and: 8> Knowpj [ Gen( kijj++11 ) > > > > Knowpj+1 = < (Knowpj [ fM ess( kijj++11 ))g) if if p = Send( kijj++11 ), p = Resp( kijj++11 ), > > > > >: Knowpj othervise.
Denition 1. By the run we call any nite sequence of the steps of protocol’s executions which fullls the following conditions: r = ki11 ; ki22 ; ki33 ; : : : ; kiss that meets the following conditions: 1. 8j=1;:::;s[kj = 1 _ 9t<j(it = ij ^ kt = kj 1)]; 2. 8j=2;:::;s[Know( kijj ) KnowSjen1d( ikjj ) [ Gen( kijj ))].
The rst condition denes the appropriate dependence between the subsequent steps of the same execution of the protocol which are in the given run. The second condition ensures the proper dependence between the knowledge of the users who send messages in the next steps - parts of the run.
This denition allows to express the actual interleaves of dierent protocol’s execution which reects the actual executions. For such runs in the xed base space we dene the chains encoding below. 4
Chains of states representing executions of protocol’s
steps
In the paper [
Now, we introduce a new mathematical model of the protocol’s executions.
The double translation of the mathematical model of executions proposed in [
In the proposed model, we code each step of every execution of a protocol as a simple chain of the states representing individual actions carried out during the step, or the conditions for making them possible.
We distinguish four types of states: 1. states representing the execution of steps, those will be labeled Sji to mark the execution of i-th step in the j-th execution, 2. states representing the generation of new condential information by users (nonces, keys) labeled onwards e.g. GANA (nonce NA generated by user A ), 3. states representing the obtaining of knowledge by receivers of steps of protocol KAX - user A acquired message X, 4. states representing the requirement of possessing a given knowledge element necessary for executing a given step described as e.g. PAX (- user A has to possess knowledge of element X in order to carry out a given step).
As you can easily notice, for execution of NSPK gave in Example 1 we have the three following communication states: S1; S21; S31. We present the chains of the 1 states representing the executions of individual steps of the discussed protocol below: 11 = (GANA ; S11; KBNA ); 21 = (PBNA ; GBNB ; S21; KANB ); 31 = (PANB ; S31): (4) The set of the states preceding the state corresponding with the execution of the steps S will be marked hereinafter by P reCond(S). Accordingly, by using P ostCond(S) we will mark the set of the states found in the sequence after the state S. Taking into consideration the above, we can model the execution of the protocol NSPK as the following sequence of the states.
N SP K =
11; 21; 31 = (GANA ; S11; KBNA ; PBNA ; GBNB ; S21; KANB ; PANB ; S31): (5)
P reCond(S21) = fPBNA ; GBNB g and P ostCond(S21) = fKANB g. 4.1
Infrastructure with Intruder The denitions introduced in the third section do not include the presence of the Intruder in the network. As we wrote in the introduction we can consider its various models. In this paper we explore some version of the Dolev-Yao model, so we assume that there is only one Intruder, who actively tries to deceive the others by executing the protocols against their assumptions. The Intruder may use any information obtained from a network, and impersonate other users. Note that the Intruder can compose sent messages contrary to the assumptions of the protocol. This can be done in many ways. Consider the following example. Example 6. If the sent message is ciphertext hNAiKA hNBiKB , the message can be composed in ve ways. In each case the Intruder can compose and use during the execution of the protocol the message: X1 = fhNAiKA hNBiKB g, X2 = fhNAiKA ; hNBiKB g, X3 = fNA; KA; hNBiKB g, X4 = fhNAiKA ; NB; KBg, X5 = fNA; KA; NB; KBg. In each case the Intruder can compose and use during the execution of the protocol the message hNAiKA ; hNBiKB . The fact, that from a given set X a message M can be composed, is denoted by X ` M .3 To express this we need to slightly modify the denition of the execution of protocol’s step where the initiator of this step is an Intruder. In the denition of the execution’s step we introduce the following change: Denition 2. If Send( ) = ; then
= ( ; Q; M; ;; fX j X ` M g).
In the case of a given execution of the protocol’s step, the Intruder is the sending message party (Send( kijj ) 2 P ) we have to adapt the knowledge condition of the run denition in the following manner. If Know( kijj ) = fX j X ` M ess( kijj )g, then, the Condition 2 of the denition 1 takes the form:: 9X2Know( ikjj )[X
Send( ikjj ) [ Gen( kijj )]:
Knowj 1 This condition says that in order to execute each step and send a message to the Intruder it is enough to compose a sent message in one of the possible ways.
The corresponding chains for the Example 2 take the following form: 11 = (GANA ; S11; KNA ); 31 = (PANB ; S31; KNB ); 21 = (P hNA NBiKA ; S21; KANB ); 32 = (P NB ; S32): 12 = (P NA ; S12; KBNA ); 22 = (PBNA ; GBNB ; S22; KhNA NBiKA ); 4.2
Correct chains of states and new approach for verication Now we proceed to dene the sequences consisting of the states dened above that represent true executions of the protocols in the computer networks. This denition will refer to the denition of the runs of the third section.
Let be the base space consisting of the users and their attributes (identiers, nonces, cryptographic keys, etc..). We have to consider all the executions of the protocol in this space and all state’s chains for all executions. Under the set of all these chains we dene a correct chain of states that represents the real executions of the protocol in the network.
Denition 3. We call the sequence of the protocol’s states: s = s1; s2; : : : a correct chain of states i the following conditions holds:
1. if si = Sjk for some j; k then j = 1 _ 9t<i(st = Sjk 1) and
P reCond(Sjk) fs1; : : : ; si 1g ^ P ostCond(Sjk) 2. if si = GUX , then 8t6=i(st 6= GUX ), 3. if si = PUX , then 9t<i(st = GUX _ st = KUX ). fsi+1; : : :g, As you can see the denition of the considered chains is based on the denition of runs.
The rst point guarantees a suitable dependence of the order of carrying out the individual steps of a given execution. Points 2 and 3 guarantee a proper dependence of the users’ knowledge necessary to execute the individual steps.
Our new proposed concept of verication is as follows. The input data consists of the generated set of chains representing the steps of the executions in the given, investigated space of executions. On an empty stack we rstly put a chain that represents one of the initial steps of executions (chains inserted into stack are labeled as explored). Next we build the limited tree of chains by adding only those unused chains conditions of which match the conditions introduced in Denition 3. Simultaneous creating and searching through the tree ends up in two cases. Firstly if we nd the path of the attack, which is derived to the output. Secondly if we utilize chains, then we return the output information about the lack of the attack. Although the time complexity of the algorithm is exponential due to the number of executions and steps, we have obtained very good experimental results as the constructed chains are very short. The space complexity is linear due to the parameters mentioned above. As the results presented below show, it seems that currently the presented approach is one of the most ecient. 5
To the verication we have modeled and veried three protocols: NSPK, NSPKL,
and the untimed version of the WMF Protocol. The experimental results
obtained by us are very promising. In all cases, the times of the encoding as well
as of the direct verication of the obtained model are smaller than 1 ms. The
attention needs to be drawn to the fact that the hitherto methods dealt
differently with the verication of the secure and unsecured protocols. In most
cases the verication of the secure protocols are quicker. In the case of the
VerICS tool [
In the published results, a division of the times of the verication into the encoding time and the time of the direct verication of the encoded model is performed. The best results of verication with the AVISPA tool (graph planning) are close to zero (less than 10 ms). However, in the process of the automatic verication the coding time needs to be noted as well. In this case, the times are approximately several-several hundred milliseconds.
We have compared our results to the best ones known to us obtained from
the AVISPA ([
Obviously, many more experiments need to be carried out to fully compare our method with the AVISPA, VerICS or the other tools. The research in this area is still in the making, and in the near future we expect the results for other protocols, and the optimization of our method as well as the implementation.
The computer used to perform the experiments was equipped with the processor Intel Pentium D (3000 MHz), 2 GB main memory, and the operating system Linux. In the table, we marked the time of the model’s encoding with the EnT. The SolT stands for the time of its direct verication. The NA means we do not have the access to the verication times of the protocol. All the times shown below are expressed in milliseconds.
NSPK NSPKLowe UnT_WMF
EnT (ms) SolT (ms) EnT (ms) SolT (ms) EnT (ms) SolT (ms) 90 <10 <1 36 <1 <1 90 <10 <1 960 <1 <1
NA NA <1 32 <1 <1 In the article, we have presented a new ecient approach for the security protocols properties’ verication, based on the structures of chains describing actions carried out by participants of protocols, as well as changes of their states of knowledge. The method has been implemented. The obtained results are very promising: the method for protocols NSPK, NSPKL as well as the untimed version of WMF Protocol gives better results than the known verication tools: the AVISPA and VerICS. A research on further optimization of the method and its implementation, as well as its application for other protocols is in progress. Also, the adaptation of the method for time dependent protocols has been planned.