{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:14:26Z","timestamp":1763468066088,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":40,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642288685"},{"type":"electronic","value":"9783642288692"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-28869-2_6","type":"book-chapter","created":{"date-parts":[[2012,3,22]],"date-time":"2012-03-22T20:44:36Z","timestamp":1332449076000},"page":"108-127","source":"Crossref","is-referenced-by-count":40,"title":["Automated Verification of Equivalence Properties of Cryptographic Protocols"],"prefix":"10.1007","author":[{"given":"Rohit","family":"Chadha","sequence":"first","affiliation":[]},{"given":"\u015etefan","family":"Ciob\u00e2c\u0103","sequence":"additional","affiliation":[]},{"given":"Steve","family":"Kremer","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1-2","key":"6_CR1","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1016\/j.tcs.2006.08.032","volume":"387","author":"M. Abadi","year":"2006","unstructured":"Abadi, M., Cortier, V.: Deciding knowledge in security protocols under equational theories. Theoretical Computer Science\u00a0387(1-2), 2\u201332 (2006)","journal-title":"Theoretical Computer Science"},{"key":"6_CR2","doi-asserted-by":"crossref","unstructured":"Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: 28th Symposium on Principles of Programming Languages (POPL 2001), pp. 104\u2013115. ACM Press (2001)","DOI":"10.1145\/373243.360213"},{"issue":"3","key":"6_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. Theoretical Computer Science\u00a0322(3), 427\u2013476 (2004)","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"6_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.\u00a0148(1), 1\u201370 (1999)","journal-title":"Inf. Comput."},{"key":"6_CR5","doi-asserted-by":"crossref","unstructured":"Arapinis, M., Chothia, T., Ritter, E., Ryan, M.D.: Analysing unlinkability and anonymity using the applied pi calculus. In: 23rd Computer Security Foundations Symposium (CSF 2010), pp. 107\u2013121. IEEE Comp. Soc. Press (2010)","DOI":"10.1109\/CSF.2010.15"},{"key":"6_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/11513988_27","volume-title":"Computer Aided Verification","author":"A. Armando","year":"2005","unstructured":"Armando, A., Basin, D., Boichut, Y., Chevalier, Y., Compagna, L., Cuellar, J., Drielsma, P.H., He\u00e1m, P.C., Kouchnarenko, O., Mantovani, J., M\u00f6dersheim, S., von Oheimb, D., Rusinowitch, M., Santiago, J., Turuani, M., Vigan\u00f2, L., Vigneron, L.: The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 281\u2013285. Springer, Heidelberg (2005)"},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"Backes, M., Hritcu, C., Maffei, M.: Automated verification of remote electronic voting protocols in the applied pi-calculus. In: 21st Computer Security Foundations Symposium (CSF 2008). IEEE Comp. Soc. Press (2008)","DOI":"10.1109\/CSF.2008.26"},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"Baudet, M.: Deciding security of protocols against off-line guessing attacks. In: 12th Conference on Computer and Communications Security (CCS 2005), pp. 16\u201325. ACM Press (2005)","DOI":"10.1145\/1102120.1102125"},{"key":"6_CR9","unstructured":"Bellovin, S.M., Merritt, M.: Encrypted key exchange: Password-based protocols secure against dictionary attacks. In: Symposium on Security and Privacy (S&P 1992), pp. 72\u201384. IEEE Comp. Soc. Press (1992)"},{"key":"6_CR10","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In: 14th Computer Security Foundations Workshop (CSFW 2001), pp. 82\u201396. IEEE Comp. Soc. Press (2001)","DOI":"10.1109\/CSFW.2001.930138"},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: Automatic proof of strong secrecy for security protocols. In: Symposium on Security and Privacy (S&P 2004), pp. 86\u2013100 (2004)","DOI":"10.1109\/SECPRI.2004.1301317"},{"key":"6_CR12","doi-asserted-by":"crossref","unstructured":"Blanchet, B., Abadi, M., Fournet, C.: Automated Verification of Selected Equivalences for Security Protocols. In: Symposium on Logic in Computer Science, pp. 331\u2013340. IEEE Comp. Soc. Press (2005)","DOI":"10.1109\/LICS.2005.8"},{"key":"6_CR13","unstructured":"Borgstr\u00f6m, J.: Equivalences and Calculi for Formal Verifiation of Cryptographic Protocols. Phd thesis, EPFL, Switzerland (2008)"},{"key":"6_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/978-3-540-28644-8_11","volume-title":"CONCUR 2004 - Concurrency Theory","author":"J. Borgstr\u00f6m","year":"2004","unstructured":"Borgstr\u00f6m, J., Briais, S., Nestmann, U.: Symbolic Bisimulation in the Spi Calculus. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol.\u00a03170, pp. 161\u2013176. Springer, Heidelberg (2004)"},{"key":"6_CR15","unstructured":"Bruso, M., Chatzikokolakis, K., den Hartog, J.: Analysing unlinkability and anonymity using the applied pi calculus. In: 23rd Computer Security Foundations Symposium (CSF 2010), pp. 107\u2013121. IEEE Comp. Soc. Press (2010)"},{"key":"6_CR16","unstructured":"Chadha, R., Ciob\u00e2c\u0103, \u015e., Kremer, S.: Automated verification of equivalence properties of cryptographic protocols. Technical report (October 2011), http:\/\/hal.inria.fr\/inria-00632564\/en\/"},{"key":"6_CR17","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"412","DOI":"10.1007\/978-3-642-14203-1_35","volume-title":"Automated Reasoning","author":"V. Cheval","year":"2010","unstructured":"Cheval, V., Comon-Lundh, H., Delaune, S.: Automating Security Analysis: Symbolic Equivalence of Constraint Systems. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol.\u00a06173, pp. 412\u2013426. Springer, Heidelberg (2010)"},{"key":"6_CR18","doi-asserted-by":"crossref","unstructured":"Cheval, V., Comon-Lundh, H., Delaune, S.: Trace equivalence decision: Negative tests and non-determinism. In: 18th Conference on Computer and Communications Security (CCS 2011), pp. 321\u2013330. ACM Press (2011)","DOI":"10.1145\/2046707.2046744"},{"key":"6_CR19","doi-asserted-by":"crossref","unstructured":"Chevalier, Y., Rusinowitch, M.: Decidability of equivalence of symbolic derivations. Journal of Automated Reasoning (2010)","DOI":"10.1007\/s10817-010-9199-5"},{"key":"6_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/978-3-540-75336-0_19","volume-title":"Trustworthy Global Computing","author":"T. Chothia","year":"2007","unstructured":"Chothia, T., Orzan, S., Pang, J., Torabi Dashti, M.: A Framework for Automatically Checking Anonymity with \u03bcCRL. In: Montanari, U., Sannella, D., Bruni, R. (eds.) TGC 2006. LNCS, vol.\u00a04661, pp. 301\u2013318. Springer, Heidelberg (2007)"},{"key":"6_CR21","unstructured":"Ciob\u00e2c\u0103, \u015e.: Computing finite variants for subterm convergent rewrite systems. Research Report LSV-11-06, LSV, ENS Cachan, France (2011)"},{"key":"6_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/978-3-540-32033-3_22","volume-title":"Term Rewriting and Applications","author":"H. Comon-Lundh","year":"2005","unstructured":"Comon-Lundh, H., Delaune, S.: The Finite Variant Property: How to Get Rid of Some Algebraic Properties. In: Giesl, J. (ed.) RTA 2005. LNCS, vol.\u00a03467, pp. 294\u2013307. Springer, Heidelberg (2005)"},{"key":"6_CR23","doi-asserted-by":"crossref","unstructured":"Cortier, V., Delaune, S.: A method for proving observational equivalence. In: 22nd Computer Security Foundations Symposium (CSF 2009), pp. 266\u2013276. IEEE Comp. Soc. Press (2009)","DOI":"10.1109\/CSF.2009.9"},{"key":"6_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/978-3-642-15497-3_4","volume-title":"Computer Security \u2013 ESORICS 2010","author":"M. Dahl","year":"2010","unstructured":"Dahl, M., Delaune, S., Steel, G.: Formal Analysis of Privacy for Vehicular Mix-Zones. In: Gritzalis, D., Preneel, B., Theoharidou, M. (eds.) ESORICS 2010. LNCS, vol.\u00a06345, pp. 55\u201370. Springer, Heidelberg (2010)"},{"key":"6_CR25","unstructured":"Delaune, S., Kremer, S., Pereira, O.: Simulation based security in the applied pi calculus. In: 29th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2009). Leibniz International Proceedings in Informatics, vol.\u00a04, pp. 169\u2013180. Leibniz-Zentrum f\u00fcr Informatik (2009)"},{"issue":"4","key":"6_CR26","doi-asserted-by":"crossref","first-page":"435","DOI":"10.3233\/JCS-2009-0340","volume":"17","author":"S. Delaune","year":"2009","unstructured":"Delaune, S., Kremer, S., Ryan, M.D.: Verifying privacy-type properties of electronic voting protocols. Journal of Computer Security\u00a017(4), 435\u2013487 (2009)","journal-title":"Journal of Computer Security"},{"issue":"2","key":"6_CR27","doi-asserted-by":"crossref","first-page":"317","DOI":"10.3233\/JCS-2010-0363","volume":"18","author":"S. Delaune","year":"2010","unstructured":"Delaune, S., Kremer, S., Ryan, M.D.: Symbolic bisimulation for the applied pi\u00a0calculus. Journal of Computer Security\u00a018(2), 317\u2013377 (2010)","journal-title":"Journal of Computer Security"},{"key":"6_CR28","series-title":"IFIP Conference Proceedings","first-page":"263","volume-title":"2nd Joint iTrust and PST Conferences on Privacy, Trust Management and Security (IFIPTM 2008)","author":"S. Delaune","year":"2008","unstructured":"Delaune, S., Ryan, M.D., Smyth, B.: Automatic verification of privacy properties in the applied pi-calculus. In: 2nd Joint iTrust and PST Conferences on Privacy, Trust Management and Security (IFIPTM 2008). IFIP Conference Proceedings, vol.\u00a0263, pp. 263\u2013278. Springer, Heidelberg (2008)"},{"key":"6_CR29","doi-asserted-by":"crossref","unstructured":"Dolev, D., Yao, A.: On the security of public key protocols. In: 22nd Symposium on Foundations of Computer Science (FOCS 1981), pp. 350\u2013357. IEEE Comp. Soc. Press (1981)","DOI":"10.1109\/SFCS.1981.32"},{"issue":"2","key":"6_CR30","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1145\/941566.941570","volume":"12","author":"L. Durante","year":"2003","unstructured":"Durante, L., Sisto, R., Valenzano, A.: Automatic testing equivalence verification of spi calculus specifications. ACM Transactions on Software Engineering and Methodology\u00a012(2), 222\u2013284 (2003)","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"key":"6_CR31","series-title":"LNCS","first-page":"1","volume-title":"FOSAD 2007\/2008\/2009","author":"S. Escobar","year":"2009","unstructured":"Escobar, S., Meadows, C., Meseguer, J.: Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) FOSAD 2007\/2008\/2009. LNCS, vol.\u00a05705, pp. 1\u201350. Springer, Heidelberg (2009)"},{"key":"6_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/3-540-57220-1_66","volume-title":"Advances in Cryptology - AUSCRYPT \u201992","author":"A. Fujioka","year":"1993","unstructured":"Fujioka, A., Okamoto, T., Ohta, K.: A Practical Secret Voting Scheme for Large Scale Elections. In: Zheng, Y., Seberry, J. (eds.) AUSCRYPT 1992. LNCS, vol.\u00a0718, pp. 244\u2013251. Springer, Heidelberg (1993)"},{"issue":"3","key":"6_CR33","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1016\/j.ipl.2005.04.007","volume":"95","author":"J. Goubault-Larrecq","year":"2005","unstructured":"Goubault-Larrecq, J.: Deciding $\\mathcal{\\MakeUppercase{h}}_1$ by resolution. Information Processing Letters\u00a095(3), 401\u2013408 (2005)","journal-title":"Information Processing Letters"},{"key":"6_CR34","unstructured":"H\u00fcttel, H.: Deciding framed bisimilarity. In: 4th International Workshop on Verification of Infinite-State Systems (INFINITY 2002), pp. 1\u201320 (2002)"},{"key":"6_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"552","DOI":"10.1007\/978-3-642-11266-9_46","volume-title":"SOFSEM 2010: Theory and Practice of Computer Science","author":"J. Liu","year":"2010","unstructured":"Liu, J., Lin, H.: A Complete Symbolic Bisimulation for Full Applied Pi Calculus. In: van Leeuwen, J., Muscholl, A., Peleg, D., Pokorn\u00fd, J., Rumpe, B. (eds.) SOFSEM 2010. LNCS, vol.\u00a05901, pp. 552\u2013563. Springer, Heidelberg (2010)"},{"key":"6_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/3-540-61042-1_43","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G. Lowe","year":"1996","unstructured":"Lowe, G.: Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol.\u00a01055, pp. 147\u2013166. Springer, Heidelberg (1996)"},{"issue":"2","key":"6_CR37","doi-asserted-by":"publisher","first-page":"636","DOI":"10.2307\/2275552","volume":"62","author":"P. Narendran","year":"1997","unstructured":"Narendran, P., Pfenning, F., Statman, R.: On the unification problem for cartesian closed categories. J. Symb. Log.\u00a062(2), 636\u2013647 (1997)","journal-title":"J. Symb. Log."},{"key":"6_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/BFb0028157","volume-title":"Security Protocols","author":"T. Okamoto","year":"1998","unstructured":"Okamoto, T.: Receipt-Free Electronic Voting Schemes for Large Scale Elections. In: Christianson, B., Lomas, M. (eds.) Security Protocols 1997. LNCS, vol.\u00a01361, pp. 25\u201335. Springer, Heidelberg (1998)"},{"key":"6_CR39","doi-asserted-by":"crossref","unstructured":"Tiu, A., Dawson, J.: Automating open bisimulation checking for the spi-calculus. In: 23rd Computer Security Foundations Symposium (CSF 2010), pp. 307\u2013321. IEEE Comp. Soc. Press (2010)","DOI":"10.1109\/CSF.2010.28"},{"key":"6_CR40","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"314","DOI":"10.1007\/3-540-48660-7_29","volume-title":"Automated Deduction - CADE-16","author":"C. Weidenbach","year":"1999","unstructured":"Weidenbach, C.: Towards an Automatic Analysis of Security Protocols in First-Order Logic. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol.\u00a01632, pp. 314\u2013328. Springer, Heidelberg (1999)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-28869-2_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,23]],"date-time":"2025-03-23T18:48:56Z","timestamp":1742755736000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-28869-2_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642288685","9783642288692"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-28869-2_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}