Even simple processes of $\pi$-calculus are hard for analysis

Mathematical models of distributed computations, based on the calculus of mobile processes ($\pi$-calculus) are widely used for checking the information security properties of cryptographic protocols. Since $\pi$-calculus is Turing-complete, this problem is undecidable in general case. Therefore, the study is carried out only for some special classes of $\pi$-calculus processes with restricted computational capabilities, for example, for non-recursive processes, in which all runs have a bounded length, for processes with a bounded number of parallel components, etc. However, even in these cases, the proposed checking procedures are time consuming. We assume that this is due to the very nature of the $\pi$ -calculus processes. The goal of this paper is to show that even for the weakest model of passive adversary and for relatively simple protocols that use only the basic $\pi$-calculus operations, the task of checking the information security properties of these protocols is co-NP-complete.