# Using Backward Induction Techniques in (Timed) Security Protocols Verification

Mirosław Kurkowski, Olga Siedlecka-Lamch, Pawel Dudek

► To cite this version:

Mirosław Kurkowski, Olga Siedlecka-Lamch, Pawel Dudek. Using Backward Induction Techniques in (Timed) Security Protocols Verification. 12th International Conference on Information Systems and Industrial Management (CISIM), Sep 2013, Krakow, Poland. pp.265-276, 10.1007/978-3-642-40925-7_25 . hal-01496073

HAL Id: hal-01496073

https://inria.hal.science/hal-01496073

Submitted on 27 Mar 2017

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Using Backward Induction Techniques in (Timed) Security Protocols Verification ★

Mirosław Kurkowski, Olga Siedlecka-Lamch, and Paweł Dudek

Institute of Computer and Information Sciences
Częstochowa University of Technology,
Dąbrowskiego 73, 42-201 Częstochowa, POLAND
mkurkowski@icis.pcz.pl, olga.siedlecka@icis.pcz.pl, pdudek@icis.pcz.pl

**Abstract.** This paper shows a new way of automatic verification of properties of untimed and timed security protocols. To do this we use a modified version of previously introduced formal model based on a network of synchronized (timed) automata that expresses behaviour and distributed knowledge of users during protocol executions. In our new approach we will use the backward induction method for searching of a tree of all real executions of an investigated protocol. Our approach uses additionally the boolean encoding of constructed structures and SAT solvers for searching answers to the questions about investigated properties which are expressed as reachability or unreachability of undesired states in a considered model. We exemplify all our notions and formalisms on the well known NSPK, and show experimental results for checking authentication and security properties of a few untimed and timed protocols.

**Keywords:** Security Protocols Verification, Backward Induction

## 1 Introduction

The modern people process tens of gigabytes of information a day, most of which is transferred electronically. "Consumption" of information is a must, it gives people the knowledge, capabilities, and does not allow to fall outside the margins of society. The transfer of information must remain undisturbed, consistent with reality and not threatened by outside intruders. Such communication should be guaranteed by a number of communication protocols, secured by modern cryptographic techniques. The heart of every communication protocol is a security protocol that meets the following requirements: mutual authentication of communicating entities, confidentiality of transmitted information, integrity of this information and a new key-session distribution.

Security protocols used in practice satisfy one or more of the above requirements using either symmetric or asymmetric cryptography. Many of the developed security protocols proved to be vulnerable to the attack by malicious Intruders [21, 22], and investigators undertook the challenge of formal methods of protocol verification.

<footnote>* The second and the third author acknowledge support from EU Project (European Social Fund.) PO KL Information technologies: Research and their interdisciplinary applications, Agreement UDA***/**-**/*POKL.04.01.01-00-051/10-00.</footnote>
The process of creating the protocol is difficult, but it seems more difficult to ver-
ify. The first step is to create a valid, full formal description. The description should
include all parties, states and actions occurring in the protocol: participants (sender and
receiver), the information about keys that encrypt the transmitted data, actions of gen-
erating, encoding, sending, receiving and decrypting information. The Common Lan-
guage is a commonly used protocol specification language, which unfortunately does
not allow for a full description. It shows only the scheme of sending messages and their
construction. In this case there is a need for using more complicated languages, for
example presented in the papers [12, 15, 16, 17].

The precisely specified protocol can be automatically verified in many possible
ways. The field of automatic verification has been exploited for many years by both
academic and commercial institutions. Basically, there are two main ways of verifica-
tion: testing real and virtual systems (simulations), or modeling and formal verification.
Of course after testing the already implemented systems, we can be sure that the sys-
tem has worked properly only so far. Formal modeling and verification is based on
building adequate mathematical structures, showing the actions that occur during the
protocol execution. Of course these methods are successfully used to model and verify
various kinds of computer systems. Good examples are [11, 16]. There are numerous
approaches to the verification of security protocols associated sometimes with appro-
priate tools [1, 2, 13, 8, 11, 14].

The algorithmic approach is based predominantly on model checking, but we can
distinguish among formal methods also those inductive [26, 4] or deductive [16, 6, 20].
Intuitively, model checking of a protocol proceeds in checking whether a formal model
of protocol executions contains an execution or a reachable state that represents an at-
tack upon the protocol. Comparing to standard model checking techniques for commu-
nication protocols or for distributed systems, the main difficulty is caused by the need
to model the Intruder which is responsible for generating attacks as well as changes of
knowledge (about keys, nonces, etc.) of the participants. The Intruder can be modeled
in several ways, although the Dolev-Yao model and its versions seems to be the most
adequate [10]. In mentioned model the Intruder has access to all the transmitted infor-
mation, can collect and use it with a precision according to its skills and resources, and
is able to send it somehow and sometime through the network. Of course, the Intruder
does not need to comply with the requirements of using the protocols and, in particular,
does not have to use fresh information or to meet time requirements.

Using model checking we face another serious problem - the exponential explo-
sion of states, which depends on the number of participants, sessions, or messages. The
model should predict all possible scenarios with a huge amount of information gen-
erated and sent by the Intruder. In considered case the computational complexity of
model checking algorithms is typically exponential in parameters of the verified proto-
cols, particularly in the number of participants and execution steps. This problem calls
for the modification of existing models and algorithms, as well as finding new ones.

So far, our studies in this area were directed at the two models: a network of syn-
chronized automata for modeling separately the executions of a protocol and the knowl-
edge of the participants like in [19, 18, 17] or using the chains of states of protocol exe-
cution, see [27]. In the first case, the constructed networks of automata were translated
to the propositional boolean formulas. The security property was firstly expressed as a property of reachability of certain global states in the automata network, and subsequently as a satisfiability of the formula. SAT-solver answered the question whether satisfying valuation exists, which was equivalent to the existence of an attack or an undesirable situation. By contrast, if the formula turned out to be unsatisfiable, it meant that no attack exists.

For the searching of models of executions of concurrent systems, the backward induction technique is sometimes used. Generally speaking the method consists in constructing a tree of executions in accordance to the reversed relation to that which determines the dependence between the states in the basic model. In some situations, for example in the case of testing the reachability of certain states, this causes the reduction of size of the constructed trees. In the case of protocols this approach was successfully used in a few works, for example in [15].

In this article we propose the approach of the backward induction technique for the investigation of properties of protocols by building a network of automata encoding the tree of protocol execution, where the runs take place inversely to the runs proposed in [19, 18, 17]. The automata built in this approach are slightly bigger in size, which is why the experimental results confirm greater efficiency of the proposed approach in the case of protocols with a small number of steps. It is interesting that this method may also be used in the case of time-dependent protocols, and the networks of time automata which model them.

## 2 The Needham-Schroeder Public Key Protocol

The designing of the communication protocols is a very hard task which is connected with the possibility of appearing many problems with later use of a made protocol. As the essential example the NSPK protocol can be presented [25].

In the notation of this protocol there are designations $i(A)$ and $i(B)$, which express identifiers of the participants of the communication, respectively the A and B participants. The expression $\langle X \rangle_{K_A}$ means the X message encrypted by the public key of A participant. Similarly, the message encrypted by the public key of B participant - $\langle X \rangle_{K_B}$.

The A participant has a very important role – starts the run of the protocol. The aim of the execution of this protocol is to achieve the mutual confirmation of the identity (the authentication) between the communicating participants. The designation $A \to B : X$ refers to sending the X message from the A participant to B participant. We assume that sending the message causes the operation of receiving it by the suitable person. The concatenation of the elements in the message was determined by the operator “.”.

*Example 1.* The scheme of NSPK protocol proposed in [25] is as follows:

$$ \alpha_1 \quad A \to B : \langle N_A \cdot i(A) \rangle_{K_B}, $$

$$ \alpha_2 \quad B \to A : \langle N_A \cdot N_B \rangle_{K_A}, $$

$$ \alpha_3 \quad A \to B : \langle N_B \rangle_{K_B}. $$

The A participant in first step of the protocol execution generates the random number (nonce) $N_A$ and sends it to the B participant with A's identifier encrypted by the public key of the B user. The next step of protocol execution starts from generating by
the *B* participant its own random number *N*<sub>B</sub>. Next it creates the message consisting of random numbers of both communicating participants, encrypts this message by the public key of the *A* participant and sends it to the *A*. In the next stage of the execution, *A* runs decrypting operation of the received message and the operation of comparing the *N*<sub>A</sub> number, which got from *B* with the number *N*<sub>A</sub>, which was prepared by him. If both numbers are equal, *A* considers *B* as authenticated. In the last step of the protocol execution *A* sends to *B* its random number *N*<sub>B</sub> encrypted by the *K*<sub>B</sub> key. After decrypting and comparing the proper numbers, the *B* participant can consider the *A* participant as authenticated. This protocol execution should guarantee both participants the identity of the communicating persons.

*Example 2.* Figure 1 presents the automata based model of honest execution of NSPK Protocol due to formal definitions from [19, 18, 17]. In the presented networks synchronisation of component automata is used, it consists in the fact that the global transition (in the network) labeled by the label $\alpha$ is enabled, if in all components if there exists transitions labeled by $\alpha$, then at least one of them in each automaton is enabled. It is assumed further that all states are accepting ones. As it can be seen the model consists of automata modeling the execution of external actions of the protocol (sending messages) $\mathcal{A}$ and automata that model distributed knowledge of participants ($\mathcal{A}_{N_A}^A, \mathcal{A}_{N_B}^A, \mathcal{A}_{N_A}^B, \mathcal{A}_{N_B}^B$). For example, the automaton $\mathcal{A}_{N_A}^A$ models the knowledge of the user *A* about the random number $N_A$. Executions of additional actions constituting the protocol are represented by labels on automata transitions. Transitions labeled by $\alpha_1$ model execution of the first step of the protocol. During execution of that step, users *A* and *B* acquire knowledge about the number $N_A$. Transitions labeled $\alpha_2$ model the performance of the second action of the protocol, in which users gain knowledge about the number $N_B$. We should pay attention on the loop in automata $\mathcal{A}_{N_A}^B$, labeled also by $\alpha_2$, it models the condition to possess knowledge about number $N_A$ by *B*, to execute the second step of the protocol. Accordingly, the transitions labeled $\alpha_3$, model the execution of the third step of the protocol.

<figure><img src="image_2.png" /><figcaption>**Fig. 1.** Automata model of execution of the NSPK Protocol</figcaption></figure>

The NSPK protocol was used through 17 years. In 1995 Gavin Lowe discovered the version of the protocol execution which consisted a possible attack, showing that the
NSPK protocol is susceptible to a break-in [21]. The Intruder is the additional participant with its own identifier and the keys, determined by $\iota$ symbol. The Intruder does not do the protocol according to the scheme but uses own ways, impersonates other users and cheats them.

*Example 3.* The attack presented by Gavin Lowe is as follows:

$$ 
\begin{align*}
\alpha_1^1 A &\to \iota : \langle N_A \cdot i(A) \rangle_{K_i}, \\
\alpha_1^2 \iota(A) &\to B : \langle N_A \cdot i(A) \rangle_{K_B}, \\
\alpha_2^2 B &\to \iota(A) : \langle N_A \cdot N_B \rangle_{K_A}, \\
\alpha_2^1 \iota &\to A : \langle N_A \cdot N_B \rangle_{K_A}, \\
\alpha_3^1 A &\to \iota : \langle N_B \rangle_{K_i}, \\
\alpha_3^2 \iota(A) &\to B : \langle N_B \rangle_{K_B}.
\end{align*}
$$

The Lowe scheme shows two simultaneously NSPK protocol executions. The $\alpha^1$ execution refers to the communication between the A participant and the Intruder. The $\alpha^2$ execution refers to the situation where the Intruder pretends to be the A participant and in his name communicates with B. To have correct protocol which cannot be broken it is enough to add the identifier of the sender to sent message in the second step of the original NSPK protocol execution: $\langle N_A \cdot N_B \cdot i(B) \rangle_{K_A}$. All known verification methods and tools confirm safety of this version of NSPK.

## 3 Backward induction in modeling and verification of untimed protocols

As mentioned earlier, in the verification of systems modeled by transitional structures, backward induction is sometimes used. This takes place when there is hope that it is easier to build an execution tree of a program or system by constructing it, so to say, from the end, moving backwards from a certain state in accordance to a specific relation of a passage in the structure. Examples indicate that sometimes this method is very efficient, especially in the case of stating unreachableity of certain states (see [15]).

In order to verify security protocols using the backward induction method, we will now define the product automaton which models inversely the runs which take place in the product automaton constructed in previous sections. An appropriate theorem of the adequacy of the calculations done in both product automata will allow the searching of the tree using the backward induction method.

Let $\mathfrak{A}$ be a family of automata $\mathcal{A}_i$, $i \in I$ meeting the following conditions. Let $\mathcal{A}_i = \{Q_i, \Sigma_i, \delta_i, s_i^0, F_i\}$ be an automaton, where:

- $Q_i = \{s_i^0, s_i^1, \dots, s_i^t\}$, for all $i \in I$ and some $t \in N$ is the set of states of automata $\mathcal{A}_i$,

- $\Sigma_i = \{k_i^1, k_i^2, \dots, k_i^s\}$ is the set of labels, where $(\Sigma_i \cap \Sigma_j = \emptyset$, dla $i \neq j$) for all automata from $\mathfrak{A}$,

- $\delta_i \subseteq Q_i \times \Sigma_i \times Q_i$ is a transition relation that meets the following conditions:

* $(s_i^l, k, s_i^j) \in \delta_i$ iff $l = j - 1$, for any $l = 0, 1, \dots, s - 1$ oraz $j = 1, 2, \dots, s$,

* if $(s_i^l, k, s_i^{l+1}) \in \delta_i$ and $(s_i^p, k, s_i^{p+1}) \in \delta_i$, then $l = p$.

- $s_i^0$ is an initial state, $F_i = Q_i$ is the set of finite states.
It is noticeable that this family defines the automata which have the same structure as automata modeling the execution of protocols defined in [17–19]. The following conditions have been met:

- the sets of states of all the automata are equally numerous.

- the relation of the passage in each automaton is determined only on a pair of states directly following one another.

- labels do not duplicate in different automata, nor do they duplicate within the scope of one automaton,

- all states of the automata are accepting ones.

We denote by $\Sigma$ the set of all labels from automata from the family $\mathfrak{A}$ ($\Sigma = \bigcup_{i \in I} \Sigma_i$).
Now the family of automata corresponding to the knowledge automata will be defined.

Let $\mathfrak{B}$ be a family of automata $\mathcal{B}_j$, $j \in J$ that meets the following conditions. $\mathcal{B}_j = \{\mathcal{R}_j, \Sigma, \rho_j, r_j^0, T_j\}$ where:

- $\mathcal{R}_j = \{r_j^0, r_j^1\}$, for all $j \in J$,

- $\Sigma$ is the set of labels constructed before,

- $\rho_j \subseteq \mathcal{R}_j \times \Sigma \times \mathcal{R}_j$ is the transition relation that meets the condition: $(r_j^l, k, r_j^p) \in \rho_j$ iff $l=0 \land p=1$ or $l=p=1$,

- $r_j^0$ is an initial state, $T_j = \mathcal{R}_j$ is a set of finite states.

It is noticeable here that these automata have the same structure as knowledge automata constructed in the previous section:

- each have two states,

- transitions are defined only from the first state to the second, and from the second state to itself,

- labels are taken from the set of all labels from the automata of the $\mathfrak{A}$ family,

- all states are accepting ones.

By $\mathfrak{A}\mathfrak{B}$ we denote the product automaton (network of automata) defined over the family $\mathfrak{A} \cup \mathfrak{B}$ due to definition of product automaton given in [17].

We will now define the product automaton modeling the runs of automaton $\mathfrak{A}\mathfrak{B}$ executed inversely.

For all automata $\mathcal{A}_i \in \mathfrak{A}$ let $\overline{\mathcal{A}}_i$ be a smallest automaton that meets the following conditions:

$$ \overline{\mathcal{A}}_i = \{Q_i, \Sigma_i, \overline{\delta}_i, s_i^l, \{s_i^l, s_i^0\}\} \text{ where:} $$

- $\overline{\delta}_i \subseteq Q_i \times \Sigma_i \times Q_i$ is a transition relation that meets the condition: if $(s_i^l, k, s_i^{l+1}) \in \delta_i$, then $(s_i^{l+1}, k, s_i^l) \in \overline{\delta}_i$ and $(s_i^{l+1}, k, s_i^0) \in \overline{\delta}_i$.

- $s_i^l$ is an initial state, $\{s_i^l, s_i^0\}$ is a set of accepting states.

One should notice that the sets of states and labels are the same as in corresponding automata of the family $\mathfrak{A}$. By $\overline{\mathfrak{A}}$ we define the family of all such constructed automata.

Moreover for all automata $\mathcal{B}_j \in \mathfrak{B}$ we define automata $\overline{\mathcal{B}}_j$ as the smallest automata that meet for every $j \in J$:

$$ \overline{\mathcal{B}}_j = \{\overline{\mathcal{R}}_j, \Sigma, \overline{\rho}_j, r_j^2, \{r_j^0, r_j^2\}\} \text{ where:} $$
- $\overline{\mathcal{R}}_j = \mathcal{R}_j \cup \{r_j^2\} = \{r_j^0, r_j^1, r_j^2\}$,

- $\Sigma$ is the set of labels constructed before,

- $\overline{\rho}_j \subseteq \overline{\mathcal{R}}_j \times \Sigma \times \overline{\mathcal{R}}_j$ is the transition relation that meets the following conditions: if $(r_j^l, k, r_j^p) \in \rho_j$, then $(r_j^p, k, r_j^l) \in \overline{\rho}_j$ and $(r_j^2, k, r_j^l) \in \overline{\rho}_j$.

- $r_j^2$ is an initial state, $\{r_j^0, r_j^2\}$ is a set of accepting states.

By $\overline{\mathfrak{B}}$ we denote the family of all automata constructed before.

**Example 4.** Figures 2 and 3 present the intuition of the constructions implemented above. According to the above mentioned definitions of the beginning states of automata $\mathcal{A}, \mathcal{B}_1, \mathcal{B}_2$ are accordingly: $s_1^0, r_1^0, r_2^0$, whereas accepting ones are all states of the automata. In the case of automata $\overline{\mathcal{A}}, \overline{\mathcal{B}}_1, \overline{\mathcal{B}}_2$, beginning states are accordingly: $s_1^3, r_1^2, r_2^2$, whereas accepting ones are states $s_1^3, s_1^0, r_1^2, r_1^0, r_2^2, r_2^0$. One should notice that in the first network runs over the words: $q_1, q_1q_2$ and $q_1q_2q_4$ exist. In the second product automaton there are accordingly runs over the words: $q_1, q_2q_1$ and $q_4q_2q_1$.

<figure><img src="image_3.png" /><figcaption>**Fig. 2.** Direct automata model</figcaption></figure>

<figure><img src="image_4.png" /><figcaption>**Fig. 3.** Reverse automata model</figcaption></figure>

One can see from the previous example that suitable accepting runs exist in the product automaton of the first type only if in the product automaton of the second type
exist accepting runs which are mirror-reversed. The suitable example of network of automata that models reverse execution of NSPK is presented in Example 5.

*Example 5.* Figure 4 show the reverse automata model for execution of NSPK Protocol given in *Example 2*.

<figure><img src="image_5.png" /><figcaption>Fig. 4. Reverse automata model for NSPK execution</figcaption></figure>

As done so previously, let's consider the product automaton $\overline{\mathfrak{A}}$. For such constructed families of automata the following theorem holds.

**Theorem 1.** In the product automaton $\overline{\mathfrak{A}}$ there exists the run over the word $q = q_1, q_2, \dots, q_w$ iff in the product automaton $\overline{\mathfrak{B}}$ there exists the run over the word $\overline{q} = q_w, \dots, q_2, q_1$.

*Proof of Theorem 1* proceeds by induction considering the length of the word $q$.

*Proof of the right implication.* In order to prove the inductive base, one should notice that if in product automaton $\overline{\mathfrak{A}}$ there exists a run over the word $q = q_1$, then there exists exactly one automaton from the family $\mathfrak{A}$ in which the transition labelled $q_1$ is the transition from the beginning state to its successor. Therefore it is fulfilled that for a given $i \in I$ we have $(s_i^0, q_1, s_i^1) \in \delta_i$. According to the definition of the automaton $\overline{\mathfrak{B}}$ in automaton $\overline{\mathcal{A}}$ there exists the transition $(s_i^t, q_1, s_i^0) \in \overline{\delta}_i$. It is noticeable that according to the definitions of knowledge automaton from the family $\overline{\mathfrak{A}}$, in which any transition is labelled with label $q_1$, then there also exists an appropriate transition labelled $q_1$ leading from the beginning state $r_1^2$ to state $r_1^0$. For automata where in their transitions the label $q_1$ does not appear, an appropriate definition of ending states of the product automaton $\overline{\mathfrak{B}}$ should be reminded.

In order to prove the inductive step, it is assumed that the right implication is true for words of length $k$, therefore it is true that if in the product automaton $\overline{\mathfrak{A}}$ there is a
run over the word $q = q_1, q_2, \dots, q_k$, then in the product automaton $\overline{\mathfrak{A}\mathfrak{B}}$ there is a run over the word $\overline{q} = q_k, \dots, q_2, q_1$. It now should be proved that the implication is true for words of length $k+1$.

Any given word $q = q_1, q_2, \dots, q_k, q_{k+1}$ should now be considered. According to the definition of the product automaton $\overline{\mathfrak{A}\mathfrak{B}}$ there exists exactly one automaton from the family $\mathfrak{A}$ in which there exists a transition labelled $q_{k+1}$. So it is fulfilled that for a given $i \in I$, $(s_i^j, q_{k+1}, s_i^{j+1}) \in \delta_i$. According to the definition of automaton $\overline{\mathfrak{A}}$ in automaton $\overline{\mathcal{A}}$ there exists a transition $(s_i^l, q_1, s_i^j) \in \overline{\delta}_i$. It is also noticeable that according to definitions of knowledge automata from the family $\overline{\mathfrak{A}\mathfrak{B}}$, in which any transition is labelled with label $q_{k+1}$, there also exists an appropriate transition labelled $q_{k+1}$. Proof of left implication is analogous.

It should also be noticed that the same property concerns the accepting runs. The reason for this results directly from the above statement and in the definition of accepting states of the components of families of both types.

## 4 Backward induction in modeling and verification of timed protocols

Just like in the previous section, a model automata of time-dependent protocol executions which allows verification using the backward induction method will now be presented. Because the knowledge automata in this chapter do not include time aspects, only the construction of timed automata representing protocol execution will be introduced.

Let $C$ be a set of time constraints defined in [19, 18]. Additionally let $\mathfrak{T}\mathfrak{A}$ be a family of timed automata $\mathcal{T}\mathcal{A}_i$ ($i \in I$ for some indices from $I$) that meet the following conditions.

Let $\mathcal{T}\mathcal{A}_i = \{Q_i, \Sigma_i, \delta_i, s_i^0, F_i, \mathcal{X}_i\}$ be a timed automaton, where:

- let $Q_i = \{s_i^0, s_i^1, \dots, s_i^l\}$, for all $i \in I$ and some $t \in N$ be a set of states in $\mathcal{A}_i$,

- let $\Sigma_i = \{k_1^1, k_1^2, \dots, k_i^s\}$ be the set of labels where $\mathfrak{A}(\Sigma_i \cap \Sigma_j = \emptyset, \text{dla } i \neq j)$,

- $\delta_i \subseteq Q_i \times \Sigma_i \times C \times 2^{\mathcal{X}_i} \times Q_i$ be a transition relation that satisfies:

* $(s_i^l, k, \text{cc}, X, s_i^j) \in \delta_i \text{ iff } l = j-1$, for all $l = 0, 1, \dots, s-1$ and $j = 1, 2, \dots, s$,

* if $(s_i^l, k, \text{cc}, X, s_i^{l+1}) \in \delta_i$ and $(s_i^p, k, \text{cc}, X, s_i^{p+1}) \in \delta_i$, then $l = p$.

- $s_i^0$ is an initial state,

- $F_i = Q_i$ is the set of accepting states,

- $\mathcal{X}_i$ is the set of clocks.

This family defines automata which have the same structure as those defined in [19, 18] timed automata modeling the execution of time-dependent protocols. A timed automaton modeling reverse protocol execution will now be constructed.
For each automaton $\mathcal{T}\mathcal{A}_i \in \mathfrak{A}$ let $\overline{\mathcal{T}\mathcal{A}_i}$ be a smallest automaton that satisfies the following conditions:

$\overline{\mathcal{A}_i} = \{Q_i, \Sigma_i, \overline{\delta}_i, s'_i, \{s'_i, s^0_i\}, X_i\}$ where:

- $\overline{\delta}_i \subseteq Q_i \times \Sigma_i \times C \times 2^{\lambda_i} \times Q_i$ be a transition relation that satisfies: if $(s'_i, k, \text{cc}, X, s^{l+1}_i) \in \delta_i$, then $(s^{l+1}_i, k, \text{cc}, X, s'_i) \in \overline{\delta}_i$ and $(s^{l+1}_i, k, \text{cc}, X, s^0_i) \in \overline{\delta}_i$.

- $s'_i$ is an initial state,

- $\{s'_i, s^0_i\}$ is a set of accepting states.

In the case presented below, there holds a proper and adequate theorem concerning the existence of accepting runs in product automata including families execution automata as well as knowledge automata. The proof is analogous like in the previous one. For it should be noticed that only execution automata include nonempty time constraints, and these are accordingly modeled in a reverse product automata.

# 5 Experimental results

In this section the results of experiments performed according to methodology discussed above will be presented and described. The results were obtained with the original implementation done in C++. For testing we used untimed and timed versions of four of well known protocols: NSPK (mentioned above), Lowe's version of NSPK (NSPKL), Wide Mouth Frog (WMF), and CCITT. The implementation generates for a given (in ProToc language [17, 18]) protocol and defined in it the space of considerations, different interpretations - executions of the tested protocol. These executions, in turn, are automatically translated to the network of untimed or timed automata. Then automata are translated to the boolean propositional formula in CNF (conjunction normal form) format. Formulas are optimized and tested using SAT-solver MiniSAT. The existence of a valuation satisfying the formula is equivalent to the existence of an attack on the protocol. Lack of satisfying valuation shows that there was no attack in the considered finite space. The module enables testing the previously described attacks. The performed calculations found the known attacks upon protocols. The tables presented below mainly focus on verification parameters: memory used by the CPU and computation time.

The verification method that uses the backward induction approach gave better results in the case of the WMF and CCITT protocols in both cases of untimed and timed versions. This may be caused by a small number of protocol steps, resulting in slight differences in the constructed model and the size of the formula. In the case of protocols with a larger number of steps automata model was a little bigger and encoding gave larger formula. In this case searching by the solver took a bit more time than in the direct method.

Table 1 and 2 show a comparison of the direct verification and the backward induction technique in the case of untimed and time dependent protocols. After conducting a series of calculations for these protocols and their analysis, the following conclusions can be made: the backward induction method gave somewhat better results in the case of protocols with a small number of steps. In the case of long protocols the method did not quicken obtained verification results.
<table><caption>**Table 1.** Comparison of direct and backward methods of untimed protocols verification</caption><thead><tr><th></th><th>Direct</th><th>Direct</th><th>Backward</th><th>Backward</th></tr><tr><th>Protocol</th><th>Memory (MB)</th><th>Time (s.)</th><th>Memory (MB)</th><th>Time (s.)</th></tr></thead><tbody><tr><td>WMF<sub>Untimed</sub></td><td>8,56</td><td>0,004</td><td>7,78</td><td>0,002</td></tr><tr><td>CCITT<sub>Untimed</sub></td><td>9,13</td><td>0,041</td><td>8,84</td><td>0,031</td></tr><tr><td>NSPK</td><td>9,57</td><td>0,102</td><td>13,5</td><td>0,137</td></tr><tr><td>NSPKL</td><td>11,3</td><td>0,156</td><td>15,61</td><td>0,171</td></tr></tbody></table>

<table><caption>**Table 2.** Comparison of direct and backward methods for time dependent protocols</caption><thead><tr><th></th><th>Direct</th><th>Direct</th><th>Backward</th><th>Backward</th></tr><tr><th>Protocol</th><th>Memory (MB)</th><th>Time (s.)</th><th>Memory (MB)</th><th>Time (s.)</th></tr></thead><tbody><tr><td>WMF</td><td>10,32</td><td>0,004</td><td>9,41</td><td>0,002</td></tr><tr><td>CCITT</td><td>10,89</td><td>0,063</td><td>10,24</td><td>0,045</td></tr><tr><td>NSPK<sub>Timed</sub></td><td>11,56</td><td>0,110</td><td>16,32</td><td>0,166</td></tr><tr><td>NSPKL<sub>Timed</sub></td><td>13,72</td><td>0,210</td><td>18,77</td><td>0,231</td></tr></tbody></table>

# 6 Summary

Research carried out by various international teams show that there is no single, "ideal" method of verification for all protocols. Often we must select the method for the given protocol. During the searching for the next models and methods we developed and implemented the backward induction method for constructing automata that model executions of security protocols. After a series of computation and their analysis we can draw the following conclusions: the backward induction method in the case of automata based modeling of executions and verification of security protocols due to methodology given in [17, 18] may give better results only in the case of protocols with a small number of steps and there it can be successfully used. For long protocol method does not speed up the computations.

# References

1. Amnell, T., et. al.: Uppaal - Now, Next, and Future, Proc. of the 4th School 'Modelling and Verification of Parallel Processes' (MOVEP'00), LNCS, 2067, 99-124, Springer-Verlag, 2001.

2. Armando, A., et. al.: The AVISPA tool for the automated validation of internet security protocols and applications. In Proc. of 17th Int. Conf. on Computer Aided Verification (CAV'05), vol. 3576 of LNCS, pp. 281-285. Springer, 2005.

3. Armando, A., Compagna, L.: Sat-based model-checking for security protocols analysis. International Journal of Information Security, 7(1):3-32, 2008.

4. Bella, G., Massacci, F., and Paulson, L. C.: Verifying the set registration protocols. IEEE Journal on Selected Areas in Communications, 20(1):77-87, 2003.

5. Bella G, Paulson L.C.: Using Isabelle to prove properties of the kerberos authentication system. In H. Orman and C. Meadows, editors, Proc. of the DIMACS Workshop on Design and Formal Verification of Security Protocols, 1997.

6. Burrows, M., Abadi, M., and Needham, R. M.: A logic of authentication. ACM Trans. Comput. Syst., 8(1):18-36, 1990.
7. Cohen E.: TAPS: A first-order verifier for cryptographic protocols. In CSFW '00: Proceedings of the 13th IEEE Computer Security Foundations Workshop (CSFW'00), page 144, Washington, DC, USA, 2000. IEEE Computer Society.

8. Corin, R., Etalle, S., Hartel, P. H., and Mader, A.: Timed model checking of security protocols. In Proc. of the 2004 ACM Workshop FMSE, pages 23-32. ACM, 2004.

9. Delzanno, G., and Ganty, P.: Automatic verification of time sensitive cryptographic protocols. In Proc. of the 10th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'04), vol. 2988 of LNCS, pages 342-356. Springer, 2004.

10. Dolev, D. and Yao, A.: On the security of public key protocols. IEEE Transactions on Information Theory, 29(2):198-207, 1983.

11. El Fray I., Kurkowski M., Pejaś J., Maćków W., A New Mathematical Model for the Analytical Risk Assessment and Prediction in IT Systems, Control&Cybernetics, vol. 41, pp. 241-268, Systems Research Institute PAS, Warsaw, 2012.

12. Evans, N., and Schneider, S.: Analysing time dependent security properties in CSP using PVS. In Proc. of the 6th European Symposium on Research in Computer Security (ESORICS'00), vol. 1895 of LNCS, pp. 222-237. Springer, 2000.

13. Jakubowska, G., and Penczek, W., and Srebrny, M.: Verifying security protocols with times-tamps via translation to timed automata. In Proc. of the International Workshop on Concurrency, Specification and Programming (CS&P'05), pages 100-115. Warsaw University, 2005.

14. Kacprzak, M., et. al.: Verics 2007 - a model checker for knowledge and real-time. Fundam. Inform., 85(1-4):313-328, 2008.

15. Kurkowski M., Maćków W.: Using Backward Strategy to the Needham-Schroeder Public Key Protocol Verification, Artificial Intelligence and Security in Computing Systems, pp. 249 - 260, Kluwer Academic Publishers, Boston, 2003.

16. Kurkowski M., Pejaś J., A Propositional Logic for Access Control Policy in Distributed Systems, Artificial Intelligence and Security in Computing Systems, pp. 157 - 191, Kluwer Academic Publishers, Boston, 2003.

17. Kurkowski, M., Penczek, W.: Verifying Security Protocols Modeled by Networks of Automata, Fund. Inform., Vol. 79 (3-4), pp. 453-471, IOS Press 2007.

18. Kurkowski, M., Penczek, W.: Verifying Timed Security Protocols via Translation to Timed Automata, Fund. Inform., vol. 93 (1-3), pp. 245-259, IOS Press 2009.

19. Kurkowski M., Penczek W.: Applying Timed Automata to Model Checking of Security Protocols, in ed. J. Wang, Handbook of Finite State Based Models and Applications, pp. 223-254, Chapman&Hall/CRC Press, Boca Raton, USA, 2012.

20. Kurkowski, M., Srebrny, M.: A Quantifier-free First-order Knowledge Logic of Authentication, Fund. Inform., vol. 72, pp. 263-282, IOS Press 2006.

21. Lowe, G.: Breaking and Fixing the Needham-Schroeder Public-key Protocol Using fdr., In TACAS, LNCS, Springer, pp. 147-166, 1996.

22. Lowe, G.: Some new attacks upon security protocols. In IEEE Computer Society Press, editor, In Proceedings of the Computer Security Foundations Workshop VIII, 1996.

23. Meadows C.: The NRL protocol analyzer: An overview. Journal of Logic Programming, 26(2):13-131, 1996.

24. Moore J.H.: Protocol failures in cryptosystems. Proceedings of the IEEE, 76(5), 1988.

25. Needham, R.M., Schroeder, M.D.: Using encryption for authentication in large networks of computers. Commun. ACM, 21(12), 993-999, 1978.

26. Paulson, L. C.: Inductive analysis of the internet protocol tls. ACM Trans. Inf. Syst. Secur., 2(3):332-351, 1999.

27. Siedlecka-Lamch O., Kurkowski M., Piech H.: A New Effective Approach for Modeling and Verification of Security Protocols, in Proceedings of 21th international Workshop on Concurrency, Specification and Programming (CS&P 2012) pp. 191-202, Humboldt University Press, Berlin, Germany, 2012.