A new method of verification of security protocols

TL;DR

This paper introduces a process graph model for security protocols and presents a novel method for their specification and verification, enhancing the analysis of protocol security.

Contribution

It proposes a new process graph-based model and verification method for security protocols, offering a fresh approach to protocol analysis.

Findings

Effective process graph model for security protocols

New verification method improves protocol analysis

Enhances security protocol reliability

Abstract

In the paper we introduce a process model of security protocols, where processes are graphs with edges labelled by actions, and present a new method of specification and verification of security protocols based on this model.

Equations

$$(s_P^0,b_P^0,D_P^0)=(s_0,b_0,D_0)\stackrel{a_1}{\to }(s_1,b_1,D_1)\stackrel{a_2}{\to }\dots \stackrel{a_n}{\to }(s_n,b_n,D_n)$$

$$\forall\,b\in{\cal B},D\subseteq{\cal E},a\in{\cal A}\quad(b,D)a=\left\{\begin{array}[]{llllllllllllll}\mbox{$(b,D\cup\{e\})$, if $a=d?e$ or $d!e$, where $d\in D^{b}$,}\\ \mbox{$(b\wedge a,D)$, if $a\in{\cal B}$,}\\ \mbox{undefined, otherwise.}\end{array}\right.$$

$$P_{i}=(\{s^{0}_{i},s_{i}\},s^{0}_{i},\{{\matrix{s^{0}_{i}&\begin{picture}(20.0,18.0)\put(-5.0,3.0){\vector(1,0){30.0}} \put(9.0,8.0){\makebox(1.0,1.0)[]{$\scriptstyle c\,!\,k_{i}(e_{i})$}} \end{picture}&s_{i}}}\},\top,\{c\},\{k_{i}\})\quad(i=1,2).$$

$$\begin{array}[]{llllllllllllll}S_{[a]P}\mathbin{{\mathop{=}\limits^{\mbox{\scriptsize def}}}}\{s\}\sqcup S_{P},\quad s^{0}_{[a]P}\mathbin{{\mathop{=}\limits^{\mbox{\scriptsize def}}}}s,\quad R_{[a]P}\mathbin{{\mathop{=}\limits^{\mbox{\scriptsize def}}}}\{s\;\mathop{\to}\limits^{\!\!a}\;s_{P}^{0}\}\sqcup R_{P},\\ b^{0}_{[a]P}\mathbin{{\mathop{=}\limits^{\mbox{\scriptsize def}}}}b^{0}_{P}$, $D^{0}_{[a]P}\mathbin{{\mathop{=}\limits^{\mbox{\scriptsize def}}}}X_{a}\cup D^{0}_{P}$, $H^{0}_{[a]P}\mathbin{{\mathop{=}\limits^{\mbox{\scriptsize def}}}}H^{0}_{P}.\end{array}$$

$$\begin{array}[]{llllllllllllll}S_{P_{1}+P_{2}}\mathbin{{\mathop{=}\limits^{\mbox{\scriptsize def}}}}\{s\}\sqcup S_{P_{1}}\sqcup S_{P_{2}},\quad s^{0}_{P_{1}+P_{2}}\mathbin{{\mathop{=}\limits^{\mbox{\scriptsize def}}}}s,\\ R_{P_{1}+P_{2}}\mathbin{{\mathop{=}\limits^{\mbox{\scriptsize def}}}}R_{P_{1}}\sqcup R_{P_{2}}\sqcup\{s\;\mathop{\to}\limits^{\!\!a}\;s^{\prime}\mid(s^{0}_{P_{i}}\;\mathop{\to}\limits^{\!\!a}\;s^{\prime})\in R_{P_{i}},\;i\in\{1,2\}\},\\ b^{0}_{P_{1}+P_{2}}\mathbin{{\mathop{=}\limits^{\mbox{\scriptsize def}}}}b^{0}_{P_{1}}\wedge b^{0}_{P_{2}},\;\;D^{0}_{P_{1}+P_{2}}\mathbin{{\mathop{=}\limits^{\mbox{\scriptsize def}}}}D^{0}_{P_{1}}\cup D^{0}_{P_{2}},\;\;H^{0}_{P_{1}+P_{2}}\mathbin{{\mathop{=}\limits^{\mbox{\scriptsize def}}}}H^{0}_{P_{1}}\cup H^{0}_{P_{2}}.\end{array}$$

$$Sys\approx \widetilde{Sys}$$

$$\begin{array}[]{llllllllllllll}Sys\approx[y=x]\,P,\quad\tilde{Sys}\approx[y^{\prime}=x]\,[y=x]\,P,\end{array}$$

$$\begin{array}[]{llllllllllllll}[y=x_{1}]\,P\approx[y=x_{2}]\,P\quad\Rightarrow\quad[x=x_{1}]\,Sys\approx[x=x_{2}]Sys\\ \mbox{(where $x_{1},x_{2}$ are fresh variables).}\end{array}$$

$$[y=x][y=x_1]P\approx [y=x][y=x_2]P,$$

$$[x=x_1][y=x]P\approx [x=x_2][y=x]P.$$

$$[x=x_1]Sys\approx [x=x_1][y=x]P\approx [x=x_2][y=x]P\approx [x=x_2]Sys.\text{vrule}height=7.0pt,width=7.0pt,depth=0.0pt$$

$$A\stackrel{\text{mbox}def}{=}[c_a!c][c!x]0,T\stackrel{\text{mbox}def}{=}[c_a?c][c_b!c]0,B\stackrel{\text{mbox}def}{=}[c_b?c][c?y]P.$$

$$\widetilde{Sys}\stackrel{\text{mbox}def}{=}(A,T,\tilde{B}{)}_{k_a,k_b},\tilde{B}\stackrel{\text{mbox}def}{=}[c_b?k_b(k_B)][c?k_B(y^{\prime })][y=x]P.$$

$$\begin{array}[]{llllllllllllll}\begin{picture}(210.0,110.0)\par\put(0.0,100.0){\oval(30.0,20.0)} \put(0.0,100.0){\oval(34.0,24.0)} \put(0.0,100.0){\makebox(0.0,0.0)[c]{$A^{0}T^{0}$}} \par\put(0.0,50.0){\oval(30.0,20.0)} \put(0.0,50.0){\makebox(0.0,0.0)[c]{$A^{0}T^{1}$}} \par\put(0.0,0.0){\oval(30.0,20.0)} \put(0.0,0.0){\makebox(0.0,0.0)[c]{$A^{0}T^{2}$}} \par\put(100.0,100.0){\oval(30.0,20.0)} \put(100.0,100.0){\makebox(0.0,0.0)[c]{$A^{1}T^{0}$}} \par\put(100.0,50.0){\oval(30.0,20.0)} \put(100.0,50.0){\makebox(0.0,0.0)[c]{$A^{1}T^{1}$}} \par\put(100.0,0.0){\oval(30.0,20.0)} \put(100.0,0.0){\makebox(0.0,0.0)[c]{$A^{1}T^{2}$}} \par\put(200.0,100.0){\oval(30.0,20.0)} \put(200.0,100.0){\makebox(0.0,0.0)[c]{$A^{2}T^{0}$}} \par\put(200.0,50.0){\oval(30.0,20.0)} \put(200.0,50.0){\makebox(0.0,0.0)[c]{$A^{2}T^{1}$}} \par\put(200.0,0.0){\oval(30.0,20.0)} \put(200.0,0.0){\makebox(0.0,0.0)[c]{$A^{2}T^{2}$}} \par\put(0.0,75.0){\makebox(0.0,0.0)[r]{ $c_{a}?\,k_{a}(k_{T})$ }} \par\put(100.0,75.0){\makebox(0.0,0.0)[l]{ $c_{a}?\,k_{a}(k_{T})$ }} \par\put(200.0,75.0){\makebox(0.0,0.0)[l]{ $c_{a}?\,k_{a}(k_{T})$ }} \par\put(0.0,25.0){\makebox(0.0,0.0)[r]{ $c_{b}\,!\,k_{b}(k_{T})$ }} \par\put(100.0,25.0){\makebox(0.0,0.0)[l]{ $c_{b}\,!\,k_{b}(k_{T})$ }} \par\put(200.0,25.0){\makebox(0.0,0.0)[l]{ $c_{b}\,!\,k_{b}(k_{T})$ }} \par\put(50.0,103.0){\makebox(0.0,0.0)[b]{ $c_{a}\,!\,k_{a}(k)$ }} \put(50.0,53.0){\makebox(0.0,0.0)[b]{ $c_{a}\,!\,k_{a}(k)$ }} \put(50.0,3.0){\makebox(0.0,0.0)[b]{ $c_{a}\,!\,k_{a}(k)$ }} \par\put(150.0,103.0){\makebox(0.0,0.0)[b]{ $c\,!\,k(x)$ }} \par\put(150.0,53.0){\makebox(0.0,0.0)[b]{ $c\,!\,k(x)$ }} \par\put(150.0,3.0){\makebox(0.0,0.0)[b]{ $c\,!\,k(x)$ }} \par\par\put(50.0,80.0){\makebox(0.0,0.0)[l]{ $k_{T}=k$ }} \par\par\put(0.0,88.0){\vector(0,-1){28.0}} \put(100.0,90.0){\vector(0,-1){30.0}} \put(200.0,90.0){\vector(0,-1){30.0}} \put(0.0,40.0){\vector(0,-1){30.0}} \put(100.0,40.0){\vector(0,-1){30.0}} \put(200.0,40.0){\vector(0,-1){30.0}} \par\put(15.0,93.0){\vector(2,-1){72.0}} \par\put(17.0,100.0){\vector(1,0){68.0}} \put(15.0,50.0){\vector(1,0){70.0}} \put(15.0,0.0){\vector(1,0){70.0}} \par\put(115.0,100.0){\vector(1,0){70.0}} \put(115.0,50.0){\vector(1,0){70.0}} \put(115.0,0.0){\vector(1,0){70.0}} \par\end{picture}\end{array}$$

$$\begin{array}[]{llllllllllllll}\begin{picture}(270.0,150.0)\par\put(0.0,150.0){\oval(30.0,20.0)} \put(0.0,150.0){\oval(34.0,24.0)} \put(0.0,150.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{0}T^{0}B^{0}}$}} \par\par\put(100.0,150.0){\oval(30.0,20.0)} \put(100.0,150.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{1}T^{0}B^{0}}$}} \par\put(100.0,100.0){\oval(30.0,20.0)} \put(100.0,100.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{1}T^{1}B^{0}}$}} \par\put(100.0,0.0){\oval(30.0,20.0)} \put(100.0,0.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{1}T^{2}B^{0}}$}} \par\put(200.0,150.0){\oval(30.0,20.0)} \put(200.0,150.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{2}T^{0}B^{0}}$}} \par\par\put(200.0,100.0){\oval(30.0,20.0)} \put(200.0,100.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{2}T^{1}B^{0}}$}} \par\put(200.0,0.0){\oval(30.0,20.0)} \put(200.0,0.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{2}T^{1}B^{1}}$}} \par\par\put(100.0,125.0){\makebox(0.0,0.0)[l]{ $c_{a}?\,k_{a}(k_{T})$ }} \par\put(200.0,125.0){\makebox(0.0,0.0)[l]{ $c_{a}?\,k_{a}(k_{T})$ }} \par\par\put(100.0,50.0){\makebox(0.0,0.0)[r]{ $c_{b}\,!\,k_{b}(k_{T})$ }} \par\put(200.0,80.0){\makebox(0.0,0.0)[r]{ $c_{b}\,!\,k_{b}(k_{T})$ }} \par\put(50.0,153.0){\makebox(0.0,0.0)[b]{ $c_{a}\,!\,k_{a}(k)$ }} \par\par\par\put(150.0,153.0){\makebox(0.0,0.0)[b]{ $c\,!\,k(x)$ }} \par\put(150.0,103.0){\makebox(0.0,0.0)[b]{ $c\,!\,k(x)$ }} \par\put(150.0,-3.0){\makebox(0.0,0.0)[t]{ $c\,!\,k(x)$ }} \par\par\put(50.0,120.0){\makebox(0.0,0.0)[r]{ $k_{T}=k$ }} \par\par\put(100.0,140.0){\vector(0,-1){30.0}} \put(200.0,140.0){\vector(0,-1){30.0}} \par\put(100.0,90.0){\vector(0,-1){80.0}} \put(200.0,90.0){\vector(0,-1){80.0}} \par\put(14.5,142.0){\vector(2,-1){72.0}} \par\put(17.0,150.0){\vector(1,0){68.0}} \par\par\par\put(115.0,150.0){\vector(1,0){70.0}} \put(115.0,100.0){\vector(1,0){70.0}} \put(115.0,0.0){\vector(1,0){70.0}} \par\put(130.0,30.0){\oval(30.0,20.0)} \put(130.0,30.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{1}T^{2}B^{1}}$}} \par\put(160.0,60.0){\oval(30.0,20.0)} \put(160.0,60.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{1}T^{2}P}$}} \par\par\put(230.0,30.0){\oval(30.0,20.0)} \put(230.0,30.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{2}T^{2}B^{1}}$}} \par\par\put(180.0,27.0){\makebox(0.0,0.0)[t]{ $c\,!\,k(x)$ }} \par\put(190.0,68.0){\makebox(0.0,0.0)[t]{ $c\,!\,k(x)$ }} \par\put(145.0,30.0){\vector(1,0){70.0}} \par\put(175.0,60.0){\vector(1,0){70.0}} \par\par\put(260.0,60.0){\oval(30.0,20.0)} \put(260.0,60.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{2}T^{2}P}$}} \par\put(110.0,8.0){\vector(1,1){12.0}} \par\put(140.0,38.0){\vector(1,1){12.0}} \put(210.0,8.0){\vector(1,1){12.0}} \put(240.0,38.0){\vector(1,1){12.0}} \put(240.0,38.0){\vector(1,1){12.0}} \par\put(205.0,90.0){\vector(1,-2){25.0}} \put(104.0,90.0){\vector(1,-2){25.0}} \par\put(144.0,34.0){\vector(4,1){100.0}} \par\par\put(113.0,10.0){\makebox(0.0,0.0)[l]{ $c_{b}?\,k_{b}(k_{B})$ }} \par\put(128.0,44.0){\makebox(0.0,0.0)[l]{ $c?k_{B}(y)$ }} \par\par\put(213.0,10.0){\makebox(0.0,0.0)[l]{ $c_{b}?\,k_{b}(k_{B})$ }} \put(243.0,40.0){\makebox(0.0,0.0)[l]{ $c?\,k_{B}(y)$ }} \par\put(110.0,80.0){\makebox(0.0,0.0)[l]{ $k_{B}=k_{T}$ }} \put(210.0,80.0){\makebox(0.0,0.0)[l]{ $k_{B}=k_{T}$ }} \par\put(200.0,48.0){\makebox(0.0,0.0)[r]{ $y=x$ }} \par\par\end{picture}\end{array}$$

$$\begin{array}[]{llllllllllllll}\begin{picture}(270.0,160.0)\par\put(0.0,150.0){\oval(30.0,20.0)} \put(0.0,150.0){\oval(34.0,24.0)} \put(0.0,150.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{0}T^{0}B^{0}}$}} \par\par\put(100.0,150.0){\oval(30.0,20.0)} \put(100.0,150.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{1}T^{0}B^{0}}$}} \par\put(100.0,100.0){\oval(30.0,20.0)} \put(100.0,100.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{1}T^{1}B^{0}}$}} \par\put(100.0,0.0){\oval(30.0,20.0)} \put(100.0,0.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{1}T^{2}B^{0}}$}} \par\put(200.0,150.0){\oval(30.0,20.0)} \put(200.0,150.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{2}T^{0}B^{0}}$}} \par\par\put(200.0,100.0){\oval(30.0,20.0)} \put(200.0,100.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{2}T^{1}B^{0}}$}} \par\put(200.0,0.0){\oval(30.0,20.0)} \put(200.0,0.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{2}T^{1}B^{1}}$}} \par\par\put(100.0,125.0){\makebox(0.0,0.0)[l]{ $c_{a}?\,k_{a}(k_{T})$ }} \par\put(200.0,125.0){\makebox(0.0,0.0)[l]{ $c_{a}?\,k_{a}(k_{T})$ }} \par\par\put(100.0,50.0){\makebox(0.0,0.0)[r]{ $c_{b}\,!\,k_{b}(k_{T})$ }} \par\put(200.0,80.0){\makebox(0.0,0.0)[r]{ $c_{b}\,!\,k_{b}(k_{T})$ }} \par\put(50.0,153.0){\makebox(0.0,0.0)[b]{ $c_{a}\,!\,k_{a}(k)$ }} \par\par\par\put(150.0,153.0){\makebox(0.0,0.0)[b]{ $c\,!\,k(x)$ }} \par\put(150.0,103.0){\makebox(0.0,0.0)[b]{ $c\,!\,k(x)$ }} \par\put(150.0,-3.0){\makebox(0.0,0.0)[t]{ $c\,!\,k(x)$ }} \par\par\put(50.0,120.0){\makebox(0.0,0.0)[r]{ $k_{T}=k$ }} \par\par\put(100.0,140.0){\vector(0,-1){30.0}} \put(200.0,140.0){\vector(0,-1){30.0}} \par\put(100.0,90.0){\vector(0,-1){80.0}} \put(200.0,90.0){\vector(0,-1){80.0}} \par\put(14.5,142.0){\vector(2,-1){72.0}} \par\put(17.0,150.0){\vector(1,0){68.0}} \par\par\par\put(115.0,150.0){\vector(1,0){70.0}} \put(115.0,100.0){\vector(1,0){70.0}} \put(115.0,0.0){\vector(1,0){70.0}} \par\put(130.0,30.0){\oval(30.0,20.0)} \put(130.0,30.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{1}T^{2}B^{1}}$}} \par\par\par\put(230.0,30.0){\oval(30.0,20.0)} \put(230.0,30.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{2}T^{2}B^{1}}$}} \par\par\put(180.0,27.0){\makebox(0.0,0.0)[t]{ $c\,!\,k(x)$ }} \par\par\put(145.0,30.0){\vector(1,0){70.0}} \par\par\par\put(260.0,60.0){\oval(30.0,20.0)} \put(260.0,60.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{2}T^{2}P}$}} \par\put(110.0,8.0){\vector(1,1){12.0}} \par\put(210.0,8.0){\vector(1,1){12.0}} \put(240.0,38.0){\vector(1,1){12.0}} \put(240.0,38.0){\vector(1,1){12.0}} \par\put(205.0,90.0){\vector(1,-2){25.0}} \put(104.0,90.0){\vector(1,-2){25.0}} \par\put(144.0,34.0){\vector(4,1){100.0}} \par\par\put(113.0,10.0){\makebox(0.0,0.0)[l]{ $c_{b}?\,k_{b}(k_{B})$ }} \par\par\par\put(213.0,10.0){\makebox(0.0,0.0)[l]{ $c_{b}?\,k_{b}(k_{B})$ }} \put(243.0,40.0){\makebox(0.0,0.0)[l]{ $c?\,k_{B}(y)$ }} \par\put(110.0,80.0){\makebox(0.0,0.0)[l]{ $k_{B}=k_{T}$ }} \put(210.0,80.0){\makebox(0.0,0.0)[l]{ $k_{B}=k_{T}$ }} \par\put(190.0,50.0){\makebox(0.0,0.0)[r]{ $y=x$ }} \end{picture}\end{array}$$

Full text

1 Introduction

1.1 Security protocols

and their properties

A security protocol (SP) is a distributed algorithm that determines an order of message passing between several agents. Examples of such agents are computer systems, bank cards, people, etc. Messages transmitted by SPs can be encrypted. We assume that encryption transformations used in SPs are perfect, i.e. satisfy some axioms expressing, for example, an impossibility of extraction of open texts from ciphertexts without knowing the corresponding cryptographic keys.

In this paper we present a new model of SPs based on Milner’s Calculus of Communicating Systems [1] and theory of processes with message passing [2]. This model is a graph analog of a Calculus of Cryptographic Protocols (spi-calculus, [3]). It can serve as a theoretical foundation for a new method (presented in the paper) of verification of SPs, where verification means a constructing of mathematical proofs that SPs meet the desired properties. Examples of such properties are integrity and secrecy. These properties are defined formally, as some conditions expressed in terms of an observational equivalence.

1.2 Verification

of security protocols

There are examples of SPs ([4]–[8]) which were used in safety-critical systems, however it turned out that the SPs contain vulnerabilities of the following forms:

• •

agents involved in these SPs can receive distorted messages (or lose them) as a result of interception, deletion or distortion of transmitted messages by an adversary, that violates the integrity property,

• •

an adversary can find out a confidential information contained in intercepted messages as a result of erroneous or fraudulent actions of SP agents.

These examples justify that for SPs used in safety-critical systems it is not enough informal analysis of required properties, it is necessary

• •

to build a mathematical model of an analyzed SP,

• •

to describe security properties of the analyzed SP as mathematical objects (e.g. graphs, or logical formulas), called a formal specification, and

• •

to construct a mathematical proof that the analyzed SP meets (or does not meet) the formal specification, this proof is called a formal verification.

In the process model described in the paper SPs and their formal specifications are represented by processes with message passing. Many important properties of SPs (in particular, integrity and secrecy) can be expressed as observational equivalence of such processes.

One of the most significant advantages of the proposed process model of SPs is a low complexity of proofs of correctness of SPs. In particular, there is no need to build a set of all reachable states of analyzed SPs, if the set of all these states and transmitted messages is unbounded.

Among other models of SPs most popular are logical models ([9]–[13]). These models provide possibility to reduce the problem of verification of SPs to the problem of proofs of theorems that analyzed SPs meet their specifications. Algebraic and logical approaches to verification are considered also in [14]–[16].

2 Description of a process model of security protocols

In the process model described below SPs and formal specifications of their properties are represented by graphs, whose edges are labeled by actions. Actions are expressions consisting of terms and formulas.

2.1 Variables, constants,

terms

We assume that there are given a set ${\cal X}$ of variables, a subset ${\cal K}\subseteq{\cal X}$ of keys, and a set ${\cal C}$ of constants. A set ${\cal E}$ of terms is defined inductively:

• •

$\forall\,x\in{\cal X},\;\forall\,c\in{\cal C}\quad x$ and $c$ are terms,

• •

for each list $e_{1},\ldots,e_{n}$ of terms the record $e_{1}\ldots e_{n}$ is a term,

(if the above list is empty, then the corresponding term is denoted by $\varepsilon$),

• •

$\forall\,k\in{\cal K}$, $\forall\,e\in{\cal E}$ the record $k(e)$ is a term (called an encrypted message (EM), this term represents a result of an encryption of $e$ on the key $k$).

Terms are designed for a representation of messages transmitted between participants of communications, a term of the form $e_{1}\ldots e_{n}$ represents a composite message consisting of messages corresponding to the components $e_{1},\ldots,e_{n}$. $\forall\,e\in{\cal E}$ the set of variables occurred in $e$ is denoted by $X_{e}$. If terms $e,e^{\prime}$ have the form $e_{1},\ldots,e_{n}$ and $e^{\prime}_{1},\ldots,e^{\prime}_{n^{\prime}}$, respectively, then the record $ee^{\prime}$ denotes the term $e_{1},\ldots,e_{n}e^{\prime}_{1},\ldots,e^{\prime}_{n^{\prime}}$, and $\forall\,e\in{\cal E}\;\;\varepsilon e=e\varepsilon=e$.

2.2 Formulas

Elementary formulas (EFs) are records of the form $e=e^{\prime}$ and $e\in E$ (where $e,e^{\prime}\in{\cal E}$, and $E$ is a subset of ${\cal E}$). A formula is a conjunction of EFs. The symbols $\top$ and $\bot$ denote true and false formulas respectively (for example, $\top=(c_{1}=c_{1})$, $\bot=(c_{1}=c_{2})$, where $c_{1}$ and $c_{2}$ are different constants). A set of formulas is denoted by ${\cal B}$. $\forall\,b\in{\cal B}\;\;X_{b}$ is a set of all variables occurring in $b$.

$\forall\,b_{1},b_{2}\in{\cal B}\quad b_{1}\leq b_{2}$ means that $b_{2}$ is a logical consequence of $b_{1}$ (where the concept of a logical consequence is defined by a standard way).

If $b_{1}\leq b_{2}$ and $b_{2}\leq b_{1}$, then $b_{1}$ and $b_{2}$ are assumed to be equal.

$\forall\,k,k^{\prime}\in{\cal K},\;\forall\,e,e^{\prime}\in{\cal E}$ the formulas $k(e)=k^{\prime}(e^{\prime})$ and $(k=k^{\prime})\wedge(e=e^{\prime})$ are assumed to be equal. The records $e_{1}=_{b}e_{2}$ and $b\in_{b}E$ means that $b\leq(e_{1}=e_{2})$ and $b\leq(e\in E)$ respectively.

2.3 Closed sets of terms

Let $E\subseteq{\cal E}$ and $b\in{\cal B}$. The set $E$ is said to be $b$–closed if

• •

\big{(}\forall\,i=1,\ldots,n\;\;e_{i}\in E\big{)}\Leftrightarrow e_{1}\ldots e_{n}\in E,

• •

\forall\,k\in E\cap{\cal K}\;\;\big{(}e\in E\Leftrightarrow k(e)\in E\big{)},

• •

\forall\,e,e^{\prime}\in{\cal E}\quad(e=_{b}e^{\prime})\;\Rightarrow\;\big{(}e\in E\;\Leftrightarrow\;e^{\prime}\in E\big{)}.

Closed sets of terms are used for representation of sets of messages which can be known to an adversary. The above conditions correspond to operations which an adversary $A$ can perform with his available messages:

• •

if $A$ has $e_{1},\ldots,e_{n}$, then it can compose the message $e_{1}\ldots e_{n}$,

• •

if $A$ has $e_{1}\ldots e_{n}$, then it may get its components $e_{1}$, $\ldots$, $e_{n}$,

• •

if $A$ has $k$ and $e$, where $k$ is a key, then it can create a EM $k(e)$,

• •

if $A$ has an EM $k(e)$ and a key $k$, then it can decrypt $k(e)$, i.e. get $e$.

Theorem 1. $\forall\,E\subseteq{\cal E}$, $\forall\,b\in{\cal B}$ there is a least (w.r.t. an inclusion of sets) $b$–closed set $E^{b}\subseteq{\cal E}$, such that $E\subseteq E^{b}$.

Let $D_{1},D_{2}\subseteq{\cal E}$, and $b_{1},b_{2}\in{\cal B}$. A binary relation $\mu\subseteq D_{1}^{b_{1}}\times D_{2}^{b_{2}}$ is said to be a similarity between $(D_{1},{b_{1}})$ and $(D_{2},{b_{2}})$, if $\forall\,(e_{1},e_{2})\in\mu$

• •

$\forall\,e^{\prime}_{1},e^{\prime}_{2}\in{\cal E}\quad(e^{\prime}_{1},e_{2})\in\mu\Leftrightarrow(e_{1}=_{b_{1}}e^{\prime}_{1}),\;\;(e_{1},e^{\prime}_{2})\in\mu\Leftrightarrow(e_{2}=_{b_{2}}e^{\prime}_{2})$,

• •

the conditions $\exists\;e_{i}^{1},\ldots,e_{i}^{n}\in D_{i}^{b_{i}}:(e_{i}=_{b_{i}}e_{i}^{1}\ldots e_{i}^{n})\;\;(i=1,2)$ are equivalent, and if these conditions hold, then $\forall\,i=1,\ldots,n\;\;(e_{1}^{i},e_{2}^{i})\in\mu$,

• •

the conditions $\exists\,k_{i},e_{i}^{\prime}\in D_{i}^{b_{i}}:(e_{i}=_{b_{i}}k_{i}(e_{i}^{\prime}))\;\;(i=1,2)$ are equivalent, and if these conditions hold, then $(k_{1},k_{2})\in\mu$ and $(e_{1}^{\prime},e_{2}^{\prime})\in\mu$.

A set of all similarities between $(D_{1},{b_{1}})$ and $(D_{2},{b_{2}})$ is denoted by the record Sim\big{(}(D_{1},{b_{1}}),(D_{2},{b_{2}})\big{)}.

2.4 Actions

An action is a record of one of the three kinds: an input, an output, an internal action. Inputs and outputs are associated with an execution, defined below.

• •

An input is an action of the form $e?e^{\prime}$, where $e,e^{\prime}\in{\cal E}$. An execution of this action consists of a receiving a message through a channel named $e$, and writing components of this message to variables occurring in $e^{\prime}$.

• •

An output is an action of the form $e!e^{\prime}$, where $e,e^{\prime}\in{\cal E}$. An execution of this action consists of a sending a message $e^{\prime}$ through a channel named $e$.

• •

An internal action is an action of the form $b$, where $b\in{\cal B}$.

The set of all actions is denoted by ${\cal A}$, $\forall\,a\in{\cal A}$ a set of variables occurred in $a$ is denoted by $X_{a}$.

2.5 Processes

with a message passing

Processes with a message passing are intended for description of SPs and formal specifications of their properties.

A process with a message passing (called below briefly as a process) is a tuple $P=(S,s^{0},R,b^{0},D^{0},H^{0})$, where

• •

$S$ is a set of states, $s^{0}\in S$ is an initial state,

• •

$R\subseteq S\times{\cal A}\times S$ is a set of transitions, each transition $(s,a,s^{\prime})\in R$ is denoted by the record $s\;\mathop{\to}\limits^{\!\!a}\;s^{\prime}$,

• •

$b^{0}\in{\cal B}$ is an initial condition,

• •

$D^{0}\subseteq{\cal E}$ is a set of disclosed terms, values of these terms are known to both the process $P$ and the environment at the initial moment, and

• •

$H^{0}\subseteq{\cal X}$ is a set of hidden variables.

A set of all processes is denoted by ${\cal P}$, $\forall\,P\in{\cal P}$ the records $S_{P}$, $s^{0}_{P}$, $R_{P}$, $b^{0}_{P}$, $D^{0}_{P}$, $H^{0}_{P}$ denote the corresponding components of $P$. A set of variables occurring in $P$ is denoted by $X_{P}$. A process $P$ such that $R_{P}=\emptyset$ is denoted by 0.

A transition $s\;\mathop{\to}\limits^{\!\!a}\;s^{\prime}$ is said to be an input, an output, or an internal transition, if $a$ is an input, an output, or an internal action, respectively.

A process $P$ can be represented as a graph (denoted by the same symbol $P$): its nodes are states from $S_{P}$, and edges are corresponded to transitions from $R_{P}$: each transition $s\;\mathop{\to}\limits^{\!\!a}\;s^{\prime}$ corresponds to an edge from $s_{1}$ to $s_{2}$ labelled by $a$. We assume that for each process $P$ under consideration the graph $P$ is acyclic.

2.6 An execution

of a process

An execution of a process $P\in{\cal P}$ can be informally understood as a walk on the graph $P$ starting from $s^{0}_{P}$, with an execution of actions that are labels of traversed edges. At each step $i\geq 0$ of this walk there are defined

• •

a state $s_{i}\in S_{P}$ of the process $P$ at the moment $i$,

• •

a condition $b_{i}\in{\cal B}$ on variables of $P$ at the moment $i$, and

• •

a set $D_{i}\subseteq{\cal E}$ of disclosed messages at the moment $i$, i.e. messages known to both the process $P$ and the environment at the moment $i$.

An execution of a process $P\in{\cal P}$ is a sequence of the form

[TABLE]

where $\forall\,i=1,\ldots,n\;\;(s_{i-1}\;\mathop{\to}\limits^{\!\!a_{i}}\;s_{i})\in R_{P}$, $(b_{i},D_{i})=(b_{i-1},D_{i-1})a_{i}$, and

[TABLE]

We assume that a value of each variable $x\in H^{0}_{P}$ is unique and unknown to an environment of $P$ at the initial moment of any execution of $P$.

A set of all executions of $P$ can be represented by a labelled tree $T_{P}$, where

• •

a root $t_{P}^{0}$ of the tree $T_{P}$ is labelled by the triple $(s^{0}_{P},b^{0}_{P},D^{0}_{P})$, and

• •

if the set of edges of $P$ outgoing from $s^{0}_{P}$ is $\{s^{0}_{P}\;\mathop{\to}\limits^{\!\!a_{i}}\;s_{i}\mid i=1,\ldots,m\}$, then for each $i\in\{1,\ldots,m\}$, such that $\exists\,(b_{i},D_{i})=(b_{P}^{0},D^{0}_{P})a_{i}$,

• –

$T_{P}$ has an edge of the form $t^{0}_{P}\;\mathop{\to}\limits^{\!\!a_{i}}\;t_{i}$, and

• –

a subtree growing from $t_{i}$ is $T_{P_{i}}$, where $P_{i}=(S_{P},s_{i},R_{P},b_{i},D_{i},H^{0}_{P}\setminus D_{i}^{b_{i}})$.

The set of nodes of $T_{P}$ is denoted by the same record $T_{P}$. For each node $t\in T_{P}$ the records $s_{t}$, $b_{t}$, $D_{t}$ denote corresponding components of a label of $t$.

$\forall\,t,t^{\prime}\in T_{P}$ the record $t\to t^{\prime}$ means that either $t=t^{\prime}$, or there is a path in $T_{P}$ of the form $t=t_{0}\;\mathop{\to}\limits^{\!\!a_{1}}\;t_{1}\;\mathop{\to}\limits^{\!\!a_{2}}\;\ldots\;\mathop{\to}\limits^{\!\!a_{m}}\;t_{m}=t^{\prime}$, where $a_{1},\ldots,a_{m}\in{\cal B}$.

2.7 Observational

equivalence of processes

In this section we introduce a concept of observational equivalence of processes. This concept has the following sense: processes $P_{1}$ and $P_{2}$ are observationally equivalent iff for any external observer (which can observe a behavior of $P_{1}$ and $P_{2}$ by sending and receiving messages) these processes are indistinguishable.

An example of a pair of observationally equivalent processes is the pair

[TABLE]

$P_{1}$ and $P_{2}$ send a unique message via channel $c$ and then terminate. Any process observing an execution of $P_{1}$ and $P_{2}$ is unable to distinguish them.

Processes $P_{1},P_{2}\in{\cal P}$, are said to be observationally equivalent iff there is a binary relation $\mu\subseteq T_{P_{1}}\times T_{P_{2}}$ satisfying the following conditions:

\forall\,(t_{1},t_{2})\in\mu\;\;\exists\,\mu_{t_{1},t_{2}}\in Sim\big{(}(D_{t_{1}},{b_{t_{1}}}),(D_{t_{2}},{b_{t_{2}}})\big{)}, 2. 2.

$(t^{0}_{P_{1}},t^{0}_{P_{2}})\in\mu$, $\forall\,(d_{1},d_{2})\in\mu_{t^{0}_{P_{1}},t^{0}_{P_{2}}}\;\exists\,d\in{\cal E}:d_{i}=_{b^{0}_{P_{i}}}d\;\;(i=1,2)$, 3. 3.

$\forall\,(t_{1},t_{2})\in\mu$, for each edge $t_{1}\;\mathop{\to}\limits^{\!\!a_{1}}\;t_{1}^{\prime}$, $\exists\,t^{\prime}_{2}\in T_{P_{2}}:(t^{\prime}_{1},t^{\prime}_{2})\in\mu$, $\mu_{t_{1},t_{2}}\subseteq\mu_{t^{\prime}_{1},t^{\prime}_{2}}$,

• •

if $a_{1}=d_{1}\triangleright e_{1}$ $(\triangleright\in\{?,!\})$, then $\exists\,t,t^{\prime}\in T_{P_{2}}$: $t_{2}\to t$, $t^{\prime}\to t_{2}^{\prime}$, and $\exists\,d_{2},e_{2}$: $t\;\mathop{\to}\limits^{\!\!d_{2}\triangleright e_{2}}\;t^{\prime}$, $(d_{1},d_{2})\in\mu_{t^{\prime}_{1},t^{\prime}_{2}}$, $(e_{1},e_{2})\in\mu_{t^{\prime}_{1},t^{\prime}_{2}}$,

• •

if $a_{1}\in{\cal B}$, then $t_{2}\to t^{\prime}_{2}$, 4. 4.

a condition which is symmetric to condition 3: for each pair $(t_{1},t_{2})\in\mu$, and each edge $t_{2}\;\mathop{\to}\limits^{\!\!a_{2}}\;t_{2}^{\prime}$ there is a node $t^{\prime}_{1}\in T_{P_{1}}$, such that $(t^{\prime}_{1},t^{\prime}_{2})\in\mu$, etc.

For example, processes $P_{i}\;(i=1,2)$ from (1) are observationally equivalent, because in this case $T_{P_{i}}$ has the form {\matrix{(s^{i}_{0},\top,\{c\})&\begin{picture}(20.0,18.0)\put(-5.0,3.0){\vector(1,0){30.0}} \put(9.0,8.0){\makebox(1.0,1.0)[]{\scriptstyle c,!,k_{i}(e_{i})}} \end{picture}&(s^{i},\top,\{c,k_{i}(e_{i})\})}}, and the required $\mu$ is $\{(s_{1}^{0},s_{1}),(s_{2}^{0},s_{2})\}$.

2.8 Operations on

processes

In this section we define operations on processes which can be used for a construction of complex processes from simpler ones.

2.8.1 Prefix action

$\forall\,a\in{\cal A},\;\forall\,P\in{\cal P}\quad[a]P$ is a process defined as follows:

[TABLE]

An execution of $[a]P$ can be informally understood as follows: at first the action $a$ is executed, then $[a]P$ is executed just like $P$.

2.8.2 Choice

$\forall\,P_{1},P_{2}\in{\cal P}\quad P_{1}+P_{2}$ is a process defined as follows: all states of $P_{1}$, that also belong to $S_{P_{2}}$, are replaced by fresh states, and

[TABLE]

An execution of $P_{1}+P_{2}$ can be understood as follows: at first it is selected (non-deterministically) a process $P_{i}\in\{P_{1},P_{2}\}$ which can execute its first action, and then $P_{1}+P_{2}$ is executed as the selected process.

2.8.3 Parallel composition

$\forall\,P_{1},P_{2}\in{\cal P}\;\;(P_{1},P_{2})$ is a process defined as follows: all variables in $X_{P_{1}}\setminus D^{0}_{P_{1}}$, that also belong to $X_{P_{2}}\setminus D^{0}_{P_{2}}$, are replaced by fresh variables, and

• •

$S_{(P_{1},P_{2})}\mathbin{{\mathop{=}\limits^{\mbox{\scriptsize def}}}}S_{P_{1}}\times S_{P_{2}}$, $s^{0}_{(P_{1},P_{2})}\mathbin{{\mathop{=}\limits^{\mbox{\scriptsize def}}}}(s^{0}_{P_{1}},s^{0}_{P_{2}})$,

• •

$R_{(P_{1},P_{2})}$ consists of the following transitions:

• –

$(s_{1},s_{2})\;\mathop{\to}\limits^{\!\!a}\;(s^{\prime}_{1},s_{2})$, where $(s_{1}\;\mathop{\to}\limits^{\!\!a}\;s^{\prime}_{1})\in R_{P_{1}}$, $s_{2}\in S_{P_{2}}$,

• –

$(s_{1},s_{2})\;\mathop{\to}\limits^{\!\!a}\;(s_{1},s^{\prime}_{2})$, where $s_{1}\in S_{P_{1}}$, $(s_{2}\;\mathop{\to}\limits^{\!\!a}\;s^{\prime}_{2})\in R_{P_{2}}$,

• –

{\matrix{(s_{1},s_{2})&\begin{picture}(40.0,18.0)\put(-5.0,3.0){\vector(1,0){50.0}} \put(20.0,8.0){\makebox(1.0,1.0)[]{\scriptstyle(d_{1}=d_{2})\wedge(e_{1}=e_{2})}} \end{picture}&(s^{\prime}_{1},s^{\prime}_{2})}}, where $(s_{i}\;\mathop{\to}\limits^{\!\!a_{i}}\;s^{\prime}_{i})\in R_{P_{i}}\;(i=1,2)$,

$\{a_{1},a_{2}\}=\{d_{1}!e_{1},d_{2}?e_{2}\}$ (such transition is said to be diagonal),

• •

$b^{0}_{(P_{1},P_{2})}\mathbin{{\mathop{=}\limits^{\mbox{\scriptsize def}}}}b^{0}_{P_{1}}\wedge b^{0}_{P_{2}}$, $D^{0}_{(P_{1},P_{2})}\mathbin{{\mathop{=}\limits^{\mbox{\scriptsize def}}}}D^{0}_{P_{1}}\cup D^{0}_{P_{2}}$, $H^{0}_{(P_{1},P_{2})}\mathbin{{\mathop{=}\limits^{\mbox{\scriptsize def}}}}H^{0}_{P_{1}}\sqcup H^{0}_{P_{2}}$.

An execution of $(P_{1},P_{2})$ can be understood as undeterministic interleaving of executions of $P_{1}$ and $P_{2}$: at each moment of an execution of $(P_{1},P_{2})$

• •

either one of $P_{1},P_{2}$ executes an action, and another is in waiting,

• •

or one of $P_{1},P_{2}$ sends a message, and another receives this message.

A process $(\ldots(P_{1},P_{2}),\ldots,P_{n})$ is denoted by $(P_{1},\ldots,P_{n})$.

2.8.4 Replication

$\forall\,P\in{\cal P}$ a replication of $P$ is a process $P^{\wedge}$ that can be understood as infinite parallel composition $(P,P,\ldots)$, and is defined as follows.

$\forall\,i\geq 1$ let $P_{i}$ be a process which is obtained from $P$ by renaming of variables: $\forall\,x\in X_{P}\setminus D^{0}_{P}$ each occurrence of $x$ in $P$ is replaced by the variable $x_{i}$, such that all the variables $x_{i}$ are fresh. Components of $P^{\wedge}$ have the following form:

• •

$S_{P^{\wedge}}\mathbin{{\mathop{=}\limits^{\mbox{\scriptsize def}}}}\{(s_{1},s_{2},\ldots)\mid\forall\,i\geq 1\;\;s_{i}\in S_{P}\}$, $s^{0}_{P^{\wedge}}\mathbin{{\mathop{=}\limits^{\mbox{\scriptsize def}}}}(s^{0}_{P},s^{0}_{P},\ldots)$,

• •

$\forall\,(s_{1},\ldots)\in S_{P^{\wedge}}$, $\forall\,i\geq 1$, $\forall\,(s_{i}\;\mathop{\to}\limits^{\!\!a}\;s)\in R_{P_{i}}\quad R_{P^{\wedge}}$ contains the transitions

• –

$(s_{1},\ldots)\;\mathop{\to}\limits^{\!\!a}\;\;(s_{1},\ldots,s_{i-1},s,s_{i+1},\ldots)$, and

• –

\!{\matrix{(s_{1},\ldots)&\begin{picture}(40.0,18.0)\put(-5.0,3.0){\vector(1,0){50.0}} \put(20.0,8.0){\makebox(1.0,1.0)[]{\scriptstyle(d_{1}=d_{2})\wedge(e_{1}=e_{2})}} \end{picture}&(s_{1},\ldots,s_{i-1},s,s_{i+1},\ldots,s_{j-1},s^{\prime},s_{j+1},\ldots)}}, where

$(s_{j}\;\mathop{\to}\limits^{\!\!a^{\prime}}\;s^{\prime})\in R_{P_{j}}$ for some $j\neq i$, and $\{a,a^{\prime}\}=\{d_{1}!e_{1},d_{2}?e_{2}\}$,

• •

$b^{0}_{P^{\wedge}}\mathbin{{\mathop{=}\limits^{\mbox{\scriptsize def}}}}b^{0}_{P}$, $D^{0}_{P^{\wedge}}\mathbin{{\mathop{=}\limits^{\mbox{\scriptsize def}}}}D^{0}_{P}$, $H^{0}_{P^{\wedge}}\mathbin{{\mathop{=}\limits^{\mbox{\scriptsize def}}}}\bigsqcup_{i\geq 1}H^{0}_{P_{i}}$.

2.8.5 Hiding

$\forall\,P\in{\cal P},\;\forall\,X\subseteq{\cal X}\quad P_{X}\mathbin{{\mathop{=}\limits^{\mbox{\scriptsize def}}}}(S_{P},s^{0}_{P},R_{P},b^{0}_{P},D^{0}_{P}\setminus X,H^{0}_{P}\cup X).$

If $X=\{x_{1},\ldots,x_{n}\}$, then $P_{X}$ is denoted by $P_{x_{1},\ldots,x_{n}}$.

Theorem 2. Observational congruence preserves operations of prefix action, parallel composition, replication and hiding.

2.9 A sufficient

condition of an observational equivalence

Let $P\in{\cal P}$. A labeling of states of $P$ is a set $\{(b_{s},D_{s})\mid s\in S\}$, such that

• •

$S\subseteq S_{P}$, $\forall\,s\in S\;\;b_{s}\in{\cal B}$ and $D_{s}\subseteq{\cal E}$, $s^{0}_{P}\in S$, $b_{s^{0}_{P}}=b^{0}_{P}$, $D_{s^{0}_{P}}=D^{0}_{P}$,

• •

for each transition $(s\;\mathop{\to}\limits^{\!\!a}\;s^{\prime})\in R_{P}$, if $s^{\prime}\in S$ then $s\in S$, and in this case

• –

if $a=d\triangleright e$, where $\triangleright\in\{?,!\}$, then $d\in D_{s}^{b_{s}}$, $b_{s}\leq b_{s^{\prime}}$, $D_{s}\cup\{e\}\subseteq D_{s^{\prime}}^{b_{s^{\prime}}}$,

• –

if $a\in{\cal B}$, then $b_{s}\wedge a\leq b_{s^{\prime}}$ and $D_{s}\subseteq D_{s^{\prime}}$.

$\forall\,s,s^{\prime}\in S_{P}$ the record $s\to s^{\prime}$ means that either $s=s^{\prime}$, or there is a set of thansitions of the form $s=s_{0}\;\mathop{\to}\limits^{\!\!a_{1}}\;s_{1}\;\mathop{\to}\limits^{\!\!a_{2}}\;\ldots\;\mathop{\to}\limits^{\!\!a_{m}}\;s_{m}=s^{\prime}$, where $a_{1},\ldots,a_{m}\in{\cal B}$.

Theorem 3 (a sufficient condition of an observational equivalence).

Let $P_{1},P_{2}\in{\cal P}$, where $S_{P_{1}}\cap S_{P_{2}}=\emptyset$. Then $P_{1}\approx P_{2}$, if there are a binary relation $\mu\subseteq S_{P_{1}}\times S_{P_{2}}$ and labelings $\{(b_{s},D_{s})\mid s\in S_{P_{1}}\}$, $\{(b_{s},D_{s})\mid s\in S_{P_{2}}\}$ of states of $P_{1}$ and $P_{2}$ respectively, such that

each pair $(s_{1},s_{2})\in\mu$ is associated with \mu_{s_{1}s_{2}}\in Sim\big{(}(D_{s_{1}},{b_{s_{1}}}),(D_{s_{2}},{b_{s_{2}}})\big{)}, 2. 2.

$(s^{0}_{P_{1}},s^{0}_{P_{2}})\in\mu$, and each element of the set $\mu^{0}\mathbin{{\mathop{=}\limits^{\mbox{\scriptsize def}}}}\mu_{s^{0}_{P_{1}}s^{0}_{P_{2}}}$ has the form $(x,x)$, where $x\in D^{0}_{P_{1}}\cap D^{0}_{P_{2}}$, 3. 3.

for each pair $(s_{1},s_{2})\in\mu$, and each transition $(s_{1}\;\mathop{\to}\limits^{\!\!a_{1}}\;s_{1}^{\prime})\in R_{P_{1}}$ there is a state $s^{\prime}_{2}\in S_{P_{2}}$, such that $(s^{\prime}_{1},s^{\prime}_{2})\in\mu$, $\mu_{s_{1}s_{2}}\subseteq\mu_{s^{\prime}_{1}s^{\prime}_{2}}$, and

• •

if $a_{1}$ is input or output, then $a_{1}=x\triangleright e_{1}$, where $\triangleright\in\{?,!\}$, $(x,x)\in\mu^{0}$, $\exists\,s,s^{\prime}\in S_{P_{2}}$: $s_{2}\to s$, $s^{\prime}\to s_{2}^{\prime}$, $\exists\,e_{2}$: $s\;\mathop{\to}\limits^{\!\!x\triangleright e_{2}}\;s^{\prime}$, $(e_{1},e_{2})\in\mu_{s^{\prime}_{1}s^{\prime}_{2}}$,

• •

if $a_{1}\in{\cal B}$, then $s_{2}\to s^{\prime}_{2}$, 4. 4.

a condition which is symmetric to condition 3: for each pair $(s_{1},s_{2})\in\mu$ and each transition $s_{2}\;\mathop{\to}\limits^{\!\!a_{2}}\;s_{2}^{\prime}$, $\exists\,s^{\prime}_{1}\in S_{P_{1}}:(s^{\prime}_{1},s^{\prime}_{2})\in\mu$, etc.

Theorem 4. Let $P$ be a process, $\{(D_{s},b_{s})\mid s\in S\}$ be a labelling of $P$, and $R_{P}$ has an edge $s\;\mathop{\to}\limits^{\!\!a}\;s^{\prime}$ such that $s,s^{\prime}\in S$, and $a$ has the form $d?k(e)$, where $D_{s}^{b_{s}}$ does not contain $k$ and any term of the form $k(e^{\prime})$. Then $P\approx P^{\prime}$, where $P^{\prime}$ is obtained from $P$ by removing the above edge and all unreachable (from $s_{P}^{0}$) states which appear after removing the edge.

3 Security protocols

A security protocol (SP) is a process $P\in{\cal P}$ of the form $(P_{1},\ldots,P_{n})_{X}$, where $P_{1},\ldots,P_{n}$ are processes corresponding to agents involved in the SP, and $X\subseteq{\cal X}$ is a shared secret of the agents. In this section we present an application of the proposed approach to description, specification of properties and verification of several examples of SPs, all of them are analogs of examples from [3].

3.1 A message

passing through a hidden channel

First example is a simplest SP for a message passing through a hidden channel. This SP consists of a sending of a message $x$ from an agent $a$ to an agent $b$ through a channel named $c$ (where only $a$ and $b$ know the name $c$ of this channel), $b$ receives the message and stores it in variable $y$, then $b$ behaves like a process $P$. This SP is represented by the diagram

[TABLE]

A behavior of $a$ and $b$ is represented by processes $A$ and $B$ respectively, $A\mathbin{{\mathop{=}\limits^{\mbox{\scriptsize def}}}}[c\,!\,x]\,{\bf 0}$, $B\mathbin{{\mathop{=}\limits^{\mbox{\scriptsize def}}}}[c\,?y]\,P$ (where $c\not\in P$). The SP is represented by the process $Sys\mathbin{{\mathop{=}\limits^{\mbox{\scriptsize def}}}}(A,B)_{c}$. Graph representations of processes in $Sys$ is the following:

• •

process $A$:

\qquad\begin{array}[]{llllllllllllll}\begin{picture}(110.0,0.0)\par\put(0.0,0.0){\oval(20.0,20.0)} \put(0.0,0.0){\oval(24.0,24.0)} \put(0.0,0.0){\makebox(0.0,0.0)[c]{{\scriptstyle A^{0}}}} \par\put(100.0,0.0){\oval(20.0,20.0)} \put(100.0,0.0){\makebox(0.0,0.0)[c]{{\scriptstyle A^{1}}}} \par\par\put(12.0,0.0){\vector(1,0){78.0}} \par\put(50.0,5.0){\makebox(0.0,0.0)[b]{c,!,x}} \par\end{picture}\\ \vspace{3mm}\end{array}

• •

process $B$:

\qquad\begin{array}[]{llllllllllllll}\begin{picture}(110.0,10.0)\par\put(0.0,0.0){\oval(20.0,20.0)} \put(0.0,0.0){\oval(24.0,24.0)} \put(0.0,0.0){\makebox(0.0,0.0)[c]{{\scriptstyle B^{0}}}} \par\put(100.0,0.0){\oval(20.0,20.0)} \put(100.0,0.0){\makebox(0.0,0.0)[c]{{\scriptstyle P}}} \par\par\put(12.0,0.0){\vector(1,0){78.0}} \par\put(50.0,5.0){\makebox(0.0,0.0)[b]{c,?,y}} \par\end{picture}\\ \vspace{0mm}\end{array}

(where ${\scriptstyle P}$ denotes a subgraph corresponded to the process $P$)

• •

process $(A,B)$:         

\begin{array}[]{llllllllllllll}\begin{picture}(110.0,60.0)\par\put(0.0,50.0){\oval(20.0,20.0)} \put(0.0,50.0){\oval(24.0,24.0)} \put(0.0,50.0){\makebox(0.0,0.0)[c]{{\scriptstyle A^{0}B^{0}}}} \par\put(100.0,0.0){\oval(20.0,20.0)} \put(100.0,0.0){\makebox(0.0,0.0)[c]{{\scriptstyle A^{1}P}}} \par\put(100.0,50.0){\oval(20.0,20.0)} \put(100.0,50.0){\makebox(0.0,0.0)[c]{{\scriptstyle A^{1}B^{0}}}} \par\put(0.0,0.0){\oval(20.0,20.0)} \put(0.0,0.0){\makebox(0.0,0.0)[c]{{\scriptstyle A^{0}P}}} \par\put(12.0,50.0){\vector(1,0){78.0}} \put(50.0,55.0){\makebox(0.0,0.0)[b]{c,!,x}} \par\par\put(10.0,0.0){\vector(1,0){80.0}} \put(50.0,5.0){\makebox(0.0,0.0)[b]{c,!,x}} \par\put(0.0,38.0){\vector(0,-1){28.0}} \put(-3.0,25.0){\makebox(0.0,0.0)[r]{c,?,y}} \par\put(100.0,40.0){\vector(0,-1){30.0}} \put(103.0,25.0){\makebox(0.0,0.0)[l]{c,?,y}} \par\par\put(8.5,41.5){\vector(2,-1){80.0}} \put(55.0,25.0){\makebox(0.0,0.0)[l]{y=x}} \par\par\end{picture}\\ \vspace{0mm}\end{array}

(where ${\scriptstyle A^{0}P}$ and ${\scriptstyle A^{1}P}$ denote subgraphs corresponded to copies of $P$ (nodes of these graphs are denoted by $A_{i}s$, where $i=0,1$, and $s\in S_{P}$), and the arrow from ${\scriptstyle A^{0}P}$ to ${\scriptstyle A^{1}P}$ denotes a set of corresponding transitions from $A^{0}s$ to $A^{1}s$, where $s\in S_{P}$).

On the reason of theorem 2.9, the process $(A,B)_{c}$ is observationally equivalent to the process

\qquad\begin{array}[]{llllllllllllll}\begin{picture}(110.0,14.0)\par\put(0.0,0.0){\oval(20.0,20.0)} \put(0.0,0.0){\oval(24.0,24.0)} \put(0.0,0.0){\makebox(0.0,0.0)[c]{{\scriptstyle A^{0}B^{0}}}} \par\put(100.0,0.0){\oval(20.0,20.0)} \put(100.0,0.0){\makebox(0.0,0.0)[c]{{\scriptstyle A^{1}P}}} \par\par\put(12.0,0.0){\vector(1,0){78.0}} \par\put(50.0,5.0){\makebox(0.0,0.0)[b]{y=x}} \par\end{picture}\\ \vspace{0mm}\end{array}

.

The process model allows formally describe and verify properties of integrity and secrecy of the above SP. These properties are as follows.

• •

An integrity of the SP is the following property: after a completion of the SP agent $b$ receives the same message that has been sent by agent $a$.

• •

A secrecy of the SP is the following property:

• –

for each pair $x_{1},x_{2}$ of messages, which $a$ can send $b$ by this SP, and

• –

for each two sessions of this SP, where the first session is a passing of $x_{1}$, and the second one is a passing of $x_{2}$,

any external (i.e. different from $a$ and $b$) agent, observing an execution of these sessions, is unable to extract from the observed information any knowledge about the messages $x_{1}$ and $x_{2}$: whether the messages are the same or different (unless these knowledges are not disclosed by participants $a$, $b$).

More accurately, the secrecy property can be described as follows: for any pair $x_{1},x_{2}$ of messages, which $a$ can send $b$ by an execution of this SP

• –

if for any external observer the process $[y=x_{1}]\,P$ (which describes a behavior of the agent $b$ after receiving $x_{1}$) is indistinguishable from the process $[y=x_{2}]\,P$ (which describes a behavior of $b$ after receiving $x_{2}$),

• –

then for any sessions of an execution of this SP, where the first one is a passing of $x_{1}$, and the second one is a passing of $x_{2}$, any external agent, observing the execution of these sessions, can not determine, are identical or different messages transmitted in those sessions.

A formal description and verification of the properties of integrity and secrecy of this SP is as follows.

A property of integrity is described by the proposition

[TABLE]

where $\tilde{Sys}$ describes a SP which is defined like the original SP, but with the following modification of $b$: after a receiving a message and storing it in a fresh variable $y^{\prime}$, a value of $y$ is changed on a value that $a$ sent really. A behavior of modified $b$ is described by the process $\tilde{B}\mathbin{{\mathop{=}\limits^{\mbox{\scriptsize def}}}}[c\,?y^{\prime}]\,[y=x]\,P$, and the process $\tilde{Sys}$ has the form $(A,\tilde{B})_{c}$.

Now we prove (2). The definition of operations on processes implies that

[TABLE]

that implies (2), because $y^{\prime}\not\in[y=x]\,P.\;\vrule height=7.0pt,width=7.0pt,depth=0.0pt$ 2. 2.

A property of secrecy of this SP is described by the implication

[TABLE]

Now we prove (4). The the premise of implication (4) implies the statement

[TABLE]

which is equivalent to the statement

[TABLE]

(5) and first proposition in (3) imply

[TABLE]

3.2 A SP with

a creation of a new channel

Second SP consists of a message passing from $a$ to $b$, with an assumption that a channel for this passing should be created during the execution of the SP. An auxiliary agent $t$ is used in the SP ($t$ is a trusted intermediary), and it is assumed that a name of a created channel must be known only to $a$, $b$, and $t$.

This SP is represented by the diagram

[TABLE]

A behavior of agents $a,t,b$ is represented by the processes $A$, $T$, $B$, where

[TABLE]

The SP is represented by the process $Sys\mathbin{{\mathop{=}\limits^{\mbox{\scriptsize def}}}}(A_{c},T,B)_{c_{a},c_{b}}$.

A formal description of integrity and secrecy of the SP is represented by propositions (2) and (4), where $\tilde{Sys}\mathbin{{\mathop{=}\limits^{\mbox{\scriptsize def}}}}(A_{c},T,\tilde{B})_{c_{a},c_{b}}$, $\tilde{B}\mathbin{{\mathop{=}\limits^{\mbox{\scriptsize def}}}}[c_{b}\,?\,c]\,[c\,?\,y^{\prime}]\,[y=x]\,P.$

3.3 A passing

of an encrypted message

Third example is a SP, which involves agents $a$ and $b$ having a common key $k$ (only $a$ and $b$ know $k$), $a$ and $b$ can encrypt and decrypt messages by this key using a symmetric encryption system. The SP is as follows:

• •

$a$ sends $b$ a ciphertext $k(x)$ through an open channel $c$,

• •

$b$ receives the ciphertext, decrypts it, stores the extracted message $x$ in the variable $y$, then behaves as a process $P$.

This SP is represented by the diagram       a$$b$$P$$c:k(x)      .

A behavior of agents $a$ and $b$ is represented by the processes $A$ and $B$, where $A\mathbin{{\mathop{=}\limits^{\mbox{\scriptsize def}}}}[c\,!\,k(x)]\,{\bf 0}$, $B\mathbin{{\mathop{=}\limits^{\mbox{\scriptsize def}}}}[c\,?k(y)]\,P$, and the SP is represented by $Sys\mathbin{{\mathop{=}\limits^{\mbox{\scriptsize def}}}}(A,B)_{k}$.

A formal description of the properties of integrity and secrecy of the SP is represented by (2) and (4), where $\tilde{Sys}\mathbin{{\mathop{=}\limits^{\mbox{\scriptsize def}}}}(A,\tilde{B})_{k}$, $\tilde{B}\mathbin{{\mathop{=}\limits^{\mbox{\scriptsize def}}}}[c\,?\,k(y^{\prime})]\,[y=x]\,P.$

An integrity property of the SP is proposition (2), which in this case has the form $\left([c\,!\,k(x)]\,{\bf 0},\,[c\,?k(y)]\,P\right)_{k}\approx\left([c\,!\,k(x)]\,{\bf 0},\,[c\,?k(y^{\prime})]\,[y=x]\,P\right)_{k}$, and can be proven with use of theorem 2.9. To prove the secrecy property we prove implication (4). With use of theorem 2.9 it is not so difficult to prove that (3) and the premise of implication (4) imply $Sys\approx[y=x]\,P\approx[y=x^{\prime}]\,P,$ that proves (4).

3.4

Wide-Mouth Frog

A SP Wide-Mouth Frog (WMF) is intended for a passing of an encrypted message $k(x)$ from an agent $a$ to an agent $b$ with use of a trusted agent $t$, open channels $c_{a}$, $c_{b}$, $c$, and keys $k_{a}$, $k_{b}$, $k$, where $k_{a}$ should be known only to $a$ and $t$, $k_{b}$ should be known only to $b$ and $t$, and $k$ should be known only to $a$, $b$ and $t$. This SP is represented by the diagram

[TABLE]

A behavior of agents $a,t,b$ is represented by processes $A,T,B$, where

A\mathbin{{\mathop{=}\limits^{\mbox{\scriptsize def}}}}\Big{(}[c_{a}\,!\,k_{a}(k)]\,[c\,!\,k(x)]\,{\bf 0}\Big{)}_{k},\;T\mathbin{{\mathop{=}\limits^{\mbox{\scriptsize def}}}}[c_{a}\,?\,k_{a}(k_{T})]\,[c_{b}\,!\,{k_{b}(k_{T})}]\,{\bf 0},

$B\mathbin{{\mathop{=}\limits^{\mbox{\scriptsize def}}}}[c_{b}\,?\,k_{b}(k_{B})]\,[c\,?\,k_{B}(y)]\,P.$ The SP is represented by $Sys\mathbin{{\mathop{=}\limits^{\mbox{\scriptsize def}}}}(A,T,B)_{k_{a},k_{b}}$.

A formal description of the properties of integrity and secrecy of the SP is represented by the propositions (2) and (4), where

[TABLE]

Graph representations of processes involved in $Sys$ have the following form:

• •

process $A$:

\qquad\begin{array}[]{llllllllllllll}\begin{picture}(210.0,10.0)\par\put(0.0,0.0){\oval(20.0,20.0)} \put(0.0,0.0){\oval(24.0,24.0)} \put(0.0,0.0){\makebox(0.0,0.0)[c]{A^{0}}} \par\put(100.0,0.0){\oval(20.0,20.0)} \put(100.0,0.0){\makebox(0.0,0.0)[c]{A^{1}}} \par\put(200.0,0.0){\oval(20.0,20.0)} \put(200.0,0.0){\makebox(0.0,0.0)[c]{A^{2}}} \par\put(12.0,0.0){\vector(1,0){78.0}} \put(110.0,0.0){\vector(1,0){80.0}} \par\put(50.0,5.0){\makebox(0.0,0.0)[b]{c_{a},!,k_{a}(k)}} \put(150.0,5.0){\makebox(0.0,0.0)[b]{c,!,k(x)}} \par\end{picture}\\ \vspace{0mm}\end{array}

• •

process $T$:

\qquad\begin{array}[]{llllllllllllll}\begin{picture}(210.0,20.0)\par\put(0.0,0.0){\oval(20.0,20.0)} \put(0.0,0.0){\oval(24.0,24.0)} \put(0.0,0.0){\makebox(0.0,0.0)[c]{T^{0}}} \par\put(100.0,0.0){\oval(20.0,20.0)} \put(100.0,0.0){\makebox(0.0,0.0)[c]{T^{1}}} \par\put(200.0,0.0){\oval(20.0,20.0)} \put(200.0,0.0){\makebox(0.0,0.0)[c]{T^{2}}} \par\put(12.0,0.0){\vector(1,0){78.0}} \put(110.0,0.0){\vector(1,0){80.0}} \par\put(50.0,5.0){\makebox(0.0,0.0)[b]{c_{a},?,k_{a}(k_{T})}} \put(150.0,5.0){\makebox(0.0,0.0)[b]{c_{b},!,{k_{b}(k_{T})}}} \par\end{picture}\\ \vspace{0mm}\end{array}

• •

process $B$:

\qquad\begin{array}[]{llllllllllllll}\begin{picture}(210.0,20.0)\par\put(0.0,0.0){\oval(20.0,20.0)} \put(0.0,0.0){\oval(24.0,24.0)} \put(0.0,0.0){\makebox(0.0,0.0)[c]{B^{0}}} \par\put(100.0,0.0){\oval(20.0,20.0)} \put(100.0,0.0){\makebox(0.0,0.0)[c]{B^{1}}} \par\put(200.0,0.0){\oval(20.0,20.0)} \put(200.0,0.0){\makebox(0.0,0.0)[c]{P}} \par\put(12.0,0.0){\vector(1,0){78.0}} \put(110.0,0.0){\vector(1,0){80.0}} \par\put(50.0,5.0){\makebox(0.0,0.0)[b]{c_{b},?,k_{b}(k_{B})}} \put(150.0,5.0){\makebox(0.0,0.0)[b]{c,?,{k_{B}(y)}}} \par\end{picture}\\ \vspace{0mm}\end{array}

• •

process $(A,T)$:

[TABLE]

(the diagonal transition in the diagram corresponds to a joint execution of the action $c_{a}\,!\,k_{a}(k)$ of $A$, and the action $c_{a}?\,k_{a}(k_{T})$ of $T$),

• •

process $(A,T,B)$:

A^{2}T^{0}P$$A^{1}T^{0}P$$A^{0}T^{0}P$$A^{2}T^{0}B^{1}$$A^{1}T^{0}B^{1}$$A^{0}T^{0}B^{1}$$A^{2}T^{0}B^{0}$$A^{1}T^{0}B^{0}$$A^{0}T^{0}B^{0}$$A^{2}T^{1}P$$A^{1}T^{1}P$$A^{0}T^{1}P$$A^{2}T^{1}B^{1}$$A^{1}T^{1}B^{1}$$A^{0}T^{1}B^{1}$$A^{2}T^{1}B^{0}$$A^{1}T^{1}B^{0}$$A^{0}T^{1}B^{0}$$A^{2}T^{2}P$$A^{1}T^{2}P$$A^{0}T^{2}P$$A^{2}T^{2}B^{1}$$A^{1}T^{2}B^{1}$$A^{0}T^{2}B^{1}$$A^{2}T^{2}B^{0}$$A^{1}T^{2}B^{0}$$A^{0}T^{2}B^{0}$$c_{a}!k_{a}(k)$$c!k(x)$$c?k_{B}(y)$$c_{a}!k_{a}(k)$$c!k(x)$$c?k_{B}(y)$$c?k_{B}(y)$$c_{b}?k_{b}(k_{B})$$c_{a}!k_{a}(k)$$c_{b}?k_{b}(k_{B})$$c!k(x)$$c_{b}?k_{b}(k_{B})$$k_{B}(y)=k(x)$$c_{a}!k_{a}(k)$$c!k(x)$$c?k_{B}(y)$$c_{a}!k_{a}(k)$$c!k(x)$$c?k_{B}(y)$$c?k_{B}(y)$$c_{b}?k_{b}(k_{B})$$c_{a}!k_{a}(k)$$c_{b}?k_{b}(k_{B})$$c!k(x)$$c_{b}?k_{b}(k_{B})$$k_{B}(y)=k(x)$$c_{a}!k_{a}(k)$$c!k(x)$$c?k_{B}(y)$$c_{a}!k_{a}(k)$$c!k(x)$$c?k_{B}(y)$$c?k_{B}(y)$$c_{b}?k_{b}(k_{B})$$c_{a}!k_{a}(k)$$c_{b}?k_{b}(k_{B})$$c!k(x)$$c_{b}?k_{b}(k_{B})$$k_{B}(y)=k(x)$$c_{a}?k_{a}(k_{T})$$c_{a}?k_{a}(k_{T})$$c_{a}?k_{a}(k_{T})$$c_{b}!k_{b}(k_{T})$$c_{b}!k_{b}(k_{T})$$c_{b}!k_{b}(k_{T})$$k_{B}=k_{T}$$c_{a}?k_{a}(k_{T})$$c_{a}?k_{a}(k_{T})$$c_{a}?k_{a}(k_{T})$$c_{b}!k_{b}(k_{T})$$c_{b}!k_{b}(k_{T})$$c_{b}!k_{b}(k_{T})$$k_{B}=k_{T}$$c_{a}?k_{a}(k_{T})$$c_{a}?k_{a}(k_{T})$$c_{a}?k_{a}(k_{T})$$c_{b}!k_{b}(k_{T})$$c_{b}!k_{b}(k_{T})$$c_{b}!k_{b}(k_{T})$$k_{B}=k_{T}$$k_{T}=k$$k_{T}=k$$k_{T}=k

this diagram has diagonal transitions, related to a joint execution of

• –

action $c_{b}\,!\,k_{b}(k_{T})$ of $(A,T)$, and action $c_{b}?\,k_{b}(k_{B})$ of $B$ (transitions of the form $A^{0}T^{1}B^{0}\to A^{0}T^{2}B^{1}$, $A^{1}T^{1}B^{0}\to A^{1}T^{2}B^{1}$, $A^{2}T^{1}B^{0}\to A^{2}T^{2}B^{1}$, labelled by $k_{B}=k_{T}$), and

• –

action $c\,!\,k(x)$ of $(A,T)$, and action $c?\,k_{B}(y)$ of $B$ (transitions of the form $A^{1}T^{0}B^{1}\to A^{2}T^{0}P$, $A^{1}T^{1}B^{1}\to A^{2}T^{1}P$, $A^{1}T^{2}B^{1}\to A^{2}T^{2}P$, labelled by $k_{B}(y)=k(x)$),

Process $Sys\mathbin{{\mathop{=}\limits^{\mbox{\scriptsize def}}}}(A,T,B)_{k_{a},k_{b}}$ has the same graph representation as the above process $(A,T,B)$. Its initial state is $A^{0}T^{0}B^{0}$.

First reduction of $Sys$ is based on an applying of theorem 2.9 for the cases

• •

the edge is {\matrix{A^{0}T^{0}B^{0}&\begin{picture}(20.0,18.0)\put(-5.0,3.0){\vector(1,0){30.0}} \put(9.0,8.0){\makebox(1.0,1.0)[]{\scriptstyle c_{a}?k_{a}(k_{T})}} \end{picture}&A^{0}T^{1}B^{0}}}, $D_{A^{0}T^{0}B^{0}}=\{c_{a},c_{b},c\}$, and

• •

the edge is {\matrix{A^{0}T^{0}B^{0}&\begin{picture}(20.0,18.0)\put(-5.0,3.0){\vector(1,0){30.0}} \put(9.0,8.0){\makebox(1.0,1.0)[]{\scriptstyle c_{b}?k_{b}(k_{B})}} \end{picture}&A^{0}T^{0}B^{1}}}, $D_{A^{0}T^{0}B^{0}}=\{c_{a},c_{b},c\}$.

Removing the above edges and all nodes and edges which become unreachable from $A^{0}T^{0}B^{0}$ will result the graph

A^{2}T^{0}P$$A^{1}T^{0}P$$A^{2}T^{0}B^{1}$$A^{1}T^{0}B^{1}$$A^{2}T^{0}B^{0}$$A^{1}T^{0}B^{0}$$A^{0}T^{0}B^{0}$$A^{2}T^{1}P$$A^{1}T^{1}P$$A^{2}T^{1}B^{1}$$A^{1}T^{1}B^{1}$$A^{2}T^{1}B^{0}$$A^{1}T^{1}B^{0}$$A^{2}T^{2}P$$A^{1}T^{2}P$$A^{2}T^{2}B^{1}$$A^{1}T^{2}B^{1}$$A^{2}T^{2}B^{0}$$A^{1}T^{2}B^{0}$$c!k(x)$$c!k(x)$$c?k_{B}(y)$$c?k_{B}(y)$$c_{a}!k_{a}(k)$$c_{b}?k_{b}(k_{B})$$c!k(x)$$c_{b}?k_{b}(k_{B})$$k_{B}(y)=k(x)$$c!k(x)$$c!k(x)$$c?k_{B}(y)$$c?k_{B}(y)$$c_{b}?k_{b}(k_{B})$$c!k(x)$$c_{b}?k_{b}(k_{B})$$k_{B}(y)=k(x)$$c!k(x)$$c!k(x)$$c?k_{B}(y)$$c?k_{B}(y)$$c_{b}?k_{b}(k_{B})$$c!k(x)$$c_{b}?k_{b}(k_{B})$$k_{B}(y)=k(x)$$c_{a}?k_{a}(k_{T})$$c_{a}?k_{a}(k_{T})$$c_{a}?k_{a}(k_{T})$$c_{b}!k_{b}(k_{T})$$c_{b}!k_{b}(k_{T})$$c_{b}!k_{b}(k_{T})$$k_{B}=k_{T}$$c_{a}?k_{a}(k_{T})$$c_{a}?k_{a}(k_{T})$$c_{a}?k_{a}(k_{T})$$c_{b}!k_{b}(k_{T})$$c_{b}!k_{b}(k_{T})$$c_{b}!k_{b}(k_{T})$$k_{B}=k_{T}$$k_{T}=k

This graph also can be reduced with use of theorem 2.9 for the following cases:

• •

the edge is {\matrix{A^{1}T^{0}B^{0}&\begin{picture}(20.0,18.0)\put(-5.0,3.0){\vector(1,0){30.0}} \put(9.0,8.0){\makebox(1.0,1.0)[]{\scriptstyle c_{b}?k_{b}(k_{B})}} \end{picture}&A^{1}T^{0}B^{1}}}, $D_{A^{1}T^{0}B^{0}}=\{c_{a},c_{b},c,k_{a}(k)\}$,

• •

the edge is {\matrix{A^{1}T^{1}B^{0}&\begin{picture}(20.0,18.0)\put(-5.0,3.0){\vector(1,0){30.0}} \put(9.0,8.0){\makebox(1.0,1.0)[]{\scriptstyle c_{b}?k_{b}(k_{B})}} \end{picture}&A^{1}T^{1}B^{1}}}, $D_{A^{1}T^{1}B^{0}}=\{c_{a},c_{b},c,k_{a}(k)\}$,

• •

the edge is {\matrix{A^{2}T^{0}B^{0}&\begin{picture}(20.0,18.0)\put(-5.0,3.0){\vector(1,0){30.0}} \put(9.0,8.0){\makebox(1.0,1.0)[]{\scriptstyle c_{b}?k_{b}(k_{B})}} \end{picture}&\!A^{2}T^{0}B^{1}}}, $D_{A^{2}T^{0}B^{0}}=\{c_{a},c_{b},c,k_{a}(k),k(x)\}$,

• •

the edge is {\matrix{A^{2}T^{1}B^{0}&\begin{picture}(20.0,18.0)\put(-5.0,3.0){\vector(1,0){30.0}} \put(9.0,8.0){\makebox(1.0,1.0)[]{\scriptstyle c_{b}?k_{b}(k_{B})}} \end{picture}&\!A^{2}T^{1}B^{1}}}, $D_{A^{2}T^{1}B^{0}}=\{c_{a},c_{b},c,k_{a}(k),k(x)\}$.

Removing the above edges and all nodes and edges which become unreachable from $A^{0}T^{0}B^{0}$ will result to the graph

[TABLE]

Third step of reduction is based on a use of theorem 2.9. It is not so difficult that there is a labelling for the process presented by the above graph:

\left\{\begin{array}[]{llllllllllllll}D_{A^{0}T^{0}B^{0}}=\{c_{a},c_{b},c\},\\ D_{A^{1}T^{0}B^{0}}=D_{A^{1}T^{1}B^{0}}=\{c_{a},c_{b},c,k_{a}(k)\}\\ D_{A^{2}T^{0}B^{0}}=D_{A^{2}T^{1}B^{0}}=\{c_{a},c_{b},c,k_{a}(k),k(x)\}\\ D_{A^{1}T^{2}B^{0}}=D_{A^{1}T^{2}B^{1}}=D_{A^{1}T^{2}B^{2}}=\{c_{a},c_{b},c,k_{a}(k),k_{b}(k_{T})\},\\ D_{A^{2}T^{2}B^{0}}=D_{A^{2}T^{2}B^{1}}=D_{A^{2}T^{2}P}=\{c_{a},c_{b},c,k_{a}(k),k_{b}(k_{T}),k(x)\},\end{array}\right.

\left\{\begin{array}[]{llllllllllllll}b_{A^{0}T^{0}B^{0}}=b_{A^{1}T^{0}B^{0}}=b_{A^{2}T^{0}B^{0}}=\top,\\ b_{A^{1}T^{1}B^{0}}=b_{A^{2}T^{1}B^{0}}=b_{A^{1}T^{2}B^{0}}=b_{A^{2}T^{2}B^{0}}=(k=k_{T}),\\ b_{A^{1}T^{2}B^{1}}=b_{A^{2}T^{2}B^{1}}=(k=k_{T})\wedge(k_{T}=k_{B}),\\ b_{A^{2}T^{2}P}=(k=k_{T})\wedge(k_{T}=k_{B})\wedge(x=y).\end{array}\right.

On the reason of theorem 2.9, the edge {\matrix{A^{1}T^{2}B^{1}&\begin{picture}(20.0,18.0)\put(-5.0,3.0){\vector(1,0){30.0}} \put(9.0,8.0){\makebox(1.0,1.0)[]{\scriptstyle c?k_{B}(y)}} \end{picture}&A^{1}T^{2}P}} in the last diagram can be removed, because $b_{A^{1}T^{2}B^{1}}\leq(k_{B}=k)$, and $(k\in D_{A^{1}T^{2}B^{1}})=\bot$.

The result of such removing is the process below:

[TABLE]

It is not so difficult to prove that the property $b_{A^{2}T^{2}P}\leq(x=y)$ and the equivalence $[y=x]\,[y=x]\,P\approx[y=x]\,P$ imply $Sys\approx\tilde{S}ys$.

The secrecy property is a direct consequence of the integrity property.