Open AccessEven Simple Processes of π-calculus are Hard for Analysis
Author(s) -
M. M. Abbas,
Vladimir A. Zakharov
Publication year - 2018
Publication title -
modelirovanie i analiz informacionnyh sistem
Language(s) - English
Resource type - Journals
eISSN - 2313-5417
pISSN - 1818-1015
DOI - 10.18255/1818-1015-2018-6-589-606
Subject(s) - undecidable problem , computer science , simple (philosophy) , calculus (dental) , process calculus , cryptographic protocol , theoretical computer science , bounded function , model checking , pi calculus , task (project management) , cryptography , mathematics , algorithm , decidability , medicine , mathematical analysis , philosophy , management , epistemology , dentistry , economics
Mathematical models of distributed computations, based on the calculus of mobile processes (π-calculus) are widely used for checking the information security properties of cryptographic protocols. Since π-calculus is Turing-complete, this problem is undecidable in general case. Therefore, the study is carried out only for some special classes of π-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 π -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 π-calculus operations, the task of checking the information security properties of these protocols is co-NP-complete.