Modelirovanie i Analiz Informacionnyh Sistem | |
Even Simple Processes of π-calculus are Hard for Analysis | |
Marat M. Abbas1  Vladimir A. Zakharov2  | |
[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