# A Distributed Process Model of Cryptographic Protocols

Andrew M. Mironov

Moscow State University, Faculty of Mechanics and Mathematics,
Russia, 119991, Moscow, GSP-1, 1 Leninskiye Gory

Innopolis University, Leading Research Centre,
Russia, 420500, Innopolis, 1 Universitetskaya

<EMAIL_ADDRESS>)

###### Abstract

Cryptographic Protocols (CP) are distributed algorithms intended for secure
communication in an insecure environment. They are used, for example, in
electronic payments, electronic voting procedures, systems of confidential
data processing, etc. Errors in CPs can bring to great financial and social
damage, therefore it is necessary to use mathematical methods to substantiate
the correctness and safety of CPs. In this paper, a distributed process model
of CPs is presented, which allows one to formally describe CPs and their
properties. It is shown how to solve the problems of verification of CPs on
the base of this model.

Keywords: cryptographic protocols, sequential processes, distributed
processes, verification

##  1 Introduction

###  1.1 A concept of a cryptographic protocol

A cryptographic protocol (CP) is a distributed algorithm that describes an
order in which messages are exchanged between communicating agents. Examples
of such agents are computer systems, bank cards, people, etc.

To ensure security properties of CPs (for example, integrity and
confidentiality of transmitted data), cryptographic transformations are used
in CPs (encryption and decryption, hash functions, etc.). We assume that the
cryptographic transformations used in CPs are ideal, i.e. satisfy some axioms
expressing, for example, the impossibility of extracting plain texts from
ciphertexts without knowing the corresponding cryptographic keys.

###  1.2 Vulnerabilities in cryptographic protocols

Many vulnerabilities in CPs are induced not by insufficient qualities of
cryptographic primitives used in CPs, but by logical errors in CPs. The most
striking example of a vulnerability in a CP is a vulnerability in the Needham-
Schroeder Public Key Authentication CP [78NS]. This CP was published in 1978,
and a logical error in this CP was discovered [95L] more than 16 years after
the start of the use of this CP. This error was related with the possibility
of dishonest behavior of participants of this CP. The peculiarity of this
error is that this CP is extremely simple, consisting of only three actions,
and in a visual analysis of this CP, the absence of errors in this CP did not
raise any doubts. The error was discovered with use of an automated
verification tool. Another example (taken from [14CK]) is the following: in
the CP, logging into the Google portal, which allows a user to identify
himself only once, and then access various applications (such as Gmail or
Google calendar), a logic error has been detected that allows a dishonest
service provider to impersonate any of its users to another service provider.
There are many other examples of CPs (see for example [81DS], [87NS], [95AN]
[08CJSTW]), in which vulnerabilities of the following types were found:

  * •

participants of these CPs can receive corrupted messages as a result of
interception and distortion of transmitted messages by an adversary, which
violates the integrity property of the transmitted messages,

  * •

an adversary can find out the secret information contained in the intercepted
messages, as a result of that the confidentiality property of the transmitted
messages is violated.

There are also examples of vulnerabilities in CPs used for authentication to
mobile phone providers, for withdrawing money from ATMs, for working with
electronic passports, conducting electronic elections, etc.

All these examples justify that in safety-critical systems there is not enough
an informal analysis of required security properties of CPs used in them, it
is necessary to build mathematical models of analyzed CPs and prove that the
models satisfy (or do not satisfy) their properties, the procedure for
constructing such proofs is called a verification of CPs.

In this work, a distributed process model of CPs is constructed. In terms of
this model it is possible to express properties of CPs such as integrity and
confidentiality of transmitted messages, and authentication of participants of
CPs. We present new verification methods of CPs based on this model.

###  1.3 An overview of methods of modeling and verification of cryptographic
protocols

The books [11CK] and [12CM] contain overviews of the most widely used methods
for modeling and verification of CPs. The main classes of models of CPs and
approaches to verification of CPs are the following.

  1. 1.

Logical models.

This class of models was the very first approach to modeling and verification
of CPs. On the base of this class of models, the problem of verification of
CPs is reduced to the problem of constructing proofs of theorems (in some
logical calculi) that CPs being analyzed have given properties. In the work
[90BAN], the first mathematical model of CPs (called BAN logic) was presented.
This model has limitations: it assumes that participants of analyzed CPs are
honest, i.e. exactly fulfill their requirements. In addition, this model does
not allow analyzing CPs with unlimited generation of sessions. The BAN logic
approach was developed in works [90GNY], [91AT], [93vO] [93SM], [94KMM],
[96SvO], [02SW], etc. An important class of logical calculi for CP modeling
and verification is the Protocol Composition Logic, see [01DMP], [07DDMR],
[08C], [11DMRS], etc.

One of the classes of CP logical models is associated with logical
programming. In these models, CPs are represented in the form of term
rewriting rules, Horn clauses and constraint systems. This approach is
described in [01B], [05AB], [14CK], etc.

An important class of logical methods for CP modeling and verification is the
Paulson’s inductive method: [97P], [98P], [99P], [00B], etc.

  2. 2.

Models based on process algebra.

The source of this class of models is Milner’s fundamental work [80M] and its
continuation [99M]. In these works, a model of communicating processes is
constructed, in which processes are represented by terms. An observational
equivalence on these terms allows to express various properties of processes
related to security (in particular, secrecy and anonymity). First work, which
expounds a CP model based on Milner’s approach, is [99AG]. Among other works
related to this direction, it should be noted [00RS], [01AF], [05KR], [07ABF],
[11RS], [16ABF], [16B], [17CW], [21CDS].

  3. 3.

Models based on CSP.

CSP (Communicating Sequential Processes) is a mathematical approach developed
by Hoare [85H] and intended for modeling and verification of distributed
communicating processes. On the basis of this approach, a method for CP
modeling and verification is built, which is most fully described in the book
[00RSGLR]. Deductive CP verification method based on this approach uses the
concept of a rank function. Among the works related to this direction, it
should be noted [96SS], [96S], [97LR], [97DS], [98S], [21RCSSS].

  4. 4.

Models based on strand spaces.

Strand spaces allow to represent processes related to an execution of a CP in
the form of graphical objects (called strands), which indicate dependencies
between actions of participants of the CP. Among the works related to CP
modeling and verification based on strand spaces approach, it should be noted
[98THG1], [98THG2], [99THG1], [99THG2], [00GT2], [02GT], [05CDLMS], [07DGT1],
[07DGT2], [07DGT3], [12G], [13LP], [16YEMM].

###  1.4 A comparison of the proposed model of cryptographic protocols with
other models

A distributed process model of CPs presented in this paper inherits the most
essential qualities of models from the above classes.

  * •

In this model, CPs are represented in the form of distributed processes (DPs).
Each DP is a set of communicating sequential processes (SPs), where SPs are
models of participants of CPs communicating by asynchronous message passing.

  * •

Typically, these SPs are sequences of actions that can be graphically
represented as strands, and an execution of the entire CP can be represented
as a strand space, where strands are connected by edges representing sending
and receiving of messages, see for example (68), (95).

  * •

Properties of CPs can be represented by logical formulas, which can be
substantiated using algorithms of logical inference. In section 3.1 we present
an inference algorithm related to the introduced model of CPs.

  * •

Some of properties of CPs (for example, a property of anonymity in CPs of
e-voting or e-commerce) can be expressed as an observational equivalence
between the corresponding DPs (section 2.3.4), similarly to how it is done in
CP models based on process algebra.

Main advantages of the proposed distributed process model are the following.

  1. 1.

Proofs of CP correctness properties based on this model are much shorter and
simpler than proofs of these properties based on other CP models. To
substantiate this statement, we give examples of verification of two CPs:
Yahalom [00RSGLR] and a CP of message transmission with unlimited number of
participants taken from [99AG]. Verification of these CPs in the above sources
takes several dozen pages, while verification of the Yahalom CP based on the
proposed model (items 3.2.3, 3.2.4, 3.2.5) takes less than 4 pages, and
verification of the second CP (item 3.3.2) - less than 3 pages. In addition,
the analysis of the proofs of the correctness of the CPs shows that these
proofs are produced according to a template method and can be generated
automatically.

  2. 2.

If a CP consists of a finite number of components without cycles, then a
verification of such CP can be carried out completely automatically. The
method of verification of such CPs is based on the concept of a transition
graph (TG) introduced in section 2.7. An application of this method is shown
on four examples of CPs (sections 3.1.4, 3.1.5, 3.1.7, 3.1.8) taken from
[99AG]. A verification of the CPs in [99AG] is a non-trivial mathematical
reasoning, while in the present work the CPs are verified by a standard
calculating of formulas related to nodes of TGs.

  3. 3.

The language for describing DPs introduced in this paper makes it possible to
construct such models of CPs that are substantially similar to the original
CPs. This is essential when a flaw in a model of an analyzed CP is found, and
it is necessary to correct the CP in such a way as to eliminate this flaw: for
an elimination of the detected flaw

     * •

the model of this CP can first be corrected,

     * •

which is then easily converted to a correction of the original CP.

The language for describing DPs introduced in this paper can be considered as
a new language for describing distributed algorithms.

##  2 Sequential and distributed processes

In this section, we introduce concepts of sequential and distributed
processes. A sequential process is a model of a CP participant, and a
distributed process is a model of the entire CP. The proposed model is a
theoretical basis for CP verification methods described in section 3.

###  2.1 Auxiliary concepts

####  2.1.1 Types, constants, variables, function symbols

We assume that there are given sets $Types$, $Con$, ${\it{\it Var}}$ and
$Fun$, elements of which are called types, constants, variables, and function
symbols (FSs), respectively. Each element $x$ of $Con$, ${\it Var}$ and $Fun$
is associated with a type $\tau(x)\in Types$, and if $x\in Fun$, then
$\tau(x)$ has the form

$(\tau_{1},\ldots,\tau_{n})\to\tau,\quad\mbox{where
}\tau_{1},\ldots,\tau_{n},\tau\in Types.$

####  2.1.2 Terms

In this section we define a set of $Tm$ of terms, which are intended to
describe messages sent during the execution of a CP. The set $Tm$ is defined
inductively. Each term $e$ is associated with a type $\tau(e)\in Types$. The
definition of a term is as follows:

  * •

$\forall\,x\in Con\cup{\it Var}\;\;x$ is a term of the type $\tau(x)$,

  * •

if $f\in Fun$, $e_{1},\ldots,e_{n}$ are terms, and

$\tau(f)=(\tau(e_{1}),\ldots,\tau(e_{n}))\to\tau,$

then $f(e_{1},\ldots,e_{n})$ is a term of the type $\tau$.

We will use the following notation: $\forall\,e\in Tm$,
$\forall\,X\subseteq{\it Var}$, $\forall\,E\subseteq Tm$, and
$\forall\,\tau\in Types$

  * •

${\it Var}({e})=\\{x\in Var\mid x\mbox{ occurrs in }e\\}$,

  * •

$Tm(X)=\\{e\in Tm\mid{\it Var}(e)\subseteq X\\}$,

  * •

$E_{\bf X}=E\cap Var$, and

  * •

$E_{\tau}=\\{e\in E\mid\tau(e)=\tau\\}$.

Let $e,e^{\prime}\in Tm$. Term $e$ is said to be a subterm of the term
$e^{\prime}$, if either $e=e^{\prime}$, or $e^{\prime}=f(e_{1},\ldots,e_{n})$,
where $f\in Fun$, and $\exists\,i\in\\{1,\ldots,n\\}$: $e$ is a subterm of
$e_{i}$. Notation $e\subseteq e^{\prime}$, where $e,e^{\prime}\in Tm$, means
that $e$ is a subterm of $e^{\prime}$. Notation $e\subset e^{\prime}$, where
$e,e^{\prime}\in Tm$, means that $e\subseteq e^{\prime}$ and $e\neq
e^{\prime}$.

By induction on the structure of a term $e\in Tm$ it is easy to prove that

$\begin{array}[]{llllllllllllll}\mbox{if $e_{1},e_{2}$ are different subterms
of $e$,}\\\ \mbox{then either $e_{1}\subset e_{2}$, or $e_{2}\subset e_{1}$,
or $e_{1}$, $e_{2}$ }\\\ \mbox{have no common components.}\end{array}$ (1)

Notation $x\in e$, where $x\in Var,e\in Tm$ denotes that $x\subseteq e$.

For each considered function $f:E\to E^{\prime}$, where $E,E^{\prime}\subseteq
Tm$, we assume that

$\forall\,e\in E\;\;\tau(f(e))=\tau(e)$

####  2.1.3 Examples of types

We assume that $Types$ contains the following types:

  * •

A, terms of this type are called agents,

  * •

C, terms of this type are called channels, they denote communication channels
through which agents communicate with each other by message passing,

  * •

K, terms of this type are called keys, they denote cryptographic keys that
agents can use to encrypt or decrypt messages,

  * •

M, terms of this type are called messages, they denote messages that agents
can send to each other during their execution,

  * •

N, terms of this type are called nonces, they denote variables with unique
values (nonce = “number only used once”),

  * •

P, terms of this type are called processes.

We use the following notations and conventions:

  * •

${\bf M}$ includes all other types from $Types$, i.e. a term of any type is
also a term of type ${\bf M}$,

  * •

$Var_{\bf C}$ contains a variable denoted by $\circ$ and called an open
channel,

  * •

$\forall\,n\geq 1,\forall\,\tau\in Types$ the set $Types$ contains type
$\tau_{n}$, whose values are $n$–tuples consisting of terms of the type
$\tau$.

####  2.1.4 Examples of function symbols

We assume that $Fun$ contains the following FSs.

  * •

FSs $encrypt$ and $decrypt$ of the type

$({\bf K},{\bf M})\to{\bf M}.$

Terms $encrypt(k,e)$ and $decrypt(k,e)$ denote messages obtained by encrypting
(and decrypting, respectively) the message $e$ on the key $k$. Term
$encrypt(k,e)$ is denoted by $k(e)$, and is called an encrypted message (EM).

  * •

FSs $shared\\_key$ of the type

${\bf A}_{n}\to{\bf K},\mbox{ where }n\geq 2.$

Term $shared\\_key(A_{1},\ldots,A_{n})$ is called a shared key of agents
$A_{1}$, $\ldots$, $A_{n}$ and is denoted by $k_{A_{1}\ldots A_{n}}$.

  * •

FSs $shared\\_channel$ of the type

${\bf A}_{n}\to{\bf C},\mbox{ where }n\geq 2.$

Term $shared\\_channel(A_{1},\ldots,A_{n})$ is called a shared channel of
agents $A_{1}$, $\ldots$, $A_{n}$ and is denoted by $c_{A_{1}\ldots A_{n}}$.

We will use the following notation: $\forall\,e\in Tm$

$Keys(e)=\\{k\in Var_{\bf K}\mid\exists\,e^{\prime}\in
Tm:k(e^{\prime})\subseteq e\\}.$

####  2.1.5 Expressions

In this section we define a set $Expr$ of expressions, where each expression
describes a set of terms. Such a set can be a set of terms that are currently
available to some process, or a set of messages that are currently in a
channel.

An expression is a notation of one of the following forms:

  * •

$E$, where $E\subseteq Tm$,

  * •

$[P]$ and $[c]$, where $P\in Var_{\bf P}$, $c\in Tm_{\bf C}$,

  * •

$k^{-1}(E)$, where $k\in Tm_{\bf K}$, and $E\in Expr$,

  * •

$E\cap E^{\prime}$, $E\cup E^{\prime}$, where $E,E^{\prime}\in Expr$.

$\forall\,E\in Expr\;\;{\it Var}({E})$ is a set of all variables occurred in
$E$.

Expressions $k^{-1}([P])$ and $k^{-1}([c])$ are denoted by $k^{-1}[P]$ and
$k^{-1}[c]$ respectively. Expressions $\\{e\\}$, where $e\in Tm$, are denoted
without braces.

####  2.1.6 Formulas

In this section we define a set $Fm$ of formulas, which are intended to
describe properties of sets of terms. In this definition, a concept of
elementary formula (EF) is used, which is a notation of one of the following
forms:

  1. 1.

$e\in E$, $E=E^{\prime}$, $E\subseteq E^{\prime}$, $E\supseteq E^{\prime}$,
where $e\in Tm$, $E,E^{\prime}\in Expr$,

  2. 2.

$E\,\bot_{\bf C}\,P$, $E\,\bot_{\bf K}\,P$, where $E\subseteq Tm,P\in Var_{\bf
P}$,

  3. 3.

$at_{P}=i$, where $P\in Var_{\bf P}$, $i\in\\{0,1,\ldots\\}$.

EFs express properties of values of expressions occurred in them. An example
of a EF is

$decrypt(k,k(e))=e,\;\mbox{where $k\in{\it Tm}_{\bf K},e\in Tm.$}$

A formula is a set of EFs. Each formula $\varphi=\\{\varphi_{i}\mid i\in I\\}$
expresses a statement that is a conjunction of statements expressed by EFs
$\varphi_{i}\;\;(i\in I)$.

$\forall\,\varphi\in Fm$ the set of all variables occurred in $\varphi$ is
denoted by ${\it Var}(\varphi)$.

$\forall\,\varphi_{1}$, $\ldots$, $\varphi_{n}\in Fm$, the formula
$\varphi_{1}\cup\ldots\cup\varphi_{n}$ is denoted by
$\\{\varphi_{1},\ldots,\varphi_{n}\\}$.

A formula
$\\{E_{0}\rho_{1}E_{1},E_{1}\rho_{2}E_{2},\ldots,E_{n-1}\rho_{n}E_{n}\\}$,
where $\rho_{1}$, $\ldots$, $\rho_{n}$ are symbols from $\\{=,\subseteq\\}$,
is denoted by $E_{0}\rho_{1}E_{1}\rho_{2}\ldots\rho_{n}E_{n}$.

####  2.1.7 Bindings

A binding is a function $\theta:{\it Var}\to Tm$. We say that $\theta$ binds a
variable $x\in{\it Var}$ with term $\theta(x)$.

We use the following notation:

  * •

the set of all bindings is denoted by $\Theta$,

  * •

$id$ denotes identical binding:

$\forall\,x\in{\it Var}\;\;id(x)=x,$

  * •

$\forall\,X\subseteq{\it Var}$
$\Theta(X)=\\{\theta\in\Theta\mid\forall\,x\in{\it Var}\setminus
X\;\;\theta(x)=x\\},$

  * •

a binding $\theta\in\Theta$ can be denoted by

$x\mapsto\theta(x)\;\mbox{or}\;(\theta(x_{1})/x_{1},\ldots,\theta(x_{n})/x_{n}),$
(2)

second notation in (2) is used when
$\theta\in\Theta({\\{x_{1},\ldots,x_{n}\\}})$,

  * •

$\forall\,\theta\in\Theta,\;\forall\,e\in Tm$ $e^{\theta}$ denotes a term
obtained from $e$ by replacing $\forall\,x\in{\it Var}(e)$ each occurrence of
$x$ in $e$ by the term $\theta(x)$, the term $e$ is called a template of
$e^{\theta}$ with respect to $\theta$,

  * •

$\forall\,\theta\in\Theta,\;\forall\,E\subseteq Tm$ the set $\\{e^{\theta}\mid
e\in E\\}$ is denoted by $E^{\theta}$,

  * •

$\forall\,\theta,\theta^{\prime}\in\Theta$ the binding
$x\mapsto(x^{\theta})^{\theta^{\prime}}$ is denoted by
$\theta\theta^{\prime}$.

If $X\subseteq X^{\prime}\subseteq Var$, $\theta\in\Theta(X)$,
$\theta^{\prime}\in\Theta(X^{\prime})$, and $\forall\,x\in
X\;\;\theta(x)=\theta^{\prime}(x)$, then $\theta^{\prime}$ is said to be an
extension of $\theta$.

###  2.2 Sequential processes

####  2.2.1 Actions

Actions are notations of the following forms:

$\begin{array}[]{llllllllllllll}c!e,\;c?e,\;e:=e^{\prime},\;\mbox{where
}\;c\in Tm_{\bf C},\;e,e^{\prime}\in Tm,\end{array}$

which is called a sending $e$ to $c$, a receiving $e$ from $c$, and an
assignment, respectively.

The set of all actions is denoted by $Act$.

$\forall\,\alpha\in{Act}$ the set of all variables occurred in $\alpha$ is
denoted by ${\it Var}({\alpha})$.

If $\theta\in\Theta$, $\alpha\in Act$, then $\alpha^{\theta}$ denotes the
action $c^{\theta}!e^{\theta}$, $c^{\theta}?e^{\theta}$ and
$e^{\theta}:=(e^{\prime})^{\theta}$, if $\alpha=$ $c!e$, $c?e$ and
$e:=e^{\prime}$, respectively.

Actions can be written in round parentheses:
$(c!e)$, $(c?e)$, $(e=e^{\prime})$.

####  2.2.2 A concept of a sequential process

A sequential process (SP) is a 4-tuple $(P,A,X,\bar{X})$, whose components
have the following meanings:

  * •

$P$ is a graph with a selected node (called an initial node, and denoted by
$Init(P)$), each edge of which is labeled by some action,

  * •

$A$ is an agent associated with this SP,

  * •

$X\subseteq{\it Var}$ is a set of initialized variables,

  * •

$\bar{X}\subseteq X$ is a set hidden variables, they denote secret keys,
hidden channels, or nonces, these variables are initialized with unique
values.

A SP is a description of a behavior of a system, a work of which consists of
sending or receiving messages, and an initialization of uninitialized
variables.

For each SP $(P,A,X,\bar{X})$

  * •

this SP can be denoted by the same notation $P$ as its graph, the set of nodes
of the graph $P$ is also is denoted by $P$,

  * •

$Agent(P)$, $X(P)$, $\bar{X}(P)$ denote corresponding components of $P$,

  * •

${\it Var}(P)$ is a set of all variables occurred in $P$,

  * •

$\tilde{X}(P)=X(P)\setminus\bar{X}(P)$,

  * •

$\hat{X}(P)=Var(P)\setminus X(P)$.

Each SP is associated with a variable of the type P, called a name of this SP.
We will denote names of SPs by the same notations as the SPs.

If $P$ has no edges and $X(P)=\emptyset$, then $P$ is denoted by 0.

Actions of the form $\circ!e$ and $\circ?e$ will be abbreviated as $!e$ and
$?e$ respectively.

####  2.2.3 A state of a sequential process

A state of a SP $P$ is a 5-tuple

$s=(at,\alpha,[P],\theta,\\{[c]\mid c\in Tm_{\bf C}\\}),$

where

  * •

$at\in P$ is a node of the graph $P$ in $s$,

  * •

$\alpha\in\\{init\\}\sqcup Act$ is an action before transition to $s$,

  * •

$[P]\subseteq{\it Var}$ is a set of initialized variables in $s$,

  * •

$\theta\in\Theta([P])$ is a binding in $s$, and

  * •

$\forall\,c\in Tm_{\bf C}\;\;[c]\subseteq Tm$ is a content of the channel $c$
in $s$.

The components of $s$ are denoted by $at_{s}$, $\alpha_{s}$, $[P]_{s}$,
$\theta_{s}$, $[c]_{s}$ respectively.

The set $Tm([P]_{s})$ is denoted by $\langle P\rangle_{s}$.

A state of SP $P$ is said to be initial, and is denoted by $0_{P}$, if it has
the form

$(Init(P),init,X(P),id,\\{\emptyset\mid c\in Tm_{\bf C}\\}).$

####  2.2.4 Values of expressions and formulas in states

Let $P$ be a SP, $s$ be a state of $P$, $E\in Expr$, and $\varphi\in Fm$.

The notation $E^{s}$ denotes a set of terms, called a value of $E$ in $s$, and
defined as follows:

  * •

$\forall\,E\subseteq Tm\quad E^{s}=\\{e^{\theta_{s}}\mid e\in E\\}$,
$\forall\,e\in Tm$ the set $\\{e\\}^{s}$, and the only element of this set, is
denoted by $e^{s}$,

  * •

$[P]^{s}=([P]_{s})^{s}$, $\langle P\rangle^{s}=(\langle P\rangle_{s})^{s}$,
$[c]^{s}=[{c^{s}}]_{s}$, where $P\in Var_{\bf P}$, $c\in Tm_{\bf C}$,

  * •

$k^{-1}(E)^{s}=\\{e\in Tm\mid\exists\,e^{\prime}\in E^{s}:k^{s}(e)\subseteq
e^{\prime}\\}$,

  * •

$(E\cap E^{\prime})^{s}=E^{s}\cap(E^{\prime})^{s}$, $(E\cup
E^{\prime})^{s}=E^{s}\cup(E^{\prime})^{s}$.

The notation $s\models\varphi$ denotes the statement

$\varphi$ holds at $s$.

This statement is true if $Var(\varphi)_{\bf P}\subseteq\\{P\\}$, and one of
the following conditions holds:

  * •

$\varphi$ has the form

$(e\in E),(E=E^{\prime}),(E\subseteq E^{\prime}),\mbox{ or }(E\supseteq
E^{\prime}),$

where $e\in Tm$, $E,E^{\prime}\in Expr$, and

$e^{s}\in
E^{s},\;E^{s}=(E^{\prime})^{s},\;E^{s}\subseteq(E^{\prime})^{s},\;E^{s}\supseteq(E^{\prime})^{s},$

respectively,

  * •

$\varphi=(E\,\bot_{\bf C}\,P),\;\forall\,e\in E^{s}\;\;Agent(P)\not\in e$, and

$\left.\begin{array}[]{llllllllllllll}\forall\,x\in E^{s}_{\bf
X},\forall\,y\in[P]_{s}\;\;x\not\in y^{s}\\\ \forall\,x\in E^{s}_{\bf
X},\forall\,c\in Tm_{\bf C}\\\ \hskip 8.53581pt\mbox{ if
}\exists\,e\in[c]_{s}:x\in e,\mbox{ then }c\in E^{s}\end{array}\right\\}$ (3)

(3) can be interpreted as the statement: each variable from $E^{s}_{\bf X}$

    * –

is not occurred in terms available to $P$ in the state $s$, and

    * –

is occurred in terms from the content of only those channels that are not
available for $P$,

  * •

$\varphi=(E\,\bot_{\bf K}\,P)$, $\forall\,e\in E^{s}\;\;Agent(P)\not\in e$,
and

$\left.\begin{array}[]{llllllllllllll}\forall\,x\in E^{s}_{\bf
X},\,\forall\,y\in[P]_{s}\;\;x\,\bot_{{\bf K},E}\,y^{s}\\\ \forall\,x\in
E^{s}_{\bf X},\,\forall\,c\in Tm_{\bf C},\forall\,e\in[c]_{s}\\\ \hskip
113.81102ptx\,\bot_{{\bf K},E}\,e\end{array}\right\\}$ (4)

where $x\,\bot_{{\bf K},E}\,e$ means that

$\begin{array}[]{llllllllllllll}\mbox{each occurrence of $x$ in $e$ }\\\
\mbox{is contained in a subterm }\\\ \mbox{$k(\ldots)\subseteq e$, where $k\in
E^{s}_{\bf K}$}\end{array}$ (5)

(4) can be interpreted as the statement: variables from $E^{s}_{\bf X}$ are
occurred

    * –

in terms available to $P$ in the state $s$, and

    * –

in terms from a content of any channel,

in a “secure” form, i.e. are occurred in subterms of the form $k(\ldots)$,
where $k\in E^{s}_{\bf K}$,

  * •

$\varphi=(at_{P}=i)$, and $at_{s}=i$,

  * •

$\varphi=\\{\varphi_{i}\mid i\in I\\}$, and $\forall\,i\in
I\;\;s\models\varphi_{i}$.

####  2.2.5 An execution of a sequential process

An execution of a SP $P$ is a walk in the graph $P$, starting from $Init(P)$,
with an execution of actions that are labels of passed edges. Each step of the
execution is associated with a state $s$ of $P$, called a current state of $P$
at this step (a current state at first step is $0_{P}$). If a step of the
execution is not final, then the current state $s$ is replaced by the state
$s^{\prime}$, which will be a current state at the next step of the execution,
for this

  1. 1.

either an edge e outgoing from $at_{s}$ is selected, whose label $\alpha$ has
the following properties:

     * •

if $\alpha^{\theta_{s}}$ contains a subterm $shared\\_key(\ldots)$ or
$shared\\_channel(\ldots)$, then $Agent(P)$ occurs in this subterm,

     * •

one of the following conditions holds:

$\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\left.\begin{array}[]{llllllllllllll}({\rm
a})&\alpha=c!e,\;c,e\in\langle P\rangle_{s}\\\ ({\rm
b})&\alpha=c?e,\;c\in\langle P\rangle_{s},\\\ &\hskip
8.53581ptKeys(e^{s})\subseteq[P]_{s},\\\ &\hskip
8.53581pt\exists\,\theta\in\Theta({{\it
Var}(e)\setminus[P]_{s}}):(e^{\theta})^{s}\in[c]^{s}\\\ ({\rm
c})&\alpha=(e:=e^{\prime}),\;e^{\prime}\in\langle P\rangle_{s},\\\ &\hskip
8.53581ptKeys(e^{s})\subseteq[P]_{s},\\\ &\hskip
8.53581pt\exists\,\theta\in\Theta({{\it
Var}(e)\setminus[P]_{s}}):e^{\theta}=e^{\prime}\end{array}\\!\\!\\!\right\\}$
(6)

and $s^{\prime}$ is defined as follows: $at_{s^{\prime}}$ is an end of the
edge e, $\alpha_{s^{\prime}}=\alpha$, and

     * •

if (a) in (6) holds, then

$\begin{array}[]{llllllllllllll}[P]_{s^{\prime}}=[P]_{s},\theta_{s^{\prime}}=\theta_{s},\\\
\,[c^{s}]_{s^{\prime}}=[c^{s}]_{s}\cup\\{e^{s}\\},\\\ \forall\,c^{\prime}\in
Tm_{\bf
C}\setminus\\{c^{s}\\}\;\;[c^{\prime}]_{s^{\prime}}=[c^{\prime}]_{s},\end{array}$

     * •

if (b) or (c) in (6) holds, then

$\begin{array}[]{llllllllllllll}[P]_{s^{\prime}}=[P]_{s}\cup{\it
Var}(e),\theta_{s^{\prime}}=\theta\theta_{s},\\\ \forall\,c^{\prime}\in
Tm_{\bf C}\;\;[c^{\prime}]_{s^{\prime}}=[c^{\prime}]_{s},\end{array}$

(we say that each $x\in{\it Var}(e)\setminus[P]_{s}$ is initialized with the
value $x^{\theta_{s^{\prime}}}$ in the transition from $s$ to $s^{\prime}$),

  2. 2.

or all components of $s^{\prime}$, with the exception of the last component,
are equal to the corresponding components of $s$, and $\forall\,c\in Tm_{\bf
C}$ the set $[c]_{s^{\prime}}$ either is equal to $[c]_{s}$, or is obtained by
adding a term to $[c]_{s}$ as a result of an execution of a step by another
SP.

If first (second) of the above situations takes place, then we say that
$s^{\prime}$ is obtained by an active (passive, respectively) transition from
$s$, and denote this by
$s\;\mathop{\to}\limits^{\begin{picture}(0.0,5.0)\put(-3.0,2.0){\makebox(0.0,1.0)[]{$\scriptstyle
P$}} \end{picture}}\;s^{\prime}$ ($s\to s^{\prime}$, respectively).

Variables in ${\it Var}({P})$ have the following features: $\forall\,x\in{\it
Var}({P})$

  * •

if $x\in X(P)$ (or $x\in\hat{X}({P})$), then $x$ is initialized (or not
initialized, respectively) at the initial moment of each execution of $P$,

  * •

if $x\in\bar{X}({P})$, then $x$ is initialized by a unique value at the
initial moment of each execution of $P$.

Conditions (a), (b) and (c) in (6) have the following meaning:

  * (a)

is related to a sending a message $c!e$:

    * –

a name $c^{s}$ of a channel to which the message is sent is available to $P$
in the state $s$, and

    * –

the sent message $e^{s}$ is a term whose components are available to $P$ in
the state $s$,

  * (b)

is related to a receiving a message $c?e$:

    * –

a name $c^{s}$ of a channel from which the message is received, is available
to $P$ in the state $s$,

    * –

each EM in the received message, which

      * *

must be decrypted during the receiving this message, and

      * *

is not encrypted on a shared key,

has the form $k(\ldots)$, where $k$ must be available to $P$ in the state $s$,
this property is expressed in second line of (6)(b),

    * –

term $e$ is a template of some term from $[c]^{s}$ with respect to some
extension of $\theta_{s}$, this property is expressed in last line of (6)(b),

  * (c)

is related to an assignment $e:=e^{\prime}$:

    * –

each component of $(e^{\prime})^{s}$ must be available to $P$ in the state
$s$,

    * –

a meaning of property in second line of (6)(c) coincides with a meaning of
corresponding properties in (6)(b): each EM in $(e^{\prime})^{s}$, which must
be decrypted during the assignment, has the form $k(\ldots)$ or
$Agent(P)(\ldots)$, and

      * *

either $k$ is a shared key,

      * *

or $k\in Var_{\bf K}$, and $k$ is available to $P$ in the state $s$,

    * –

$e$ is a template of $e^{\prime}$ with respect to some $\theta\in\Theta({{\it
Var}(e)\setminus[P]_{s}})$.

####  2.2.6 An adversary

An adversary is a SP $P_{\dagger}$ with the properties:

  * •

the graph $P_{\dagger}$ consists of a single node,

  * •

$\forall\,\tau\in Types$ the sets $\bar{X}({P_{\dagger}})_{\tau}$ and
$\hat{X}({P_{\dagger}})_{\tau}$ are countable,

  * •

$\forall\,\alpha\in Act\;\;{P_{\dagger}}$ has an edge labelled by $\alpha$.

We assume that $P_{\dagger}$ is the only SP whose graph has cycles.

####  2.2.7 Renamings

A renaming is an injective map $\eta:X\to X^{\prime}$, where
$X,X^{\prime}\subseteq Var$.

For each renaming $\eta:X\to X^{\prime}$, each $e\in Tm$ and each SP $P$,
notations $e^{\eta}$ and $P^{\eta}$ denote a term or a SP respectively,
obtained from $e$ or $P$ respectively by replacing $\forall\,x\in X$ each
occurrence of $x$ with $\eta(x)$.

If a renaming $\eta$ has the form

$\eta:\bar{X}(P)\cup\hat{X}(P)\to{\it Var}\setminus\tilde{X}(P),$

then SPs $P$ and $P^{\eta}$ are considered as equal.

###  2.3 Distributed processes

In this section we introduce a concept of a distributed process (DP). DPs are
models of CPs. All CPs considered in the paper are represented as DPs.

####  2.3.1 A concept of a distributed process

A distributed process (DP) is a family of SPs: ${\cal P}=\\{P_{i}\mid i\in
I\\}$. Each DP is associated with a variable of the type P, called a name of
this DP.

A DP is a model of a distributed algorithm, components of which communicate
with each other by message passing through channels.

Let ${\cal P}$ be a DP. We will use the following notations and assumptions:

  * •

${\it Var}({\cal P})=\bigcup_{P\in{\cal P}}{\it Var}({P})$, the sets $X({\cal
P})$, $\bar{X}({\cal P})$, $\tilde{X}({\cal P})$, $\hat{X}({\cal P})$ are
defined similarly,

  * •

we will assume that

$\begin{array}[]{llllllllllllll}\mbox{components of the family}\\\
\\{\bar{X}({P})\cup\hat{X}(P)\mid P\in{\cal P}\\}\\\ \mbox{are disjoint
sets}\\\ \mbox{and do not intersect with $\tilde{X}({\cal P})$}\end{array}$
(7)

(if this is not the case, then replace each $P\in{\cal P}$ by an equal SP in
the sense described at the end of 2.2.7, so that (7) will be satisfied),

  * •

a DP ${\cal P}=\\{P_{i}\mid i\in I\\}$ can be denoted by

    * –

$\\{P_{1},\ldots,P_{n}\\}$, if $I=\\{1,\ldots,n\\}$ (in the case $n=1$ the
brackets can be omitted, i.e. the DP $\\{P_{1}\\}$ is denoted by $P_{1}$), and

    * –

$P^{*}$, if $I=\\{1,2,\ldots\\}$, and all SPs in ${\cal P}$ are equal to $P$,

  * •

the notation ${\cal P}_{\dagger}$ denotes the DP $\\{{\cal P},P_{\dagger}\\}$,

  * •

if $\\{{\cal P}_{i}\mid i\in I\\}$ is a family of DPs, and for each $i\in I$
${\cal P}_{i}=\\{P_{i^{\prime}}\mid{i^{\prime}\in I_{i}}\\}$, where sets of
indices $I_{i}\;(i\in I)$ are disjoint (if this is not the case, then we
replace them with the corresponding disjoint copies), then the notation
$\\{{\cal P}_{i}\mid i\in I\\}$ denotes also the DP
$\\{P_{i^{\prime}}\mid{i^{\prime}}\in\bigsqcup_{i\in I}{I_{i}}\\}$.

We will use the following convention:

  * •

if, in some reasoning related to a DP of the form $P^{*}$, some SP is the
first of the considered SPs from $P^{*}$, then this SP and all its variables
are denoted by the same notations as in $P$,

  * •

if, in addition to this SP, another SP from $P^{*}$ is considered, then it is
denoted by $\grave{P}$, and in the notation of those of its variables that
correspond to variables from $\bar{X}({P})\cup\hat{X}(P)$ are used
backstrokes, etc.

####  2.3.2 A concept of a state of a distributed process

A state of a DP ${\cal P}$ is a family $s=\\{s_{P}\mid P\in{\cal P}\\}$ of
states of SPs occurred in ${\cal P}$ such that $\forall\,c\in Tm_{\bf C}$ all
components of the family $\\{[c]_{s_{P}}\mid P\in{\cal P}\\}$ are the same (we
will denote them by $[c]_{s}$).

Let $s=\\{s_{P}\mid P\in{\cal P}\\}$ be a state of a DP ${\cal P}$. Then

  * •

$s$ is said to be an initial state of ${\cal P}$, and is denoted by $0_{\cal
P}$ (or more briefly by 0, if the DP ${\cal P}$ is clear from the context), if
$\forall\,P\in{\cal P}$ $s_{P}=0_{P},$

  * •

$at_{s}=\\{at_{s_{P}}\mid P\in{\cal P}\\}$, $[{\cal P}]_{s}=\bigcup_{P\in{\cal
P}}[P]_{s}$, $\langle{\cal P}\rangle_{s}=Tm([{\cal P}]_{s})$,

  * •

$\theta_{s}$ denotes a binding from $\Theta({[{\cal P}]_{s}})$ such that

$\forall\,P\in{\cal
P},\;\forall\,x\in[P]_{s}\quad\theta_{s_{P}}(x)=\theta_{s}(x)$

(an existence of such a binding follows from assumption (7)).

Concepts of values of expressions and formulas in states of DPs are defined
similarly to the corresponding concepts for SPs.

$\forall\,\varphi,\psi\in Fm$, the notation $\varphi\leq\psi$ means that for
each DP ${\cal P}$ and each state $s$ of ${\cal P}$ the implication
$s\models\varphi\Rightarrow s\models\psi$ holds.

If formulas $\varphi,\psi\in Fm$ are such that $\varphi\leq\psi$ and
$\psi\leq\varphi$, then we will consider such formulas as equal. If the
formulas $\varphi$ and $\psi$ are equal, then we will denote this fact by
$\varphi=\psi$.

Examples of equal formulas are the following:

  * •

$\\{f(e_{1},\ldots,e_{n})=f(e^{\prime}_{1},\ldots,e^{\prime}_{n})\\}\;(f\in
Fun)$ and $\\{e_{1}=e^{\prime}_{1},\ldots,e_{n}=e^{\prime}_{n}\\}$,

  * •

$\\{[c]=\\{e\\},e^{\prime}\in[c]\\}$ and $\\{[c]=\\{e\\},e=e^{\prime}\\}.$

####  2.3.3 An execution of a distributed process

An execution of a DP ${\cal P}$ is a non-deterministic alternation of
executions of SPs occurred in ${\cal P}$. At each step of the execution only
one SP from ${\cal P}$ executes an active transition, and other SPs from
${\cal P}$ execute passive transitions.

An execution of a DP ${\cal P}$ can be understood as a generation of a
sequence of states of ${\cal P}$ (starting from $0_{\cal P}$), in which each
pair $(s,s^{\prime})$ of adjacent states belongs to a transition relation,
which means the following: $\exists\,P\in{\cal P}$:

$\\!\\!\\!\begin{array}[]{llllllllllllll}s_{P}\;\mathop{\to}\limits^{\begin{picture}(0.0,5.0)\put(-3.0,2.0){\makebox(0.0,1.0)[]{$\scriptstyle
P$}} \end{picture}}\;s^{\prime}_{P},\;\;\forall\,P^{\prime}\in{\cal
P}\setminus\\{P\\}\;\;s_{P^{\prime}}\to s^{\prime}_{P^{\prime}}\\\ \mbox{where
$s=\\{s_{P}\mid P\in{\cal P}\\}$, $s^{\prime}=\\{s^{\prime}_{P}\mid P\in{\cal
P}\\}$.}\end{array}$ (8)

The property (8) is denoted by
$s\;\mathop{\longrightarrow}\limits^{\\!\alpha_{P}}\;s^{\prime}$, where
$\alpha=\alpha_{s_{P}^{\prime}}$.

A set of states of a DP ${\cal P}$ can be considered as a graph in which there
is an edge from $s$ to $s^{\prime}$ labeled by $\alpha_{P}$ iff
$s\;\mathop{\longrightarrow}\limits^{\\!\alpha_{P}}\;s^{\prime}$. The
designation $P$ in the label $\alpha_{P}$ can be omitted.

For each pair $(s,s^{\prime})$ of states of a DP ${\cal P}$

  * •

$s\to s^{\prime}$ means that $(s,s^{\prime})$ belongs to the transition
relation, and

  * •

$s\Rightarrow s^{\prime}$ means that there is a sequence $s_{1},\ldots,s_{n}$
of states of ${\cal P}$ such that $s_{1}=s$, $s_{n}=s^{\prime}$, and
$\forall\,i=1,\ldots,n-1\;\;s_{i}\to s_{i+1}$.

A state $s$ of ${\cal P}$ is said to be reachable if $0_{\cal P}\Rightarrow
s$. The set of reachable states of ${\cal P}$ is denoted by $\Sigma_{\cal P}$.
$\forall\,s,s^{\prime}\in\Sigma_{\cal P}$, the notation
$s\leq_{\pi}s^{\prime}$ means that $\pi$ is a path such that
$s,s^{\prime}\in\pi$, and either $s=s^{\prime}$, or $s$ is located on $\pi$ to
the left of $s^{\prime}$. The notation $s<_{\pi}s^{\prime}$ means that
$s\leq_{\pi}s^{\prime}$ and $s\neq s^{\prime}$. If $\pi$ is clear from the
context, then the designation of $\pi$ in $\leq_{\pi}$ and $<_{\pi}$ can be
omitted.

####  2.3.4 Observational equivalence of distributed processes

A concept of an observational equivalence of DPs has the following meaning:
DPs ${\cal P}$ and ${\cal P}^{\prime}$ are observationally equivalent if for
each observer who analyzes an execution of ${\cal P}_{\dagger}$ and ${\cal
P}^{\prime}_{\dagger}$ by observing the contents of $\circ$, these DPs are
indistinguishable.

Let ${\cal P}$, ${\cal P}^{\prime}$ be DPs, $s\in\Sigma_{{\cal P}_{\dagger}}$,
$s^{\prime}\in\Sigma_{{\cal P}^{\prime}_{\dagger}}$, and $\eta:X\to
X^{\prime}$ be a renaming. The notation
$s\mathop{\sim}\limits_{\eta}s^{\prime}$ means that $[\circ]_{s}\subseteq
Tm(X)$ and $[\circ]_{s^{\prime}}=\\{e^{\eta}\mid e\in[\circ]_{s}\\}$.

${\cal P}$ and ${\cal P}^{\prime}$ are said to be observationally equivalent
if there is a set $\mu$ of triples $(s,s^{\prime},\eta)$, where
$s\in\Sigma_{{\cal P}_{\dagger}}$, $s^{\prime}\in\Sigma_{{\cal
P}^{\prime}_{\dagger}}$, $s\mathop{\sim}\limits_{\eta}s^{\prime}$, such that

  * •

$(0_{{\cal P}_{\dagger}},0_{{\cal P}^{\prime}_{\dagger}},\emptyset)\in\mu$
(where $\emptyset$ is a function with empty domain), and

  * •

$\forall\,(s,s^{\prime},\eta)\in\mu$ if $s\to\tilde{s}$ or
$s^{\prime}\to\tilde{s}^{\prime}$, then
$\exists\,(\tilde{s},\tilde{s}^{\prime},\tilde{\eta})\in\mu$: $\tilde{\eta}$
is an extension of $\eta$, and $s^{\prime}\Rightarrow\tilde{s}^{\prime}$ or
$s\Rightarrow\tilde{s}$, respectively.

Note that the above definition is not the only possible definition of an
observational equivalence, and can be modified depending on the problem being
solved. In some problems, a more appropriate definition of an observational
equivalence is a coarsening of the equivalence defined above, such that, for
example, the DPs ${\cal P}=\\{P\\}$ and ${\cal P}^{\prime}=\\{P^{\prime}\\}$
are equivalent, where
$P=\bullet\\!\\!\\!\;\mathop{\longrightarrow}\limits^{\\!\\!\\!!k(e)}\;\\!\\!\\!\bullet$,
$P^{\prime}=\bullet\\!\\!\\!\;\mathop{\longrightarrow}\limits^{\\!!k^{\prime}(e^{\prime})}\;\\!\\!\\!\bullet$,
$k\in\bar{X}({P})_{\bf K},$ $k^{\prime}\in\bar{X}({P}^{\prime})_{\bf K}.$

###  2.4 Preservation theorems for values of formulas

In this section, we formulate and prove theorems about a preservation of
values of some formulas under transitions of DPs. These theorems are used for
verification of DPs. In examples of applications of these theorems below,

  * •

SP $P$ mentioned in these theorems is $P_{\dagger}$, and

  * •

informally speaking, these theorems state that

    * –

if names of some channels are secure with respect to $P_{\dagger}$, then
contents of these channels cannot be changed by $P_{\dagger}$, and

    * –

if some keys are secure with respect to $P_{\dagger}$, then contents of EMs
encrypted with these keys are inaccessible to $P_{\dagger}$.

####  2.4.1 Secure channel theorems

First theorem is related to a preservation of values of formulas of the form

$E\,\bot_{\bf C}\,P,\quad\mbox{where $E\subseteq Tm$, and $P$ is a SP}$ (9)

under transitions of DPs. This theorem can be interpreted as the following
statement: if ${\cal P}$ is a DP, $P\in{\cal P}$, there is no messages in $E$
which are available for $P$, and in a current state of ${\cal P}$ there are no
messages from $E$ in channels available to $P$, then no own activity of $P$
will lead to availability for $P$ messages from $E$. Channels whose names are
occurred in $E$ can be interpreted as channels secure with respect to $P$.

Theorem 1.

Let ${\cal P}$ be a DP, $P\in{\cal P}$, and $s,s^{\prime}$ be states of ${\cal
P}$ such that
$s\;\mathop{\longrightarrow}\limits^{\\!\\!\alpha_{P}}\;s^{\prime}$.

Then $\forall\,E\subseteq\langle{\cal P}\rangle_{0}$ the following implication
holds:

$s\models E\,\bot_{\bf C}\,P\;\;\Rightarrow\;\;s^{\prime}\models E\,\bot_{\bf
C}\,P.$

Proof.

$s\models E\,\bot_{\bf C}\,P$ means that $\forall\,e\in E\;\;Agent(P)\not\in
e$, and $\forall\,x\in E_{\bf X}$, $\forall\,c\in Tm_{\bf C}$

$\left.\begin{array}[]{llllllllllllll}\forall\,y\in[P]_{s}\;\;x\not\in
y^{s}\\\ \mbox{if }\exists\,e\in[c]_{s}:x\in e,\mbox{ then }c\in
E\end{array}\right\\}$ (10)

Prove that (10) implies that $s^{\prime}\models E\,\bot_{\bf C}\,P$, i.e.
$\forall\,x\in E_{\bf X}$, $\forall\,c\in Tm_{\bf C}$

$\left.\begin{array}[]{llllllllllllll}\forall\,y\in[P]_{s^{\prime}},\;\;x\not\in
y^{s^{\prime}}\\\ \mbox{if }\exists\,e\in[c]_{s^{\prime}}:x\in e,\mbox{ then
}c\in E\end{array}\right\\}$ (11)

  1. 1.

If first statement in (11) is false, then first statement in (10) implies
$[P]_{s}\neq[P]_{s^{\prime}}$, and one of the following two cases holds.

     * •

First case:

$\\!\\!\\!\\!\\!\\!\left.\begin{array}[]{llllllllllllll}\mbox{$\alpha=c?e$,
where }\\\ c\in\langle P\rangle_{s},e^{s^{\prime}}\in[c^{s}]_{s},\\\
\,[P]_{s^{\prime}}=[P]_{s}\cup{\it Var}(e),\\\ \exists\,x\in E_{\bf
X},\exists\,y\in Var(e):x\in y^{s^{\prime}}.\end{array}\right\\}$ (12)

The statement $x\in y^{s^{\prime}}\subseteq e^{s^{\prime}}\in[c^{s}]_{s}$ and
second statement in (10) imply $c^{s}\in E$.

If $c^{s}\not\in E_{\bf X}$, then $c$ has the form $shared\\_channel(\ldots)$,
and in this case, the definition of an execution of a SP in 2.2.5 implies that
$Agent(P)\in c^{s}$. But this fact and the statement $c^{s}\in E$ contradict
the assumption $\forall\,e\in E\;\;Agent(P)\not\in e$.

Thus, $c^{s}\in E_{\bf X}$, that implies $c\in[P]_{s}$. According to first
statement in (10) (in which we take $c^{s}$ and $c$ as $x$ and $y$,
respectively), the statement $c^{s}\not\in c^{s}$ holds, but this is false.

     * •

Second case:

$\\!\\!\\!\\!\\!\\!\left.\begin{array}[]{llllllllllllll}\mbox{$\alpha=(e:=e^{\prime})$,
where}\\\ e^{\prime}\in\langle
P\rangle_{s},e^{s^{\prime}}=(e^{\prime})^{s},\\\
\,[P]_{s^{\prime}}=[P]_{s}\cup{\it Var}(e),\\\ \exists\,x\in E_{\bf
X},\exists\,y\in{\it Var}(e):x\in y^{s^{\prime}}\end{array}\right\\}$ (13)

Since $x\in y^{s^{\prime}}\subseteq e^{s^{\prime}}=(e^{\prime})^{s}\in\langle
P\rangle^{s}$, then

$\exists\,z\in[P]_{s}:x\in z^{s}.$ (14)

(14) contradicts first statement in (10).

  2. 2.

If second statement in (11) is false, i.e.

$\begin{array}[]{llllllllllllll}\exists\,x\in E_{\bf X},\exists\,c^{\prime}\in
Tm_{\bf C},\exists\,e^{\prime}\in[c^{\prime}]_{s^{\prime}}:\\\ x\in
e^{\prime},\mbox{ but }c^{\prime}\not\in E\end{array}$

then second statement in (10) implies that
$[c^{\prime}]_{s^{\prime}}\neq[c^{\prime}]_{s}$, and

$\mbox{$\alpha=c!e$, where $c,e\in\langle P\rangle_{s},x\in
e^{\prime}=e^{s}$}.$

From $x\in e^{s}$ it follows that $\exists\,y\in[P]_{s}:x\in y^{s}$, which
contradicts first statement in (10).

The following theorem is a strengthening of theorem 2.4.1. It states that
under conditions of theorem 2.4.1 the lower and upper bounds on the contents
of secure channels do not change when actions of $P$ are executed.

Theorem 2.

Let ${\cal P}$ be a DP, $P\in{\cal P}$, and $s,s^{\prime}$ be states of ${\cal
P}$ such that
$s\;\mathop{\longrightarrow}\limits^{\\!\\!\alpha_{P}}\;s^{\prime}$.

Then $\forall\,E\subseteq\langle{\cal P}\rangle_{0}$,
$E^{\prime},E^{\prime\prime}\subseteq Tm$, $c\in E_{\bf C}$ the following
implication holds:

$\begin{array}[]{llllllllllllll}s\models\varphi\Rightarrow
s^{\prime}\models\varphi,\\\ \mbox{ where }\varphi=\\{E\,\bot_{\bf
C}\,P,E^{\prime}\subseteq[c]\subseteq E^{\prime\prime}\\}.\end{array}$

Proof.

According to theorem 2.4.1, $s\models E\,\bot_{\bf C}\,P$ implies
$s^{\prime}\models E\,\bot_{\bf C}\,P$. In addition,
$[c]_{s}\subseteq[c]_{s^{\prime}}$. Thus, to prove the theorem, it suffices to
prove implication

$s\models\varphi\;\;\Rightarrow\;\;s^{\prime}\models[c]\subseteq
E^{\prime\prime}.$ (15)

If the conclusion of implication (15) does not hold, then
$[c]_{s}\neq[c]_{s^{\prime}}$.

By assumption $c\in E_{\bf C}\subseteq\langle{\cal P}\rangle_{0}$, so
$[c]_{s}\neq[c]_{s^{\prime}}$ is possible only if $\alpha=c^{\prime}!e$, where
$(c^{\prime})^{s}=c$.

If $c$ is not a variable, then $c$ is a shared channel, and by definition of
an execution the action $c^{\prime}!e$, in this case the condition
$Agent(P)\in c$ holds, which contradicts the assumption $s\models E\,\bot_{\bf
C}\,P$ (because, in particular, $Agent(P)$ has no occurrences in terms from
$E$). Thus, $c\in Var$, $c^{\prime}\in Var$, $c^{\prime}\in[P]_{s}$.

Since $c\in E_{\bf X}$ and $c^{\prime}\in[P]_{s}$, then by assumption
$s\models E\,\bot_{\bf C}\,P$ we have $c\not\in c$, which is false.

####  2.4.2 Secure key theorems

In this subsection, we prove theorems similar to theorems 2.4.1 and 2.4.1. Now
we consider secure keys instead of secure channels.

First theorem is related to a preservation of values of formulas

$E\,\bot_{\bf K}\,P,\quad\mbox{where $E\subseteq Tm$, and $P$ is a SP}$ (16)

under transitions of DPs. This theorem can be interpreted as the following
statement: if ${\cal P}$ is a DP, $P\in{\cal P}$, there is no messages in $E$
which are available for $P$, and in a current state of ${\cal P}$ (16) holds,
then no own activity of $P$ will lead to availability for $P$ keys from $E$.
These keys can be interpreted as secure keys with respect to $P$.

Theorem 3.

Let ${\cal P}$ be a DP, $P\in{\cal P}$, and $s,s^{\prime}$ be states of ${\cal
P}$ such that
$s\;\mathop{\longrightarrow}\limits^{\\!\\!\alpha_{P}}\;s^{\prime}$.

Then $\forall\,E\subseteq\langle{\cal P}\rangle_{0}$ the following implication
holds:

$s\models E\,\bot_{\bf K}\,P\Rightarrow s^{\prime}\models E\,\bot_{\bf K}\,P.$

Proof.

$s\models E\,\bot_{\bf K}\,P$ means that $\forall\,e\in E\;\;Agent(P)\not\in
e$, and $\forall\,x\in E_{\bf X}$, $\forall\,c\in Tm_{\bf C}$

$\\!\\!\\!\\!\\!\\!\\!\\!\left.\begin{array}[]{llllllllllllll}\forall\,y\in[P]_{s}\;\;x\,\bot_{{\bf
K},E}\,y^{s}\\\ \forall\,e\in[c]_{s}\;\;x\,\bot_{{\bf
K},E}\,e\end{array}\right\\}$ (17)

Prove that (17) implies that $s^{\prime}\models E\,\bot_{\bf K}\,e$, i.e.
$\forall\,x\in E_{\bf X}$, $\forall\,c\in Tm_{\bf C}$

$\\!\\!\\!\left.\begin{array}[]{llllllllllllll}\forall\,y\in[P]_{s^{\prime}}\;\;s^{\prime}\models
x\,\bot_{{\bf K},E}\,y^{s^{\prime}}\\\
\forall\,e\in[c]_{s^{\prime}}\;\;s^{\prime}\models x\,\bot_{{\bf
K},E}\,e\end{array}\right\\}$ (18)

  1. 1.

If first statement in (18) is wrong, then first statement in (17) implies
$[P]_{s}\neq[P]_{s^{\prime}}$, and one of two cases does hold:

     * •

First case: the following statement holds

$\left.\begin{array}[]{llllllllllllll}\mbox{$\alpha=c?e$},c\in\langle
P\rangle_{s},e^{s^{\prime}}\in[c^{s}]_{s},\\\
\,[P]_{s^{\prime}}=[P]_{s}\cup{\it Var}(e),\\\ \mbox{$\exists\,y\in{\it
Var}(e)$},\\\ \mbox{$\exists$ an occurrence of $x$ in $y^{s^{\prime}}$}\\\
\mbox{that is not contained }\\\ \mbox{in any subterm of the form }\\\
\mbox{$k(\ldots)\subseteq y^{s^{\prime}}$, where $k\in E_{\bf
K}$.}\end{array}\right\\}$ (19)

Since the occurrence of $x$ mentioned in (19) occurs in the term
$y^{s^{\prime}}\subseteq e^{s^{\prime}}\in[c^{s}]_{s}$, then second statement
in (17) implies that this occurrence of $x$ occurs in the subterm
$k(\tilde{e})\subseteq e^{s^{\prime}}$, where $k\in E_{\bf K}$.

(19) implies that $k(\tilde{e})$ is not a subterm of $y^{s^{\prime}}$. Since
the terms $k(\tilde{e})$ and $y^{s^{\prime}}$ have a non-empty intersection
(both contain the above occurrence of $x$), then (1) implies that
$y^{s^{\prime}}\subset k(\tilde{e})$. Thus,

$y^{s^{\prime}}\subset k(\tilde{e})\subseteq e^{s^{\prime}}.$ (20)

Prove by induction on the structure of $e$ that (20) implies

$\exists\,z\in Var(e):\;\;k(\tilde{e})\subseteq z^{s^{\prime}}\subseteq
e^{s^{\prime}}.$ (21)

If $e\in Con\cup{\it Var}$, then (21) holds.

If $e=f(e_{1},\ldots,e_{n})$, where $f\in Fun$, then

       * –

if $f=encrypt$, i.e. $e=k_{1}(e_{1})$, then $k_{1}\in Keys(e)$, and (6)(b)
implies the inclusion $Keys(e)\subseteq[P]_{s}$, thus $k_{1}\in[P]_{s}$, and
the following cases are possible:

         * *

$k(\tilde{e})=e^{s^{\prime}}=k_{1}^{s^{\prime}}(e_{1}^{s^{\prime}})$, in this
case $k=k_{1}^{s^{\prime}}=k_{1}^{s}\in[P]^{s}$, but since $k\in E_{\bf K}$,
then, according to first statement in (17), the occurrence of $k$ in $k$
occurs in a subterm of the form $k^{\prime}(\ldots)\subseteq k$, which is
impossible,

         * *

$k(\tilde{e})\subseteq k_{1}^{s^{\prime}}$, this case is impossible by the
definition of terms of the type ${\bf K}$,

         * *

$k(\tilde{e})\subseteq e_{1}^{s^{\prime}}$, in this case statement (21)
follows from the inductive hypothesis,

       * –

if $f\neq encrypt$, then $\exists\,i\in\\{1,\ldots,n\\}:k(\tilde{e})\subseteq
e_{i}^{s^{\prime}}$, and statement (21) follows from inductive hypothesis.

From (20) and (21) it follows that

$y^{s^{\prime}}\subset k(\tilde{e})\subseteq z^{s^{\prime}}\subseteq
e^{s^{\prime}}.$ (22)

Thus, the term $e$ contains occurrences of the variables $y$ and $z$ with the
following property: $y^{s^{\prime}}\subset z^{s^{\prime}}$, whence for these
occurrences the inclusion $y\subset z$ holds, which is impossible.

     * •

Second case: the following statement holds

$\left.\begin{array}[]{llllllllllllll}\mbox{$\alpha=(e:=e^{\prime})$, }\\\
\mbox{ $e^{\prime}\in\langle
P\rangle_{s},e^{s^{\prime}}=(e^{\prime})^{s}$},\\\
\mbox{$[P]_{s^{\prime}}=[P]_{s}\cup{\it Var}(e)$,}\\\ \mbox{$\exists\,y\in{\it
Var}(e)$, }\\\ \mbox{$\exists$ an occurrence of $x$ in $y^{s^{\prime}}$}\\\
\mbox{that is not contained}\\\ \mbox{in any subterm of the form }\\\
\mbox{$k(\ldots)\subseteq y^{s^{\prime}}$, where $k\in E_{\bf
K}$.}\end{array}\right\\}$ (23)

Since the occurrence of $x$ mentioned in (23) is contained in the term
$y^{s^{\prime}}\subseteq e^{s^{\prime}}=(e^{\prime})^{s}$, then this
occurrence of $x$ is contained in the subterm
$(z^{\prime})^{s}\subseteq(e^{\prime})^{s}$, where $z^{\prime}\in
Var(e^{\prime})$.

By assumption, $e^{\prime}\in\langle P\rangle_{s}$, therefore
$Var(e^{\prime})\subseteq[P]_{s}$, so $z^{\prime}\in[P]_{s}$. From first
statement in (17) it follows that the occurrence of $x$ in $(z^{\prime})^{s}$
mentioned in (23) is contained in some subterm
$k(\tilde{e})\subseteq(z^{\prime})^{s}$, where $k\in E_{\bf K}$.

From (23) it follows that $k(\tilde{e})$ is not a subterm of $y^{s^{\prime}}$.

Since the terms $k(\tilde{e})$ and $y^{s^{\prime}}$ have a non-empty
intersection (both contain the occurrence of $x$ mentioned in (23)), then from
(1) it follows that $y^{s^{\prime}}\subset k(\tilde{e})$.

The equality $e^{\prime}=e^{\theta}$ implies that $\exists\,z\in Var(e)$: the
above occurrence of $z^{\prime}$ in $e^{\prime}$ occurs in the subterm
$z^{\theta}\subseteq e^{\theta}=e^{\prime}$. Therefore,
$(z^{\prime})^{s}\subseteq(z^{\theta})^{s}=z^{s^{\prime}}\subseteq
e^{s^{\prime}}$.

So we get:

$y^{s^{\prime}}\subset k(\tilde{e})\subseteq(z^{\prime})^{s}\subseteq
z^{s^{\prime}}\subseteq e^{s^{\prime}}.$ (24)

As in the previous section, on the reason of (24), we conclude that the term
$e$ contains occurrences of the variables $y$ and $z$ with the following
property: $y^{s^{\prime}}\subset z^{s^{\prime}}$, whence the inclusion of
$y\subset z$ holds for these occurrences, which is impossible.

  2. 2.

If second statement in (18) is not true, then from second statement in (17) it
follows that

$\left.\begin{array}[]{llllllllllllll}\mbox{$\alpha=c!e$, where $e\in\langle
P\rangle_{s}$},\\\ \mbox{$\exists$ occurrence of $x$ in $e^{s}$}\\\ \mbox{that
is not contained}\\\ \mbox{in any subterm of the form }\\\
\mbox{$k(\ldots)\subseteq e^{s}$, where $k\in E_{\bf
K}$.}\end{array}\right\\}$ (25)

Since $e\in\langle P\rangle_{s}$, then the occurrence of $x$ in $e^{s}$
mentioned in (25) is contained in a subterm of the form $y^{s}$ of the term
$e^{s}$, where $y$ is some variable from $[P]_{s}$. According to first
statement in (17), this occurrence of $x$ in $y^{s}$ is contained in a subterm
of the form $k(\ldots)\subseteq y^{s}\subseteq e^{s}$, where $k\in E_{\bf K}$.
But this contradicts to (25).

Theorem 4.

Let ${\cal P}$ be a DP such that $Var({\cal P})_{\bf C}=\\{\circ\\}$,
$P\in{\cal P}$, $s,s^{\prime}$ be states from $\Sigma_{\cal P}$ such that
$s\;\mathop{\longrightarrow}\limits^{\\!\\!\alpha_{P}}\;s^{\prime}$, and
$E\subseteq\langle{\cal P}\rangle_{0}$.

Then $\forall\,k\in E_{\bf K}$ the following implication holds:

$s\models\varphi\Rightarrow s^{\prime}\models\varphi$

where $\varphi=\\{E\,\bot_{\bf K}\,P,k^{-1}[{P}]\subseteq k^{-1}[\circ]\\}.$

Proof.

By theorem 2.4.2, the statement $s\models E\,\bot_{\bf K}\,P$ implies
$s^{\prime}\models E\,\bot_{\bf K}\,P$. Thus, to prove theorem 2.4.2, it
suffices to prove the implication

$s\models\varphi\;\;\Rightarrow\;\;s^{\prime}\models k^{-1}[{P}]\subseteq
k^{-1}[\circ].$ (26)

If (26) does not hold, then $\alpha$ is not a sending,
$[P]_{s^{\prime}}=[P]_{s}\cup{\it Var}({e^{\prime}})$, and $\exists\,e\in
k^{-1}[P]^{s^{\prime}}$ such that

$\begin{array}[]{llllllllllllll}\mbox{$e\not\in k^{-1}[\circ]_{s}$, i.e.
$\exists\,x\in[P]_{s^{\prime}}:$}\\\ \mbox{$k(e)\subseteq
x^{{s^{\prime}}},\forall\,\dot{e}\in[\circ]_{s}\;\;k(e)\not\subseteq\dot{e}.$}\end{array}$
(27)

The assumption $s\models\varphi$ and (27) imply that $x\in{\it
Var}({e^{\prime}})$, whence we get: $k(e)\subseteq
x^{{s^{\prime}}}\subseteq(e^{\prime})^{{s^{\prime}}}$.

Consider separately each of the two possible types of $\alpha$.

  1. 1.

$\alpha=?e^{\prime}$, in this case
$k(e)\subseteq(e^{\prime})^{{s^{\prime}}}\in[\circ]_{s}$. Setting in (27) the
term $\dot{e}$ be equal to $(e^{\prime})^{{s^{\prime}}}$, we get a
contradiction.

  2. 2.

$\alpha=(e^{\prime}:=e^{\prime\prime})$, in this case
$e^{\prime\prime}\in\langle P\rangle_{s}$,
$(e^{\prime})^{{s^{\prime}}}=(e^{\prime\prime})^{s}$, so

$k(e)\subseteq(e^{\prime\prime})^{s}.$ (28)

Prove that $k\not\in e^{\prime\prime}$ and $k\in E_{\bf X}$.

Suppose $k\in e^{\prime\prime}$. If $k=shared\\_key(\ldots)$, then, according
to the definition of SP execution in section 2.2.5, the statement $Agent(P)\in
k\in E_{\bf K}$ holds, which contradicts first condition of the property
$s\models E\,\bot_{\bf K}\,P$. Recall that this property has the form:
$\forall\,\tilde{e}\in E$ $Agent(P)\not\in\tilde{e}$, and

$\left.\begin{array}[]{llllllllllllll}\forall\,x\in E_{\bf
X},\,\forall\,y\in[P]_{s}\;\;x\,\bot_{{\bf K},E}\,y^{s}\\\ \forall\,x\in
E_{\bf X},\,\forall\,\tilde{e}\in[\circ]_{s}\;\;x\,\bot_{{\bf
K},E}\,\tilde{e}\end{array}\right\\}$ (29)

Therefore, $k\in E_{\bf X}$, so $k\in e^{\prime\prime}\in\langle P\rangle_{s}$
implies $k\in[P]_{s}$. However, assuming in first statement in (29) $x$ and
$y$ be equal to $k$, we get $k\,\bot_{{\bf K},E}\,k$, which is false by
definition (5).

Similarly to the proof of the implication (20) $\Rightarrow$ (21) in theorem
2.4.2, we prove that the statements $k\not\in e^{\prime\prime}$ and (28) imply

$\exists\,y\in{\it Var}({e^{\prime\prime}})\subseteq[P]_{s}:k(e)\subseteq
y^{{s}}.$ (30)

By assumption, $s\models k^{-1}[{P}]\subseteq k^{-1}[\circ]$, i.e.
$k^{-1}[{P}]^{s}\subseteq k^{-1}[\circ]_{s}$. From (30) it follows that $e\in
k^{-1}[P]^{s}$. Therefore, $e\in k^{-1}[\circ]_{s}$, which contradicts the
assumption (27).

The following theorem is a strengthening of theorem 2.4.2. It states that
under the conditions of theorem 2.4.2 the lower and upper bounds for the set
of EMs contained in open channel and encrypted with secure keys do not change
when actions of the SP $P$ are executed.

Theorem 5 .

Let ${\cal P}$ be a DP such that $Var({\cal P})_{\bf C}=\\{\circ\\}$,
$P\in{\cal P}$, $s,s^{\prime}$ be states from $\Sigma_{\cal P}$ such that
$s\;\mathop{\longrightarrow}\limits^{\\!\\!\alpha_{P}}\;s^{\prime}$, and
$E\subseteq\langle{\cal P}\rangle_{0}$, $E^{\prime},E^{\prime\prime}\subseteq
Tm$.

Then $\forall\,k\in E_{\bf K}$ the following implication holds:

$\begin{array}[]{llllllllllllll}s\models\varphi\Rightarrow
s^{\prime}\models\varphi,\mbox{where }\\\
\varphi={\left\\{\begin{array}[]{lllll}E\,\bot_{\bf K}\,P,k^{-1}[{P}]\subseteq
k^{-1}[\circ]\\\ E^{\prime}\subseteq k^{-1}[\circ]\subseteq
E^{\prime\prime}\end{array}\right\\}}.\end{array}$ (31)

Proof.

By theorem 2.4.2, to prove (31) it is enough to prove that

$s\models\varphi\Rightarrow s^{\prime}\models\\{E^{\prime}\subseteq
k^{-1}[\circ],k^{-1}[\circ]\subseteq E^{\prime\prime}\\}.$ (32)

  * •

The statement $s^{\prime}\models E^{\prime}\subseteq k^{-1}[\circ]$ follows
from $[\circ]_{s}\subseteq[\circ]_{s^{\prime}}$.

  * •

Prove the statement $s^{\prime}\models k^{-1}[\circ]\subseteq
E^{\prime\prime}$. If it is not true, then
$[\circ]_{s}\neq[\circ]_{s^{\prime}}$. This is possible only if $\alpha=!e$,
where $e\in\langle P\rangle_{s}$, and

$\begin{array}[]{llllllllllllll}[\circ]_{s^{\prime}}=[\circ]_{s}\cup\\{e^{s}\\},\\\
\exists\,e^{\prime}\not\in(E^{\prime\prime})^{s}\supseteq
k^{-1}[\circ]_{s}:k(e^{\prime})\subseteq e^{s}.\end{array}$ (33)

As in theorem 2.4.2, we prove that $k\in E_{\bf X}$, and $e\in\langle
P\rangle_{s}$ implies $k\not\in e$.

Similarly to the proof of implication (20) $\Rightarrow$ (21) in theorem
2.4.2, we can prove that the statements $k\not\in e$ and
$k(e^{\prime})\subseteq e^{s}$ imply

$\exists\,x\in{\it Var}({e})\subseteq[P]_{s}:\;k(e^{\prime})\subseteq
x^{{s}},$

therefore $e^{\prime}\in k^{-1}[P]^{s}$. Hence, using the assumption
$s\models\varphi$, which results to the inclusion $k^{-1}[{P}]^{s}\subseteq
k^{-1}[\circ]_{s}$, we get: $e^{\prime}\in k^{-1}[\circ]_{s}$, which
contradicts (33).

###  2.5  Theorem for proving a correspondence property

A theorem stated in this section can be used to prove a correspondence
property of authentication protocols, which has the following meaning: if one
of participants of an authentication protocol, after executing this protocol,
has come to the conclusion that declared name and parameters of other
participant of this protocol are authentic, then then this is indeed the case.
A theorem proved below is used to prove that if

  * •

a DP ${\cal P}$ uses only open channel $\circ$ for communication, and

  * •

in some state $s\in\Sigma_{\cal P}$ this channel contains a message containing
a subterm $k(e)$, where the key $k$ is secure in $s$ with respect to
$P\in{\cal P}$,

then in some state $s^{\prime}<_{\pi}s$ another SP $P^{\prime}\in{\cal
P}\setminus\\{P\\}$ sent a message to $\circ$, containing the subterm $k(e)$.

In sections 3.2 and 3.3 we consider examples of applying this theorem to
verification of the Yahalom CP, and to verification of the CP of EMs passing
between several agents.

Theorem 6.

Let ${\cal P}$ be a DP, $Var({\cal P})_{\bf C}=\\{\circ\\}$, $P\in{\cal P}$,
$E$ be a subset of $\langle{\cal P}\rangle_{0}$ and $s\in\Sigma_{\cal P}$ be a
state such that

  * •

$s\models E\,\bot_{\bf K}\,P$, and

  * •

$[\circ]_{s}$ contains a term with a subterm $k(e)$, where $k\in E_{\bf K}$.

Then, for each path $\pi$ from $0_{\cal P}$ to $s$, there is a SP
$P^{\prime}\in{\cal P}\setminus\\{P\\}$ such that $\pi$ has an edge of the
form

${\dot{s}}\;\mathop{\longrightarrow}\limits^{\\!(!\dot{e})_{P^{\prime}}}\;s^{\prime},\quad\mbox{where
$k(e)\subseteq\dot{e}^{\dot{s}}$.}$ (34)

Proof.

Let $s^{\prime}$ be a first state on $\pi$ such that $[\circ]_{s^{\prime}}$
has a term $e^{\prime}$ with the subterm $k(e)$. Since
$[\circ]_{0}=\emptyset$, then $s^{\prime}\neq 0$.

Let
$\dot{s}\;\mathop{\to}\limits^{\begin{picture}(0.0,5.0)\put(-3.0,2.0){\makebox(0.0,1.0)[]{$\scriptstyle\alpha_{P^{\prime}}$}}
\end{picture}}\;s^{\prime}$ be an edge on $\pi$ ending at $s^{\prime}$. Since
$e^{\prime}\not\in[\circ]_{\dot{s}}$, then $\alpha=!\dot{e}$, where
$\dot{e}^{\dot{s}}=e^{\prime}$. If $P^{\prime}\neq P$, then the theorem is
proven.

Prove that another possible case ($P^{\prime}=P$) is impossible.

Suppose $P^{\prime}=P$, i.e.
$\dot{s}\;\mathop{\longrightarrow}\limits^{\\!(!\dot{e})_{P}}\;s^{\prime}$.

Prove that $k\in E_{\bf X}$. If $k\not\in E_{\bf X}$, i.e. $k$ is a shared
key, then, by the definition of an execution of a SP in 2.2.5, $Agent(P)\in
k\in E_{\bf K}$, which contradicts the assumption $\forall\,\tilde{e}\in
E\;\;Agent(P)\not\in\tilde{e}$.

$s\models E\,\bot_{\bf K}\,P$ implies $\dot{s}\models E\,\bot_{\bf K}\,P$,
whence we get $k\not\in[P]_{\dot{s}}$, because if $k\in[P]_{\dot{s}}$, then,
according to (4), the occurrence of $k$ in $k^{\dot{s}}=k$ must be contained
in a subterm of the form $k^{\prime}(\ldots)$, which is impossible.

The statement $k\not\in[P]_{\dot{s}}$ and condition $\dot{e}\in\langle
P\rangle_{\dot{s}}$ (which is true according to (6)(a)) imply
$k\not\in\dot{e}$.

Similarly to the proof of the implication (20) $\Rightarrow$ (21) in theorem
2.4.2, we can prove that statements $k(e)\subseteq
e^{\prime}=\dot{e}^{\dot{s}}$ and $k\not\in\dot{e}$ imply

$\exists\,x\in Var(\dot{e})\subseteq[P]_{\dot{s}}:k(e)\subseteq
x^{\dot{s}}\in[P]^{\dot{s}}.$ (35)

Let $s^{\prime\prime}$ be a first state on $\pi$ such that
$[P]^{s^{\prime\prime}}$ has a term with the subterm $k(e)$, that is,

$\exists\,x\in[P]_{s^{\prime\prime}}:k(e)\subseteq x^{s^{\prime\prime}}.$ (36)

(35) implies that $s^{\prime\prime}$ is to the left of $s^{\prime}$ on $\pi$.
It is clear that $s^{\prime\prime}\neq 0$, so there is an edge
$\ddot{s}\;\mathop{\longrightarrow}\limits^{\\!\;\alpha_{P^{\prime\prime}}}\;s^{\prime\prime}$
on $\pi$. From the choice of $s^{\prime\prime}$ it follows that
$x\not\in[P]_{\ddot{s}}$, thus $P^{\prime\prime}=P$, and two cases are
possible:

  1. 1.

$\alpha=?\ddot{e},x\in
Var(\ddot{e}),\ddot{e}^{s^{\prime\prime}}\in[\circ]_{\ddot{s}}$,

since $k(e)\subseteq
x^{s^{\prime\prime}}\subseteq\ddot{e}^{s^{\prime\prime}}\in[\circ]_{\ddot{s}}$,
then we get a contradiction with the choice of $s^{\prime}$ as the first state
on $\pi$ such that $[\circ]_{s^{\prime}}$ contains the term $e^{\prime}$ with
the subterm $k(e)$: the state $\ddot{s}$ has the same property, and is located
to the left of $s^{\prime}$,

  2. 2.

$\alpha=(\ddot{e}:=\tilde{e}),x\in Var(\ddot{e}),\tilde{e}\in\langle
P\rangle_{\ddot{s}},\ddot{e}^{s^{\prime\prime}}=\tilde{e}^{\ddot{s}}$,

since

     * •

$k(e)\subseteq
x^{s^{\prime\prime}}\subseteq\ddot{e}^{s^{\prime\prime}}=\tilde{e}^{\ddot{s}}$
and

     * •

$\tilde{e}$ does not contain $k$, because it was proven above that
$k\not\in[P]_{\dot{s}}$, therefore, taking into account the property
$\ddot{s}\leq\dot{s}$, which implies the inclusion
$[P]_{\ddot{s}}\subseteq[P]_{\dot{s}}$, we get: $k\not\in[P]_{\ddot{s}}$, and
therefore the term $\tilde{e}\in\langle P\rangle_{\ddot{s}}$ also does not
contain $k$,

then, similarly to the proof of the implication (20) $\Rightarrow$ (21) in
theorem 2.4.2, we can prove that

$\exists\,y\in[P]_{\ddot{s}}:k(e)\subseteq y^{\ddot{s}},$

which contradicts the choice of $s^{\prime\prime}$ as a first state on $\pi$
with the property (36): $\ddot{s}$ has the same property and is located to the
left of $s^{\prime\prime}$.

###  2.6 Diagrams of distributed processes

####  2.6.1 Prefix sequential processes

A SP $P$ is said to be a prefix SP if

$\begin{array}[]{llllllllllllll}\begin{picture}(20.0,15.0)\put(-70.0,0.0){\circle*{4.0}}
\put(-25.0,0.0){\circle*{4.0}} \put(25.0,0.0){\circle*{4.0}}
\put(75.0,0.0){\circle*{4.0}} \put(-68.0,0.0){\vector(1,0){41.0}}
\put(27.0,0.0){\vector(1,0){46.0}} \put(-23.0,0.0){\line(1,0){10.0}}
\put(13.0,0.0){\vector(1,0){10.0}}
\put(0.0,0.0){\makebox(0.0,0.0)[]{$\ldots$}}
\put(-90.0,0.0){\makebox(0.0,0.0)[]{$P=$}}
\put(-70.0,5.0){\makebox(0.0,0.0)[b]{$0$}}
\put(-25.0,5.0){\makebox(0.0,0.0)[b]{$1$}}
\put(25.0,5.0){\makebox(0.0,0.0)[b]{$n-1$}}
\put(75.0,5.0){\makebox(0.0,0.0)[b]{$n$}}
\put(-48.0,2.0){\makebox(0.0,0.0)[b]{$\alpha_{1}$}}
\put(50.0,2.0){\makebox(0.0,0.0)[b]{$\alpha_{n}$}}
\put(80.0,0.0){\makebox(0.0,0.0)[l]{$P^{\prime}$}}
\put(80.0,3.0){\oval(40.0,22.0)} \end{picture}\end{array}$ (37)

i.e. $P$ contains nodes numbered by natural numbers $0,1,\ldots,n\;(n\geq 1)$,
and $Init(P)=0$, $\forall\,i=0,\ldots,n-1$ there is exactly one outgoing edge
from node $i$ with the end $i+1$ and labeled by $\alpha_{i}$. The notation
$P^{\prime}$ in (37) denotes a subgraph of the graph $P$, consisting of the
nodes and edges of the graph $P$, with the exception of the nodes
$0,\ldots,n-1$ and edges associated with these nodes.

The subgraphs
$0\;\mathop{\to}\limits^{\begin{picture}(0.0,5.0)\put(-3.0,2.0){\makebox(0.0,1.0)[]{$\scriptstyle\alpha_{1}$}}
\end{picture}}\;1\;\mathop{\to}\limits^{\begin{picture}(0.0,5.0)\put(-3.0,2.0){\makebox(0.0,1.0)[]{$\scriptstyle\alpha_{2}$}}
\end{picture}}\;\ldots\;\mathop{\to}\limits^{\begin{picture}(0.0,5.0)\put(-3.0,2.0){\makebox(0.0,1.0)[]{$\scriptstyle\alpha_{n}$}}
\end{picture}}\;n$ and $P^{\prime}$ of the graph (37) are called a prefix and
a postfix of the SP $P$, respectively, and are denoted by ${\it Pref}(P)$ and
${\it Post}(P)$ respectively. The last node of ${\it Pref}(P)$ is called a
final node of this prefix. If ${\it Post}(P)$ consists of one node, then it is
denoted by 0.

If a SP $P$ has the form (37), then we will denote this fact by

$P=\alpha_{1};\ldots;\alpha_{n};P^{\prime}.$ (38)

####  2.6.2 A concept of a diagram of a distributed process

Let ${\cal P}$ be a DP, such that each $P\in{\cal P}$ is a prefix SP, and for
each sending (each receivng) in ${\it Pref}(P)$ it is assumed that

  * •

an intended receiver (an intended sender) of the message that is sent
(received) when performing this action is some $P^{\prime}\in{\cal P}$, and

  * •

an action of the SP $P^{\prime}$ corresponding to the receiveng (sending) of
this message is in ${\it Pref}(P^{\prime})$.

These dependencies between the actions can be expressed by a diagram of the DP
${\cal P}$, which has the following form:

  * •

each SP $P\in{\cal P}$ is represented by a thread in this diagram, i.e. by a
vertical line on which points corresponding to nodes of ${\it Pref}(P)$ are
marked, the upper point corresponds to $Init(P)$, and

    * –

each point has the number of the corresponding node,

    * –

a name $P$ of the SP $P$ is indicated near the upper point,

    * –

if ${\it Post}(P)=P^{\prime}\neq{\bf 0}$, then $P^{\prime}$ is indicated at
the bottom point,

    * –

near to each segment $l$ connecting adjacent points on the thread, there is a
label $\alpha_{l}$ of an edge from ${\it Pref}(P_{i})$ corresponding to $l$,

  * •

for each segment $l$ connecting adjacent points of the thread, if $\alpha_{l}$
is a sending, $\alpha_{l^{\prime}}$ is an intended receiving for $\alpha_{l}$,
then the diagram contains an arrow, a start of which lies on $l$, and an end
of which lies on $l^{\prime}$.

For example if $P_{i}=\alpha_{1};\;\ldots\;\alpha_{n};P^{\prime}_{i}$, where
$\alpha_{1}$ is a sending, and $\alpha_{n}$ is a receiving, then SP $P_{i}$
corresponds to a thread

$\begin{array}[]{llllllllllllll}\begin{picture}(0.0,90.0)\put(0.0,90.0){\circle*{4.0}}
\put(0.0,60.0){\circle*{4.0}} \put(0.0,30.0){\circle*{4.0}}
\put(0.0,0.0){\circle*{4.0}} \put(0.0,90.0){\line(0,-1){40.0}}
\put(0.0,0.0){\line(0,1){40.0}} \put(0.0,45.0){\makebox(0.0,0.0)[]{$\ldots$}}
\put(-2.0,75.0){\makebox(0.0,0.0)[r]{$\alpha_{1}$}}
\put(-2.0,15.0){\makebox(0.0,0.0)[r]{$\alpha_{n}$}}
\put(-3.0,90.0){\makebox(0.0,0.0)[r]{$0$}}
\put(-3.0,60.0){\makebox(0.0,0.0)[r]{$1$}}
\put(-3.0,30.0){\makebox(0.0,0.0)[r]{${n-1}$}}
\put(-3.0,0.0){\makebox(0.0,0.0)[r]{$n$}}
\put(3.0,-5.0){\makebox(0.0,0.0)[l]{$P_{i}^{\prime}$}}
\put(3.0,90.0){\makebox(0.0,0.0)[l]{$P_{i}$}}
\put(0.0,75.0){\vector(1,0){30.0}} \put(30.0,15.0){\vector(-1,0){30.0}}
\put(36.0,75.0){\makebox(0.0,0.0)[l]{$\ldots$}}
\put(36.0,15.0){\makebox(0.0,0.0)[l]{$\ldots$}} \end{picture}\end{array}$ (39)

Note that the arrows depict only the desired connection between sendings and
receivings, but they have no relation with real communication: it is possible
that the sent message will be received by a SP which is different from a SP to
which it was intended.

For the sake of greater clarity, we will use the following convention in the
notation of variables:

  * •

we will indicate a horizontal bar above a designation of a variable $x$ if
$x\in\bar{X}({\cal P})$ (i.e. this variable is denoted by $\bar{x}$),

  * •

if $P$ is a SP of the form (38), $x\in\hat{X}(P)$, and $i$ is the first index
such that $x\in\alpha_{i}$ (i.e. $\forall\,i^{\prime}=1,\ldots,i-1$
$x\not\in\alpha_{i^{\prime}}$), then occurrences of $x$ in the label
$\alpha_{i}$ of the $i$–th segment of the thread of $P$ are denoted by
$\hat{x}$.

These variable designations also will be used in notations of the form (38).

####  2.6.3 Examples of diagrams of distributed processes

  1. 1.

First example is DP ${\cal P}_{1}=\\{A,B\\}$, which is a model of a
transmission from $A$ to $B$ a message $x$ through a channel $c_{AB}$, where
only $A$ and $B$ know the name of this channel, i.e.

$c_{AB}=shared\\_channel(A,B).$

This DP works as follows:

     * •

$A$ sends the message $x$ to $c_{AB}$,

     * •

$B$ receives this message from $c_{AB}$ and writes it to the variable $y$,
after which it behaves like the SP $P$.

SPs $A$ and $B$ are defined as follows:

$A=c_{AB}!x;{\bf 0},\;\;B=c_{AB}?\hat{y};P.$

A diagram of ${\cal P}_{1}$ has the following form:

$\begin{array}[]{llllllllllllll}\begin{picture}(60.0,40.0)\put(0.0,15.0){\vector(1,0){60.0}}
\put(0.0,0.0){\line(0,1){40.0}} \put(60.0,0.0){\line(0,1){40.0}}
\put(4.0,40.0){\makebox(0.0,0.0)[l]{$A$}}
\put(64.0,40.0){\makebox(0.0,0.0)[l]{$B$}} \put(0.0,40.0){\circle*{4.0}}
\put(60.0,40.0){\circle*{4.0}} \put(0.0,0.0){\circle*{4.0}}
\put(60.0,0.0){\circle*{4.0}} \put(-4.0,40.0){\makebox(0.0,0.0)[r]{$0$}}
\put(-4.0,0.0){\makebox(0.0,0.0)[r]{$1$}}
\put(56.0,40.0){\makebox(0.0,0.0)[r]{$0$}}
\put(56.0,0.0){\makebox(0.0,0.0)[r]{$1$}}
\put(64.0,0.0){\makebox(0.0,0.0)[l]{$P$}}
\put(-3.0,15.0){\makebox(0.0,0.0)[r]{$c_{AB}!x$}}
\put(63.0,15.0){\makebox(0.0,0.0)[l]{$c_{AB}?\hat{y}$}}
\end{picture}\end{array}$ (40)

  2. 2.

Second example is DP ${\cal P}_{2}=\\{A,B\\}$, which is a model of
transmission from $A$ to $B$ EM $k_{AB}(x)$ through an open channel $\circ$.
It is assumed that $A$ and $B$ have a shared secret key $k_{AB}$, on which
they can encrypt and decrypt messages using a symmetric encryption system, and
only $A$ and $B$ know $k_{AB}$, i.e.

$k_{AB}=shared\\_key(A,B).$

This DP works as follows:

     * •

$A$ sends EM $k_{AB}(x)$ to $\circ$,

     * •

$B$ receives EM $k_{AB}(x)$ from $\circ$, decrypts it, writes the extracted
message $x$ to variable $y$, after which it behaves like SP $P$.

SPs $A$ and $B$ are defined as follows:

$A=!k_{AB}(x);{\bf 0},\;\;B=?k_{AB}(\hat{y});P.$

A diagram of ${\cal P}_{2}$ has the following form:

$\begin{array}[]{llllllllllllll}\begin{picture}(60.0,40.0)\put(0.0,40.0){\circle*{4.0}}
\put(60.0,40.0){\circle*{4.0}} \put(0.0,0.0){\circle*{4.0}}
\put(60.0,0.0){\circle*{4.0}} \put(-4.0,40.0){\makebox(0.0,0.0)[r]{$0$}}
\put(-4.0,0.0){\makebox(0.0,0.0)[r]{$1$}}
\put(56.0,40.0){\makebox(0.0,0.0)[r]{$0$}}
\put(56.0,0.0){\makebox(0.0,0.0)[r]{$1$}} \put(0.0,15.0){\vector(1,0){60.0}}
\put(0.0,0.0){\line(0,1){40.0}} \put(60.0,0.0){\line(0,1){40.0}}
\put(4.0,40.0){\makebox(0.0,0.0)[l]{$A$}}
\put(64.0,40.0){\makebox(0.0,0.0)[l]{$B$}}
\put(64.0,0.0){\makebox(0.0,0.0)[l]{$P$}}
\put(-3.0,15.0){\makebox(0.0,0.0)[r]{$!k_{AB}(x)$}}
\put(63.0,15.0){\makebox(0.0,0.0)[l]{$?k_{AB}(\hat{y})$}}
\end{picture}\end{array}$ (41)

  3. 3.

Third example is DP ${\cal P}_{3}=\\{A,B,J\\}$, which is a model of
transmission from $A$ to $B$ a message $x$ over secret channel $\bar{c}$ with
use of a trusted intermediary $J$, where $A$ and $J$ ($B$ and $J$) interact
via channel $c_{AJ}$ ($c_{BJ}$), and only $A$ and $J$ ($B$ and $J$) know the
name $c_{AJ}$ ($c_{BJ}$), i.e.

$\begin{array}[]{llllllllllllll}c_{AJ}=shared\\_channel(A,J),\\\
c_{BJ}=shared\\_channel(B,J).\end{array}$

This DP works as follows:

     * •

$A$ sends $J$ the name of secret channel $\bar{c}$ (which at first only $A$
knows) through the channel $c_{AJ}$,

     * •

$J$ sends $B$ the received channel name $\bar{c}$ through channel $c_{BJ}$,

     * •

$A$ sends to channel $\bar{c}$ the message $x$,

     * •

$B$ receives from channel $\bar{c}$ the message $x$ and writes it to the
variable $y$, after which it behaves like SP $P$.

SPs $A$, $B$ and $J$ are defined as follows:

$\\!\\!\\!\\!\begin{array}[]{llllllllllllll}A=\alpha_{1};\alpha_{2};{\bf
0},\;\alpha_{1}=c_{AJ}!\bar{c},\;\alpha_{2}=\bar{c}!x,\\\ J=j_{1};j_{2};{\bf
0},\;j_{1}=c_{AJ}?\hat{u},\;j_{2}=c_{BJ}!u,\\\
B=\beta_{1};\beta_{2};P,\;\beta_{1}=c_{BJ}?\hat{v},\;\beta_{2}=v?\hat{y}.\end{array}$
(42)

A diagram of ${\cal P}_{3}$ has the following form:

$\begin{array}[]{llllllllllllll}\begin{picture}(0.0,85.0)\put(-60.0,80.0){\circle*{4.0}}
\put(0.0,80.0){\circle*{4.0}} \put(60.0,80.0){\circle*{4.0}}
\par\put(-60.0,45.0){\circle*{4.0}} \put(0.0,57.5){\circle*{4.0}}
\put(60.0,32.5){\circle*{4.0}} \par\put(-60.0,5.0){\circle*{4.0}}
\put(0.0,5.0){\circle*{4.0}} \put(60.0,5.0){\circle*{4.0}}
\par\put(-64.0,85.0){\makebox(0.0,0.0)[r]{$0$}}
\put(-64.0,45.0){\makebox(0.0,0.0)[r]{$1$}}
\put(-64.0,5.0){\makebox(0.0,0.0)[r]{$2$}}
\par\par\put(-4.0,85.0){\makebox(0.0,0.0)[r]{$0$}}
\put(-4.0,60.0){\makebox(0.0,0.0)[r]{$1$}}
\put(-4.0,5.0){\makebox(0.0,0.0)[r]{$2$}}
\par\par\put(56.0,85.0){\makebox(0.0,0.0)[r]{$0$}}
\put(56.0,32.5){\makebox(0.0,0.0)[r]{$1$}}
\put(56.0,5.0){\makebox(0.0,0.0)[r]{$2$}}
\par\put(-60.0,70.0){\vector(1,0){60.0}} \put(0.0,45.0){\vector(1,0){60.0}}
\put(-60.0,20.0){\vector(1,0){120.0}} \put(60.0,5.0){\line(0,1){75.0}}
\put(0.0,5.0){\line(0,1){75.0}} \put(-60.0,5.0){\line(0,1){75.0}}
\par\put(-56.0,85.0){\makebox(0.0,0.0)[l]{$A$}}
\put(4.0,85.0){\makebox(0.0,0.0)[l]{$J$}}
\put(64.0,85.0){\makebox(0.0,0.0)[l]{$B$}}
\put(64.0,0.0){\makebox(0.0,0.0)[l]{$P$}}
\put(-63.0,70.0){\makebox(0.0,0.0)[r]{$\alpha_{1}$}}
\put(-3.0,45.0){\makebox(0.0,0.0)[r]{$j_{2}$}}
\put(3.0,70.0){\makebox(0.0,0.0)[l]{$j_{1}$}}
\put(-63.0,20.0){\makebox(0.0,0.0)[r]{$\alpha_{2}$}}
\put(63.0,20.0){\makebox(0.0,0.0)[l]{$\beta_{2}$}}
\put(63.0,48.0){\makebox(0.0,0.0)[l]{$\beta_{1}$}}
\par\end{picture}\end{array}$ (43)

  4. 4.

Fourth example is ${\cal P}_{4}=\\{A,B,J\\}$ (called Wide-Mouth Frog (WMF)
protocol), which is a model of a transmission from $A$ to $B$ EM $\bar{k}(x)$
through open channel $\circ$ with use of a trusted intermediary $J$, with whom
$A$ and $B$ interact through $\circ$. $A$ creates a secret key $\bar{k}$,
sends $J$ this encrypted key for $B$, and then sends $B$ EM $\bar{k}(x)$.

It is assumed that $A$ and $J$ ($B$ and $J$) have a shared secret key $k_{AJ}$
($k_{BJ}$), on which they can encrypt and decrypt messages using a symmetric
encryption system, and only $A$ and $J$ ($B$ and $J$) know $k_{AJ}$
($k_{BJ}$), i.e.

$\begin{array}[]{llllllllllllll}k_{AJ}=shared\\_key(A,J),\\\
k_{BJ}=shared\\_key(B,J).\end{array}$

This DP works as follows.

     * •

$A$ creates a secret key $\bar{k}$ (at first only $A$ knows this key) and
sends $J$ EM $k_{AJ}(\bar{k})$ through $\circ$, then $A$ sends $B$ EM
$\bar{k}(x)$,

     * •

$J$ receives a message from $A$, decrypts it, then encrypts the extracted key
$\bar{k}$ with the key $k_{BJ}$, and sends $B$ the EM $k_{BJ}(\bar{k})$,

     * •

$B$ extracts the key $\bar{k}$ from the received message from $J$, and then
uses this key to extract the message $x$ from the received message from $A$,
writes it to the variable $y$, and then behaves like SP $P$.

SPs $A$, $B$ and $J$ are defined as follows:

$\\!\\!\\!\\!\\!\\!\\!\\!\begin{array}[]{llllllllllllll}A=\alpha_{1};\alpha_{2};{\bf
0},\;\alpha_{1}=!k_{AJ}(\bar{k}),\;\alpha_{2}=!\bar{k}(x),\\\
J=j_{1};j_{2};{\bf 0},\;j_{1}=?k_{AJ}(\hat{u}),\;j_{2}=!{k_{BJ}(u)},\\\
B=\beta_{1};\beta_{2};P,\;\beta_{1}=?k_{BJ}(\hat{v}),\;\beta_{2}=?v(\hat{y}).\end{array}$
(44)

A diagram of ${\cal P}_{4}$ has the form (43).

###  2.7 Transition graphs of distributed processes

In this section, we consider DPs consisting of a finite number of SPs. For a
visual representation of an execution of such DPs, the concept of transition
graph of a DP is introduced. An execution of a DP can be presented as a walk
in a GP corresponding to this DP.

Below in this section, the symbol ${\cal P}$ denotes a DP consisting of a
finite number of SPs, each of which is different from $P_{\dagger}$.

####  2.7.1 A concept of a transition graph of a distributed process

Let ${\cal P}$ be a DP of the form $\\{P_{1},\ldots,P_{n}\\}$. A transition
graph (TG) of ${\cal P}$ is a graph $G_{\cal P}$, where

  * •

each node of $G_{\cal P}$ is a list $at=(at_{1},\ldots,at_{n})$, where
$\forall\,i=1,\ldots,n\;\;at_{i}\in P_{i},$

  * •

each edge of $G_{\cal P}$ has the form

$(at_{1},\ldots,at_{n})\;\mathop{\longrightarrow}\limits^{\\!\\!\alpha_{P_{i}}}\;(at^{\prime}_{1},\ldots,at^{\prime}_{n}),$

where $i\in\\{1,\dots,n\\}$, $P_{i}$ has edge
$at_{i}\;\mathop{\to}\limits^{\begin{picture}(0.0,5.0)\put(-3.0,2.0){\makebox(0.0,1.0)[]{$\scriptstyle\alpha$}}
\end{picture}}\;at^{\prime}_{i}$, and
$at_{i^{\prime}}=at^{\prime}_{i^{\prime}}$ for $i^{\prime}\neq i$.

A node $Init(G_{\cal P})=(Init(P_{1}),\ldots,Init(P_{n}))$ of $G_{\cal P}$ is
said to be initial.

$\forall\,s\in\Sigma_{\cal P}$, the component $at_{s}$ of $s$ can be
considered as a node of $G_{\cal P}$.

Let there is given an execution of a DP ${\cal P}$, and
$s_{0},s_{1},\ldots,s_{n}$ be a sequence of states generated in this
execution. From the definition of a transition relation (8) it follows that
this sequence corresponds to a walk in TG $G_{\cal P}$, which can be
considered as a representation of the execution of ${\cal P}$:

$\\!\\!\\!\begin{array}[]{llllllllllllll}Init(G_{\cal
P})=at_{s_{0}}\\!\;\mathop{\longrightarrow}\limits^{\\!(\alpha_{1})_{P_{i_{1}}}}\;\\!at_{s_{1}}\\!\;\mathop{\longrightarrow}\limits^{\\!(\alpha_{2})_{P_{i_{2}}}}\;\\!\ldots\\!\;\mathop{\longrightarrow}\limits^{\\!(\alpha_{n})_{P_{i_{n}}}}\;\\!at_{s_{n}}\end{array}$

Recall that ${\cal P}_{\dagger}=\\{{\cal P},P_{\dagger}\\}$. The TG $G_{{\cal
P}_{\dagger}}$ can be considered as a graph obtained from $G_{{\cal P}}$ by
adding edges
$at\;\mathop{\longrightarrow}\limits^{\\!\alpha_{P_{\dagger}}}\;at$, where
$at\in G_{{\cal P}}$, $\alpha\in Act$.

A node $at\in G_{{\cal P}}$ is said to be reachable if for some
$s\in\Sigma_{{\cal P}_{\dagger}}\;\;at=at_{s}$.

An edge of $G_{\cal P}$ is said to be realizable, if it lies on a path
corresponding to some execution of ${\cal P}_{\dagger}$.

The following conventions will be used in graphical representation of TGs:

  * •

each node $at=(at_{1},\ldots,at_{n})$ of a TG is represented by an oval, with
a list $at_{1}\ldots at_{n}$ of components of $at$ inside this oval,

  * •

an initial node is represented by a double oval,

  * •

a black circle on an edge of a TG means that this edge is unrealizable (this
unrealizability should be justified by special reasoning),

  * •

in order to abbreviate notations, a label of an edge
$at\;\mathop{\longrightarrow}\limits^{\\!\alpha_{P}}\;at^{\prime}$ of a TG can
be denoted simply by the action $\alpha$ in this label (without specifying the
SP $P$ performing the action $\alpha$ on this transition).

####  2.7.2 Examples of transition graphs of distributed processes

In this section we present TGs for DPs defined in 2.6.3. We use the following
convention: if $A$ is a name of a SP occurred in some of these DPs, and $i$ is
a number of a point on a thread corresponding to this SP, then the node of the
graph $A$ corresponding to this point is denoted by $A^{i}$.

  1. 1.

TGs for ${\cal P}_{1}$, ${\cal P}_{2}$ described by (40), (41), have the form

$\begin{array}[]{llllllllllllll}\begin{picture}(150.0,65.0)\put(25.0,50.0){\circle*{4.0}}
\put(0.0,50.0){\oval(34.0,20.0)}
\put(0.0,50.0){\makebox(0.0,0.0)[c]{${A^{0}B^{0}}$}}
\put(100.0,50.0){\oval(34.0,20.0)}
\put(100.0,50.0){\makebox(0.0,0.0)[c]{${A^{0}B^{1}}$}}
\put(0.0,0.0){\oval(34.0,20.0)} \put(0.0,50.0){\oval(38.0,24.0)}
\put(0.0,0.0){\makebox(0.0,0.0)[c]{${A^{1}B^{0}}$}}
\put(100.0,0.0){\oval(34.0,20.0)}
\put(100.0,0.0){\makebox(0.0,0.0)[c]{${A^{1}B^{1}}$}}
\par\put(0.0,38.0){\vector(0,-1){28.0}} \put(100.0,40.0){\vector(0,-1){30.0}}
\par\put(17.0,0.0){\vector(1,0){66.0}} \put(19.0,50.0){\vector(1,0){64.0}}
\par\put(2.0,25.0){\makebox(0.0,0.0)[r]{ $c_{AB}!x$ }}
\put(98.0,25.0){\makebox(0.0,0.0)[r]{ $c_{AB}!x$ }}
\par\put(50.0,0.0){\makebox(0.0,0.0)[b]{ $c_{AB}?\hat{y}$ }}
\par\put(50.0,50.0){\makebox(0.0,0.0)[b]{ $c_{AB}?\hat{y}$ }}
\par\par\put(117.0,54.0){\vector(3,1){20.0}}
\put(117.0,46.0){\vector(3,-1){20.0}} \put(130.0,50.0){\makebox(0.0,0.0)[]{
$\ldots$ }} \par\put(117.0,4.0){\vector(3,1){20.0}}
\put(117.0,-4.0){\vector(3,-1){20.0}} \put(130.0,0.0){\makebox(0.0,0.0)[]{
$\ldots$ }} \end{picture}\end{array}$ (45)

$\begin{array}[]{llllllllllllll}\begin{picture}(150.0,65.0)\put(25.0,50.0){\circle*{4.0}}
\put(0.0,50.0){\oval(34.0,20.0)}
\put(0.0,50.0){\makebox(0.0,0.0)[c]{${A^{0}B^{0}}$}}
\put(100.0,50.0){\oval(34.0,20.0)}
\put(100.0,50.0){\makebox(0.0,0.0)[c]{${A^{0}B^{1}}$}}
\par\put(0.0,0.0){\oval(34.0,20.0)} \put(0.0,50.0){\oval(38.0,24.0)}
\put(0.0,0.0){\makebox(0.0,0.0)[c]{${A^{1}B^{0}}$}}
\put(100.0,0.0){\oval(34.0,20.0)}
\put(100.0,0.0){\makebox(0.0,0.0)[c]{${A^{1}B^{1}}$}}
\par\put(0.0,38.0){\vector(0,-1){28.0}} \put(100.0,40.0){\vector(0,-1){30.0}}
\par\put(17.0,0.0){\vector(1,0){66.0}} \put(19.0,50.0){\vector(1,0){64.0}}
\par\put(2.0,25.0){\makebox(0.0,0.0)[l]{ $!k_{AB}(x)$ }}
\put(98.0,25.0){\makebox(0.0,0.0)[l]{ $!k_{AB}(x)$ }}
\par\put(50.0,0.0){\makebox(0.0,0.0)[b]{ $?k_{AB}(\hat{y})$ }}
\par\put(50.0,50.0){\makebox(0.0,0.0)[b]{ $?k_{AB}(\hat{y})$ }}
\par\par\put(117.0,54.0){\vector(3,1){20.0}}
\put(117.0,46.0){\vector(3,-1){20.0}} \put(130.0,50.0){\makebox(0.0,0.0)[]{
$\ldots$ }} \put(117.0,4.0){\vector(3,1){20.0}}
\put(117.0,-4.0){\vector(3,-1){20.0}} \put(130.0,0.0){\makebox(0.0,0.0)[]{
$\ldots$}} \par\par\end{picture}\par\end{array}\vspace{4mm}$ (46)

where slant arrows indicate edges of the TGs outgoing from the corresponding
nodes, as well as parts of the TGs that are reachable after traversing those
edges that are not represented in this graphical representation, this
convention will also be used in other TG examples.

  2. 2.

A TG for DPs ${\cal P}_{3}$ and ${\cal P}_{4}$, described by (43) has the form
(47).

$\begin{array}[]{llllllllllllll}\begin{picture}(150.0,270.0)\put(-75.0,200.0){\circle*{4.0}}
\put(-89.0,216.0){\circle*{4.0}} \par\par\put(117.0,4.0){\vector(3,1){20.0}}
\put(117.0,-4.0){\vector(3,-1){20.0}}
\put(130.0,0.0){\makebox(0.0,0.0)[]{$\ldots$}}
\put(147.0,34.0){\vector(3,1){20.0}} \put(147.0,26.0){\vector(3,-1){20.0}}
\put(160.0,30.0){\makebox(0.0,0.0)[]{$\ldots$}}
\put(177.0,64.0){\vector(3,1){20.0}} \put(177.0,56.0){\vector(3,-1){20.0}}
\put(190.0,60.0){\makebox(0.0,0.0)[]{$\ldots$}}
\par\put(117.0,104.0){\vector(3,1){20.0}}
\put(117.0,96.0){\vector(3,-1){20.0}}
\put(130.0,100.0){\makebox(0.0,0.0)[]{$\ldots$}}
\put(147.0,134.0){\vector(3,1){20.0}} \put(147.0,126.0){\vector(3,-1){20.0}}
\put(160.0,130.0){\makebox(0.0,0.0)[]{$\ldots$}}
\put(177.0,164.0){\vector(3,1){20.0}} \put(177.0,156.0){\vector(3,-1){20.0}}
\put(190.0,160.0){\makebox(0.0,0.0)[]{$\ldots$}}
\par\put(117.0,204.0){\vector(3,1){20.0}}
\put(117.0,196.0){\vector(3,-1){20.0}}
\put(130.0,200.0){\makebox(0.0,0.0)[]{$\ldots$}}
\put(147.0,234.0){\vector(3,1){20.0}} \put(147.0,226.0){\vector(3,-1){20.0}}
\put(160.0,230.0){\makebox(0.0,0.0)[]{$\ldots$}}
\put(177.0,264.0){\vector(3,1){20.0}} \put(177.0,256.0){\vector(3,-1){20.0}}
\put(190.0,260.0){\makebox(0.0,0.0)[]{$\ldots$}}
\par\par\par\put(-100.0,200.0){\oval(34.0,20.0)}
\put(-100.0,200.0){\oval(38.0,24.0)}
\put(-100.0,200.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{0}J^{0}B^{0}}$}}
\put(0.0,200.0){\oval(34.0,20.0)}
\put(0.0,200.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{0}J^{0}B^{1}}$}}
\put(100.0,200.0){\oval(34.0,20.0)}
\put(100.0,200.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{0}J^{0}B^{2}}$}}
\par\put(-70.0,230.0){\oval(34.0,20.0)}
\put(-70.0,230.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{0}J^{1}B^{0}}$}}
\put(30.0,230.0){\oval(34.0,20.0)}
\put(30.0,230.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{0}J^{1}B^{1}}$}}
\put(130.0,230.0){\oval(34.0,20.0)}
\put(130.0,230.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{0}J^{1}B^{2}}$}}
\par\put(-40.0,260.0){\oval(34.0,20.0)}
\put(-40.0,260.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{0}J^{2}B^{0}}$}}
\put(60.0,260.0){\oval(34.0,20.0)}
\put(60.0,260.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{0}J^{2}B^{1}}$}}
\put(160.0,260.0){\oval(34.0,20.0)}
\put(160.0,260.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{0}J^{2}B^{2}}$}}
\par\par\put(-100.0,100.0){\oval(34.0,20.0)}
\put(-100.0,100.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{1}J^{0}B^{0}}$}}
\put(0.0,100.0){\oval(34.0,20.0)}
\put(0.0,100.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{1}J^{0}B^{1}}$}}
\put(100.0,100.0){\oval(34.0,20.0)}
\put(100.0,100.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{1}J^{0}B^{2}}$}}
\par\put(-70.0,130.0){\oval(34.0,20.0)}
\put(-70.0,130.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{1}J^{1}B^{0}}$}}
\put(30.0,130.0){\oval(34.0,20.0)}
\put(30.0,130.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{1}J^{1}B^{1}}$}}
\put(130.0,130.0){\oval(34.0,20.0)}
\put(130.0,130.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{1}J^{1}B^{2}}$}}
\par\put(-40.0,160.0){\oval(34.0,20.0)}
\put(-40.0,160.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{1}J^{2}B^{0}}$}}
\put(60.0,160.0){\oval(34.0,20.0)}
\put(60.0,160.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{1}J^{2}B^{1}}$}}
\put(160.0,160.0){\oval(34.0,20.0)}
\put(160.0,160.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{1}J^{2}B^{2}}$}}
\par\par\put(-100.0,0.0){\oval(34.0,20.0)}
\put(-100.0,0.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{2}J^{0}B^{0}}$}}
\put(0.0,0.0){\oval(34.0,20.0)}
\put(0.0,0.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{2}J^{0}B^{1}}$}}
\put(100.0,0.0){\oval(34.0,20.0)}
\put(100.0,0.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{2}J^{0}B^{2}}$}}
\par\put(-70.0,30.0){\oval(34.0,20.0)}
\put(-70.0,30.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{2}J^{1}B^{0}}$}}
\put(30.0,30.0){\oval(34.0,20.0)}
\put(30.0,30.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{2}J^{1}B^{1}}$}}
\put(130.0,30.0){\oval(34.0,20.0)}
\put(130.0,30.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{2}J^{1}B^{2}}$}}
\par\put(-40.0,60.0){\oval(34.0,20.0)}
\put(-40.0,60.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{2}J^{2}B^{0}}$}}
\put(60.0,60.0){\oval(34.0,20.0)}
\put(60.0,60.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{2}J^{2}B^{1}}$}}
\put(160.0,60.0){\oval(34.0,20.0)}
\put(160.0,60.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{2}J^{2}B^{2}}$}}
\par\par\put(-100.0,188.0){\vector(0,-1){78.0}}
\put(0.0,190.0){\vector(0,-1){80.0}} \put(100.0,190.0){\vector(0,-1){80.0}}
\put(-100.0,90.0){\vector(0,-1){80.0}} \put(0.0,90.0){\vector(0,-1){80.0}}
\put(100.0,90.0){\vector(0,-1){80.0}}
\par\put(-70.0,220.0){\vector(0,-1){80.0}}
\put(30.0,220.0){\vector(0,-1){80.0}} \put(130.0,220.0){\vector(0,-1){80.0}}
\put(-70.0,120.0){\vector(0,-1){80.0}} \put(30.0,120.0){\vector(0,-1){80.0}}
\put(130.0,120.0){\vector(0,-1){80.0}}
\par\put(-40.0,250.0){\vector(0,-1){80.0}}
\put(60.0,250.0){\vector(0,-1){80.0}} \put(160.0,250.0){\vector(0,-1){80.0}}
\put(-40.0,150.0){\vector(0,-1){80.0}} \put(60.0,150.0){\vector(0,-1){80.0}}
\put(160.0,150.0){\vector(0,-1){80.0}}
\par\par\put(-81.0,200.0){\vector(1,0){64.0}}
\put(17.0,200.0){\vector(1,0){66.0}} \put(-83.0,100.0){\vector(1,0){66.0}}
\put(17.0,100.0){\vector(1,0){66.0}} \put(-83.0,0.0){\vector(1,0){66.0}}
\put(17.0,0.0){\vector(1,0){66.0}} \par\put(-53.0,230.0){\vector(1,0){66.0}}
\put(47.0,230.0){\vector(1,0){66.0}} \put(-53.0,130.0){\vector(1,0){66.0}}
\put(47.0,130.0){\vector(1,0){66.0}} \put(-53.0,30.0){\vector(1,0){66.0}}
\put(47.0,30.0){\vector(1,0){66.0}} \par\put(-23.0,260.0){\vector(1,0){66.0}}
\put(77.0,260.0){\vector(1,0){66.0}} \put(-23.0,160.0){\vector(1,0){66.0}}
\put(77.0,160.0){\vector(1,0){66.0}} \put(-23.0,60.0){\vector(1,0){66.0}}
\put(77.0,60.0){\vector(1,0){66.0}}
\par\par\put(-93.0,212.0){\vector(1,1){10.0}}
\put(10.0,210.0){\vector(1,1){10.0}} \put(110.0,210.0){\vector(1,1){10.0}}
\put(-60.0,240.0){\vector(1,1){10.0}} \put(40.0,240.0){\vector(1,1){10.0}}
\put(140.0,240.0){\vector(1,1){10.0}}
\par\put(-90.0,110.0){\vector(1,1){10.0}} \put(10.0,110.0){\vector(1,1){10.0}}
\put(110.0,110.0){\vector(1,1){10.0}} \put(-60.0,140.0){\vector(1,1){10.0}}
\put(40.0,140.0){\vector(1,1){10.0}} \put(140.0,140.0){\vector(1,1){10.0}}
\par\put(-90.0,10.0){\vector(1,1){10.0}} \put(10.0,10.0){\vector(1,1){10.0}}
\put(110.0,10.0){\vector(1,1){10.0}} \put(-60.0,40.0){\vector(1,1){10.0}}
\put(40.0,40.0){\vector(1,1){10.0}} \put(140.0,40.0){\vector(1,1){10.0}}
\par\par\par\put(-97.0,150.0){\makebox(0.0,0.0)[r]{ $\alpha_{1}$ }}
\put(3.0,150.0){\makebox(0.0,0.0)[r]{ $\alpha_{1}$ }}
\put(103.0,150.0){\makebox(0.0,0.0)[r]{ $\alpha_{1}$ }}
\par\put(-67.0,180.0){\makebox(0.0,0.0)[r]{ $\alpha_{1}$ }}
\put(33.0,180.0){\makebox(0.0,0.0)[r]{ $\alpha_{1}$ }}
\put(133.0,180.0){\makebox(0.0,0.0)[r]{ $\alpha_{1}$ }}
\par\put(-42.0,210.0){\makebox(0.0,0.0)[l]{ $\alpha_{1}$ }}
\put(58.0,210.0){\makebox(0.0,0.0)[l]{ $\alpha_{1}$ }}
\put(158.0,210.0){\makebox(0.0,0.0)[l]{ $\alpha_{1}$ }}
\par\par\par\par\put(-97.0,50.0){\makebox(0.0,0.0)[r]{ $\alpha_{2}$ }}
\put(3.0,50.0){\makebox(0.0,0.0)[r]{ $\alpha_{2}$ }}
\put(103.0,50.0){\makebox(0.0,0.0)[r]{ $\alpha_{2}$ }}
\par\put(-67.0,80.0){\makebox(0.0,0.0)[r]{ $\alpha_{2}$ }}
\put(33.0,80.0){\makebox(0.0,0.0)[r]{ $\alpha_{2}$ }}
\put(133.0,80.0){\makebox(0.0,0.0)[r]{ $\alpha_{2}$ }}
\par\put(-42.0,110.0){\makebox(0.0,0.0)[l]{ $\alpha_{2}$ }}
\put(58.0,110.0){\makebox(0.0,0.0)[l]{ $\alpha_{2}$ }}
\put(158.0,110.0){\makebox(0.0,0.0)[l]{ $\alpha_{2}$ }}
\par\par\put(-50.0,0.0){\makebox(0.0,0.0)[b]{ $\beta_{1}$ }}
\put(50.0,0.0){\makebox(0.0,0.0)[b]{ $\beta_{2}$ }}
\put(-20.0,30.0){\makebox(0.0,0.0)[b]{ $\beta_{1}$ }}
\put(70.0,30.0){\makebox(0.0,0.0)[b]{ $\beta_{2}$ }}
\put(10.0,60.0){\makebox(0.0,0.0)[b]{ $\beta_{1}$ }}
\put(110.0,60.0){\makebox(0.0,0.0)[b]{ $\beta_{2}$ }}
\par\put(-50.0,100.0){\makebox(0.0,0.0)[b]{ $\beta_{1}$ }}
\put(50.0,100.0){\makebox(0.0,0.0)[b]{ $\beta_{2}$ }}
\put(-20.0,130.0){\makebox(0.0,0.0)[b]{ $\beta_{1}$ }}
\put(70.0,130.0){\makebox(0.0,0.0)[b]{ $\beta_{2}$ }}
\put(10.0,160.0){\makebox(0.0,0.0)[b]{ $\beta_{1}$ }}
\put(110.0,160.0){\makebox(0.0,0.0)[b]{ $\beta_{2}$ }}
\par\put(-50.0,200.0){\makebox(0.0,0.0)[b]{ $\beta_{1}$ }}
\put(50.0,200.0){\makebox(0.0,0.0)[b]{ $\beta_{2}$ }}
\put(-20.0,230.0){\makebox(0.0,0.0)[b]{ $\beta_{1}$ }}
\put(70.0,230.0){\makebox(0.0,0.0)[b]{ $\beta_{2}$ }}
\put(10.0,260.0){\makebox(0.0,0.0)[b]{ $\beta_{1}$ }}
\put(110.0,260.0){\makebox(0.0,0.0)[b]{ $\beta_{2}$ }}
\par\par\put(-82.0,17.0){\makebox(0.0,0.0)[r]{ $j_{1}$ }}
\put(18.0,17.0){\makebox(0.0,0.0)[r]{ $j_{1}$ }}
\put(118.0,17.0){\makebox(0.0,0.0)[r]{ $j_{1}$ }}
\par\put(-82.0,117.0){\makebox(0.0,0.0)[r]{ $j_{1}$ }}
\put(18.0,117.0){\makebox(0.0,0.0)[r]{ $j_{1}$ }}
\put(118.0,117.0){\makebox(0.0,0.0)[r]{ $j_{1}$ }}
\par\put(-87.0,221.0){\makebox(0.0,0.0)[r]{ $j_{1}$ }}
\put(18.0,217.0){\makebox(0.0,0.0)[r]{ $j_{1}$ }}
\put(118.0,217.0){\makebox(0.0,0.0)[r]{ $j_{1}$ }}
\par\par\put(-52.0,47.0){\makebox(0.0,0.0)[r]{ $j_{2}$ }}
\put(48.0,47.0){\makebox(0.0,0.0)[r]{ $j_{2}$ }}
\put(148.0,47.0){\makebox(0.0,0.0)[r]{ $j_{2}$ }}
\par\put(-52.0,147.0){\makebox(0.0,0.0)[r]{ $j_{2}$ }}
\put(48.0,147.0){\makebox(0.0,0.0)[r]{ $j_{2}$ }}
\put(148.0,147.0){\makebox(0.0,0.0)[r]{ $j_{2}$ }}
\par\put(-52.0,247.0){\makebox(0.0,0.0)[r]{ $j_{2}$ }}
\put(48.0,247.0){\makebox(0.0,0.0)[r]{ $j_{2}$ }}
\put(148.0,247.0){\makebox(0.0,0.0)[r]{ $j_{2}$ }}
\par\par\par\end{picture}\end{array}$ (47)

####  2.7.3 Validity of formulas at nodes of transition graphs of distributed
processes

Let ${\cal P}$ be a DP. $\forall\,at\in G_{\cal P}$, $\forall\,\varphi\in Fm$,
the notation $at\models\varphi$ denotes the statement

$\mbox{$\varphi$ is true at the node $at$}.$ (48)

(48) is valid iff $\forall\,s\in\Sigma_{{\cal
P}_{\dagger}}\;\;at_{s}=at\Rightarrow s\models\varphi.$

It is easy to prove that TGs $G_{{\cal P}_{i}}$, where ${\cal
P}_{i}\;(i=1,\ldots,4)$ are DPs defined in section 2.6.3 , have the following
properties:

$\left.\begin{array}[]{llllllllllllll}Init(G_{{\cal
P}_{1}})\models\\{\varphi_{1},[{c_{AB}}]=\emptyset\\}\\\ Init(G_{{\cal
P}_{2}})\models\\{\varphi_{2},k_{AB}^{-1}[\circ]=\emptyset\\}\\\ Init(G_{{\cal
P}_{3}})\models\\{\varphi_{3},[{c_{AJ}}]=\emptyset,\\\ \hskip
56.9055pt[{c_{BJ}}]=\emptyset,[\bar{c}]=\emptyset\\}\\\ Init(G_{{\cal
P}_{4}})\models\\{\varphi_{4},k_{AJ}^{-1}[\circ]=\emptyset,\\\ \hskip
56.9055ptk_{BJ}^{-1}[\circ]=\emptyset,\bar{k}^{-1}[\circ]=\emptyset\\}\end{array}\right\\}$
(49)

where

$\begin{array}[]{llllllllllllll}\varphi_{1}=\\{c_{AB}\\}\,\bot_{\bf
C}\,P_{\dagger}\\\
\varphi_{2}={\left\\{\begin{array}[]{lllll}\\{k_{AB}\\}\,\bot_{\bf
K}\,P_{\dagger}\\\ k_{AB}^{-1}[P_{\dagger}]\subseteq
k_{AB}^{-1}[\circ]\end{array}\right\\}}\\\
\varphi_{3}=\\{c_{AJ},c_{BJ},\bar{c}\\}\,\bot_{\bf C}\,P_{\dagger}\\\
\varphi_{4}={\left\\{\begin{array}[]{lllll}\\{k_{AJ},k_{BJ},\bar{k}\\}\,\bot_{\bf
K}\,P_{\dagger}\\\ k_{AJ}^{-1}[P_{\dagger}]\subseteq k_{AJ}^{-1}[\circ]\\\
k_{BJ}^{-1}[P_{\dagger}]\subseteq k_{BJ}^{-1}[\circ]\\\
\bar{k}^{-1}[P_{\dagger}]\subseteq\bar{k}^{-1}[\circ]\end{array}\right\\}}\end{array}$

Indeed, for any DP ${\cal P}$, a state $s\in\Sigma_{{\cal P}_{\dagger}}$ has
the property $at_{s}=Init(G_{{\cal P}})$ if $s=0$, or there is a path from 0
to $s$ with edge labels of the form $\alpha_{P_{\dagger}}$, and for each
formula $\psi_{i}=\\{\varphi_{i},\ldots\\}$ in (49)

  * •

the truth of $\psi_{i}$ in the initial state of DP $({\cal P}_{i})_{\dagger}$
follows from the definitions of the concept of an initial state and the SP
$P_{\dagger}$, and

  * •

the truth of $\psi_{i}$ in a state $s$, to which there is a path from 0 with
edge labels of the form $\alpha_{P_{\dagger}}$, is substantiated by the
statement

$\begin{array}[]{llllllllllllll}\forall\,s^{\prime},s^{\prime\prime}\in\Sigma_{{\cal
P}_{\dagger}}:s^{\prime}\;\mathop{\longrightarrow}\limits^{\\!\alpha_{P_{\dagger}}}\;s^{\prime\prime}\\\
(s^{\prime}\models\psi_{i}\;\;\Rightarrow\;\;s^{\prime\prime}\models\psi_{i})\end{array}$
(50)

which follows from theorem 2.4.1 ($i=1,3$), or theorem 2.4.2 ($i=2,4$).

We will use statements (49) in solutions for the verification problem for some
properties of DPs ${\cal P}_{i}\;(i=1,\ldots,4)$ presented below.

##  3 Verification of cryptographic protocols

Methods of verification of CPs presented in this section are based on a
representation of CPs in the form of DPs. To prove properties of DPs, we use
theorems from previous section. First method of verification of CPs described
below is based on the concept of a TG, and the second method is based on
theorem 2.5 and is most suitable for verification of authentication CPs.

In this section we assume that the symbol ${\cal P}$ denotes a DP that does
not contain $P_{\dagger}$.

###  3.1 Verification method based on transition graphs

####  3.1.1 Method description

Some properties of DPs can be expressed by formulas, related to reachable
nodes of corresponding TGs. For example, one of properties of DP ${\cal
P}_{i}$, where $i=1,\ldots,4$, defined in section 2.6.3, has the following
form:

$\begin{array}[]{llllllllllllll}\mbox{if a reachable node $at=(at_{A},at_{B})$
or}\\\ \mbox{$(at_{A},at_{J},at_{B})$ of TG $G_{{\cal P}_{i}}$ is such that
}\\\ \mbox{$at_{B}=1$ ($i=1,2$) or $at_{B}=2$ ($i=3,4$),}\\\ \mbox{then
$at\models x=y$.}\end{array}$ (51)

This property is called an integrity and has the following meaning:

  * •

if an execution of the DP $({\cal P}_{i})_{\dagger}=\\{A,B,P_{\dagger}\\}$ or
$\\{A,J,B,P_{\dagger}\\}$ has reached a state where the receiver $B$ ends a
part of its execution, related to a receiving of a message from the sender
$A$,

  * •

then for any opposition of the adversary $P_{\dagger}$ the transmitted message
$x$ in $A$ is equal to the value that the variable $y$ in $B$ will be
assigned.

If a property of a DP ${\cal P}$ has the form $at\models\varphi$, where $at$
is a reachable node of $G_{{\cal P}}$, then a method for verification this
property is the following:

  * •

for each reachable node $at^{\prime}$ located on some path from $Init(G_{{\cal
P}})$ to $at$, a formula $\varphi_{at^{\prime}}$ which is true in
$at^{\prime}$, is calculated, and

  * •

the property $\varphi_{at}\leq\varphi$ is checked.

The need to calculate the above formulas for all nodes on paths from
$Init(G_{{\cal P}})$ to $at$ is due to the fact that to calculate
$\varphi_{at}$ you need to know the formulas $\varphi_{at^{\prime}}$ for each
reachable node $at^{\prime}$ from which there is a realizable edge to $at$,
and so on.

The method for calculating $\varphi_{at}$ is as follows:

  * •

if $\varphi_{at^{\prime}}$ is calculated for some reachable node $at^{\prime}$
such that there is an edge
$at^{\prime}\;\mathop{\to}\limits^{\begin{picture}(0.0,5.0)\put(-3.0,2.0){\makebox(0.0,1.0)[]{$\scriptstyle\alpha$}}
\end{picture}}\;at$, then the formula $\alpha(\varphi_{at^{\prime}})$ is
calculated, the meaning of which is as follows: if $\varphi_{at^{\prime}}$ is
true in state $s$, and
$s\;\mathop{\to}\limits^{\begin{picture}(0.0,5.0)\put(-3.0,2.0){\makebox(0.0,1.0)[]{$\scriptstyle\alpha$}}
\end{picture}}\;s^{\prime}$, then $\alpha(\varphi_{at^{\prime}})$ is true in
each state to which there is a path from $s^{\prime}$ with edge labels of the
form $\alpha_{P_{\dagger}}$,

  * •

$\varphi_{at}$ is defined as an analogue of a disjunction of formulas from the
set $\\{\alpha(\varphi_{at^{\prime}})\mid
at^{\prime}\;\mathop{\to}\limits^{\begin{picture}(0.0,5.0)\put(-3.0,2.0){\makebox(0.0,1.0)[]{$\scriptstyle\alpha$}}
\end{picture}}\;at\\}.$

For an initial node $at^{0}=Init(G_{{\cal P}})$ the corresponding formula
$\varphi_{at^{0}}$ is assumed to be given. For example, for DPs ${\cal
P}_{i}\;(i=1,\ldots,4)$ defined in 2.6.3, such formulas can be taken from the
corresponding statements in (49).

Below we present examples of using this method for a verification of DPs, in
which secure channels (${\cal P}_{1}$ and ${\cal P}_{3}$) or secure keys
(${\cal P}_{2}$ and ${\cal P}_{4}$) are used. Before verification of these
DPs, we state theorems used for verification of these DPs.

####  3.1.2 Theorems for verification of processes with secure channels

In this section, we will use the following notation:

$\begin{array}[]{llllllllllllll}\forall\,E\subseteq Tm,\forall\,\alpha\in
Act,\forall\,c\in Tm_{\bf C}\\\ E_{c,\alpha}=E\cup\\{e\\},\mbox{ if
$\alpha=c!e$, and }\\\ E_{c,\alpha}=E,\mbox{ otherwise.}\end{array}$ (52)

Theorem 7.

Let ${\cal P}$ be a DP, $E$ be a subseteq of $\langle{\cal P}\rangle_{0}$,
$s,s^{\prime}$ be states from $\Sigma_{{\cal P}_{\dagger}}$ such that
$s\;\mathop{\longrightarrow}\limits^{\\!\\!\alpha_{P}}\;s^{\prime}$, where
$P\in{\cal P}$, and if $\alpha=c!e$, then the implication holds:

$c^{s}\not\in E\;\;\Rightarrow\;\;Var(e^{s})\cap E=\emptyset.$ (53)

Then $\forall\,E^{\prime},E^{\prime\prime}\subseteq Tm$, $\forall\,c\in E_{\bf
C}$ the following implication holds:

$\begin{array}[]{llllllllllllll}s\models{\left\\{\begin{array}[]{lllll}E\,\bot_{\bf
C}\,P_{\dagger}\\\ E^{\prime}\subseteq[c]\subseteq
E^{\prime\prime}\end{array}\right\\}}\Rightarrow\\\ \Rightarrow
s^{\prime}\models{\left\\{\begin{array}[]{lllll}E\,\bot_{\bf
C}\,P_{\dagger}\\\ E^{\prime}_{c,\alpha}\subseteq[c]\subseteq
E^{\prime\prime}_{c,\alpha}\end{array}\right\\}}\end{array}$

Proof.

According to (3), the value of the formula $E\,\bot_{\bf C}\,P_{\dagger}$ in
$s$ depends only on the sets $[P_{\dagger}]^{s}$ and $[c]^{s}\;(\forall\,c\in
Tm_{\bf C})$, and when passing from $s$ to $s^{\prime}$

  * •

if $\alpha=c?e$ or $\alpha=(e:=e^{\prime})$, then these sets do not change,

  * •

if $\alpha=c!e$, then only $[c]^{s}$ can change by adding the term $e^{s}$ to
it,

therefore (53) implies that

$s\models E\,\bot_{\bf C}\,P_{\dagger}\Rightarrow s^{\prime}\models
E\,\bot_{\bf C}\,P_{\dagger}.$

Implication

$s\models E^{\prime}\subseteq[c]\subseteq E^{\prime\prime}\Rightarrow
s^{\prime}\models E^{\prime}_{c,\alpha}\subseteq[c]\subseteq
E^{\prime\prime}_{c,\alpha}$

follows from definition (52).

Theorem 8.

Let there are given

  * •

DP ${\cal P}$, subset $E\subseteq\langle{\cal P}\rangle_{0}$, node $at\in
G_{{\cal P}}$,

  * •

set
$\\{at_{i}\;\mathop{\to}\limits^{\begin{picture}(0.0,5.0)\put(-3.0,2.0){\makebox(0.0,1.0)[]{$\scriptstyle\alpha_{i}$}}
\end{picture}}\;at\mid i\in I\\}$ of edges of TG $G_{{\cal P}}$ (with a common
end $at$), and if $G_{{\cal P}}$ contains an edge of the form
$at^{\prime}\;\mathop{\to}\limits^{\begin{picture}(0.0,5.0)\put(-3.0,2.0){\makebox(0.0,1.0)[]{$\scriptstyle\alpha$}}
\end{picture}}\;at$, which does not belong this set, then $at^{\prime}$ is
unreachable,

  * •

set $\\{\varphi_{i}\mid i\in I\\}$ of formulas corresponding to the above
edges, where $\forall\,i\in I\;\;at_{i}\models\varphi_{i}$, and $\varphi_{i}$
consists of the following EFs:

    * –

$E\,\bot_{\bf C}\,P_{\dagger}$,

    * –

$E^{\prime}_{i,c}\subseteq[c]\subseteq E^{\prime\prime}_{i,c}$, where $c\in
E_{\bf C}$, and $E^{\prime}_{i,c},E^{\prime\prime}_{i,c}\subseteq Tm$,

    * –

equalities $e=e^{\prime}$, where $e,e^{\prime}\in Tm$.

Then $at\models\varphi$, where $\varphi$ consists of the EFs

  * •

$E\,\bot_{\bf C}\,P_{\dagger}$,

  * •

$\bigcap_{i\in
I}(E^{\prime}_{i,c})_{c,\alpha_{i}}\subseteq[c]\subseteq\bigcup_{i\in
I}(E^{\prime\prime}_{i,c})_{c,\alpha_{i}}$, and

  * •

equalities $e=e^{\prime}$, occurred in each $\varphi_{i}\;(i\in I)$.

Proof.

This theorem is a consequence of theorems 3.1.2 and 2.4.1.

Theorem 9 .

Let states $s,s^{\prime}\in\Sigma_{{\cal P}_{\dagger}}$ are such that
$s\;\mathop{\longrightarrow}\limits^{\\!\\!c?\hat{x}}\;s^{\prime}$.

Then the following implication holds:

$s\models\\{[c^{\prime}]=\\{e\\},c=c^{\prime}\\}\Rightarrow
s^{\prime}\models\\{x=e\\}.$

Proof.

This theorem follows directly from the definition of an execution of an action
of the form $c?\hat{x}$ (see section 2.2.5).

####  3.1.3 Reduction of transition graphs

If analyzed property of a TG $G_{{\cal P}}$ is related with its reachable
nodes, then unreachable nodes and edges associated with these nodes can be
removed from this TG. Such operation of a removing is called a reduction of a
TG. The resulting graph is called a reduced TG, and is denoted by the same
notation $G_{{\cal P}}$. If the reduced TG has unreachable nodes, then this TG
can be reduced again, and so on.

Unrealizable edges and unreachable nodes of TGs can be detected with use of
the following theorems (we omit proofs of these theorems).

Theorem 10.

Let ${\cal P}$ be a DP, and $at\in G_{{\cal P}}$. If

  * •

$at\models\\{[c]=\emptyset,c=c^{\prime}\\}$, where $c,c^{\prime}\in Tm_{\bf
C}$, or

  * •

$at\models\\{k^{-1}[\circ]=\emptyset,k=k^{\prime}\\}$, where $k,k^{\prime}\in
Tm_{\bf K}$,

and there is an edge
$at\;\mathop{\to}\limits^{\begin{picture}(0.0,5.0)\put(-3.0,2.0){\makebox(0.0,1.0)[]{$\scriptstyle\alpha$}}
\end{picture}}\;at^{\prime}$, where $\alpha$ has the form $c^{\prime}?e$ or
$?k^{\prime}(e)$ respectively, then this edge is unrealizable.

Theorem 11 .

Let ${\cal P}$ be a DP, and $at\in G_{{\cal P}}$, then

  * •

if all edges ending in $at$ are unrealizable, then $at$ is unreachable, and

  * •

if $at$ is unreachable, then all edges starting with $at$ are unrealizable.

####  3.1.4 Verification of ${\cal P}_{1}$

Let us apply the theorems stated above to verification property (51) for DP
${\cal P}_{1}$ described by diagram (40). TG $G_{{\cal P}_{1}}$ has the form
(45).

Theorem 3.1.3 and first statement in (49), which has the form

$A^{0}B^{0}\models\\{\varphi_{1},[{c_{AB}}]=\emptyset\\}$ (54)

justify the unrealizability of the edge marked with a black circle in TG (45).
By theorem 3.1.3, this implies unreachability of node $A^{0}B^{1}$.

After reduction of TG (45) by removing unreachable nodes and associated edges
we get the graph

$\begin{array}[]{llllllllllllll}\begin{picture}(50.0,0.0)\put(-60.0,0.0){\oval(34.0,20.0)}
\put(-60.0,0.0){\oval(38.0,24.0)}
\put(-60.0,0.0){\makebox(0.0,0.0)[c]{${A^{0}B^{0}}$}}
\par\put(0.0,0.0){\oval(34.0,20.0)}
\put(0.0,0.0){\makebox(0.0,0.0)[c]{${A^{1}B^{0}}$}}
\par\par\put(60.0,0.0){\oval(34.0,20.0)}
\put(60.0,0.0){\makebox(0.0,0.0)[c]{${A^{1}B^{1}}$}}
\par\put(-41.0,0.0){\vector(1,0){24.0}} \put(17.0,0.0){\vector(1,0){26.0}}
\par\put(30.0,6.0){\makebox(0.0,0.0)[b]{ $c_{AB}?\hat{y}$ }}
\put(-28.0,6.0){\makebox(0.0,0.0)[b]{ $c_{AB}!x$ }}
\put(77.0,4.0){\vector(3,1){20.0}} \put(77.0,-4.0){\vector(3,-1){20.0}}
\put(90.0,0.0){\makebox(0.0,0.0)[]{ $\ldots$}} \end{picture}\end{array}$ (55)

In (55) there is only one node $(A^{1}B^{1})$ satisfying the condition in
(51). Thus, it is required to prove that

$A^{1}B^{1}\models x=y.$ (56)

From (54) by theorem 3.1.2 we get

$A^{1}B^{0}\models\\{\varphi_{1},[{c_{AB}}]=\\{x\\}\\},$

whence, by theorems 3.1.2 and 3.1.2, we get (56).

####  3.1.5 Verification of ${\cal P}_{3}$

Now consider the problem of proving (51) for DP ${\cal P}_{3}$, described by
(43), in which actions are defined according to (42). $G_{{\cal P}_{3}}$ has
the form (47).

Theorem 3.1.3 and third statement in (49), which has the form

$A^{0}J^{0}B^{0}\models\\{\varphi_{3},[{c_{AJ}}]=\emptyset,[{c_{BJ}}]=\emptyset,[{\bar{c}}]=\emptyset\\}$
(57)

justify the unrealizability of the edges marked with black circles in (47). By
theorem 3.1.3, this implies unreachability of all nodes of the upper tier in
TG (47) except for the node $A^{0}J^{0}B^{0}$.

After reduction of TG (47) by removing the unreachable top tier nodes and
associated edges we get the reduced TG (58).

$\begin{array}[]{llllllllllllll}\begin{picture}(120.0,170.0)\par\put(-75.0,0.0){\circle*{4.0}}
\put(-75.0,100.0){\circle*{4.0}} \put(-45.0,30.0){\circle*{4.0}}
\put(-45.0,130.0){\circle*{4.0}} \par\par\put(117.0,4.0){\vector(3,1){20.0}}
\put(117.0,-4.0){\vector(3,-1){20.0}}
\put(130.0,0.0){\makebox(0.0,0.0)[]{$\ldots$}}
\put(147.0,34.0){\vector(3,1){20.0}} \put(147.0,26.0){\vector(3,-1){20.0}}
\put(160.0,30.0){\makebox(0.0,0.0)[]{$\ldots$}}
\put(177.0,64.0){\vector(3,1){20.0}} \put(177.0,56.0){\vector(3,-1){20.0}}
\put(190.0,60.0){\makebox(0.0,0.0)[]{$\ldots$}}
\par\put(117.0,104.0){\vector(3,1){20.0}}
\put(117.0,96.0){\vector(3,-1){20.0}}
\put(130.0,100.0){\makebox(0.0,0.0)[]{$\ldots$}}
\put(147.0,134.0){\vector(3,1){20.0}} \put(147.0,126.0){\vector(3,-1){20.0}}
\put(160.0,130.0){\makebox(0.0,0.0)[]{$\ldots$}}
\put(177.0,164.0){\vector(3,1){20.0}} \put(177.0,156.0){\vector(3,-1){20.0}}
\put(190.0,160.0){\makebox(0.0,0.0)[]{$\ldots$}}
\par\put(-100.0,100.0){\oval(34.0,20.0)}
\put(-100.0,100.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{1}J^{0}B^{0}}$}}
\put(0.0,100.0){\oval(34.0,20.0)}
\put(0.0,100.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{1}J^{0}B^{1}}$}}
\put(100.0,100.0){\oval(34.0,20.0)}
\put(100.0,100.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{1}J^{0}B^{2}}$}}
\par\put(-70.0,130.0){\oval(34.0,20.0)}
\put(-70.0,130.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{1}J^{1}B^{0}}$}}
\put(30.0,130.0){\oval(34.0,20.0)}
\put(30.0,130.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{1}J^{1}B^{1}}$}}
\put(130.0,130.0){\oval(34.0,20.0)}
\put(130.0,130.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{1}J^{1}B^{2}}$}}
\par\par\put(-100.0,160.0){\oval(34.0,20.0)}
\put(-100.0,160.0){\oval(38.0,24.0)}
\put(-100.0,160.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{0}J^{0}B^{0}}$}}
\par\par\put(-40.0,160.0){\oval(34.0,20.0)}
\put(-40.0,160.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{1}J^{2}B^{0}}$}}
\put(60.0,160.0){\oval(34.0,20.0)}
\put(60.0,160.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{1}J^{2}B^{1}}$}}
\put(160.0,160.0){\oval(34.0,20.0)}
\put(160.0,160.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{1}J^{2}B^{2}}$}}
\par\par\put(-100.0,0.0){\oval(34.0,20.0)}
\put(-100.0,0.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{2}J^{0}B^{0}}$}}
\put(0.0,0.0){\oval(34.0,20.0)}
\put(0.0,0.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{2}J^{0}B^{1}}$}}
\put(100.0,0.0){\oval(34.0,20.0)}
\put(100.0,0.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{2}J^{0}B^{2}}$}}
\par\put(-70.0,30.0){\oval(34.0,20.0)}
\put(-70.0,30.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{2}J^{1}B^{0}}$}}
\put(30.0,30.0){\oval(34.0,20.0)}
\put(30.0,30.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{2}J^{1}B^{1}}$}}
\put(130.0,30.0){\oval(34.0,20.0)}
\put(130.0,30.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{2}J^{1}B^{2}}$}}
\par\put(-40.0,60.0){\oval(34.0,20.0)}
\put(-40.0,60.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{2}J^{2}B^{0}}$}}
\put(60.0,60.0){\oval(34.0,20.0)}
\put(60.0,60.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{2}J^{2}B^{1}}$}}
\put(160.0,60.0){\oval(34.0,20.0)}
\put(160.0,60.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{2}J^{2}B^{2}}$}}
\par\put(-100.0,148.0){\vector(0,-1){38.0}}
\par\put(-100.0,90.0){\vector(0,-1){80.0}} \put(0.0,90.0){\vector(0,-1){80.0}}
\put(100.0,90.0){\vector(0,-1){80.0}}
\par\put(-70.0,120.0){\vector(0,-1){80.0}}
\put(30.0,120.0){\vector(0,-1){80.0}} \put(130.0,120.0){\vector(0,-1){80.0}}
\par\put(-40.0,150.0){\vector(0,-1){80.0}}
\put(60.0,150.0){\vector(0,-1){80.0}} \put(160.0,150.0){\vector(0,-1){80.0}}
\par\par\put(-83.0,100.0){\vector(1,0){66.0}}
\put(17.0,100.0){\vector(1,0){66.0}} \put(-83.0,0.0){\vector(1,0){66.0}}
\put(17.0,0.0){\vector(1,0){66.0}} \par\put(-53.0,130.0){\vector(1,0){66.0}}
\put(47.0,130.0){\vector(1,0){66.0}} \put(-53.0,30.0){\vector(1,0){66.0}}
\put(47.0,30.0){\vector(1,0){66.0}} \par\put(-23.0,160.0){\vector(1,0){66.0}}
\put(77.0,160.0){\vector(1,0){66.0}} \put(-23.0,60.0){\vector(1,0){66.0}}
\put(77.0,60.0){\vector(1,0){66.0}}
\par\par\put(-90.0,110.0){\vector(1,1){10.0}}
\put(10.0,110.0){\vector(1,1){10.0}} \put(110.0,110.0){\vector(1,1){10.0}}
\put(-60.0,140.0){\vector(1,1){10.0}} \put(40.0,140.0){\vector(1,1){10.0}}
\put(140.0,140.0){\vector(1,1){10.0}} \par\put(-90.0,10.0){\vector(1,1){10.0}}
\put(10.0,10.0){\vector(1,1){10.0}} \put(110.0,10.0){\vector(1,1){10.0}}
\put(-60.0,40.0){\vector(1,1){10.0}} \put(40.0,40.0){\vector(1,1){10.0}}
\put(140.0,40.0){\vector(1,1){10.0}}
\par\par\par\put(-97.0,130.0){\makebox(0.0,0.0)[r]{ $\alpha_{1}$ }}
\put(3.0,150.0){\makebox(0.0,0.0)[r]{ $\alpha_{1}$ }}
\put(103.0,150.0){\makebox(0.0,0.0)[r]{ $\alpha_{1}$ }}
\par\put(-97.0,50.0){\makebox(0.0,0.0)[r]{ $\alpha_{2}$ }}
\put(3.0,50.0){\makebox(0.0,0.0)[r]{ $\alpha_{2}$ }}
\put(103.0,50.0){\makebox(0.0,0.0)[r]{ $\alpha_{2}$ }}
\par\put(-67.0,80.0){\makebox(0.0,0.0)[r]{ $\alpha_{2}$ }}
\put(33.0,80.0){\makebox(0.0,0.0)[r]{ $\alpha_{2}$ }}
\put(133.0,80.0){\makebox(0.0,0.0)[r]{ $\alpha_{2}$ }}
\par\put(-42.0,110.0){\makebox(0.0,0.0)[l]{ $\alpha_{2}$ }}
\put(58.0,110.0){\makebox(0.0,0.0)[l]{ $\alpha_{2}$ }}
\put(158.0,110.0){\makebox(0.0,0.0)[l]{ $\alpha_{2}$ }}
\par\par\put(-50.0,0.0){\makebox(0.0,0.0)[b]{ $\beta_{1}$ }}
\put(50.0,0.0){\makebox(0.0,0.0)[b]{ $\beta_{2}$ }}
\put(-20.0,30.0){\makebox(0.0,0.0)[b]{ $\beta_{1}$ }}
\put(70.0,30.0){\makebox(0.0,0.0)[b]{ $\beta_{2}$ }}
\put(10.0,60.0){\makebox(0.0,0.0)[b]{ $\beta_{1}$ }}
\put(110.0,60.0){\makebox(0.0,0.0)[b]{ $\beta_{2}$ }}
\par\put(-50.0,100.0){\makebox(0.0,0.0)[b]{ $\beta_{1}$ }}
\put(50.0,100.0){\makebox(0.0,0.0)[b]{ $\beta_{2}$ }}
\put(-20.0,130.0){\makebox(0.0,0.0)[b]{ $\beta_{1}$ }}
\put(70.0,130.0){\makebox(0.0,0.0)[b]{ $\beta_{2}$ }}
\put(10.0,160.0){\makebox(0.0,0.0)[b]{ $\beta_{1}$ }}
\put(110.0,160.0){\makebox(0.0,0.0)[b]{ $\beta_{2}$ }}
\par\par\put(-82.0,17.0){\makebox(0.0,0.0)[r]{ $j_{1}$ }}
\put(18.0,17.0){\makebox(0.0,0.0)[r]{ $j_{1}$ }}
\put(118.0,17.0){\makebox(0.0,0.0)[r]{ $j_{1}$ }}
\par\put(-82.0,117.0){\makebox(0.0,0.0)[r]{ $j_{1}$ }}
\put(18.0,117.0){\makebox(0.0,0.0)[r]{ $j_{1}$ }}
\put(118.0,117.0){\makebox(0.0,0.0)[r]{ $j_{1}$ }}
\par\put(-52.0,47.0){\makebox(0.0,0.0)[r]{ $j_{2}$ }}
\put(48.0,47.0){\makebox(0.0,0.0)[r]{ $j_{2}$ }}
\put(148.0,47.0){\makebox(0.0,0.0)[r]{ $j_{2}$ }}
\par\put(-52.0,147.0){\makebox(0.0,0.0)[r]{ $j_{2}$ }}
\put(48.0,147.0){\makebox(0.0,0.0)[r]{ $j_{2}$ }}
\put(148.0,147.0){\makebox(0.0,0.0)[r]{ $j_{2}$ }}
\par\end{picture}\end{array}$ (58)

Below we give a list of statements, each of which follows from the previous
ones (the first follows from (57)) according to theorems 3.1.2 and 3.1.2:

$\begin{array}[]{llllllllllllll}A^{1}J^{0}B^{0}\models\\{\varphi_{3},[{c_{AJ}}]=\\{\bar{c}\\},[{c_{BJ}}]=\emptyset,\\\
\hskip 56.9055pt[{\bar{c}}]=\emptyset\\}\\\
A^{2}J^{0}B^{0}\models\\{\varphi_{3},[{c_{AJ}}]=\\{\bar{c}\\},[{c_{BJ}}]=\emptyset,\\\
\hskip 56.9055pt[{\bar{c}}]=\\{x\\}\\}\\\
A^{1}J^{1}B^{0}\models\\{\varphi_{3},[{c_{AJ}}]=\\{\bar{c}\\},[{c_{BJ}}]=\emptyset,\\\
\hskip 56.9055pt[{\bar{c}}]=\emptyset,u=\bar{c}\\}\\\
A^{2}J^{1}B^{0}\models\\{\varphi_{3},[{c_{AJ}}]=\\{\bar{c}\\},[{c_{BJ}}]=\emptyset,\\\
\hskip 56.9055pt[{\bar{c}}]=\\{x\\},u=\bar{c}\\}\end{array}$ (59)

By theorem 3.1.3, these statements imply unrealizability of the edges marked
with black circles in TG (59). After removing these edges and the
corresponding unreachable nodes (using theorem 3.1.3), we get the reduced TG
(60).

$\begin{array}[]{llllllllllllll}\begin{picture}(120.0,120.0)\par\put(85.0,110.0){\circle*{4.0}}
\par\par\put(177.0,64.0){\vector(3,1){20.0}}
\put(177.0,56.0){\vector(3,-1){20.0}}
\put(190.0,60.0){\makebox(0.0,0.0)[]{$\ldots$}}
\par\put(177.0,114.0){\vector(3,1){20.0}}
\put(177.0,106.0){\vector(3,-1){20.0}}
\put(190.0,110.0){\makebox(0.0,0.0)[]{$\ldots$}}
\par\put(-100.0,50.0){\oval(34.0,20.0)}
\put(-100.0,50.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{1}J^{0}B^{0}}$}}
\par\put(-70.0,80.0){\oval(34.0,20.0)}
\put(-70.0,80.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{1}J^{1}B^{0}}$}}
\par\par\put(-100.0,110.0){\oval(34.0,20.0)}
\put(-100.0,110.0){\oval(38.0,24.0)}
\put(-100.0,110.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{0}J^{0}B^{0}}$}}
\par\par\put(-40.0,110.0){\oval(34.0,20.0)}
\put(-40.0,110.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{1}J^{2}B^{0}}$}}
\put(60.0,110.0){\oval(34.0,20.0)}
\put(60.0,110.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{1}J^{2}B^{1}}$}}
\put(160.0,110.0){\oval(34.0,20.0)}
\put(160.0,110.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{1}J^{2}B^{2}}$}}
\par\par\put(-100.0,0.0){\oval(34.0,20.0)}
\put(-100.0,0.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{2}J^{0}B^{0}}$}}
\par\put(-70.0,30.0){\oval(34.0,20.0)}
\put(-70.0,30.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{2}J^{1}B^{0}}$}}
\par\put(-40.0,60.0){\oval(34.0,20.0)}
\put(-40.0,60.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{2}J^{2}B^{0}}$}}
\put(60.0,60.0){\oval(34.0,20.0)}
\put(60.0,60.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{2}J^{2}B^{1}}$}}
\put(160.0,60.0){\oval(34.0,20.0)}
\put(160.0,60.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{2}J^{2}B^{2}}$}}
\par\put(-100.0,98.0){\vector(0,-1){38.0}}
\par\put(-100.0,40.0){\vector(0,-1){30.0}}
\par\put(-70.0,70.0){\vector(0,-1){30.0}}
\par\put(-40.0,100.0){\vector(0,-1){30.0}}
\put(60.0,100.0){\vector(0,-1){30.0}} \put(160.0,100.0){\vector(0,-1){30.0}}
\par\par\par\put(-23.0,110.0){\vector(1,0){66.0}}
\put(77.0,110.0){\vector(1,0){66.0}} \put(-23.0,60.0){\vector(1,0){66.0}}
\put(77.0,60.0){\vector(1,0){66.0}}
\par\par\put(-90.0,60.0){\vector(1,1){10.0}}
\put(-60.0,90.0){\vector(1,1){10.0}} \par\put(-90.0,10.0){\vector(1,1){10.0}}
\put(-60.0,40.0){\vector(1,1){10.0}}
\par\par\par\put(-97.0,80.0){\makebox(0.0,0.0)[r]{ $\alpha_{1}$ }}
\put(-97.0,25.0){\makebox(0.0,0.0)[r]{ $\alpha_{2}$ }}
\put(-67.0,55.0){\makebox(0.0,0.0)[r]{ $\alpha_{2}$ }}
\par\put(-42.0,85.0){\makebox(0.0,0.0)[l]{ $\alpha_{2}$ }}
\put(58.0,85.0){\makebox(0.0,0.0)[l]{ $\alpha_{2}$ }}
\put(158.0,85.0){\makebox(0.0,0.0)[l]{ $\alpha_{2}$ }}
\par\par\put(10.0,60.0){\makebox(0.0,0.0)[b]{ $\beta_{1}$ }}
\put(110.0,60.0){\makebox(0.0,0.0)[b]{ $\beta_{2}$ }}
\par\put(10.0,110.0){\makebox(0.0,0.0)[b]{ $\beta_{1}$ }}
\put(110.0,110.0){\makebox(0.0,0.0)[b]{ $\beta_{2}$ }}
\par\par\put(-82.0,17.0){\makebox(0.0,0.0)[r]{ $j_{1}$ }}
\par\put(-82.0,67.0){\makebox(0.0,0.0)[r]{ $j_{1}$ }}
\par\put(-52.0,47.0){\makebox(0.0,0.0)[r]{ $j_{2}$ }}
\par\put(-52.0,97.0){\makebox(0.0,0.0)[r]{ $j_{2}$ }}
\par\end{picture}\end{array}$ (60)

From the last statement in (59) using theorems 3.1.2 and 3.1.2 we get:

$\begin{array}[]{llllllllllllll}A^{1}J^{2}B^{0}\models\\{\varphi_{3},[{c_{AJ}}]=\\{\bar{c}\\},[{c_{BJ}}]=\\{u\\},\\\
\hskip 56.9055pt[{\bar{c}}]=\emptyset,u=\bar{c}\\}\\\
A^{1}J^{2}B^{1}\models\\{\varphi_{3},[{c_{AJ}}]=\\{\bar{c}\\},[{c_{BJ}}]=\\{u\\},\\\
\hskip 56.9055pt[{\bar{c}}]=\emptyset,u=\bar{c},v=u\\}\end{array}$ (61)

By theorem 3.1.3, from the last statement in (61) it follows that the edge in
TG (60) marked with a black circle is unrealizable. Removing this edge and the
corresponding unreachable nodes (to find which we use theorem 3.1.3), we get
the reduced TG (62).

$\begin{array}[]{llllllllllllll}\begin{picture}(50.0,130.0)\par\put(147.0,4.0){\vector(3,1){20.0}}
\put(147.0,-4.0){\vector(3,-1){20.0}} \put(160.0,0.0){\makebox(0.0,0.0)[]{
$\ldots$}} \par\put(-130.0,120.0){\oval(34.0,20.0)}
\put(-130.0,120.0){\oval(38.0,24.0)}
\put(-130.0,120.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{0}J^{0}B^{0}}$}}
\par\par\put(-50.0,120.0){\oval(34.0,20.0)}
\put(-50.0,120.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{1}J^{0}B^{0}}$}}
\par\put(-50.0,80.0){\oval(34.0,20.0)}
\put(-50.0,80.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{1}J^{1}B^{0}}$}}
\par\put(-50.0,40.0){\oval(34.0,20.0)}
\put(-50.0,40.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{1}J^{2}B^{0}}$}}
\par\put(50.0,120.0){\oval(34.0,20.0)}
\put(50.0,120.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{2}J^{0}B^{0}}$}}
\par\par\put(50.0,80.0){\oval(34.0,20.0)}
\put(50.0,80.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{2}J^{1}B^{0}}$}}
\par\put(50.0,40.0){\oval(34.0,20.0)}
\put(50.0,40.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{2}J^{2}B^{0}}$}}
\par\par\put(-50.0,100.0){\makebox(0.0,0.0)[r]{ $j_{1}$ }}
\par\put(50.0,100.0){\makebox(0.0,0.0)[l]{ $j_{1}$ }}
\par\put(-50.0,60.0){\makebox(0.0,0.0)[r]{ $j_{2}$ }}
\par\put(50.0,60.0){\makebox(0.0,0.0)[l]{ $j_{2}$ }}
\par\put(-90.0,122.0){\makebox(0.0,0.0)[b]{ $\alpha_{1}$ }}
\par\par\par\put(0.0,123.0){\makebox(0.0,0.0)[b]{ $\alpha_{2}$ }}
\par\put(0.0,83.0){\makebox(0.0,0.0)[b]{ $\alpha_{2}$ }}
\par\put(0.0,43.0){\makebox(0.0,0.0)[b]{ $\alpha_{2}$ }}
\par\put(-50.0,110.0){\vector(0,-1){20.0}}
\put(50.0,110.0){\vector(0,-1){20.0}}
\par\put(-50.0,70.0){\vector(0,-1){20.0}} \put(50.0,70.0){\vector(0,-1){20.0}}
\par\par\put(-111.0,120.0){\vector(1,0){44.0}}
\par\par\put(-33.0,120.0){\vector(1,0){66.0}}
\put(-33.0,80.0){\vector(1,0){66.0}} \put(-33.0,40.0){\vector(1,0){66.0}}
\par\put(-50.0,0.0){\oval(34.0,20.0)}
\put(-50.0,0.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{1}J^{2}B^{1}}$}}
\par\put(50.0,0.0){\oval(34.0,20.0)}
\put(50.0,0.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{2}J^{2}B^{1}}$}}
\par\par\put(0.0,3.0){\makebox(0.0,0.0)[b]{ $\alpha_{2}$ }}
\par\put(-33.0,0.0){\vector(1,0){66.0}} \par\put(130.0,0.0){\oval(34.0,20.0)}
\put(130.0,0.0){\makebox(0.0,0.0)[c]{${\scriptstyle A^{2}J^{2}B^{2}}$}}
\par\put(-50.0,30.0){\vector(0,-1){20.0}} \put(50.0,30.0){\vector(0,-1){20.0}}
\put(67.0,0.0){\vector(1,0){46.0}}
\par\par\put(-50.0,20.0){\makebox(0.0,0.0)[r]{ $\beta_{1}$ }}
\par\put(50.0,20.0){\makebox(0.0,0.0)[l]{ $\beta_{1}$ }}
\put(90.0,3.0){\makebox(0.0,0.0)[b]{ $\beta_{2}$ }}
\par\end{picture}\end{array}$ (62)

Applying theorems 3.1.2 and 3.1.2, we calculate the formulas corresponding to
the remaining nodes:

$\begin{array}[]{llllllllllllll}A^{2}J^{2}B^{0}\models\\{\varphi_{3},[{c_{AJ}}]=\\{\bar{c}\\},[{c_{BJ}}]=\\{u\\},\\\
\hskip 56.9055pt[{\bar{c}}]=\\{x\\},u=\bar{c}\\}\\\
A^{2}J^{2}B^{1}\models\\{\varphi_{3},[{c_{AJ}}]=\\{\bar{c}\\},[{c_{BJ}}]=\\{u\\},\\\
\hskip 56.9055pt[{\bar{c}}]=\\{x\\},u=\bar{c},v=u\\}\\\
A^{2}J^{2}B^{2}\models\\{x=y\\}\end{array}$ (63)

Since

  * •

in TG (62) node $A^{2}J^{2}B^{2}$ is the only node that satisfies the
condition in (51), and

  * •

according to the last statement in (63), this node satisfies the statement in
(51),

then the problem of proving property (51) for DP ${\cal P}_{3}$ is solved.

####  3.1.6 Theorems for verification of distributed processes with secure
keys

In this section, we will use the following notation:

$\begin{array}[]{llllllllllllll}\forall\,E\subseteq Tm,\forall\,\alpha\in
Act,\forall\,k\in Tm_{\bf K}\\\ E_{k,\alpha}=E\cup\\{e\\},\mbox{ if
$\alpha=!k(e)$, and }\\\ E_{k,\alpha}=E,\mbox{ otherwise.}\end{array}$ (64)

Theorem 12.

Let ${\cal P}$ be a DP, $Var({\cal P})_{\bf C}=\\{\circ\\}$, $P\in{\cal P}$,
$E$ be a subset of $\langle{\cal P}\rangle_{0}$, $s,s^{\prime}$ be states from
$\Sigma_{{\cal P}_{\dagger}}$, such that
$s\;\mathop{\longrightarrow}\limits^{\\!\\!\alpha_{P}}\;s^{\prime}$, and if
$\alpha=!e$, then

$\forall\,x\in E_{\bf X}\;\;x\,\bot_{{\bf K},E}\,e^{s}.$ (65)

Then $\forall\,E^{\prime},E^{\prime\prime}\subseteq Tm$, $\forall\,k\in E_{\bf
K}$ the following implication holds:

$\begin{array}[]{llllllllllllll}s\models{\left\\{\begin{array}[]{lllll}E\,\bot_{\bf
K}\,P_{\dagger},k^{-1}[P_{\dagger}]\subseteq k^{-1}[\circ]\\\
E^{\prime}\subseteq k^{-1}[\circ]\subseteq
E^{\prime\prime}\end{array}\right\\}}\Rightarrow\\\ \Rightarrow
s^{\prime}\models{\left\\{\begin{array}[]{lllll}E\,\bot_{\bf
K}\,P_{\dagger},k^{-1}[P_{\dagger}]\subseteq k^{-1}[\circ]\\\
E^{\prime}_{k,\alpha}\subseteq k^{-1}[\circ]\subseteq
E^{\prime\prime}_{k,\alpha}\end{array}\right\\}}\end{array}$

Proof.

Values of formulas $E\,\bot_{\bf K}\,P_{\dagger}$ and
$k^{-1}[P_{\dagger}]\subseteq k^{-1}[\circ]$ in $s$ depend only on sets
$[P_{\dagger}]^{s}$ and $[\circ]_{s}$ (for $E\,\bot_{\bf K}\,P_{\dagger}$ this
follows from (4)), and

  * •

if $\alpha=?e$ or $\alpha=(e:=e^{\prime})$, then $[P_{\dagger}]^{s}$ and
$[\circ]_{s}$ do not change when passing from $s$ to $s^{\prime}$ , and

  * •

if $\alpha=!e$, then only $[\circ]_{s}$ changes by adding $e^{s}$ when passing
from $s$ to $s^{\prime}$,

therefore, (65) implies the implication

$\begin{array}[]{llllllllllllll}s\models\\{E\,\bot_{\bf
K}\,P_{\dagger},k^{-1}[P_{\dagger}]\subseteq k^{-1}[\circ]\\}\Rightarrow\\\
\Rightarrow s^{\prime}\models\\{E\,\bot_{\bf
K}\,P_{\dagger},k^{-1}[P_{\dagger}]\subseteq k^{-1}[\circ]\\}.\end{array}$

Implication

$\begin{array}[]{llllllllllllll}s\models E^{\prime}\subseteq
k^{-1}[\circ]\subseteq E^{\prime\prime}\Rightarrow\\\ \Rightarrow
s^{\prime}\models E^{\prime}_{k,\alpha}\subseteq k^{-1}[\circ]\subseteq
E^{\prime\prime}_{k,\alpha}\end{array}$

follows from (64).

Moreover, an analog of theorem 3.1.2 holds, with the replacement

  * •

$E\,\bot_{\bf C}\,P_{\dagger}$ on $\\{E\,\bot_{\bf
K}\,P_{\dagger},k^{-1}[P_{\dagger}]\subseteq k^{-1}[\circ]\\}$,

  * •

$[c]$ on $k^{-1}[\circ]$,

  * •

$E_{i,c}$ on $E_{i,k}$, $(E_{i,c})_{c,\alpha_{i}}$ on
$(E_{i,k})_{k,\alpha_{i}}$,

and an analog of theorem 3.1.2 holds, with the replacement $c?\hat{x}$ on
$?k(\hat{x})$, $[c^{\prime}]$ on $(k^{\prime})^{-1}[\circ]$, $c=c^{\prime}$ on
$k=k^{\prime}$.

####  3.1.7 Verification of ${\cal P}_{2}$

A proof of property (51) for DP ${\cal P}_{2}$ described by diagram (41) is
carried out similarly to the proof of this property for DP ${\cal P}_{1}$ in
section 3.1.4. TG $G_{{\cal P}_{2}}$ has the form (46). An unrealizability of
the edge marked with a black circle in $G_{{\cal P}_{2}}$ is substantiated
with use of theorem 3.1.3 and second statement in (49). By theorem 3.1.3, we
get an unreachability of the node $A^{0}B^{1}$. After reduction of TG
$G_{{\cal P}_{2}}$ we get the TG

$\begin{array}[]{llllllllllllll}\begin{picture}(50.0,20.0)\put(-60.0,0.0){\oval(34.0,20.0)}
\put(-60.0,0.0){\oval(38.0,24.0)}
\put(-60.0,0.0){\makebox(0.0,0.0)[c]{${A^{0}B^{0}}$}}
\par\put(0.0,0.0){\oval(34.0,20.0)}
\put(0.0,0.0){\makebox(0.0,0.0)[c]{${A^{1}B^{0}}$}}
\par\par\put(60.0,0.0){\oval(34.0,20.0)}
\put(60.0,0.0){\makebox(0.0,0.0)[c]{${A^{1}B^{1}}$}}
\par\put(-41.0,0.0){\vector(1,0){24.0}} \put(17.0,0.0){\vector(1,0){26.0}}
\par\put(30.0,8.0){\makebox(0.0,0.0)[b]{ $?k_{AB}(\hat{y})$ }}
\put(-28.0,8.0){\makebox(0.0,0.0)[b]{ $!k_{AB}(x)$ }}
\put(77.0,4.0){\vector(3,1){20.0}} \put(77.0,-4.0){\vector(3,-1){20.0}}
\put(90.0,0.0){\makebox(0.0,0.0)[]{ $\ldots$}} \par\end{picture}\end{array}$
(66)

In (66) there is a single node $(A^{1}B^{1})$ that satisfies the condition in
(51). Thus, it is required to prove that $A^{1}B^{1}\models x=y$. This
property follows from the statement
$A^{1}B^{0}\models\\{\varphi_{2},k_{AB}^{-1}[{\circ}]=\\{x\\}\\}.$

####  3.1.8 Verification of ${\cal P}_{4}$

Proof of property (51) for DP ${\cal P}_{4}$ described by diagram (43), where
actions $\alpha_{i},\beta_{i},j_{i}\;(i=1,2)$ are defined according to (44),
is carried out similarly to the proof of this property for DP ${\cal P}_{3}$
in section 3.1.5. TG $G_{{\cal P}_{4}}$ has the form (47). After reduction of
TG (47) we get the same TGs (58), (60), (62), as in the case of verification
of DP ${\cal P}_{3}$. We will not describe in detail a solution of the
verification problem for DP ${\cal P}_{4}$, we will only present statements
associated with nodes of TG (62) for this case.

${\begin{array}[]{llllllllllllll}A^{1}J^{0}B^{0}\models\\{\varphi_{4},k_{AJ}^{-1}[\circ]=\\{\bar{k}\\},k_{BJ}^{-1}[\circ]=\emptyset,\\\
\hskip 56.9055pt\bar{k}^{-1}[\circ]=\emptyset\\}\\\
A^{2}J^{0}B^{0}\models\\{\varphi_{4},k_{AJ}^{-1}[\circ]=\\{\bar{k}\\},k_{BJ}^{-1}[\circ]=\emptyset,\\\
\hskip 56.9055pt\bar{k}^{-1}[\circ]=\\{x\\}\\}\\\
A^{1}J^{1}B^{0}\models\\{\varphi_{4},k_{AJ}^{-1}[\circ]=\\{\bar{k}\\},k_{BJ}^{-1}[\circ]=\emptyset,\\\
\hskip 56.9055pt\bar{k}^{-1}[\circ]=\emptyset,u=\bar{k}\\}\\\
A^{2}J^{1}B^{0}\models\\{\varphi_{4},k_{AJ}^{-1}[\circ]=\\{\bar{k}\\},k_{BJ}^{-1}[\circ]=\emptyset,\\\
\hskip 56.9055pt\bar{k}^{-1}[\circ]=\\{x\\},u=\bar{k}\\}\\\
A^{1}J^{2}B^{0}\models\\{\varphi_{4},k_{AJ}^{-1}[\circ]=\\{\bar{k}\\},k_{BJ}^{-1}[\circ]=\\{u\\},\\\
\hskip 56.9055pt\bar{k}^{-1}[\circ]=\emptyset,u=\bar{k}\\}\\\
A^{1}J^{2}B^{1}\models\\{\varphi_{4},k_{AJ}^{-1}[\circ]=\\{\bar{k}\\},k_{BJ}^{-1}[\circ]=\\{u\\},\\\
\hskip 56.9055pt\bar{k}^{-1}[\circ]=\emptyset,u=\bar{k},v=u\\}\\\
A^{2}J^{2}B^{0}\models\\{\varphi_{4},k_{AJ}^{-1}[\circ]=\\{\bar{k}\\},k_{BJ}^{-1}[\circ]=\\{u\\},\\\
\hskip 56.9055pt\bar{k}^{-1}[\circ]=\\{x\\},u=\bar{k}\\}\\\