Even simple pi-calculus processes are difficult to analyzeстатья
Информация о цитировании статьи получена из
Web of Science,
Scopus
Статья опубликована в журнале из списка Web of Science и/или Scopus
Дата последнего поиска статьи во внешних источниках: 4 мая 2020 г.
Аннотация:Mathematical models of distributed computations, based on calculus of mobile processes
(π-calculus) are widely used for checking information security properties of cryptographic protocols.
Since -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.