Even Simple π-Calculus Processes Are Difficult to Analyze
- 作者: Abbas M.1, Zakharov V.2,3
-
隶属关系:
- Moscow State University
- National Research University University Higher School of Economy
- Ivannikov Institute of System Programming, Russian Academy of Sciences (ISP RAS)
- 期: 卷 53, 编号 7 (2019)
- 页面: 573-583
- 栏目: Article
- URL: https://journals.rcsi.science/0146-4116/article/view/175882
- DOI: https://doi.org/10.3103/S0146411619070022
- ID: 175882
如何引用文章
详细
Mathematical models of distributed computations, based on calculus of mobile processes (π-calculus) are widely used for checking information security properties of cryptographic protocols. Since \(\pi \)-calculus is a Turing-complete computation model, this problem is unsolvable in the general case. Therefore, its study is carried out only for some special classes of π-calculus processes with restricted computational capabilities, for example, for nonrecursive processes with all runs limited in length, for processes with a limited number of parallel components, etc. However, even in these cases the proposed checking procedures are very 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 passive adversary model and for relatively simple protocols that make use of only basic π-calculus operations, the checking of the information security properties of these protocols is a co-NP-complete problem.
作者简介
M. Abbas
Moscow State University
编辑信件的主要联系方式.
Email: unlock96@gmail.com
俄罗斯联邦, Moscow, 119991
V. Zakharov
National Research University University Higher School of Economy; Ivannikov Institute of System Programming, Russian Academy of Sciences (ISP RAS)
编辑信件的主要联系方式.
Email: zakh@cs.msu.ru
俄罗斯联邦, Moscow, 101000; Moscow, 109004