INTRODUCTION

Aiming to extend the expressive capacities of Calculus of Communicating Systems (CCS), Rober Milner and his colleagues introduced in [25] a new mathematical model of distributed computation environments (DCEs) called mobile process calculi or, in short, π-calculus. Its two distinct features are the pattern (ν-operator) of generating new names and the opportunity to transfer communication channel names along communication channels. These qualities enable π-calculus processes to change the communicative environment by introducing new communication channels in the course of computations and thuswise model the migration of processes. As shown by Milner in article [26], π-calculus processes can simulate computations of λ-calculus terms. This is why, unlike CCS, π-calculus is a Turing-complete computation model. The Turing-completeness of π-calculus stems from the combination of the two specified features with the replication operator inherited from CCS; should any of the three factors be absent, π-calculus ceases being a universal computational model.

Within a relatively short period following the publication of [25] it was found out that, in addition to describing the behavior of mobile process systems, π-calculus could be used with success to formally describe patterns of handling objects in object-oriented programming [33] and model business processes [30] and biochemical reactions [28]. However, the greatest interest was sparked by the fact that the authors of [1] revealed that π-calculus could be used for constructing formal models of cryptographic protocols.

In their seminal work [19], D. Dolev and E. Yao propose to divide the check of cryptographic protocol security properties in two subtasks: (1) prove the security properties (confidentiality, integrity, etc.) for basic functions (encryptions, hashing, etc.) used in cryptographic protocols; (2) check cryptographic protocols for resistance under the assumption that all the cryptographic primitives used in them meet necessary security requirements. That said, the Dolev–Yao model endows an adversary with powerful capabilities, including the one to intercept, form, and send messages along open communication channels. The spi-calculus proposed in [1] for modeling cryptographic protocols has appeared an efficient model in the framework of which the security check of cryptographic protocols in the Dolev–Yao model can be reduced (or, more formally, defined by reduction) to checking various kinds of equivalence of spi-calculus processes or to checking specially distinguished vulnerability states of processes for reachability. The paper [2] proposes one more expansion of π-calculus—so called applied π-calculus, which allows constructing complex terms and describing their algebraic properties through equations. Applied π-calculus can also be enriched with auxiliary memory with shared and confidential cells [5, 9]; this memory makes it convenient to describe authentication and key distribution protocols, etc.

There are a lot of works about analyzing the behavior of processes in calculi of cryptographic protocols based on π-calculus. Since π-calculus is an algorithmically complete computational model, all the specified tasks are algorithmically undecidable in the general case. This is why, they are studied only for some special classes of processes with limited computation capabilities, e.g., for nonrecursive processes with all runs limited in length, for processes with a limited number of parallel components, etc. The major achievements of exploring the tasks of analyzing the behavior of spi-calculus processes are exposed below. The reachabilty check has been proven a decidable task for nonrecursive spi-calculus processes [3, 23] and is NP-complete [29]. The most useful kinds of process equivalence for cryptographic apps are test [1] and visible equivalence [2]. The decidability of checking nonrecursive processes for test equivalence was established in [20]; however, the proposed decision procedure has high computational complexity. The algorithms of checking visible equivalence for some classes of spi-calculus processes and applied π-calculus were presented and corrected in [10, 15, 16, 18]. As also shown in [16], the visible equivalence check for nonrecursive applied π-calculus processes is an NP-complete task. In addition to visible processes equivalence, more primitive bisimulation relationships were examined as well [8]. According to [32], the check of the open bisimulation of nonrecursive spi-calculus processes is a decidable task. In addition, it was explored in [7] whether spi-calculus processes could be verified by static analysis. The strength of this approach is that it can be applied to any processes, recursive processes included. The proposed formal techniques of analyzing cryptographic protocols with the help of π-calculus were applied in practice and make it possible to detect and eliminate a vulnerability in the authenticated routing protocol (ARAN) [22].

Even when nonrecursive spi-calculus process P has only a finite set of computations, it is not a simple task to analyze the behavior of P in interaction with the outside environment. The reason is that in the Dolev–Yao model the outside environment (adversary) is presented as an infinite family of processes 𝒜 and the task of checking information security properties consists in analyzing the behavior of all \(\left. P \right|{\kern 1pt} R\) processes, where \(R \in \mathcal{A}\). Generally speaking, the processes from 𝒜 are capable of generating as complex messages as possible, which is why the system of processes \(\left\{ {\left. P \right|{\kern 1pt} R:R \in \mathcal{A}} \right\}\) can have an infinitely large number of states and computations. The techniques proposed and developed in works [10, 15, 16, 18, 20, 32] allow distinguishing (sometimes indirectly) such finite subset of processes \(\mathcal{A}{\kern 1pt} ',\,\,\mathcal{A}{\kern 1pt} ' \subseteq \mathcal{A}\), which describes the outside environment, that in the Dolev–Yao model the security check of protocol P requires only analyzing a finite number of \(\left. P \right|{\kern 1pt} R\) processes, where \(R \in \mathcal{A}{\kern 1pt} '\). To say the least, the size of set of processes \(\mathcal{A}{\kern 1pt} '\) appears exponentially dependent on the size of process P, which is why the algorithms of checking properties of spi-calculus or applied π-calculus for security, proposed in the indicated works, are not efficient.

The papers [3, 4] were the first ones, where the task of checking insecurity properties of cryptographic protocols with a limited number of sessions (nonrecursive protocols) was declared NP-complete. However, those works considered only model cryptographic protocols with simple (atomic) encryption keys. In addition, the authors of [4] provide only outline the estimation of the complexity of the decision procedure they describe. For the full proof of the theorem of NP-completeness of checking insecurity properties of nonrecursive cryptographic protocols with atomic encryption keys see publications [21, 31]. The paper [29] supported that result by showing that the insecurity property checking task also remained NP-complete for nonrecursive cryptographic protocols with composite encryption keys. The proof that this task belongs to the complexity class NP relies on the proposition that any unsecure protocol in the Dolev–Yao model can be compromised by an active adversary able to generate messages the size of which polynomially depends on the protocol size. In subsequent articles [11–14] this approach to designing insecure checking procedures and estimating their complexity was applied to protocols with more intricate cryptographic primitives. However, as shown in article [24], the proof of the proposition about the existence of the minimal polynomial adversary model, which is exposed in article [29], contains a mistake corrected in [24].

In all the works mentioned above the authors explored the task of checking insecurity properties for cryptographic protocols with an ever growing diversity of computational and communicative actions, and the main emphasis was to prove that the problem under consideration is in NP. The NP-completeness of the task in question was proven by reducing the satisfiability problem for 3-CNF to that task. Naturally, the reduction would be simplified with the growing complexity of the cryptographic protocols model. Various means accepted in spi-calculus were used for the purpose, including encryption/decryption functions, pair functions, branching operators, etc. We assume, however, that the difficulties with analyzing the security of cryptographic protocols modeled by various extensions of π-calculus are conditioned, first of all, by the algorithmic difficulties typical of π-calculus proper as the basic model of distributed mobile computation systems. We consider the task of checking for security of protocols, described by the basic means of π-calculus, in the passive adversary model. The analyzed protocols are a parallel composition of processes \(\left. {{{P}_{1}}} \right|{{P}_{2}}\left| \cdots \right|{{P}_{n}}\), each of which is a sequential composition of message sending and receiving \({{P}_{i}} = ac{{t}_{1}}.ac{{t}_{2}}. \cdots .ac{{t}_{m}}\). Only one among all the names used as messages is confidential; all the others are considered either commonly known or random names used only once. The passive adversary can intercept (eavesdrop) messages transferred along communication channels the names of which he knows. The captured names expand the adversary’s knowledge and can be used in subsequent interceptions. A protocol is considered secure when, whatever its execution, confidential names will not be part of the adversary’s knowledge.

In this article we show that even basic π-calculus tools will suffice for constructing for any 3-CNF φ such \(Pro{{c}_{\varphi }} = \left. {{{P}_{1}}} \right|{{P}_{2}}\left| \cdots \right|{{P}_{n}}\) process of the specified kind that will resist the passive adversary if and only if a 3-CNF φ is unsatisfiable. That said, the size of \(Pro{{c}_{\varphi }}\) linearly depends on the size of formula φ, and all the runs of this process are completed in a normal manner, without getting caught in a deadlock. In light of the results on the NP-completeness of checking the insecurity properties and cryptographic protocols, that are obtained in articles [3, 4, 11–14, 21, 24, 29, 31], the main theorem of this article shows that the main factor determinative to the complexity of the considered task is the limited computating length of cryptographic protocols; the influence of other factors such as diversity of cryptographic primitives and protocol computing control tools used in the protocols, structure and size of transferred messages, etc., is secondary.

The article is structured as exposed below. Section 2 describes the syntax and semantics of π-calculus. Section 3 defines the passive adversary model and formulates the task of checking π-calculus processes for security in the passive adversary model. Section 4 describes the structure of \(Pro{{c}_{\varphi }}\), correspondent to arbitrary 3-CNF φ, and shows that this process is characterized by normal termination—all of its computations are completed in one and the same empty process. It has also been found out that all the computations in \(Pro{{c}_{\varphi }}\) are safe if and only if 3-CNF φ is unsatisfiable. It follows hereforth that the satisfiability of 3-CNF can be reduced to checking the insecurity properties of π-calculus processes in the passive adversary model. In the concluding section we discuss the significance of the results.

Syntaxis and Semantics of π-Calculus

We shall confine only to considering the basic recursive fragment of synchronous monadic calculus of mobile processes. Assume there is some infinite number of objects 𝒩, that will be referred to as names. They serve to indicate communication channels and also data transferred along such. Names will be recorded in lowercase letters as \(a,b, \ldots ,x,y,z\).

Elementary synchronous communicative actionE is any expression \(\bar {x}\left\langle y \right\rangle \) (message y sent along communication channel x) or \(x(y)\) (reception of a message, binding name y, along communication channel x). A π-calculus process is any expression made up according to the following rules:

$$\begin{gathered} P,Q:: = \;\;\;\,\,{\mathbf{0}}\,\,\,\,\,\,\,\,\,\,\,\,\left( {{\text{complete}}\,\,{\text{the}}\,\,{\text{process}}} \right) \hfill \\ \;\;\;\;\;\;\;\;\;\left| {\,\,\,\,E.P\,\,\,\,\,\,\,\,\left( {{\text{take}}\,\,{\text{action}}\,\,E\,\,{\text{and}}\,\,{\text{proceed}}\,\,{\text{to}}\,\,{\text{executing}}\,\,{\text{process}}\,\,P} \right)} \right. \hfill \\ \;\;\;\;\;\;\;\;\;\left| {\,\,\,\,\left. P \right|Q\,\,\,\,\,\,\,\,\left( {{\text{execute}}\,\,{\text{processes}}\,\,P\,\,{\text{and}}\,\,Q\,\,{\text{in}}\,\,{\text{parallel}}} \right)} \right. \hfill \\ \;\;\;\;\;\;\;\;\;\left| {\,\,\,\,\left( {\nu x} \right)P\,\,\,\,\left( {{\text{enter}}\,\,{\text{new}}\,\,{\text{name}}\,\,x\,\,{\text{and}}\,\,{\text{proceed}}\,\,{\text{to}}\,\,{\text{executing}}\,\,P} \right).} \right. \hfill \\ \end{gathered} $$

The set of processes thus defined will be referred to as 𝒫.

The occurrences of names in a process are divided in free and bound.

Set fn(P) of the free names of P is defined with respect to the process structure according to the following rules:

1. \(fn(\mathbf{0})=\varnothing\),

2. \(fn(\bar {x}\left\langle y \right\rangle .P) = fn(P) \cup \{ x,y\} ,\,\,\,\,fn(x(y).P) = fn(P) \cup \{ x\} ){\kern 1pt} \backslash {\kern 1pt} \{ y\} ,\)

3. \(fn((\nu x)P) = fn(P){\kern 1pt} \backslash {\kern 1pt} \{ x\} ,\)

4. \(fn\left( {\left. P \right|Q} \right) = fn(P) \cup fn(Q)\).

The occurrence of a name x in P is considered free if it is not appeared in any subprocess \((\nu x)P{\kern 1pt} '\) or \(y(x).P{\kern 1pt} '\) of P. We write \(P\left\{ {{x \mathord{\left/ {\vphantom {x y}} \right. \kern-0em} y}} \right\}\) to indicate a process derived from P by synchronously replacing all the free occurrences of name y with name x. Substitution {x/y} is called correct for process P when any free occurrence of y is not found in any subprocess \((\nu x)P{\kern 1pt} '\) of \(P\).

The operation semantics of mobile processes is determined by structural congruence relation \({{ \equiv }_{\pi }}\) and reduction relation \({{ \to }_{\pi }}\). The relation \({{ \equiv }_{\pi }}\) is the smallest congruence relation in set of processes 𝒫, that satisfies the following equalities:

1. \(\left. {\mathbf{0}} \right|P{{ \equiv }_{\pi }}\,P\), \(\left. P \right|Q{{ \equiv }_{\pi }}\left. Q \right|P\), \(\left. P \right|\left( {\left. Q \right|{\kern 1pt} R} \right){{ \equiv }_{\pi }}\left. {\left( {\left. P \right|{\kern 1pt} Q} \right)} \right|{\kern 1pt} R\), i.e., system \(\left( {\left. {\mathcal{P},} \right|,{\mathbf{0}}} \right)\) is a commutative semigroup;

2. \((\nu y)P{{ \equiv }_{\pi }}(\nu x)P\left\{ {{x \mathord{\left/ {\vphantom {x y}} \right. \kern-0em} y}} \right\}\) for any name \(x,x { \notin }fn(P)\), and correct for the process P substitution \(\{ {x \mathord{\left/ {\vphantom {x y}} \right. \kern-0em} y}\} \);

3. \(\left. {((\nu x)P)} \right|{\kern 1pt} Q{{ \equiv }_{\pi }}(\nu x)\left( {\left. P \right|{\kern 1pt} Q} \right)\) for any name \(x,x { \notin }fn(Q)\);

4. \((\nu x).{\mathbf{0}}{{ \equiv }_{\pi }}{\mathbf{0}}\), \((\nu x)((\nu y)P){{ \equiv }_{\pi }}(\nu y)((\nu x)P)\).

It is easy to see that if \(P{{ \equiv }_{\pi }}Q\) then \(fn(P) = fn(Q)\).

The reduction relation is the smallest relationship \({{ \to }_{\pi }} \subseteq \mathcal{P} \times \mathcal{N} \times \mathcal{N} \times \mathcal{P}\) which for any processes \(P,\,\,Q,\,\,P{\kern 1pt} ',\,\,Q{\kern 1pt} '\) and names \(x,\,\,y,\,\,z\) meets the following requirements (the satisfiability of \({{ \to }_{\pi }}\) for a quadruple \(P,\,\,x,\,\,y,\,\,Q\) is traditionally denoted as \(P{{\xrightarrow{{x(y)}}}_{\pi }}Q\)):

1. \(\left. {(\bar {x}\left\langle y \right\rangle .P)} \right|(x(z).Q){{\xrightarrow{{x(y)}}}_{\pi }}\left. P \right|Q\left\{ {{y \mathord{\left/ {\vphantom {y z}} \right. \kern-0em} z}} \right\}\);

2. \(P{{\xrightarrow{{x(y)}}}_{\pi }}P{\kern 1pt} '\) at \(\left. P \right|{\kern 1pt} Q{{\xrightarrow{{x(y)}}}_{\pi }}\left. {P{\kern 1pt} '} \right|{\kern 1pt} Q\);

3. \(P{{\xrightarrow{{x(y)}}}_{\pi }}P{\kern 1pt} '\) at \((\nu z).P{{\xrightarrow{{x(y)}}}_{\pi }}(\nu z).P{\kern 1pt} '\);

4. \(P{{ \equiv }_{\pi }}Q\), \(P{{\xrightarrow{{x(y)}}}_{\pi }}P{\kern 1pt} '\) and \(P{\kern 1pt} '{{ \equiv }_{\pi }}Q{\kern 1pt} '\) at \(Q{{\xrightarrow{{x(y)}}}_{\pi }}Q{\kern 1pt} '\).

Quadruples \(P{{\xrightarrow{{x(y)}}}_{\pi }}Q\) meeting the process reduction relation will be referred to as reductions (in other words, communications along communication channels \(x\)). A channel \(x\), along which it is possible to reduce process \(P\), is called active in process\(P\).

The run of a process \({{P}_{0}}\) is any sequence of reductions recorded as

$${{P}_{0}}{{\xrightarrow{{{{x}_{1}}({{y}_{1}})}}}_{\pi }}{{P}_{1}}{{\xrightarrow{{{{x}_{2}}({{y}_{2}})}}}_{\pi }} \cdots {{\xrightarrow{{{{x}_{{n - 1}}}({{y}_{{n - 1}}})}}}_{\pi }}{{P}_{{n - 1}}}{{\xrightarrow{{{{x}_{n}}({{y}_{n}})}}}_{\pi }}{{P}_{n}}.$$
((1))

A process not admitting any kind of reduction is called deadlock. The run (1) is called complete if \({{P}_{n}}\) is a deadlock. If \({{P}_{n}}{{ \equiv }_{\pi }}\,{\mathbf{0}}\) then the run completion is normal. The obvious proposition we shall use in analyzing process calculations is exposed below.

Proposition 1.If a communication channel \(x\) is active in a process \({{P}_{0}}\), then the communication along \(x\) occurs in any complete run (1).

In other words, a message will be eventually sent along each active channel in \({{P}_{0}}\).

Passive Adversary Model

An outside observer (adversary) relative to π-calculus process P is regarded as some process R that can be engaged in interaction with \(P\). This interaction is determined by parallel composition \(\left. P \right|{\kern 1pt} R\). All the names of P that are connected by the operator \(\nu \) can be interpreted as one-time used data generated by the process. This is why the communication of P and R can initially be executed only along the communication channels from the set \(fn(P)\). Then, however, the adversary gets (intercepts) the messages communicated along these channels and thus finds out new names he can use for subsequently communicating with \(P\). A passive adversary R is able only to eavesdrop messages sent by P along the communication channels known to the adversary in the course of sending and receiving messages. This ability of a passive adversary is modeled by a pair of successively executed actions \(x(y).\bar {x}\left\langle y \right\rangle \). The messages thus eavesdropped are not lost or replaced. A passive adversary can be represented by any process R emerging as a successive composition of pairs of reception and sending of one and the same message along one and the same communication channel. Unlike a passive adversary, an active adversary is able not only to eavesdrop messages, but, also to construct new messages and substitute intercepted messages; an active adversary can be represented by any \(\pi \)-calculus process \(R\).

Information security properties of process P display itself in its interaction with an adversary of a particular kind. An abstract adversary model usually used to avoid the need for considering the behavior of all possible \(\left. P \right|{\kern 1pt} R\) compositions is determined by the state of its knowledge K defined as the set of names known to the adversary. This set may change while process P performs actions. If a process P interacts with a passive adversary, state \((P,K)\) of the interacting system can be transformed to \((P{\kern 1pt} ',K{\kern 1pt} ')\) only through a certain transition of the process \(P\). If an adversary is active, \((P,K)\) can be transformed to \((P{\kern 1pt} ',K{\kern 1pt} ')\) by both, making a certain reduction of the process P and performing some action \(x(y)\) or \(\bar {x}\left\langle y \right\rangle \) of the process \(P\) on condition that the state of the adversary’s knowledge \(K\) allows him to form pairwise action \(\bar {x}\left\langle z \right\rangle \) or \(x(z)\). The adversary’s purpose is to achieve the state of knowledge from some distinguished family \(S\) that poses a security threat.

In this article we confine ourselves to considering the interaction of π-calculus processes with the passive adversary. He is characterized by the list of entries about the names he knows. To form the entries we shall introduce new operator \(\kappa \) and use expression \((\kappa x)\), where \(x \in \mathcal{N}\), to indicate the entry of name \(x\) in the adversary’s database. The passive adversary model is any list of entries (database) A that can be constructed according to the following rules:

$$\begin{gathered} A:: = \,\,\,\,\,{\mathbf{0}}\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\left( {{\text{empty}}\,\,{\text{database}}} \right) \hfill \\ \,\,\,\,\,\,\,\,\,\,\,\left| {\,\,\,\left( {\kappa x} \right).A\,\,\,\,\left( {{\text{database}}\,\,{\text{with}}\,\,{\text{the}}\,\,{\text{entry}}\,\,{\text{of}}\,\,{\text{name}}\,\,x} \right).} \right. \hfill \\ \end{gathered} $$

Unlike the operator \(\nu \), the entry operator \(\kappa \) does not bind names, which is why the set \(fn(A)\) of the free names of an adversary \(A\) consists of all the names included in expression \(A\).

A passive adversary may follow π-calculus runs; we shall formally describe this phenomenon through the parallel composition operator.

We shall use the term “monitoring of a process P by an adversary A” to refer to any expression M that can be derived according to the following rules:

$$\begin{gathered} M:: = \,\,\,\,\,\,\,\left. P \right|{\kern 1pt} A\,\,\,\,\,\,\,\,\,\,\,\left( {{\text{adversary}}\,\,A\,\,{\text{follows}}\,\,{\text{process}}\,\,P} \right) \hfill \\ \,\,\,\,\,\,\,\,\,\,\,\,\,\,\left| {\,\,\,\left( {\nu x} \right).M\,\,\,\,\left( {{\text{monitoring}}\,\,M\,\,{\text{is}}\,\,{\text{performed}}\,\,{\text{in}}\,\,{\text{the}}\,\,{\text{region}}\,\,{\text{of}}\,\,{\text{determining}}\,\,{\text{name}}\,\,x\,\,{\text{used}}\,\,{\text{once}}} \right).} \right. \hfill \\ \end{gathered} $$

We shall indicate the set of all possible monitorings as \(\mathcal{M}\), and the set of free names of a monitoring M as fn(M), in which we are especially interested in free names included in adversary entries (κx). We shall use expression open(M) to denote the subset of all free names of the specified kind.

Similarly to the semantics of π-calculus processes, the operation semantics of monitorings is determined by structural congruence relation \( \equiv \) and transition relation \( \to \). The relation \( \equiv \) is the smallest congruence relation on the set of monitorings ℳ that includes structural congruence relation \({{ \equiv }_{\pi }}\) on the set of processes and meets the following equalities:

1. \((\nu y).\,\,M \equiv (\nu x).\,\,M\left\{ {{x \mathord{\left/ {\vphantom {x y}} \right. \kern-0em} y}} \right\}\) for any name \(x,\,\,x { \notin }fn(M)\), and a correct for monitoring \(M\) substitution \(\left\{ {{x \mathord{\left/ {\vphantom {x y}} \right. \kern-0em} y}} \right\}\);

2. \((\kappa x){\kern 1pt} .{\kern 1pt} (\kappa y){\kern 1pt} .{\kern 1pt} A \equiv (\kappa y){\kern 1pt} .{\kern 1pt} (\kappa x){\kern 1pt} .{\kern 1pt} A\) for any pair of names \(x,y\) and an adversary \(A\);

3. \((\kappa x){\kern 1pt} .{\kern 1pt} (\kappa x){\kern 1pt} .{\kern 1pt} A \equiv (\kappa x){\kern 1pt} .{\kern 1pt} A\) for any names \(x\) and an adversary \(A\).

The first of these identities means that all of the adversary’s data about one-time names are valid only for the observed process whereas the other two identities allow considering the adversary’s knowledge base as an unordered set of entries. Taking account of the latter circumstance, we shall settle with A(X) to denote adversary \((\kappa {{x}_{1}}){\kern 1pt} .{\kern 1pt} (\kappa {{x}_{2}}). \ldots .(\kappa {{x}_{n}}){\kern 1pt} .{\kern 1pt} {\mathbf{0}}\) for an arbitrary set of names.

Transition relation \( \to \) is the smallest binary relation on the set of monitorings ℳ, that meets the following requirements for any processes \(P,Q,P{\kern 1pt} ',Q{\kern 1pt} '\), model adversary \(A\), monitorings \(M,N,M{\kern 1pt} ',N{\kern 1pt} '\), and names \(x,y\):

1. \(\left. P \right|{\kern 1pt} A \to \left. {P{\kern 1pt} '} \right|{\kern 1pt} A\) at \(P{{\xrightarrow{{x(y)}}}_{\pi }}P{\kern 1pt} '\);

2. \(\left. P \right|{\kern 1pt} (\kappa x){\kern 1pt} .{\kern 1pt} A \to \left. {P{\kern 1pt} '} \right|(\kappa y){\kern 1pt} .{\kern 1pt} (\kappa x){\kern 1pt} .{\kern 1pt} A\) at \(P{{\xrightarrow{{x(y)}}}_{\pi }}P{\kern 1pt} '\);

3. \((\nu x){\kern 1pt} .{\kern 1pt} M \to (\nu x){\kern 1pt} .{\kern 1pt} M{\kern 1pt} '\) at \(M \to M{\kern 1pt} '\);

4. \(N \to N{\kern 1pt} '\) at \(M \equiv N\), \(M \to M{\kern 1pt} '\), and \(M{\kern 1pt} ' \equiv N{\kern 1pt} '\).

According to the second of the herein cited rules, if an observed process communicates certain data along a communication channel, the name of which is known to the adversary, the communicated data will also be known to the adversary. We shall refer to the reflective transitive closure of the transition relation as \({{ \to }^{ * }}\). If \(M{{ \to }^{ * }}M{\kern 1pt} '\) holds, monitoring \(M{\kern 1pt} '\) is considered reachable from monitoring \(M\).

Case 1. Assume that there is a process

$$P = \left. {((\nu x){\kern 1pt} .{\kern 1pt} (\nu y){\kern 1pt} .{\kern 1pt} \overline {ch} \left\langle x \right\rangle {\kern 1pt} .{\kern 1pt} x(y){\kern 1pt} .{\kern 1pt} {\mathbf{0}})} \right|((\nu z).{\kern 1pt} ch(z){\kern 1pt} .{\kern 1pt} \bar {z}\left\langle {secret} \right\rangle {\kern 1pt} .{\kern 1pt} {\mathbf{0}})$$

and a passive adversary model \(A = (\kappa \,\,ch){\kern 1pt} .{\kern 1pt} {\mathbf{0}}\). Then the monitoring \(M = \left. P \right|{\kern 1pt} A\) generates the following sequence of transitions:

$$\begin{array}{*{20}{c}} M \\ \downarrow \\ {(\nu x){\kern 1pt} .{\kern 1pt} (\nu z){\kern 1pt} .{\kern 1pt} (((\nu y){\kern 1pt} .{\kern 1pt} x(y){\kern 1pt} .{\kern 1pt} 0)\left| {(\bar {x}\left\langle {secret} \right\rangle {\kern 1pt} .{\kern 1pt} 0)} \right|(\kappa x){\kern 1pt} .{\kern 1pt} (\kappa \,\,ch){\kern 1pt} .{\kern 1pt} {\mathbf{0}})} \\ \downarrow \\ {(\nu x){\kern 1pt} .{\kern 1pt} (\nu y){\kern 1pt} .{\kern 1pt} (\nu z){\kern 1pt} .{\kern 1pt} ((\kappa \,\,secret){\kern 1pt} .{\kern 1pt} (\kappa x){\kern 1pt} .{\kern 1pt} (\kappa \,\,ch){\kern 1pt} .{\kern 1pt} {\mathbf{0}}).} \end{array}$$

An adversary with certain a priori data about the process aims to find out certain confidential data handled in the process. This is why finite name sets X and Y are both the attack and the threat relative to which the process security requirement is formulated. We shall say that a process P secure with respect to the threat Y in carrying out the attack X (in short, P is \((X,Y)\)-secure) if \(Y \subseteq open(M)\) is not true for any monitoring M reachable from the initial monitoring \(\left. P \right|{\kern 1pt} A(X)\), i.e., none of the runs of the process P allows a passive adversary, knowing only name set X in the beginning, to eavesdrop the process communications so as to form set Y from the eavesdropped names. In a passive adversary model the security checking problem for processes is to find out whether the process P is \((X,Y)\)-resistant for an arbitrary process P, an attack X, and a threat Y. In the aforementioned example process P is not secure w.r.t the threat \(\{ secret\} \) in carrying out the attack \(\{ ch\} \).

Complexity of the Security Checking Problem for Processes

Theorem 1.In the passive adversary model the security checking problem for processes from the set 𝒫 is co-NP-complete.

Proof. Since the processes from the set 𝒫 contain no replication operator \(!\) or other means of describing computations recursively, the length of each run of process P from set 𝒫 does not exceed the size of the process P. In addition, as seen from the definition of transition relation \( \to \), the number of pairwise incongruent descendants (images) \(M{\kern 1pt} '\) for each monitoring M by the relation \( \to \) does not exceed the squared size of M. It follows hereforth that the security checking problem for processes from the set 𝒫 is in co-NP.

To prove the co-NP-completeness of the considered problem, we shall show that the problem of checking 3-CNF for unsatisfiability is log-space reducible to it. A process \(Pro{{c}_{\varphi }}\) we shall construct for an arbitrarily specified 3-CNF φ is able to model the computation of the value of formula \(\varphi \) on all sets of variable values and allows an adversary to eavesdrop confidential name \(secret\) transmitted along open communication channel \(ch\) iff \(\varphi \) is satisfiable.

Assume that an arbitrary 3-CNF \(\varphi = {{D}_{1}} \wedge {{D}_{2}} \wedge \ldots \wedge {{D}_{N}}\) depends on variables \({{x}_{1}},{{x}_{2}}, \ldots ,{{x}_{n}}\); each clause \({{D}_{i}},\,\,1 \leqslant i \leqslant N,\) in 3-CNF is recorded as \({{\ell }_{{1i}}} \vee {{\ell }_{{2i}}} \vee {{\ell }_{{3i}}}\), where \({{\ell }_{{1i}}},{{\ell }_{{2i}}},{{\ell }_{{3i}}}\) are literals that are variables or their negations. We shall distinguish the name of literal \(\ell \) from the name of the variable this literal is based on. Each literal \(\ell \) will be denoted as \({{x}^{\sigma }}\), where \(\sigma = 1\) if \(\ell = x\) and \(\sigma = 0\) if \(\ell = \neg {\kern 1pt} x\). It can be reckoned without loss of generality that each literal \(x_{i}^{\sigma },\,\,1 \leqslant i \leqslant n,\,\,\sigma \in \{ 0,1\} ,\) is included in 3-CNF φ. In addition, for every literal \(\ell \) we shall write \({{\ell }^{*}}\) to denote the contrary literal of opposite polarity and write \({{m}_{\ell }}\) to denote the total number of occurences of literal \(\ell \) in the formula φ.

Let us describe the structure of the process \(Pro{{c}_{\varphi }}\). The only two free names it contains are \(ch\) and \(secret\). The former denotes an open communication channel (exposed to eavesdropping) and constitutes an attack. The name \(secret\) denotes confidential data and constitutes a threat. All the other names occurred in \(Pro{{c}_{\varphi }}\) are bounded by operators \(\nu \). This set of names consists of names of variables \({{x}_{1}}, \ldots ,{{x}_{n}}\), names \({{\ell }_{1}}, \ldots ,{{\ell }_{n}},\ell _{1}^{ * }, \ldots ,\ell _{n}^{ * }\) of positive and negative literals corresponding to these variables, clause names \({{d}_{1}}, \ldots ,{{d}_{N}}\), and also three special names g, h, and r. The process \(Pro{{c}_{\varphi }}\) is a composition of parallel subprocesses meant to play the roles exposed below.

1. A subprocess \(Init\) is meant to activate for each variable \({{x}_{i}},\,\,1 \leqslant i \leqslant n,\) precisely one of literals \({{x}_{i}}\) or \(\neg {{x}_{i}}\) by sending for each \({{x}_{i}}\) a message that can be received either by process \({{S}_{{{{\ell }_{i}}}}}\)or by process \({{S}_{{\ell _{i}^{ * }}}}\):

$$Init = \overline {{{x}_{1}}} \left\langle z \right\rangle {\kern 1pt} .{\kern 1pt} \overline {{{x}_{2}}} \left\langle z \right\rangle . \ldots .{\kern 1pt} \overline {{{x}_{n}}} \left\langle z \right\rangle {\kern 1pt} .{\kern 1pt} {\mathbf{0}}.$$

2. For each of \(2n\) literals \(\ell = x_{i}^{\sigma }\), \(1 \leqslant i \leqslant n\), and \(\sigma \in \{ 0,1\} \) a subprocess \({{S}_{\ell }}\) is meant to activate all the name \(\ell \) communication channels used in the process \(Pro{{c}_{\varphi }}\):

$${{S}_{\ell }} = {{x}_{i}}(z){\kern 1pt} .{\kern 1pt} \underbrace {\overline \ell \left\langle z \right\rangle {\kern 1pt} .{\kern 1pt} \overline \ell \left\langle z \right\rangle . \ldots .\overline \ell \left\langle z \right\rangle }_{{{m}_{\ell }} + {{m}_{{{{\ell }^{ * }}}}}\,\,{\text{times}}}{\kern 1pt} .{\kern 1pt} {\mathbf{0}}.$$

3. A subprocess \(Chec{{k}_{{\varphi = 0}}}\) is meant to check that formula \(\varphi \) takes the value 0 on the set of variable values correspondent to activated literals:

$$Chec{{k}_{{\varphi = 0}}} = \left. {Chec{{k}_{{{{D}_{1}} = 0}}}} \right|Chec{{k}_{{{{D}_{2}} = 0}}}\left| \ldots \right|Chec{{k}_{{{{D}_{N}} = 0}}},$$

where a subprocess \(Chec{{k}_{{{{D}_{i}} = 0}}}\) is recorded for each clause \({{D}_{i}} = {{\ell }_{{1i}}} \vee {{\ell }_{{2i}}} \vee {{\ell }_{{3i}}}\) as

$$Chec{{k}_{{{{D}_{i}} = 0}}} = \ell _{{1i}}^{*}(z){\kern 1pt} .{\kern 1pt} \ell _{{2i}}^{*}(z){\kern 1pt} .{\kern 1pt} \ell _{{3i}}^{*}(z){\kern 1pt} .{\kern 1pt} \bar {r}\left\langle {ch} \right\rangle {\kern 1pt} .{\kern 1pt} {\mathbf{0}}.$$

Thus, if the literals contrary to literals \({{\ell }_{{1i}}},{{\ell }_{{2i}}},{{\ell }_{{3i}}}\) are activated, each process \(Chec{{k}_{{{{D}_{i}} = 0}}}\) sends the name of the open channel \(ch\) along the communication channel \(r\).

4. A subprocess \(Chec{{k}_{{\varphi = 1}}}\) is meant to check that the formula φ takes the value 1 on the set of variable values correspondent to activated literals:

$$Chec{{k}_{{\varphi = 1}}} = \left. {Chec{{k}_{{{{D}_{1}} = 1}}}} \right|Chec{{k}_{{{{D}_{2}} = 1}}}\left| \ldots \right|\left. {Chec{{k}_{{{{D}_{N}} = 1}}}} \right|CheckAll,$$

where a subprocess \(Chec{{k}_{{{{D}_{i}} = 1}}}\) for each clause \({{D}_{i}} = {{\ell }_{{1i}}} \vee {{\ell }_{{2i}}} \vee {{\ell }_{{3i}}}\) is recorded as

$$Chec{{k}_{{{{D}_{i}} = 1}}} = ({{\ell }_{{1i}}}(z){\kern 1pt} .{\kern 1pt} \overline {{{d}_{i}}} \left\langle z \right\rangle {\kern 1pt} .{\kern 1pt} {\mathbf{0}})\left| {({{\ell }_{{2i}}}(z){\kern 1pt} .{\kern 1pt} \overline {{{d}_{i}}} \left\langle z \right\rangle {\kern 1pt} .{\kern 1pt} {\mathbf{0}})} \right|({{\ell }_{{3i}}}(z){\kern 1pt} .{\kern 1pt} \overline {{{d}_{i}}} \left\langle z \right\rangle {\kern 1pt} .{\kern 1pt} {\mathbf{0}}),$$

and a subprocess \(CheckAll\) as

$$CheckAll = {{d}_{1}}(z){\kern 1pt} .{\kern 1pt} {{d}_{2}}(z). \ldots .{{d}_{N}}(z){\kern 1pt} .{\kern 1pt} \bar {r}\left\langle {secret} \right\rangle {\kern 1pt} .{\kern 1pt} {\mathbf{0}}.$$

Thus, if at least one literal \({{\ell }_{{ji}}},\,\,1 \leqslant j \leqslant 3\) included in each clause \({{D}_{i}} = {{\ell }_{{1i}}} \vee {{\ell }_{{2i}}} \vee {{\ell }_{{3i}}},\,\,1 \leqslant i \leqslant N,\) is activated, then the process \(Chec{{k}_{{\varphi = 1}}}\) sends the secret name \(secret\) along the communication channel \(r\).

5. A subprocess \(OpenCh\) is meant to ensure communication along the open communication channel ch after checking the value of φ and launch the garbage collection process that will allow executing all unfinished actions of the process \(Pro{{c}_{\varphi }}\):

$$OpenCh = \left. {(r(y){\kern 1pt} .{\kern 1pt} \overline {ch} \left\langle y \right\rangle {\kern 1pt} .{\kern 1pt} \bar {g}\left\langle z \right\rangle {\kern 1pt} .{\kern 1pt} \bar {h}\left\langle z \right\rangle {\kern 1pt} .{\kern 1pt} {\mathbf{0}})} \right|(ch(x){\kern 1pt} .{\kern 1pt} {\mathbf{0}}).$$

The collection of garbage is launched by message sending actions \(\bar {g}\left\langle z \right\rangle \) and \(\bar {h}\left\langle z \right\rangle \).

6. Garbage collection subprocess \(Garbage\) is meant to activate all the literals not activated by the subprocess \(Init\) and force to execute all the actions of subprocesses \(Chec{{k}_{{\varphi = 0}}}\) and \(Chec{{k}_{{\varphi = 1}}}\) that remained untaken after the first activation of the literals by the process \(Init\):

$$Garbage = \left. {Final} \right|{\kern 1pt} Collect,$$

where

$$Final = g(z){\kern 1pt} .{\kern 1pt} \overline {{{x}_{1}}} \left\langle z \right\rangle {\kern 1pt} .{\kern 1pt} \overline {{{x}_{2}}} \left\langle z \right\rangle . \ldots .\overline {{{x}_{n}}} \left\langle z \right\rangle {\kern 1pt} .{\kern 1pt} {\mathbf{0}},$$
$$Collect = h(z){\kern 1pt} .{\kern 1pt} {{d}_{1}}(z){\kern 1pt} .{\kern 1pt} {{d}_{1}}(z){\kern 1pt} .{\kern 1pt} {{d}_{2}}(z){\kern 1pt} .{\kern 1pt} {{d}_{2}}(z). \ldots .{{d}_{N}}(z){\kern 1pt} .{\kern 1pt} {{d}_{N}}(z){\kern 1pt} .{\kern 1pt} r({{y}_{1}}){\kern 1pt} .{\kern 1pt} r({{y}_{2}}). \ldots .r({{y}_{N}}){\kern 1pt} .{\kern 1pt} {\mathbf{0}}.$$

We shall denote by \(names\) the set of all nemes, except for \(ch\) and \(secret\), appeared in the aforemetioned processes. The process \(Pro{{c}_{\varphi }}\) is the parallel composition of all those subprocesses. In this composition all the names from the list \(names\) are bounded by the operator \(\nu \) as

$$Pro{{c}_{\varphi }} = \left( {\nu \,\,names} \right){\kern 1pt} .{\kern 1pt} \left( {Init\left| {{{S}_{{{{\ell }_{1}}}}}} \right|{{S}_{{\ell _{1}^{ * }}}}\left| \ldots \right|\left. {{{S}_{{{{\ell }_{n}}}}}} \right|{{S}_{{\ell _{n}^{ * }}}}\left| {Chec{{k}_{{\varphi = 0}}}} \right|Chec{{k}_{{\varphi = 1}}}\left| {OpenCh} \right|Garbage} \right).$$

It is easy to see that, with CNF φ available, \(Pro{{c}_{\varphi }}\) can be constructed in logarithmic space.

We shall show first that any complete run of \(Pro{{c}_{\varphi }}\) recorded as

$$Pro{{c}_{\varphi }} = {{P}_{0}}{{ \to }_{\pi }}{{P}_{1}}{{ \to }_{\pi }} \cdots {{ \to }_{\pi }}{{P}_{{m - 1}}}{{ \to }_{\pi }}{{P}_{m}}$$
((2))

finishes in a normal way, i.e., \({{P}_{m}} = {\mathbf{0}}\).

First of all, note that none of names \(u\) being the argument of any message reception action \({v}(u)\) is the name of any communication channel. This means that in the course of the run (2) the names of communication channels are unchanged (only renaming acceptable for congruence relation \({{ \equiv }_{\pi }}\) is possible). In addition, for every name \(u\) of a channel the number of message sendings along this channel in the process \(Pro{{c}_{\varphi }}\) is equal to the number of message receptions from the same channel. This is why, to prove the normal completion of the run (2), it is enough to show that all the message sending actions of the process \(Pro{{c}_{\varphi }}\) are executed in this run.

Note that in \(Pro{{c}_{\varphi }}\) the channel \({{x}_{1}}\) is active, whereas the process \({{P}_{m}}\) is deadlock. This means that, by Proposition 1, the communication along the channel \({{x}_{1}}\) was carried out during the run (2). The receptions of messages from this channel are observed only in literal activation subprocesses \({{S}_{{{{x}_{1}}}}}\) and \({{S}_{{\neg {{x}_{1}}}}}\). We shall consider one of those subprocesses, in which the communication along the channel \({{x}_{1}}\) was carried out earliest in the run (2); assume that this subprocess is meant to activate a literal \({{\ell }_{1}} = x_{1}^{{{{\sigma }_{1}}}}\). Then, after the first communication along the channel \({{x}_{1}}\) is executed, the communication channel \({{\ell }_{1}}\) is activated. According to the description of the subprocess \({{S}_{\ell }}\), the activity of the channel \({{\ell }_{1}}\) will be maintained during the run until all the possible actions aimed at receiving messages from this channel are completed.

After the communication is executed along \({{x}_{1}}\) (in either \(Init\) or \(Final\)), the channel \({{x}_{2}}\) also becomes active, and reasonings similar to the ones provided above for the channel \({{x}_{1}}\) will hold. Extending these reasonings to all communication channels \({{x}_{1}},{{x}_{2}}, \ldots ,{{x}_{n}}\), we conclude that in the run (2) communication channels \({{\ell }_{1}} = x_{1}^{{{{\sigma }_{1}}}},\,\,{{l}_{2}} = x_{2}^{{{{\sigma }_{2}}}},\,\, \ldots ,\,\,{{\ell }_{n}} = x_{n}^{{{{\sigma }_{n}}}}\) become activated for certain binary tuple \(\alpha = ({{\sigma }_{1}},{{\sigma }_{1}}, \ldots ,{{\sigma }_{n}})\); these channels will be maintained as active during the run until all possible actions aimed at receiving messages from these channels are completed.

Then we need to consider two cases, depending on the value taken on by the formula \(\varphi \) on the set of variable values \(\alpha \).

If \(\varphi (\alpha ) = 0\) then CNF φ contains a clause \({{D}_{j}} = \neg {{\ell }_{{{{i}_{1}}}}} \vee \neg {{\ell }_{{{{i}_{2}}}}} \vee \neg {{\ell }_{{{{i}_{3}}}}}\) for a certain triplet of above distinguished literals \({{\ell }_{{{{i}_{1}}}}},{{\ell }_{{{{i}_{2}}}}},{{\ell }_{{{{i}_{3}}}}}\). According to the description of the subprocess \(Chec{{k}_{{\varphi = 0}}}\), one of the components of its parallel compositions is a subprocess

$$Chec{{k}_{{{{D}_{j}} = 0}}} = {{\ell }_{{{{i}_{1}}}}}(z){\kern 1pt} .{\kern 1pt} {{\ell }_{{{{i}_{2}}}}}(z){\kern 1pt} .{\kern 1pt} {{\ell }_{{{{i}_{3}}}}}(z){\kern 1pt} .{\kern 1pt} \bar {r}\left\langle {ch} \right\rangle {\kern 1pt} .{\kern 1pt} {\mathbf{0}}.$$

Since, as it was shown above, the subprocesses \({{S}_{\ell }}\) sustain the activity of paths \({{\ell }_{{{{i}_{1}}}}},{{\ell }_{{{{i}_{2}}}}},{{\ell }_{{{{i}_{3}}}}}\) until all possible actions aimed at receiving messages from these channels are performed, the communication in the run (2) is executed along the channels \({{\ell }_{{{{i}_{1}}}}},{{\ell }_{{{{i}_{2}}}}},{{\ell }_{{{{i}_{3}}}}}\), involving the message receiving actions of the subprocess \(Chec{{k}_{{{{D}_{j}} = 0}}}\). After the last of the three reductions is made, the communication channel \(r\) becomes active, because the reception of messages from this channel launches one of the components of the parallel composition of the subprocess \(OpenCh\). If \(\varphi (\alpha ) = 1\), then each clause \({{D}_{j}},\,\,1 \leqslant j \leqslant N,\)contains one of above distinguished literals \({{\ell }_{1}},{{\ell }_{2}}, \ldots ,{{\ell }_{n}}\). Therefore, according to the description of the subprocess \(Chec{{k}_{{\varphi = 1}}}\) for each \(j,\,\,1 \leqslant j \leqslant N\), the parallel composition of this subprocess contains the component \({{\ell }_{i}}(z){\kern 1pt} .{\kern 1pt} \overline {{{d}_{j}}} \left\langle z \right\rangle {\kern 1pt} .{\kern 1pt} {\mathbf{0}}\), where \({{\ell }_{i}}\) is one of the literals distinguished above that is the name of an activated communication channel. Since the literals channels are maintained as active until all possible actions aimed at receiving messages from these channels are performed, reductions are made in the run (2) involving all the message receiving actions occurred in the beginning of the indicated components. After these reductions are executed, communication channels with names \({{d}_{1}},{{d}_{2}}, \ldots ,{{d}_{N}}\) are activated in sequence. The activation of these channels is conditioned by the fact that the receptions of messages from these channels appear in the beginning of the sequential composition of actions forming subprocess \(CheckAll\). Then, according to Proposition 1, the run (2) involves communications along the channels \({{d}_{1}},{{d}_{2}}, \ldots ,{{d}_{N}}.\)

If all the mentioned message exchanges along \({{d}_{1}},{{d}_{2}}, \ldots ,{{d}_{N}}\) include the message receiving actions from the subprocess \(CheckAll\), the communication channel \(r\) is activated upon their execution. If at least one of the mentioned communications includes an act of message reception from the subprocess \(Collect\), this will be possible according to the description of this subprocess only upon a communication along the channel \(h\). However, according to the description of the subprocess \(OpenCh\), a message can be transmitted along this channel only upon a communication along the channel \(r\).

Thus, the channel \(r\) in the run (2) is activated irrespective of the value of \(\varphi (\alpha )\). So, according to Proposition 1, an act of communication takes place along the channel \(r\)in the run (2). Let us consider the very first of such reductions. It cannot be made via message receptions from the subprocess \(Collect\); as indicated above, these actions can be used only upon message exchange along the communication channel \(h\), which can be activated only after at least one act of communication along \(r\). Therefore, the first communication along \(r\) in the run (2) involves the reception of a message along this channel from the subprocess \(OpenCh\).

According to the description of this subprocess, after the first act of message reception from the channel \(r\) is executed that is contained in the subprocess, the channels \(ch\), \(g\), and \(h\) are activated in sequence. This is why, according to Proposition (1), the communications in the run (2) take place along the indicated channels. After these reductions all channels \({{x}_{1}},{{x}_{2}}, \ldots ,{{x}_{n}}\) appear reactivated. After the acts of communication are executed along these channels through the acts of message receptions from subprocesses \({{S}_{\ell }}\), all the channels correspondent to all CNF φ literals are activated. After the communication along all the activated literal communication channels through the acts of message reception from the subprocesses \(Chec{{k}_{{\varphi = 0}}}\) and \(Chec{{k}_{{\varphi = 1}}}\), all channels \({{d}_{1}},{{d}_{2}}, \ldots ,{{d}_{N}}\) as well as the channel \(r\) become activated. The communications along these paths are executed through the acts of message reception from the subprocess \(Collect\) as well as \(CheckAll\) in case of \(\varphi (\alpha ) = 0\). The process \({{P}_{m}}\) appeared in the run (2) as a result of these actions contains no actions at all; i.e., \({{P}_{m}} \equiv {\mathbf{0}}.\)

Thus, any run (2) of the process \(Pro{{c}_{\varphi }}\) is completed in a normal manner.

Then we should note that the only names allowed by process \(Pro{{c}_{\varphi }}\) for transmission along the channels by \(r\) are \(ch\) and \(secret\). We shall show that a reduction \({{P}_{i}}{{\xrightarrow{{ch(secret)}}}_{\pi }}{{P}_{{i + 1}}}\) will be possible in any run (2) of \(Pro{{c}_{\varphi }}\) if and only if 3-CNF φ is satisfiable.

The only act of message transmission along the open communication channel \(ch\) occurs in the subprocess \(OpenCh\) structured so that in the (2) the reduction \({{P}_{i}}{{\xrightarrow{{ch(secret)}}}_{\pi }}{{P}_{{i + 1}}}\) shall be preceded by the reduction \({{P}_{j}}{{\xrightarrow{{r(secret)}}}_{\pi }}{{P}_{{j + 1}}}\) and cannot be preceded by any communication with acts from the subprocess \(Garbage\).

All the acts of message sending along the channel \(r\) appear only in the subprocesses \(Chec{{k}_{{\varphi = 0}}}\) and \(Chec{{k}_{{\varphi = 1}}}\). However, in \(Chec{{k}_{{\varphi = 0}}}\) these actions are meant to send the name \(ch\) along the channel \(r\) and the name \(secret\) can be sent along the channel \(r\) only in the subprocess \(CheckAll\). In this subprocess, such an action is preceded by the reception of messages from the communication channels \({{d}_{1}},{{d}_{2}}, \ldots ,{{d}_{N}}\). Therefore, in the run (2), the reduction \({{P}_{j}}{{\xrightarrow{{r(secret)}}}_{\pi }}{{P}_{{j + 1}}}\) can be made if and only if this action is preceded by the communications along the paths \({{d}_{1}},{{d}_{2}}, \ldots ,{{d}_{N}}\).

The acts of message sending along the indicated channels are contained only in the subprocesses \(Chec{{k}_{{{{D}_{k}} = 1}}},\,\,1 \leqslant k \leqslant N\). In the description of each of subprocesses \(Chec{{k}_{{{{D}_{k}} = 1}}}\) the activation of communication channel \({{d}_{k}}\) is preceded by a communication along one of three channels \({{\ell }_{{1k}}},{{\ell }_{{2k}}},{{\ell }_{{3k}}}\). Denote by \({{\ell }_{{{{i}_{k}}}}}\) the name of the channel \({{\ell }_{{1k}}},{{\ell }_{{2k}}},~\,\,{\text{or}}\,\,{{\ell }_{{3k}}}\) the communication along which in the run (2) preceded the activation of the channel \({{d}_{k}}\).

Let us consider set of singled out literals \(L = \left\{ {{{\ell }_{{{{i}_{k}}}}}:1 \leqslant k \leqslant N} \right\}\). According to the description of the subprocesses \(Chec{{k}_{{{{D}_{k}} = 1}}},\,\,1 \leqslant k \leqslant N\), each clause \({{D}_{k}}\) of CNF φ contains one of the literals of the considered set. In addition, one can see that the set \(L\) has no complementary pairs. Actually, if \(L\) had complementary pair of literals \(\ell = x_{{{{i}_{k}}}}^{0}\) and \({{\ell }^{*}} = x_{{{{i}_{k}}}}^{1}\), that would mean that in the run (2) communication channels \(\ell \) and \({{\ell }^{*}}\) would have been activated before the reduction \({{P}_{i}}{{\xrightarrow{{ch(secret)}}}_{\pi }}{{P}_{{i + 1}}}\). According to the description of the subprocesses \({{S}_{\ell }}\) and \({{S}_{{{{\ell }^{ * }}}}}\), both indicated channels can be activated only after two communications along the channel \({{x}_{m}}\) are executed. The acts of message sending along the channel \({{x}_{m}}\) occur in subprocesses \(Garbage\) and \(Init\); however, in the section of the run (2), preceding the execution of the reduction \({{P}_{i}}{{\xrightarrow{{ch(secret)}}}_{\pi }}{{P}_{{i + 1}}}\), all the actions of the subprocess \(Garbage\) are still blocked and the subprocess \(Init\) has only one act of message sending along the channel \({{x}_{m}}\). Hence, only one of two channels \(\ell \) and \({{\ell }^{*}}\) can be activated before the reduction \({{P}_{i}}{{\xrightarrow{{ch(secret)}}}_{\pi }}{{P}_{{i + 1}}}\) in the run (2).

The existence of a noncontradictory set of literals with at least one literal in common with each clause in CNF \(Pro{{c}_{\varphi }}\) means that CNF φ is satisfiable. Thus, if the reduction \({{P}_{i}}{{\xrightarrow{{ch(secret)}}}_{\pi }}{{P}_{{i + 1}}}\) is executed in some run of the process \(Pro{{c}_{\varphi }}\), CNF φ is satisfiable. On the contrary, if CNF φ is satisfiable, it is easy to make the run of \(Pro{{c}_{\varphi }}\) in which the name \(secret\) is transmitted along the open communication channel \(ch\). Therefore, \(Pro{{c}_{\varphi }}\) is secure with respect to the threat \(\{ secret\} \) in carrying out the attack \(\{ ch\} \) if and only if CNF φ is unsatisfiable. Hence, the unsatisfiability of 3-CNF is log-space reducible to checking the security of processes from set \(\mathcal{P}\) in the passive adversary model.

CONCLUSIONS

We should note once again that the result of the co-NP-completeness of checking nonrecursive cryptographic protocol models for security is not an essential novelty. The novelty of the result is that it has been obtained for perhaps the most basic computational model in which it is possible to formulate the task of checking information security properties. Theorem 1 shows that, even in the simplest setting, when there are no cryptographic primitives in protocols being checked and an adversary is passive this problem is intractable.

The passive adversary model and the new understanding of monitoring, which expands the expressive capabilities of mobile process calculi as a means for specifying cryptographic protocols, worth special attention. As far as we know, the adversary and its interactions with the protocol were earlier modeled beyond the limits of the rigid model of π-calculus. We are convinced that the notion of monitoring will allow developing the general active adversary model correspondent to the Dolev–Yao concept. The purpose of our further research is to create this model and obtain for it results on the complexity of checking the resistance of protocols similar to the ones determined in articles [4, 11, 21, 24, 29, 31].

Since the check of nonrecursive π-calculus processes appears to be a difficult problem, it is interesting to find out for which classes of processes this problem is decidable in polynomial time. According to the proof of theorem 1, this problem is closely related to the check of π-calculus processes for normal termination. The latter is a topical problem of checking the behavior of systems of interacting processes for correctness. One of the topics we also consider for further research is that of finding efficiently verifiable sufficient conditions for normal termination of π-calculus processes.