{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,23]],"date-time":"2026-03-23T13:24:32Z","timestamp":1774272272217,"version":"3.50.1"},"reference-count":33,"publisher":"Allerton Press","issue":"7","license":[{"start":{"date-parts":[[2019,12,1]],"date-time":"2019-12-01T00:00:00Z","timestamp":1575158400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2019,12,1]],"date-time":"2019-12-01T00:00:00Z","timestamp":1575158400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Aut. Control Comp. Sci."],"published-print":{"date-parts":[[2019,12]]},"DOI":"10.3103\/s0146411619070022","type":"journal-article","created":{"date-parts":[[2020,3,4]],"date-time":"2020-03-04T10:02:40Z","timestamp":1583316160000},"page":"573-583","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Even Simple \u03c0-Calculus Processes Are Difficult to Analyze"],"prefix":"10.3103","volume":"53","author":[{"given":"M. M.","family":"Abbas","sequence":"first","affiliation":[]},{"given":"V. A.","family":"Zakharov","sequence":"additional","affiliation":[]}],"member":"1627","published-online":{"date-parts":[[2020,3,4]]},"reference":[{"key":"7159_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1998.2740","volume":"148","author":"M. Abadi","year":"1999","unstructured":"Abadi, M. and Gordon, A.D., A calculus for cryptographic protocols: The spi calculus, Inf. Comput., 1999, vol.\u00a0148, no. 1, pp. 1\u201370.","journal-title":"Inf. Comput."},{"issue":"3","key":"7159_CR2","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1145\/373243.360213","volume":"36","author":"Mart\u00edn Abadi","year":"2001","unstructured":"Abadi, M. and Fournet, C., Mobile values, new names, and secure communication, Proceedings of the 28-th ACM Symposium on Principles of Programming Languages, 2001, pp. 104\u2013115.","journal-title":"ACM SIGPLAN Notices"},{"key":"7159_CR3","doi-asserted-by":"crossref","unstructured":"Amadio, M.R. and Lugiez, D., On the reachability problem for cryptographic protocols, Proceedings of the 11-th International Conference on Concurrency Theory, 2000, pp. 380\u2013394.","DOI":"10.1007\/3-540-44618-4_28"},{"key":"7159_CR4","doi-asserted-by":"publisher","first-page":"695","DOI":"10.1016\/S0304-3975(02)00090-7","volume":"290","author":"M.R. Amadio","year":"2003","unstructured":"Amadio, M.R., Lugiez, D., and Vanackere, V., On the symbolic reduction of processes with cryptographic functions, Theor. Comput. Sci., 2003, vol. 290, no. 1, pp. 695\u2013740.","journal-title":"Theor. Comput. Sci."},{"key":"7159_CR5","doi-asserted-by":"crossref","unstructured":"Arapinis, M., Liu, J., Ritter, E., and Ryan, M., Stateful applied pi calculus, Proceedings of the Principles of Security and Trust\u2014Third International Conference, 2014, pp. 22\u201341.","DOI":"10.1007\/978-3-642-54792-8_2"},{"key":"7159_CR6","doi-asserted-by":"crossref","unstructured":"Blanchet, B. and Smith, B., Automated reasoning for equivalences in the applied pi calculus with barriers, Proceedings of the 29-th IEEE Computer Security Foundations Symposium, 2014, pp. 310\u2013324.","DOI":"10.1109\/CSF.2016.29"},{"key":"7159_CR7","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1006\/inco.2000.3020","volume":"168","author":"C. Bodei","year":"2001","unstructured":"Bodei, C., Degano, P., Nielson, F., and Nielson, H.R., Static analysis for the pi-calculus with applications to security, Inf. Comput., 2001, vol. 168, no. 1, pp. 68\u201392.","journal-title":"Inf. Comput."},{"key":"7159_CR8","doi-asserted-by":"publisher","first-page":"487","DOI":"10.1017\/S0960129505004706","volume":"15","author":"J. Borgstrom","year":"2005","unstructured":"Borgstrom, J. and Nestmann, U., On bisimulations for the spi calculus, Math. Struct. Comput. Sci., 2005, vol.\u00a015, no. 3, pp. 487\u2013552.","journal-title":"Math. Struct. Comput. Sci."},{"key":"7159_CR9","doi-asserted-by":"crossref","unstructured":"Bruni, A., Modersheim, S., Nielson, F., and Nielson, H.R., Set-pi: Set membership pi-calculus, Proceedings of the 28-th IEEE Computer Security Foundations Symposium, 2015, pp. 185\u2013198.","DOI":"10.1109\/CSF.2015.20"},{"key":"7159_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2926715","volume":"17","author":"R. Chadha","year":"2016","unstructured":"Chadha, R., Cheval, V., Ciobaca, S., and Kremer, S., Automated verification of equivalence properties of cryptographic protocols, ACM Trans. Comput. Logic, 2016, vol. 17, no. 4, pp. 1\u201332.","journal-title":"ACM Trans. Comput. Logic"},{"key":"7159_CR11","doi-asserted-by":"crossref","unstructured":"Chevalier, Y., Kusters, R., Rusinowitch, M., and 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, pp. 124\u2013135.","DOI":"10.1007\/978-3-540-24597-1_11"},{"key":"7159_CR12","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1016\/j.tcs.2005.01.015","volume":"338","author":"Y. Chevalier","year":"2005","unstructured":"Chevalier, Y., Kusters, R., Rusinowitch, M., and Turuani, M., An NP decision procedure for protocol insecurity with XOR, Theor. Comput. Sci., 2005, vol. 338, nos. 1\u20133, pp. 247\u2013274.","journal-title":"Theor. Comput. Sci."},{"key":"7159_CR13","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1016\/j.entcs.2004.05.019","volume":"125","author":"Y. Chevalier","year":"2005","unstructured":"Chevalier, Y., Kusters, R., Rusinowitch, M., and Turuani, M., Deciding the security of protocols with commuting public key encryption, Electron. Notes Theor. Comput. Sci., 2005, vol. 125, no. 1, pp. 55\u201366.","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"7159_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1380572.1380573","volume":"9","author":"Y. Chevalier","year":"2008","unstructured":"Chevalier, Y., Kusters, R., Rusinowitch, M., and Turuani, M., Complexity results for security protocols with Diffie-Hellman exponentiation and commuting public key encryption, ACM Trans. Comput. Logic, 2008, vol. 9, no. 4, pp. 1\u201352.","journal-title":"ACM Trans. Comput. Logic"},{"key":"7159_CR15","doi-asserted-by":"crossref","unstructured":"Chretien, R., Cortier, V., and Delaune, S., Decidability of trace equivalence for protocols with nonces, Proceedings of the 28-th IEEE Computer Security Foundations Symposium, 2015, pp. 170\u2013184.","DOI":"10.1109\/CSF.2015.19"},{"key":"7159_CR16","doi-asserted-by":"crossref","unstructured":"Cortier, V. and Delaune, S., A method for proving observational equivalence, Proceedings of the 2009 22nd IEEE Computer Security Foundations Symposium, 2009, pp. 266\u2013276.","DOI":"10.1109\/CSF.2009.9"},{"key":"7159_CR17","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1016\/j.tcs.2004.03.066","volume":"325","author":"M. Curti","year":"2004","unstructured":"Curti, M., Degano, P., Priami, C., and Balardi, C.T., Modelling biochemical pathways through enhanced pi-calculus, Theor. Comput. Sci., 2004, vol. 325, no. 1, pp. 111\u2013140.","journal-title":"Theor. Comput. Sci."},{"key":"7159_CR18","first-page":"263","volume":"263","author":"S. Delaune","year":"2008","unstructured":"Delaune, S., Ryan, M., and Smyth, B., Automatic verification of privacy properties in the applied pi calculus, Trust Manage. II, 2008, vol. 263, pp. 263\u2013278.","journal-title":"Trust Manage. II"},{"key":"7159_CR19","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"29","author":"D. Dolev","year":"1983","unstructured":"Dolev, D. and Yao, A., On the security of public key protocols, IEEE Trans. Inf. Theory, 1983, vol. 29, no. 2, pp. 198\u2013208.","journal-title":"IEEE Trans. Inf. Theory"},{"key":"7159_CR20","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1145\/941566.941570","volume":"12","author":"L. Durante","year":"2003","unstructured":"Durante, L., Sisto, R., and Valenzano, A., Automatic testing equivalence verification of spi calculus specifications, ACM Trans. Software Eng. Methodol., 2003, vol. 12, no. 2, pp. 222\u2013284.","journal-title":"ACM Trans. Software Eng. Methodol."},{"key":"7159_CR21","doi-asserted-by":"publisher","first-page":"247","DOI":"10.3233\/JCS-2004-12203","volume":"12","author":"N.A. Durgin","year":"2004","unstructured":"Durgin, N.A., Lincoln, P., and Mitchell, J.C., Multiset rewriting and the complexity of bounded security protocols, J. Comput. Secur., 2004, vol. 12, no. 2, pp. 247\u2013311.","journal-title":"J. Comput. Secur."},{"key":"7159_CR22","unstructured":"Godskesen, J.C., Formal verification of the ARAN protocol using the applied pi-calculus, Proceedings of the Sixth International IFIP WG 1.7 Workshop on Issues in the Theory of Security, 2006, pp. 99\u2013113."},{"key":"7159_CR23","unstructured":"Huima, A., Efficient infinite state analysis of security protocols, Proceedings of the Workshop on Formal Methods and Security Protocols, 1999."},{"key":"7159_CR24","doi-asserted-by":"crossref","unstructured":"Liang, Z. and 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, pp. 101\u2013116.","DOI":"10.1007\/978-3-642-10772-6_9"},{"key":"7159_CR25","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(92)90008-4","volume":"100","author":"R. Milner","year":"1992","unstructured":"Milner, R., Parrow, J., and Walker, D., A calculus of mobile processes, I and II, Inf. Comput., 1992, vol. 100, no. 1, pp. 1\u201377.","journal-title":"Inf. Comput."},{"key":"7159_CR26","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1017\/S0960129500001407","volume":"2","author":"R. Milner","year":"1992","unstructured":"Milner, R., Functions as processes, Math. Struct. Comput. Sci., 1992, vol. 2, pp. 119\u2013141.","journal-title":"Math. Struct. Comput. Sci."},{"key":"7159_CR27","volume-title":"Communicating and Mobile Systems\u2014The Pi-Calculus","author":"R. Milner","year":"1999","unstructured":"Milner, R., Communicating and Mobile Systems\u2014The Pi-Calculus, MIT Press, 1999."},{"key":"7159_CR28","doi-asserted-by":"crossref","unstructured":"Regev, A., Representation and simulation of biochemical processes using the pi-calculus process algebra, Proceedings of the 6-th Pacific Symposium on Biocomputing, 2001, pp. 459\u2013470.","DOI":"10.1142\/9789814447362_0045"},{"key":"7159_CR29","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1016\/S0304-3975(02)00490-5","volume":"299","author":"M. Rusinowitch","year":"2003","unstructured":"Rusinowitch, M. and Turuani, M., Protocol insecurity with finite number of sessions is NP-complete, Theor. Comput. Sci., 2003, vol. 299, nos. 1\u20133, pp. 451\u2013475.","journal-title":"Theor. Comput. Sci."},{"key":"7159_CR30","volume-title":"Business Process Management: The Third Wave","author":"H. Smith","year":"2003","unstructured":"Smith, H. and Fingar, P., Business Process Management: The Third Wave, Meghan-Kiffer Press Tampa, 2003."},{"key":"7159_CR31","series-title":"Decidability and complexity results for security protocols","volume-title":"Verification of Infinite-State Systems with Applications to Security","author":"F.L. Tiplea","year":"2006","unstructured":"Tiplea, F.L., Enea, C., and Birjoveanu, C.V., Decidability and complexity results for security protocols, in Verification of Infinite-State Systems with Applications to Security, Amsterdam: IOS Press, 2006, pp. 185\u2013211."},{"key":"7159_CR32","doi-asserted-by":"crossref","unstructured":"Tiu, A. and Dawson, J., Automating open bisimulation checking for the spi calculus, Proceedings of the 23rd IEEE Computer Security Foundations Symposium, 2010, pp. 307\u2013321.","DOI":"10.1109\/CSF.2010.28"},{"key":"7159_CR33","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1006\/inco.1995.1018","volume":"116","author":"D. Walker","year":"1995","unstructured":"Walker, D., Objects in the \u03c0-calculus, Inf. Comput., 1995, vol. 116, no. 4, pp. 253\u2013271.","journal-title":"Inf. Comput."}],"container-title":["Automatic Control and Computer Sciences"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411619070022.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.3103\/S0146411619070022","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.3103\/S0146411619070022.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,15]],"date-time":"2026-03-15T21:57:20Z","timestamp":1773611840000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.3103\/S0146411619070022"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,12]]},"references-count":33,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2019,12]]}},"alternative-id":["7159"],"URL":"https:\/\/doi.org\/10.3103\/s0146411619070022","relation":{},"ISSN":["0146-4116","1558-108X"],"issn-type":[{"value":"0146-4116","type":"print"},{"value":"1558-108X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,12]]},"assertion":[{"value":"15 September 2018","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"30 October 2018","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"10 November 2018","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"4 March 2020","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"The authors declare that they have no conflicts of interest.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"CONFLICT OF INTEREST"}}]}}