Even Simple Processes of π-calculus are Hard for Analysis
https://doi.org/10.18255/1818-1015-2018-6-589-606
Abstract
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.
Keywords
Supporting agencies: Grant N 18-01-00854, Grant N 16-01-00714
About the Authors
Marat M. Abbas
Lomonosov Moscow State University
Russian Federation
Russian Federation
student
GSP-1, Leninskie Gory, Moscow, 119991
Vladimir A. Zakharov
National Research University Higher School of Economics (HSE);
Institute for system programming of the Russian Academy of Science (ISP RAS)
Russian Federation
Russian Federation
Dr. of Science, professor
20 Myasnitskaya st., Moscow, 101000
25 Alexander Solzhenitsyn st., Moscow, 109004
References
1. Abadi M., Gordon A.D., “A Calculus for Cryptographic Protocols: The Spi Calculus”, Information and Computation, 148:1 (1999), 1–70.
2. 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.
3. 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.
4. Amadio M.R., Lugiez D., Vanackere V., “On the symbolic reduction of processes with cryptographic functions”, Theoretical Computer Science, 290:1 (2003), 695–740.
5. 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.
6. 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.
7. 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.
8. Borgstrom J., Nestmann U., “On bisimulations for the spi calculus”, Mathematical Structures in Computer Science, 15:3 (2005), 487–552.
9. BruniA.,ModersheimS.,NielsonF.,NielsonH.R.,“Set-Pi:SetMembershipPi-Calculus”, Proceedings of the 28-th IEEE Computer Security Foundations Symposium, 2015, 185–198.
10. 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.
11. 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.
12. 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.
13. 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.
14. 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.
15. 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.
16. Cortier V., Delaune S., “A method for proving observational equivalence”, Proceedings of the 2009 22nd IEEE Computer Security Foundations Symposium, 2009, 266–276.
17. Curti M., Degano P., Priami C., Balardi C. T., “Modelling biochemical pathways through enhanced pi-calculus”, Theoretical Computer Science, 325:1 (2004), 111–140.
18. 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.
19. Dolev D., Yao A., “On the security of public key protocols”, IEEE Transactoions on Information Theory, 29:2 (1983), 198–208.
20. 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.
21. DurginN.A.,LincolnP.,MitchellJ.C.,“Multisetrewritingandthecomplexityofbounded security protocols”, Journal of Computer Security, 12:2 (2004), 247–311.
22. 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.
23. Huima A., “Efficient infinite state analysis of security protocols”, Proceedings of the Workshop on Formal Methods and Security Protocols, 1999.
24. 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.
25. 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.
26. Milner R., “Functions as Processes”, Mathematical Structures in Computer Science, 2 (1992), 119–141.
27. Milner R., Communicating and mobile systems — the Pi-calculus, MIT Press, 1999.
28. 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.
29. Rusinowitch M., Turuani M., “Protocol Insecurity with Finite Number of Sessions is NP- complete”, Theoretical Computer Science, 299:1–3 (2003), 451–475.
30. Smith H., Fingar P., Business Process Management: The Third Wave, Meghan-Kiffer Press Tampa, 2003.
31. 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.
32. Tiu A., Dawson J., “Automating Open Bisimulation Checking for the Spi Calculus”, Proceedings of the 23rd IEEE Computer Security Foundations Symposium, 2010, 307–321.
33. Walker D., “Objects in the π-calculus”, Information and Computation, 116:4 (1995), 253– 271.
Review
For citations:
Abbas M.M., Zakharov V.A. Even Simple Processes of π-calculus are Hard for Analysis. Modeling and Analysis of Information Systems. 2018;25(6):589-606. (In Russ.) https://doi.org/10.18255/1818-1015-2018-6-589-606
Views:
857
Email this article 