Даже простые процессы π-исчисления трудны для анализа
https://doi.org/10.18255/1818-1015-2018-6-589-606
Аннотация
Математические модели распределенных вычислений, построенные на основе исчисления мобильных процессов (\(π\)-исчисления), широко используются для проверки свойств информационной безопасности криптографических протоколов. Поскольку \(π\)-исчисление является полной по Тьюрингу моделью вычислений, эта задача в общем случае алгоритмически неразрешима. Поэтому ее исследование проводится лишь для некоторых специальных классов процессов \(π\)-исчисления с ограниченными вычислительными возможностями, например, для нерекурсивных процессов, в которых все вычисления имеют ограниченную длину, для процессов с ограниченным числом параллельных компонентов и др. Однако и в этих случаях предложенные разрешающие алгоритмы оказываются весьма трудоемкими. Мы полагаем, что это обусловлено самой природой процессов \(π\)-исчисления. Цель данной работы — показать, что даже для наиболее слабой модели пассивного противника и для сравнительно простых протоколов, в которых используются лишь базовые операции \(π\)-исчисления, задача проверки свойств информационной безопасности этих протоколов является co-NP-полной.
Ключевые слова
При поддержке: РФФИ N 18-01-00854, РФФИ N 16-01-00714
Об авторах
Марат Мазен Аббас
Московский государственный университет им. М.В. Ломоносова
Россия
Россия
студент
Ленинские горы, 1, г. Москва, 119991
Владимир Анатольевич Захаров
Национальный исследовательский университет «Высшая школа экономики»;
Институт системного программирования им. В.П. Иванникова РАН
Россия
Россия
доктор физ.-мат. наук, профессор
ул. Мясницкая, 20, г. Москва, 101000
ул. А. Солженицына, 25, 109004, г. Москва
Список литературы
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.
Рецензия
Для цитирования:
Аббас М.М., Захаров В.А. Даже простые процессы π-исчисления трудны для анализа. Моделирование и анализ информационных систем. 2018;25(6):589-606. https://doi.org/10.18255/1818-1015-2018-6-589-606
For citation:
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
Просмотров:
860
Послать статью по эл. почте 