{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,21]],"date-time":"2026-09-21T21:08:51Z","timestamp":1790024931620,"version":"4.0.1"},"publisher-location":"Cham","reference-count":50,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030620769","type":"print"},{"value":"9783030620776","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-62077-6_10","type":"book-chapter","created":{"date-parts":[[2020,10,28]],"date-time":"2020-10-28T11:25:37Z","timestamp":1603884337000},"page":"127-145","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["The Hitchhiker\u2019s Guide to Decidability and Complexity of Equivalence Properties in Security Protocols"],"prefix":"10.1007","author":[{"given":"Vincent","family":"Cheval","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Steve","family":"Kremer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Itsaka","family":"Rakotonirina","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2020,10,28]]},"reference":[{"key":"10_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3127586","volume":"65","author":"M Abadi","year":"2017","unstructured":"Abadi, M., Blanchet, B., Fournet, C.: The applied pi calculus: mobile values, new names, and secure communication. J. ACM (JACM) 65, 1\u201341 (2017)","journal-title":"J. ACM (JACM)"},{"key":"10_CR2","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1016\/j.tcs.2006.08.032","volume":"367","author":"M Abadi","year":"2006","unstructured":"Abadi, M., Cortier, V.: Deciding knowledge in security protocols under equational theories. Theoret. Comput. Sci. 367, 2\u201332 (2006)","journal-title":"Theoret. Comput. Sci."},{"key":"10_CR3","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1016\/j.tcs.2003.12.023","volume":"322","author":"M Abadi","year":"2004","unstructured":"Abadi, M., Fournet, C.: Private authentication. Theoret. Comput. Sci. 322, 427\u2013476 (2004)","journal-title":"Theoret. Comput. Sci."},{"key":"10_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1998.2740","volume":"148","author":"M Abadi","year":"1999","unstructured":"Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: the spi calculus. Inf. Comput. 148, 1\u201370 (1999)","journal-title":"Inf. Comput."},{"key":"10_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-540-73449-9_4","volume-title":"Term Rewriting and Applications","author":"S Anantharaman","year":"2007","unstructured":"Anantharaman, S., Narendran, P., Rusinowitch, M.: Intruders with caps. In: Baader, F. (ed.) RTA 2007. LNCS, vol. 4533, pp. 20\u201335. Springer, Heidelberg (2007). \nhttps:\/\/doi.org\/10.1007\/978-3-540-73449-9_4"},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"Arapinis, M., Chothia, T., Ritter, E., Ryan, M.: Analysing unlinkability and anonymity using the applied pi calculus. In: IEEE Computer Security Foundations Symposium (CSF) (2010)","DOI":"10.1109\/CSF.2010.15"},{"key":"10_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1007\/978-3-319-45741-3_13","volume-title":"Computer Security \u2013 ESORICS 2016","author":"M Arapinis","year":"2016","unstructured":"Arapinis, M., Cortier, V., Kremer, S.: When are three voters enough for privacy properties? In: Askoxylakis, I., Ioannidis, S., Katsikas, S., Meadows, C. (eds.) ESORICS 2016. LNCS, vol. 9879, pp. 241\u2013260. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-45741-3_13"},{"issue":"1","key":"10_CR8","doi-asserted-by":"publisher","first-page":"71","DOI":"10.3233\/JCS-191366","volume":"28","author":"K Babel","year":"2020","unstructured":"Babel, K., Cheval, V., Kremer, S.: On the semantics of communications when verifying equivalence properties. J. Comput. Secur. 28(1), 71\u2013127 (2020)","journal-title":"J. Comput. Secur."},{"key":"10_CR9","unstructured":"Baelde, D., Delaune, S., Hirschi, L.: Partial order reduction for security protocols. In: International Conference on Concurrency Theory (CONCUR) (2015)"},{"key":"10_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2658996","volume":"17","author":"DA Basin","year":"2014","unstructured":"Basin, D.A., Cremers, C.: Know your enemy: compromising adversaries in protocol analysis. ACM Trans. Inf. Syst. Secur. (TISSEC) 17, 1\u201331 (2014)","journal-title":"ACM Trans. Inf. Syst. Secur. (TISSEC)"},{"key":"10_CR11","doi-asserted-by":"crossref","unstructured":"Basin, D.A., Dreier, J., Hirschi, L., Radomirovic, S., Sasse, R., Stettler, V.: A formal analysis of 5G authentication. In: ACM Conference on Computer and Communications Security (CCS) (2018)","DOI":"10.1145\/3243734.3243846"},{"key":"10_CR12","unstructured":"Baudet, M.: S\u00e9curit\u00e9 des protocoles cryptographiques: aspects logiques et calculatoires. Ph.D. thesis (2007)"},{"key":"10_CR13","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2422085.2422089","volume":"14","author":"M Baudet","year":"2013","unstructured":"Baudet, M., Cortier, V., Delaune, S.: YAPA: a generic tool for computing intruder knowledge. ACM Trans. Comput. Log. (TOCL) 14, 1\u201332 (2013)","journal-title":"ACM Trans. Comput. Log. (TOCL)"},{"key":"10_CR14","doi-asserted-by":"crossref","unstructured":"Bhargavan, K., Blanchet, B., Kobeissi, N.: Verified models and reference implementations for the TLS 1.3 standard candidate. In: IEEE Symposium on Security and Privacy, (S&P) (2017)","DOI":"10.1109\/SP.2017.26"},{"key":"10_CR15","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: Modeling and verifying security protocols with the applied pi calculus and ProVerif. In: Foundations and Trends in Privacy and Security (2016)","DOI":"10.1561\/9781680832075"},{"key":"10_CR16","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.jlap.2007.06.002","volume":"75","author":"B Blanchet","year":"2008","unstructured":"Blanchet, B., Abadi, M., Fournet, C.: Automated verification of selected equivalences for security protocols. J. Log. Algebraic Program. 75, 3\u201351 (2008)","journal-title":"J. Log. Algebraic Program."},{"key":"10_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2926715","volume":"17","author":"R Chadha","year":"2016","unstructured":"Chadha, R., Cheval, V., Ciob\u00e2c\u0103, \u015e., Kremer, S.: Automated verification of equivalence properties of cryptographic protocols. ACM Trans. Comput. Log. (TOCL) 17, 1\u201332 (2016)","journal-title":"ACM Trans. Comput. Log. (TOCL)"},{"key":"10_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"587","DOI":"10.1007\/978-3-642-54862-8_50","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"V Cheval","year":"2014","unstructured":"Cheval, V.: APTE: an algorithm for proving trace equivalence. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 587\u2013592. Springer, Heidelberg (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-642-54862-8_50"},{"key":"10_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/978-3-642-36830-1_12","volume-title":"Principles of Security and Trust","author":"V Cheval","year":"2013","unstructured":"Cheval, V., Blanchet, B.: Proving more observational equivalences with ProVerif. In: Basin, D., Mitchell, J.C. (eds.) POST 2013. LNCS, vol. 7796, pp. 226\u2013246. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-36830-1_12"},{"key":"10_CR20","doi-asserted-by":"crossref","unstructured":"Cheval, V., Comon-Lundh, H., Delaune, S.: Trace equivalence decision: negative tests and non-determinism. In: ACM Conference on Computer and Communications Security (CCS) (2011)","DOI":"10.1145\/2046707.2046744"},{"key":"10_CR21","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.tcs.2013.04.016","volume":"492","author":"V Cheval","year":"2013","unstructured":"Cheval, V., Cortier, V., Delaune, S.: Deciding equivalence-based properties using constraint solving. Theoret. Comput. Sci. 492, 1\u201339 (2013)","journal-title":"Theoret. Comput. Sci."},{"key":"10_CR22","doi-asserted-by":"crossref","unstructured":"Cheval, V., Kremer, S., Rakotonirina, I.: DEEPSEC: deciding equivalence properties in security protocols theory and practice. In: IEEE Symposium on Security and Privacy (S&P) (2018)","DOI":"10.1109\/SP.2018.00033"},{"key":"10_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-319-96142-2_4","volume-title":"Computer Aided Verification","author":"V Cheval","year":"2018","unstructured":"Cheval, V., Kremer, S., Rakotonirina, I.: The DEEPSEC prover. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 28\u201336. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-319-96142-2_4"},{"key":"10_CR24","doi-asserted-by":"crossref","unstructured":"Cheval, V., Kremer, S., Rakotonirina, I.: Exploiting symmetries when proving equivalence properties for security protocols. In: ACM Conference on Computer and Communications Security (CCS) (2019)","DOI":"10.1145\/3319535.3354260"},{"key":"10_CR25","unstructured":"Cheval, V., Kremer, S., Rakotonirina, I.: The Hitchhiker\u2019s guide to decidability and complexity of equivalence properties in security protocols (Technical report) (2020). \nhttps:\/\/hal.archives-ouvertes.fr\/hal-02501577"},{"key":"10_CR26","doi-asserted-by":"crossref","unstructured":"Chr\u00e9tien, R., Cortier, V., Delaune, S.: Decidability of trace equivalence for protocols with nonces. In: IEEE Computer Security Foundations Symposium (CSF) (2015)","DOI":"10.1109\/CSF.2015.19"},{"key":"10_CR27","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2811262","volume":"17","author":"R Chr\u00e9tien","year":"2015","unstructured":"Chr\u00e9tien, R., Cortier, V., Delaune, S.: From security protocols to pushdown automata. ACM Trans. Comput. Log. (TOCL) 17, 1\u201345 (2015)","journal-title":"ACM Trans. Comput. Log. (TOCL)"},{"key":"10_CR28","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-642-02959-2_27","volume-title":"Automated Deduction \u2013 CADE-22","author":"\u015e Ciob\u00e2c\u0103","year":"2009","unstructured":"Ciob\u00e2c\u0103, \u015e., Delaune, S., Kremer, S.: Computing knowledge in security protocols under convergent equational theories. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 355\u2013370. Springer, Heidelberg (2009). \nhttps:\/\/doi.org\/10.1007\/978-3-642-02959-2_27"},{"key":"10_CR29","doi-asserted-by":"crossref","unstructured":"Cohn-Gordon, K., Cremers, C., Garratt, L., Millican, J., Milner, K.: On ends-to-ends encryption: Asynchronous group messaging with strong security guarantees. In: ACM Conference on Computer and Communications Security (CCS) (2018)","DOI":"10.1145\/3243734.3243747"},{"key":"10_CR30","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1016\/j.tcs.2004.09.036","volume":"331","author":"H Comon","year":"2005","unstructured":"Comon, H., Cortier, V.: Tree automata with one memory set constraints and cryptographic protocols. Theoret. Comput. Sci. 331, 143\u2013214 (2005)","journal-title":"Theoret. Comput. Sci."},{"key":"10_CR31","doi-asserted-by":"crossref","unstructured":"Conchinha, B., Basin, D.A., Caleiro, C.: Fast: an efficient decision procedure for deduction and static equivalence. In: International Conference on Rewriting Techniques and Applications (RTA) (2011)","DOI":"10.1007\/978-3-642-19751-2_3"},{"key":"10_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/978-3-319-99073-6_24","volume-title":"Computer Security","author":"V Cortier","year":"2018","unstructured":"Cortier, V., Dallon, A., Delaune, S.: Efficiently deciding equivalence for standard primitives and phases. In: Lopez, J., Zhou, J., Soriano, M. (eds.) ESORICS 2018. LNCS, vol. 11098, pp. 491\u2013511. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-319-99073-6_24"},{"key":"10_CR33","doi-asserted-by":"crossref","unstructured":"Cortier, V., Grimm, N., Lallemand, J., Maffei, M.: A type system for privacy properties. In: ACM Conference on Computer and Communications Security (CCS) (2017)","DOI":"10.1145\/3133956.3133998"},{"key":"10_CR34","doi-asserted-by":"crossref","unstructured":"Cremers, C., Horvat, M., Hoyland, J., Scott, S., van der Merwe, T.: A comprehensive symbolic analysis of TLS 1.3. In: ACM Conference on Computer and Communications Security (CCS) (2017)","DOI":"10.1145\/3133956.3134063"},{"key":"10_CR35","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1016\/S0304-3975(96)00325-8","volume":"183","author":"M Dam","year":"1997","unstructured":"Dam, M.: On the decidability of process equivalences for the $$\\pi $$-calculus. Theoret. Comput. Sci. 183, 215\u2013228 (1997)","journal-title":"Theoret. Comput. Sci."},{"key":"10_CR36","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1016\/j.jlamp.2016.10.005","volume":"87","author":"S Delaune","year":"2017","unstructured":"Delaune, S., Hirschi, L.: A survey of symbolic methods for establishing equivalence-based properties in cryptographic protocols. J. Log. Algebraic Methods Program. 87, 127\u2013144 (2017)","journal-title":"J. Log. Algebraic Methods Program."},{"key":"10_CR37","doi-asserted-by":"publisher","first-page":"435","DOI":"10.3233\/JCS-2009-0340","volume":"17","author":"S Delaune","year":"2009","unstructured":"Delaune, S., Kremer, S., Ryan, M.: Verifying privacy-type properties of electronic voting protocols. J. Comput. Secur. 17, 435\u2013487 (2009)","journal-title":"J. Comput. Secur."},{"key":"10_CR38","doi-asserted-by":"crossref","unstructured":"Dolev, D., Yao, A.: On the security of public key protocols. In: Symposium on Foundations of Computer Science (FOCS) (1981)","DOI":"10.1109\/SFCS.1981.32"},{"key":"10_CR39","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1016\/S0019-9958(82)90401-6","volume":"55","author":"D Dolev","year":"1982","unstructured":"Dolev, D., Even, S., Karp, R.M.: On the security of ping-pong protocols. Inf. Control 55, 57\u201368 (1982)","journal-title":"Inf. Control"},{"key":"10_CR40","doi-asserted-by":"publisher","first-page":"247","DOI":"10.3233\/JCS-2004-12203","volume":"12","author":"NA Durgin","year":"2004","unstructured":"Durgin, N.A., Lincoln, P., Mitchell, J.C.: Multiset rewriting and the complexity of bounded security protocols. J. Comput. Secur. 12, 247\u2013311 (2004)","journal-title":"J. Comput. Secur."},{"key":"10_CR41","unstructured":"Durgin, N.A., Lincoln, P., Mitchell, J.C., Scedrov, A.: Undecidability of bounded security protocols. In: Proceedings of Workshop on Formal Methods in Security Protocols (1999)"},{"key":"10_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"577","DOI":"10.1007\/978-3-030-29959-0_28","volume-title":"Computer Security \u2013 ESORICS 2019","author":"I Filimonov","year":"2019","unstructured":"Filimonov, I., Horne, R., Mauw, S., Smith, Z.: Breaking unlinkability of the ICAO 9303 Standard for e-passports using bisimilarity. In: Sako, K., Schneider, S., Ryan, P.Y.A. (eds.) ESORICS 2019. LNCS, vol. 11735, pp. 577\u2013594. Springer, Cham (2019). \nhttps:\/\/doi.org\/10.1007\/978-3-030-29959-0_28"},{"key":"10_CR43","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S1571-0661(04)80530-9","volume":"68","author":"H H\u00fcttel","year":"2003","unstructured":"H\u00fcttel, H.: Deciding framed bisimilarity. Electron. Notes Theoret. Comput. Sci 68, 1\u201318 (2003)","journal-title":"Electron. Notes Theoret. Comput. Sci"},{"key":"10_CR44","doi-asserted-by":"crossref","unstructured":"H\u00fcttel, H., Srba, J.: Recursive ping-pong protocols. BRICS Report Series (2003)","DOI":"10.7146\/brics.v10i47.21819"},{"key":"10_CR45","doi-asserted-by":"crossref","unstructured":"Jacomme, C., Kremer, S.: An extensive formal analysis of multi-factor authentication protocols. In: IEEE Computer Security Foundations Symposium (CSF) (2018)","DOI":"10.29007\/xrx7"},{"issue":"3\u20134","key":"10_CR46","first-page":"137","volume":"40","author":"MI Kanovich","year":"2014","unstructured":"Kanovich, M.I., Kirigin, T.B., Nigam, V., Scedrov, A.: Bounded memory protocols. Comput. Lang. Syst. Struct. 40(3\u20134), 137\u2013154 (2014)","journal-title":"Comput. Lang. Syst. Struct."},{"key":"10_CR47","doi-asserted-by":"crossref","unstructured":"Kobeissi, N., Bhargavan, K., Blanchet, B.: Automated verification for secure messaging protocols and their implementations: a symbolic and computational approach. In: IEEE European Symposium on Security and Privacy (EuroS&P) (2017)","DOI":"10.1109\/EuroSP.2017.38"},{"key":"10_CR48","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., Walker, D.: A calculus of mobile processes. I. Inf. Comput. 100, 1\u201340 (1992)","journal-title":"Inf. Comput."},{"key":"10_CR49","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., Turuani, M.: Protocol insecurity with a finite number of sessions, composed keys is NP-complete. Theoret. Comput. Sci. 299, 451\u2013475 (2003)","journal-title":"Theoret. Comput. Sci."},{"key":"10_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"696","DOI":"10.1007\/978-3-642-39799-8_48","volume-title":"Computer Aided Verification","author":"S Meier","year":"2013","unstructured":"Meier, S., Schmidt, B., Cremers, C., Basin, D.: The TAMARIN prover for the symbolic analysis of security protocols. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 696\u2013701. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-39799-8_48"}],"container-title":["Lecture Notes in Computer Science","Logic, Language, and Security"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-62077-6_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,10,28]],"date-time":"2020-10-28T12:07:59Z","timestamp":1603886879000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-62077-6_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030620769","9783030620776"],"references-count":50,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-62077-6_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"28 October 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}