maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2018-6-589-606mais-761Research ArticleОригинальные статьиArticlesДаже простые процессы π-исчисления трудны для анализаEven Simple Processes of π-calculus are Hard for Analysishttps://orcid.org/0000-0001-8019-7090АббасМарат МазенAbbasMarat M.

студент

Ленинские горы, 1, г. Москва, 119991

student

GSP-1, Leninskie Gory, Moscow, 119991

unlock96@gmail.comhttps://orcid.org/0000-0002-3794-9565ЗахаровВладимир АнатольевичZakharovVladimir A.

доктор физ.-мат. наук, профессор

ул. Мясницкая, 20, г. Москва, 101000

ул. А. Солженицына, 25, 109004, г. Москва

Dr. of Science, professor

20 Myasnitskaya st., Moscow, 101000

25 Alexander Solzhenitsyn st., Moscow, 109004

zakh@cs.msu.ruМосковский государственный университет им. М.В. ЛомоносоваРоссияLomonosov Moscow State UniversityRussian FederationНациональный исследовательский университет «Высшая школа экономики»; Институт системного программирования им. В.П. Иванникова РАНРоссияNational Research University Higher School of Economics (HSE); Institute for system programming of the Russian Academy of Science (ISP RAS)Russian Federation201819122018256589606Copyright © Аббас М.М., Захаров В.А., 20182018Аббас М.М., Захаров В.А.Abbas M.M., Zakharov V.A.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/761

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

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.

π-исчислениепротоколбезопасностьпассивный противникверификациясложностьNP-полнотаπ-calculusprotocolsecuritypassive adversaryverificationcomplexityNP-completenessРФФИ N 18-01-00854, РФФИ N 16-01-00714Grant N 18-01-00854, Grant N 16-01-00714ReferencesAbadi M., Gordon A.D., “A Calculus for Cryptographic Protocols: The Spi Calculus”, Information and Computation, 148:1 (1999), 1–70.Abadi M., Gordon A.D., “A Calculus for Cryptographic Protocols: The Spi Calculus”, Information and Computation, 148:1 (1999), 1–70.Abadi M., Fournet C., “Mobile Values, New Names, and Secure Communication”, Proceedings of the 28-th ACM Symposium on Principles of Programming Languages, 2001, 104–115.Abadi M., Fournet C., “Mobile Values, New Names, and Secure Communication”, Proceedings of the 28-th ACM Symposium on Principles of Programming Languages, 2001, 104–115.Amadio M.R., Lugiez D., “On the Reachability Problem for Cryptographic Protocols”, Proceedings of the 11-th International Conference on Concurrency Theory, 2000, 380–394.Amadio M.R., Lugiez D., “On the Reachability Problem for Cryptographic Protocols”, Proceedings of the 11-th International Conference on Concurrency Theory, 2000, 380–394.Amadio M.R., Lugiez D., Vanackere V., “On the symbolic reduction of processes with cryptographic functions”, Theoretical Computer Science, 290:1 (2003), 695–740.Amadio M.R., Lugiez D., Vanackere V., “On the symbolic reduction of processes with cryptographic functions”, Theoretical Computer Science, 290:1 (2003), 695–740.Arapinis M., Liu J., Ritter E., Ryan M., “Stateful Applied Pi Calculus”, Proceedings of the Principles of Security and Trust—Third International Conference, 2014, 22–41.Arapinis M., Liu J., Ritter E., Ryan M., “Stateful Applied Pi Calculus”, Proceedings of the Principles of Security and Trust—Third International Conference, 2014, 22–41.Blanchet B., Smith B., “Automated reasoning for equivalences in the applied pi calculus with barriers”, Proceedings of the 29-th IEEE Computer Security Foundations Symposium, 2014, 310–324.Blanchet B., Smith B., “Automated reasoning for equivalences in the applied pi calculus with barriers”, Proceedings of the 29-th IEEE Computer Security Foundations Symposium, 2014, 310–324.Bodei C., Degano P., Nielson F., Nielson H. R., “Static Analysis for the pi-Calculus with Applications to Security”, Information and Computation, 168:1 (2001), 68–92.Bodei C., Degano P., Nielson F., Nielson H. R., “Static Analysis for the pi-Calculus with Applications to Security”, Information and Computation, 168:1 (2001), 68–92.Borgstrom J., Nestmann U., “On bisimulations for the spi calculus”, Mathematical Structures in Computer Science, 15:3 (2005), 487–552.Borgstrom J., Nestmann U., “On bisimulations for the spi calculus”, Mathematical Structures in Computer Science, 15:3 (2005), 487–552.BruniA.,ModersheimS.,NielsonF.,NielsonH.R.,“Set-Pi:SetMembershipPi-Calculus”, Proceedings of the 28-th IEEE Computer Security Foundations Symposium, 2015, 185–198.BruniA.,ModersheimS.,NielsonF.,NielsonH.R.,“Set-Pi:SetMembershipPi-Calculus”, Proceedings of the 28-th IEEE Computer Security Foundations Symposium, 2015, 185–198.Chadha R., Cheval V., Ciobaca S., Kremer S., “Automated Verification of Equivalence Properties of Cryptographic Protocols”, ACM Transactions on Computational Logic, 17:4 (2016), 1–32.Chadha R., Cheval V., Ciobaca S., Kremer S., “Automated Verification of Equivalence Properties of Cryptographic Protocols”, ACM Transactions on Computational Logic, 17:4 (2016), 1–32.Chevalier Y., Kusters R., Rusinowitch M., Turuani M., “Deciding the security of protocols with Diffie-Hellman exponentiation and products in exponents”, Proceedings of the 23-rd Annual Conference on the Foundations of Software Technology and Theoretical Computer Science, 2003, 124–135.Chevalier Y., Kusters R., Rusinowitch M., Turuani M., “Deciding the security of protocols with Diffie-Hellman exponentiation and products in exponents”, Proceedings of the 23-rd Annual Conference on the Foundations of Software Technology and Theoretical Computer Science, 2003, 124–135.Chevalier Y., Kusters R., Rusinowitch M., Turuani M., “An NP decision procedure for protocol insecurity with XOR”, Theoretical Computer Science, 338:1–3 (2005), 247–274.Chevalier Y., Kusters R., Rusinowitch M., Turuani M., “An NP decision procedure for protocol insecurity with XOR”, Theoretical Computer Science, 338:1–3 (2005), 247–274.Chevalier Y., Kusters R., Rusinowitch M., Turuani M., “Deciding the security of protocols with commuting public key encryption”, Electronic Notes in Theoretical Computer Science, 125:1 (2005), 55–66.Chevalier Y., Kusters R., Rusinowitch M., Turuani M., “Deciding the security of protocols with commuting public key encryption”, Electronic Notes in Theoretical Computer Science, 125:1 (2005), 55–66.Chevalier Y., Kusters R., Rusinowitch M., Turuani M., “Complexity results for security protocols with Diffie-Hellman exponentiation and commuting public key encryption”, ACM Transactions on Computational Logic, 9:4 (2008), 1–52.Chevalier Y., Kusters R., Rusinowitch M., Turuani M., “Complexity results for security protocols with Diffie-Hellman exponentiation and commuting public key encryption”, ACM Transactions on Computational Logic, 9:4 (2008), 1–52.Chretien R., Cortier V., Delaune S., “Decidability of trace equivalence for protocols with nonces”, Proceedings of the 28-th IEEE Computer Security Foundations Symposium, 2015, 170–184.Chretien R., Cortier V., Delaune S., “Decidability of trace equivalence for protocols with nonces”, Proceedings of the 28-th IEEE Computer Security Foundations Symposium, 2015, 170–184.Cortier V., Delaune S., “A method for proving observational equivalence”, Proceedings of the 2009 22nd IEEE Computer Security Foundations Symposium, 2009, 266–276.Cortier V., Delaune S., “A method for proving observational equivalence”, Proceedings of the 2009 22nd IEEE Computer Security Foundations Symposium, 2009, 266–276.Curti M., Degano P., Priami C., Balardi C. T., “Modelling biochemical pathways through enhanced pi-calculus”, Theoretical Computer Science, 325:1 (2004), 111–140.Curti M., Degano P., Priami C., Balardi C. T., “Modelling biochemical pathways through enhanced pi-calculus”, Theoretical Computer Science, 325:1 (2004), 111–140.Delaune S., Ryan M., Smyth B., “Automatic verification of privacy properties in the applied pi calculus”, Trust Management II, IFIP International Federation for Information Processing, 263, Springer, Boston, 2008, 263–278.Delaune S., Ryan M., Smyth B., “Automatic verification of privacy properties in the applied pi calculus”, Trust Management II, IFIP International Federation for Information Processing, 263, Springer, Boston, 2008, 263–278.Dolev D., Yao A., “On the security of public key protocols”, IEEE Transactoions on Information Theory, 29:2 (1983), 198–208.Dolev D., Yao A., “On the security of public key protocols”, IEEE Transactoions on Information Theory, 29:2 (1983), 198–208.Durante L., Sisto R., Valenzano A., “Automatic Testing Equivalence Verification of Spi Calculus Specifications”, ACM Transactions on Software Engineering and Methodology, 12:2 (2003), 222–284.Durante L., Sisto R., Valenzano A., “Automatic Testing Equivalence Verification of Spi Calculus Specifications”, ACM Transactions on Software Engineering and Methodology, 12:2 (2003), 222–284.DurginN.A.,LincolnP.,MitchellJ.C.,“Multisetrewritingandthecomplexityofbounded security protocols”, Journal of Computer Security, 12:2 (2004), 247–311.DurginN.A.,LincolnP.,MitchellJ.C.,“Multisetrewritingandthecomplexityofbounded security protocols”, Journal of Computer Security, 12:2 (2004), 247–311.Godskesen J.C., “Formal Verification of the ARAN Protocol Using the Applied Picalculus”, Proceedings of the Sixth International IFIP WG 1.7 Workshop on Issues in the Theory of Security, 2006, 99–113.Godskesen J.C., “Formal Verification of the ARAN Protocol Using the Applied Picalculus”, Proceedings of the Sixth International IFIP WG 1.7 Workshop on Issues in the Theory of Security, 2006, 99–113.Huima A., “Efficient infinite state analysis of security protocols”, Proceedings of the Workshop on Formal Methods and Security Protocols, 1999.Huima A., “Efficient infinite state analysis of security protocols”, Proceedings of the Workshop on Formal Methods and Security Protocols, 1999.Liang Z., Verma R.M., “Correcting and Improving the NP Proof for Cryptographic Protocol Insecurity”, Proceedings of the 5-th International Conference on Information Systems Security, 2009, 101–116.Liang Z., Verma R.M., “Correcting and Improving the NP Proof for Cryptographic Protocol Insecurity”, Proceedings of the 5-th International Conference on Information Systems Security, 2009, 101–116.Milner R., Parrow J., Walker D., “A calculus of mobile processes, I and II”, Information and Computation, 100:1 (1992), 1–40 and 41–77.Milner R., Parrow J., Walker D., “A calculus of mobile processes, I and II”, Information and Computation, 100:1 (1992), 1–40 and 41–77.Milner R., “Functions as Processes”, Mathematical Structures in Computer Science, 2 (1992), 119–141.Milner R., “Functions as Processes”, Mathematical Structures in Computer Science, 2 (1992), 119–141.Milner R., Communicating and mobile systems — the Pi-calculus, MIT Press, 1999.Milner R., Communicating and mobile systems — the Pi-calculus, MIT Press, 1999.Regev A., “Representation and Simulation of Biochemical Processes Using the pi-Calculus Process Algebra”, Proceedings of the 6-th Pacific Symposium on Biocomputing, 2001, 459– 470.Regev A., “Representation and Simulation of Biochemical Processes Using the pi-Calculus Process Algebra”, Proceedings of the 6-th Pacific Symposium on Biocomputing, 2001, 459– 470.Rusinowitch M., Turuani M., “Protocol Insecurity with Finite Number of Sessions is NP- complete”, Theoretical Computer Science, 299:1–3 (2003), 451–475.Rusinowitch M., Turuani M., “Protocol Insecurity with Finite Number of Sessions is NP- complete”, Theoretical Computer Science, 299:1–3 (2003), 451–475.Smith H., Fingar P., Business Process Management: The Third Wave, Meghan-Kiffer Press Tampa, 2003.Smith H., Fingar P., Business Process Management: The Third Wave, Meghan-Kiffer Press Tampa, 2003.Tiplea F. L., Enea C., Birjoveanu C. V., “Decidability and complexity results for security protocols”, Verification of Infinite-State Systems with Applications to Security, IOS Press, Amsterdam, 2006, 185–211.Tiplea F. L., Enea C., Birjoveanu C. V., “Decidability and complexity results for security protocols”, Verification of Infinite-State Systems with Applications to Security, IOS Press, Amsterdam, 2006, 185–211.Tiu A., Dawson J., “Automating Open Bisimulation Checking for the Spi Calculus”, Proceedings of the 23rd IEEE Computer Security Foundations Symposium, 2010, 307–321.Tiu A., Dawson J., “Automating Open Bisimulation Checking for the Spi Calculus”, Proceedings of the 23rd IEEE Computer Security Foundations Symposium, 2010, 307–321.Walker D., “Objects in the π-calculus”, Information and Computation, 116:4 (1995), 253– 271.Walker D., “Objects in the π-calculus”, Information and Computation, 116:4 (1995), 253– 271.

The authors declare that there are no conflicts of interest present.