Even Simple Processes of π-calculus are Hard for Analysis

Modelirovanie i Analiz Informacionnyh Sistem

Marat M. Abbas¹  Vladimir A. Zakharov² 

[1] Lomonosov Moscow State University;National Research University Higher School of Economics (HSE);

关键词: π-calculus;    protocol;    security;    passive adversary;    verification;    complexity;    np-completeness;   

DOI  :  10.18255/1818-1015-2018-6-589-606

来源: DOAJ

【 摘 要 】

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.

【 授权许可】

Unknown