Аннотация:Математические модели распределенных вычислений, построенные на основе исчисления мобильных процессов (π-исчисления), широко используются для проверки свойств информационной безопасности криптографических протоколов. Поскольку π-исчисление является полной по Тьюрингу моделью вычислений, эта задача в общем случае алгоритмически неразрешима. Поэтому ее исследование проводится лишь для некоторых специальных классов процессов π-исчисления с ограниченными вычислительными возможностями, например, для нерекурсивных процессов, в которых все вычисления имеют ограниченную длину, для процессов с ограниченным числом параллельных компонентов и др. Однако и в этих случаях предложенные разрешающие алгоритмы оказываются весьма трудоемкими. Мы полагаем, что это обусловлено самой природой процессов π-исчисления. Цель данной работы — показать, что даже для наиболее слабой модели пассивного противника и для сравнительно простых протоколов, в которых используются лишь базовые операции π-исчисления, задача проверки свойств информационной безопасности этих протоколов является co-NP-полной.