{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T04:05:21Z","timestamp":1748664321163,"version":"3.41.0"},"publisher-location":"Cham","reference-count":83,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319231648"},{"type":"electronic","value":"9783319231655"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","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":[[2015]]},"DOI":"10.1007\/978-3-319-23165-5_22","type":"book-chapter","created":{"date-parts":[[2015,8,26]],"date-time":"2015-08-26T03:57:43Z","timestamp":1440561463000},"page":"475-492","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Emerging Issues and Trends in Formal Methods in Cryptographic Protocol Analysis: Twelve Years Later"],"prefix":"10.1007","author":[{"given":"Catherine","family":"Meadows","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,8,27]]},"reference":[{"key":"22_CR1","doi-asserted-by":"crossref","unstructured":"Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: Hankin, C., Schmidt, D., (eds.) Conference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 17-19 January 2001, pp. 104\u2013115, London, UK. ACM (2001)","DOI":"10.1145\/360204.360213"},{"issue":"2","key":"22_CR2","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/s00145-001-0014-7","volume":"15","author":"M Abadi","year":"2002","unstructured":"Abadi, M., Rogaway, P.: Reconciling two views of cryptography (the computational soundness of formal encryption). J. Cryptol. 15(2), 103\u2013127 (2002)","journal-title":"J. Cryptol."},{"key":"22_CR3","unstructured":"Adida, B., De Marneffe, O., Pereira, O., Quisquater, J.-J.: Electing a university president using open-audit voting: analysis of real-world use of helios. In: Electrionic Voting Technology\/Workshop on Trustworthy Elections: EVT\/WOTE (2009). https:\/\/www.usenix.org\/legacy\/event\/evtwote09\/tech\/"},{"key":"22_CR4","unstructured":"Adida, B.: Helios: web-based open-audit voting. In: van Oorschot, P.C. (ed.) Proceedings of the 17th USENIX Security Symposium, 28 July - 1 August 2008, San Jose, CA, USA, pp. 335\u2013348. USENIX Association (2008)"},{"key":"22_CR5","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. 3576, pp. 281\u2013285. Springer, Heidelberg (2005)"},{"key":"22_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-642-22438-6_6","volume-title":"Automated Deduction \u2013 CADE-23","author":"M Arnaud","year":"2011","unstructured":"Arnaud, M., Cortier, V., Delaune, S.: Deciding security for protocols with recursive tests. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 49\u201363. Springer, Heidelberg (2011)"},{"issue":"2","key":"22_CR7","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/s10207-011-0125-6","volume":"10","author":"M Backes","year":"2011","unstructured":"Backes, M., Cervesato, I., Jaggard, A.D., Scedrov, A., Tsay, J.-K.: Cryptographically sound security proofs for basic and public-key kerberos. Int. J. Inf. Sec. 10(2), 107\u2013134 (2011)","journal-title":"Int. J. Inf. Sec."},{"key":"22_CR8","doi-asserted-by":"crossref","unstructured":"Backes, M., Goldberg, I., Kate, A., Mohammadi, E.: Provably secure and practical onion routing. In: Chong, S. (ed.) 25th IEEE Computer Security Foundations Symposium, CSF 2012, 25\u201327 June 2012, Cambridge, MA, USA, pp. 369\u2013385. IEEE (2012)","DOI":"10.1109\/CSF.2012.32"},{"key":"22_CR9","doi-asserted-by":"crossref","unstructured":"Backes, M., Hofheinz, D., Unruh, D.: Cosp: a general framework for computational soundness proofs. In: Al-Shaer, E., Jha, S., Keromytis, A.D. (eds.) Proceedings of the 2009 ACM Conference on Computer and Communications Security, CCS 2009, Chicago, Illinois, USA, 9-13 November2009, pp. 66\u201378. ACM (2009)","DOI":"10.1145\/1653662.1653672"},{"key":"22_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1007\/3-540-36494-3_59","volume-title":"STACS 2003","author":"M Backes","year":"2003","unstructured":"Backes, M., Jacobi, C.: Cryptographically sound and machine-assisted verification of security protocols. In: Alt, H., Habib, M. (eds.) STACS 2003. Lecture Notes in Computer Science, vol. 2607, pp. 675\u2013686. Springer, Heidelberg (2003)"},{"key":"22_CR11","doi-asserted-by":"crossref","unstructured":"Backes, M., Pfitzmann, B., Waidner, M.: A universally composable cryptographic library. IACR Cryptology ePrint Archive 2003:15 (2003)","DOI":"10.1145\/948109.948140"},{"key":"22_CR12","doi-asserted-by":"crossref","unstructured":"Bana, G., Comon-Lundh, H.: Towards unconditional soundness: computationally complete symbolic attacker. In: Degano, P., Guttman, J.D. (eds.) [38], pp.189\u2013208","DOI":"10.1007\/978-3-642-28641-4_11"},{"key":"22_CR13","doi-asserted-by":"crossref","unstructured":"Bana, G., Comon-Lundh, H.: A computationally complete symbolic attacker for equivalence properties. In: Ahn, G-J., Yung, M., Li, N. (eds.) Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, Scottsdale, AZ, USA, 3\u20137 November 2014, pp. 609\u2013620. ACM (2014)","DOI":"10.1145\/2660267.2660276"},{"key":"22_CR14","doi-asserted-by":"crossref","unstructured":"Barthe, G., Crespo, J.M., Gr\u00e9goire, B., Kunz, C., Lakhnech, Y., Schmidt, B., B\u00e9guelin, S.Z.: Fully automated analysis of padding-based encryption in the computational model. In: Sadeghi, A.R., Gligor, V.D., Yung, M. (eds.) 2013 ACM SIGSAC Conference on Computer and Communications Security, CCS 2013, Berlin, Germany, 4\u20138 November 2013 pp. 1247\u20131260. ACM (2013)","DOI":"10.1145\/2508859.2516663"},{"key":"22_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-642-22792-9_5","volume-title":"Advances in Cryptology \u2013 CRYPTO 2011","author":"G Barthe","year":"2011","unstructured":"Barthe, G., Gr\u00e9goire, B., Heraud, S., B\u00e9guelin, S.Z.: Computer-aided security proofs for the working cryptographer. In: Rogaway, P. (ed.) CRYPTO 2011. LNCS, vol. 6841, pp. 71\u201390. Springer, Heidelberg (2011)"},{"key":"22_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"652","DOI":"10.1007\/11523468_53","volume-title":"Automata, Languages and Programming","author":"M Baudet","year":"2005","unstructured":"Baudet, M., Cortier, V., Kremer, S.: Computationally sound implementations of equational theories against passive adversaries. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 652\u2013663. Springer, Heidelberg (2005)"},{"issue":"1","key":"22_CR17","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1109\/JSAC.2002.806133","volume":"21","author":"G Bella","year":"2003","unstructured":"Bella, G., Massacci, F., Paulson, L.C.: Verifying the SET registration protocols. IEEE J. Sel. Areas Commun. 21(1), 77\u201387 (2003)","journal-title":"IEEE J. Sel. Areas Commun."},{"issue":"1\u20132","key":"22_CR18","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/s10817-005-9018-6","volume":"36","author":"G Bella","year":"2006","unstructured":"Bella, G., Massacci, F., Paulson, L.C.: Verifying the SET purchase protocols. J. Autom. Reasoning 36(1\u20132), 5\u201337 (2006)","journal-title":"J. Autom. Reasoning"},{"key":"22_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"602","DOI":"10.1007\/11818175_36","volume-title":"Advances in Cryptology - CRYPTO 2006","author":"M Bellare","year":"2006","unstructured":"Bellare, M.: New proofs for NMAC and HMAC: security without collision-resistance. In: Dwork, C. (ed.) CRYPTO 2006. LNCS, vol. 4117, pp. 602\u2013619. Springer, Heidelberg (2006)"},{"key":"22_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/978-3-642-23822-2_19","volume-title":"Computer Security \u2013 ESORICS 2011","author":"D Bernhard","year":"2011","unstructured":"Bernhard, D., Cortier, V., Pereira, O., Smyth, B., Warinschi, B.: Adapting helios for provable ballot privacy. In: Atluri, V., Diaz, C. (eds.) ESORICS 2011. LNCS, vol. 6879, pp. 335\u2013354. Springer, Heidelberg (2011)"},{"issue":"4","key":"22_CR21","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1109\/TDSC.2007.1005","volume":"5","author":"B Blanchet","year":"2008","unstructured":"Blanchet, B.: A computationally sound mechanized prover for security protocols. IEEE Trans. Dependable Sec. Comput. 5(4), 193\u2013207 (2008)","journal-title":"IEEE Trans. Dependable Sec. Comput."},{"key":"22_CR22","doi-asserted-by":"crossref","unstructured":"Blanchet, B., Abadi, M., Fournet, C.: Automated verification of selected equivalences for security protocols. In: Proceedings of 20th IEEE Symposium on Logic in Computer Science (LICS 2005), 26\u201329 June 2005, Chicago, IL, USA, pp. 331\u2013340. IEEE Computer Society, Chicago (2005)","DOI":"10.1109\/LICS.2005.8"},{"key":"22_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1007\/11861386_12","volume-title":"Security Protocols","author":"M Blaze","year":"2006","unstructured":"Blaze, M.: Toward a broader view of security protocols. In: Christianson, B., Crispo, B., Malcolm, J.A., Roe, M. (eds.) Security Protocols 2004. LNCS, vol. 3957, pp. 106\u2013120. Springer, Heidelberg (2006)"},{"key":"22_CR24","unstructured":"Bond, M.: A chosen key difference attack on control vectors (2000). http:\/\/www.cl.cam.ac.uk\/mkb23\/research.html"},{"key":"22_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1007\/BFb0000433","volume-title":"Advances in Cryptology - ASIACRYPT 1994","author":"C Boyd","year":"1995","unstructured":"Boyd, C., Mao, W.: Design and analysis of key exchange protocols via secure channel identification. In: Safavi-Naini, R., Pieprzyk, J.P. (eds.) ASIACRYPT 1994. LNCS, vol. 917, pp. 171\u2013181. Springer, Heidelberg (1995)"},{"key":"22_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"344","DOI":"10.1007\/3-540-48285-7_30","volume-title":"Advances in Cryptology - EUROCRYPT 1993","author":"S Brands","year":"1994","unstructured":"Brands, S., Chaum, D.: Distance bounding protocols. In: Helleseth, T. (ed.) EUROCRYPT 1993. LNCS, vol. 765, pp. 344\u2013359. Springer, Heidelberg (1994)"},{"key":"22_CR27","doi-asserted-by":"crossref","unstructured":"Burrows, M., Abadi, M., Needham, R.M.: A logic of authentication. In: SOSP, pp. 1\u201313 (1989)","DOI":"10.1145\/74851.74852"},{"key":"22_CR28","unstructured":"Burton, C., Culnane, C., Heather, J., Peacock, T., Ryan, P.Y.A., Schneider, S., Teague, V., Wen, R., Xia, Z., Srinivasan, S.: Using pr\u00eat \u00e0 voter in victoria state elections. In: Halderman, J.A., Pereira, O. (eds.) 2012 Electronic Voting Technology Workshop\/Workshop on Trustworthy Elections, EVT\/WOTE 2012, Bellevue, WA, USA, 6\u20137 August 2012. USENIX Association (2012)"},{"issue":"1\u20132","key":"22_CR29","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1016\/j.tcs.2006.08.040","volume":"367","author":"F Butler","year":"2006","unstructured":"Butler, F., Cervesato, I., Jaggard, A.D., Scedrov, A., Walstad, C.: Formal analysis of kerberos 5. Theor. Comput. Sci. 367(1\u20132), 57\u201387 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"22_CR30","doi-asserted-by":"crossref","unstructured":"Canetti, R.: Universally composable security: a new paradigm for cryptographic protocols. In: 42nd Annual Symposium on Foundations of Computer Science, FOCS 2001, Las Vegas, Nevada, USA, 14\u201317 October 2001, pp. 136\u2013145. IEEE Computer Society (2001)","DOI":"10.1109\/SFCS.2001.959888"},{"key":"22_CR31","unstructured":"Carback, R., Chaum, D., Clark, J., Conway, J., Essex, A., Herrnson, P.S., Mayberry, T., Popoveniuc, S., Rivest, R.L., Shen, E., Sherman, A.T., Vora, P.L.: Scantegrity II municipal election at takoma park: the first E2E binding governmental election with ballot privacy. In: Proceedings of 19th USENIX Security Symposium, Washington, DC, USA, 11\u201313 August 2010, pp. 291\u2013306. USENIX Association (2010)"},{"key":"22_CR32","doi-asserted-by":"crossref","unstructured":"Clarkson, M.R., Chong, S., Myers, A.C.: Civitas: A secure voting system. Technical report, Cornell University (2007)","DOI":"10.1109\/SP.2008.32"},{"key":"22_CR33","unstructured":"Comon-Lundh, H., Cortier, V.: How to prove security of communication protocols? a discussion on the soundness of formal models w.r.t. computational ones. In: Schwentick, T., D\u00fcrr, C. (eds.) 28th International Symposium on Theoretical Aspects of Computer Science, STACS 2011, 10\u201312 March 2011, Dortmund, Germany, vol. 9, LIPIcs, pp. 29\u201344. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2011)"},{"key":"22_CR34","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. 3467, pp. 294\u2013307. Springer, Heidelberg (2005)"},{"key":"22_CR35","doi-asserted-by":"crossref","unstructured":"Cortier, V., Degrieck, J., Delaune, S.: Analysing routing protocols: four nodes topologies are sufficient. In: Degano, P., Guttman, J.D. (eds.) [38], pp. 30\u201350","DOI":"10.1007\/978-3-642-28641-4_3"},{"issue":"1","key":"22_CR36","doi-asserted-by":"publisher","first-page":"89","DOI":"10.3233\/JCS-2012-0458","volume":"21","author":"V Cortier","year":"2013","unstructured":"Cortier, V., Smyth, B.: Attacking and fixing helios: an analysis of ballot secrecy. J. Comput. Secur. 21(1), 89\u2013148 (2013)","journal-title":"J. Comput. Secur."},{"key":"22_CR37","unstructured":"Cryptosense. Cryptosense web page. cryptosense.com"},{"key":"22_CR38","series-title":"Lecture Notes in Computer Science","volume-title":"Principles of Security and Trust","year":"2012","unstructured":"Degano, P., Guttman, J.D. (eds.): POST 2012. LNCS, vol. 7215. Springer, Heidelberg (2012)"},{"key":"22_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"523","DOI":"10.1007\/978-3-540-71209-1_41","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"SF Doghmi","year":"2007","unstructured":"Doghmi, S.F., Guttman, J.D., Thayer, F.J.: Searching for shapes in cryptographic protocols. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 523\u2013537. Springer, Heidelberg (2007)"},{"key":"22_CR40","doi-asserted-by":"crossref","unstructured":"Dolev, D., Yao, A, C-C.: On the security of public key protocols (extended abstract). In: 22nd Annual Symposium on Foundations of Computer Science, Nashville, Tennessee, USA, 28\u201330 October 1981, pp. 350\u2013357. IEEE Computer Society (1981)","DOI":"10.1109\/SFCS.1981.32"},{"key":"22_CR41","unstructured":"Ellison, C.M.: Ceremony design and analysis. IACR Cryptology ePrint Archive 2007:399 (2007)"},{"key":"22_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/978-3-642-38574-2_16","volume-title":"Automated Deduction \u2013 CADE-24","author":"S Erbatur","year":"2013","unstructured":"Erbatur, S., Escobar, S., Kapur, D., Liu, Z., Lynch, C.A., Meadows, C., Meseguer, J., Narendran, P., Santiago, S., Sasse, R.: Asymmetric unification: a new unification paradigm for cryptographic protocol analysis. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 231\u2013248. Springer, Heidelberg (2013)"},{"issue":"7\u20138","key":"22_CR43","doi-asserted-by":"publisher","first-page":"898","DOI":"10.1016\/j.jlap.2012.01.002","volume":"81","author":"S Escobar","year":"2012","unstructured":"Escobar, S., Sasse, R., Meseguer, J.: Folding variant narrowing and optimal variant termination. J. Log. Algebr. Program. 81(7\u20138), 898\u2013928 (2012)","journal-title":"J. Log. Algebr. Program."},{"issue":"3","key":"22_CR44","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1145\/2382448.2382452","volume":"15","author":"J Feigenbaum","year":"2012","unstructured":"Feigenbaum, J., Johnson, A., Syverson, P.F.: Probabilistic analysis of onion routing in a black-box model. ACM Trans. Inf. Syst. Secur. 15(3), 14 (2012)","journal-title":"ACM Trans. Inf. Syst. Secur."},{"key":"22_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-642-23082-0_2","volume-title":"Foundations of Security Analysis and Design VI","author":"R Focardi","year":"2011","unstructured":"Focardi, R., Luccio, F.L., Steel, G.: An introduction to security API analysis. In: Aldini, A., Gorrieri, R. (eds.) FOSAD 2011. LNCS, vol. 6858, pp. 35\u201365. Springer, Heidelberg (2011)"},{"issue":"2","key":"22_CR46","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1145\/293411.293443","volume":"42","author":"DM Goldschlag","year":"1999","unstructured":"Goldschlag, D.M., Reed, M.G., Syverson, P.F.: Onion routing. Commun. ACM 42(2), 39\u201341 (1999)","journal-title":"Commun. ACM"},{"key":"22_CR47","doi-asserted-by":"crossref","unstructured":"Gro\u00df, T., M\u00f6dersheim, s.: Vertical protocol composition. In: Proceedings of the 24th IEEE Computer Security Foundations Symposium, CSF 2011, Cernay-la-Ville, France, 27\u201329 June 2011, pp. 235\u2013250. IEEE Computer Society (2011)","DOI":"10.1109\/CSF.2011.23"},{"issue":"1","key":"22_CR48","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/s10623-013-9816-5","volume":"73","author":"B Groza","year":"2014","unstructured":"Groza, B., Warinschi, B.: Cryptographic puzzles and dos resilience, revisited. Des. Codes Crypt. 73(1), 177\u2013207 (2014)","journal-title":"Des. Codes Crypt."},{"key":"22_CR49","unstructured":"Halevi, S.: A plausible approach to computer-aided cryptographic proofs. IACR Cryptology ePrint Archive 2005:181 (2005)"},{"key":"22_CR50","unstructured":"Juels, A., Brainard, J.G.: Client puzzles: a cryptographic countermeasure against connection depletion attacks. In: Proceedings of the Network and Distributed System Security Symposium, NDSS 1999, San Diego, California, USA. The Internet Society (1999)"},{"key":"22_CR51","doi-asserted-by":"crossref","unstructured":"Kemmerer, R.A.: Using formal verification techniques to analyze encryption protocols. In: Proceedings of the 1987 IEEE Symposium on Security and Privacy, Oakland, California, USA, 27\u201329 April 1987, pp. 134\u2013139. IEEE Computer Society (1987)","DOI":"10.1109\/SP.1987.10005"},{"key":"22_CR52","unstructured":"Khader, D., Tang, Q., Ryan, P.Y.A.: Proving pr\u00eat \u00e0 voter receipt free using computational security models. In: 2013 Electronic Voting Technology Workshop\/Workshop on Trustworthy Elections, EVT\/WOTE 2013, Washington, D.C., USA, 12\u201313 August 2013. USENIX Association (2013)"},{"key":"22_CR53","doi-asserted-by":"crossref","unstructured":"K\u00fcrtz, K.O., K\u00fcsters, R., Wilke, T.: Selecting theories and nonce generation for recursive protocols. In: Ning, P., Atluri, V., Gligor, V.D., Mantel, H. (eds.) Proceedings of the 2007 ACM workshop on Formal methods in security engineering, FMSE 2007, Fairfax, VA, USA, 2 November 2007, pp. 61\u201370. ACM (2007)","DOI":"10.1145\/1314436.1314445"},{"key":"22_CR54","doi-asserted-by":"crossref","unstructured":"K\u00fcsters, R., Truderung, T.: An epistemic approach to coercion-resistance for electronic voting protocols. In: 30th IEEE Symposium on Security and Privacy (S&P 2009), 17\u201320 May 2009, Oakland, California, USA, pp. 251\u2013266. IEEE Computer Society (2009)","DOI":"10.1109\/SP.2009.13"},{"key":"22_CR55","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/978-3-642-17650-0_20","volume-title":"Information and Communications Security","author":"R K\u00fcsters","year":"2010","unstructured":"K\u00fcsters, R., Truderung, T., Vogt, A.: Proving coercion-resistance of scantegrity II. In: Soriano, M., Qing, S., L\u00f3pez, J. (eds.) ICICS 2010. LNCS, vol. 6476, pp. 281\u2013295. Springer, Heidelberg (2010)"},{"key":"22_CR56","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1007\/978-3-540-24749-4_34","volume-title":"STACS 2004","author":"R K\u00fcsters","year":"2004","unstructured":"K\u00fcsters, R., Wilke, T.: Automata-based analysis of recursive cryptographic protocols. In: Diekert, V., Habib, M. (eds.) STACS 2004. LNCS, vol. 2996, pp. 382\u2013393. Springer, Heidelberg (2004)"},{"key":"22_CR57","unstructured":"Lowe, G.: Analysing protocols subject to guessing attacks. In: WITS 2002 (2002)"},{"key":"22_CR58","doi-asserted-by":"crossref","unstructured":"Malozemoff, A.J., Katz, J., Green, M.D.: Automated analysis and synthesis of block-cipher modes of operation. In: IEEE 27th Computer Security Foundations Symposium, CSF 2014, Vienna, Austria, 19\u201322 July 2014, pp. 140\u2013152. IEEE (2014)","DOI":"10.1109\/CSF.2014.18"},{"issue":"1","key":"22_CR59","doi-asserted-by":"publisher","first-page":"55","DOI":"10.3233\/JCS-1996-4104","volume":"4","author":"UM Maurer","year":"1996","unstructured":"Maurer, U.M., Schmid, P.E.: A calculus for security bootstrapping in distributed systems. J. Comput. Secur. 4(1), 55\u201380 (1996)","journal-title":"J. Comput. Secur."},{"issue":"1","key":"22_CR60","doi-asserted-by":"publisher","first-page":"5","DOI":"10.3233\/JCS-1992-1102","volume":"1","author":"C Meadows","year":"1992","unstructured":"Meadows, C.: Applying formal methods to the analysis of a key management protocol. J. Comput. Secur. 1(1), 5\u201336 (1992)","journal-title":"J. Comput. Secur."},{"key":"22_CR61","doi-asserted-by":"crossref","unstructured":"Meadows, C.: Analysis of the internet key exchange protocol using the NRL protocol analyzer. In: 1999 IEEE Symposium on Security and Privacy, Oakland, California, USA, 9\u201312 May 1999, pp. 216\u2013231. IEEE Computer Society (1999)","DOI":"10.21236\/ADA465466"},{"issue":"1\/2","key":"22_CR62","doi-asserted-by":"publisher","first-page":"143","DOI":"10.3233\/JCS-2001-91-206","volume":"9","author":"C Meadows","year":"2001","unstructured":"Meadows, C.: A cost-based framework for analysis of denial of service networks. J. Comput. Secur. 9(1\/2), 143\u2013164 (2001)","journal-title":"J. Comput. Secur."},{"issue":"1","key":"22_CR63","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1109\/JSAC.2002.806125","volume":"21","author":"C Meadows","year":"2003","unstructured":"Meadows, C.: Formal methods for cryptographic protocol analysis: emerging issues and trends. IEEE J. Sel. Areas Commun. 21(1), 44\u201354 (2003)","journal-title":"IEEE J. Sel. Areas Commun."},{"key":"22_CR64","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/BFb0055477","volume-title":"Financial Cryptography","author":"C Meadows","year":"1998","unstructured":"Meadows, C., Syverson, P.F.: A formal specification of requirements for payment transactions in the SET protocol. In: Hirschfeld, R. (ed.) FC 1998. LNCS, vol. 1465, pp. 122\u2013140. Springer, Heidelberg (1998)"},{"key":"22_CR65","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)"},{"key":"22_CR66","unstructured":"Mitchell, J.C., Shmatikov, V., Stern, U.: Finite-state analysis of SSL 3.0. In: Rubin, A.D.: (ed.) Proceedings of the 7th USENIX Security Symposium, San Antonio, TX, USA, 26\u201329 January 1998. USENIX Association (1998)"},{"key":"22_CR67","doi-asserted-by":"crossref","unstructured":"M\u00f6dersheim, S., Vigan\u00f2, L.: Sufficient conditions for vertical composition of security protocols. In: Moriai, S., Jaeger, T., Sakurai, K. (eds.) 9th ACM Symposium on Information, Computer and Communications Security, ASIA CCS 2014, Kyoto, Japan, 03\u201306 June 2014, pp. 435\u2013446. ACM (2014)","DOI":"10.1145\/2590296.2590330"},{"key":"22_CR68","unstructured":"Nakamoto, S.: Bitcoin: a peer-to-peer electronic cash system (2008). https:\/\/bitcoin.org"},{"issue":"6","key":"22_CR69","doi-asserted-by":"publisher","first-page":"781","DOI":"10.3233\/JCS-130471","volume":"21","author":"M Paiola","year":"2013","unstructured":"Paiola, M., Blanchet, B.: Verification of security protocols with lists: From length one to unbounded length. J. Comput. Secur. 21(6), 781\u2013816 (2013)","journal-title":"J. Comput. Secur."},{"key":"22_CR70","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1007\/978-3-642-36213-2_27","volume-title":"Security Protocols XVII","author":"D Pavlovic","year":"2013","unstructured":"Pavlovic, D., Meadows, C.: Deriving ephemeral authentication using channel axioms. In: Christianson, B., Malcolm, J.A., Maty\u00e1\u0161, V., Roe, M. (eds.) Security Protocols 2009. LNCS, vol. 7028, pp. 240\u2013261. Springer, Heidelberg (2013)"},{"key":"22_CR71","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1007\/978-3-642-28073-3_2","volume-title":"Distributed Computing and Internet Technology","author":"D Pavlovic","year":"2012","unstructured":"Pavlovic, D., Meadows, C.: Actor-network procedures. In: Ramanujam, R., Ramaswamy, S. (eds.) ICDCIT 2012. LNCS, vol. 7154, pp. 7\u201326. Springer, Heidelberg (2012)"},{"issue":"1","key":"22_CR72","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1145\/290163.290168","volume":"1","author":"MK Reiter","year":"1998","unstructured":"Reiter, M.K., Rubin, A.D.: Crowds: anonymity for web transactions. ACM Trans. Inf. Syst. Secur. 1(1), 66\u201392 (1998)","journal-title":"ACM Trans. Inf. Syst. Secur."},{"key":"22_CR73","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1007\/978-3-540-78663-4_21","volume-title":"Trustworthy Global Computing","author":"A Roy","year":"2008","unstructured":"Roy, A., Datta, A., Mitchell, J.C.: Formal proofs of cryptographic security of diffie-hellman-based protocols. In: Barthe, G., Fournet, C. (eds.) TGC 2007. LNCS, vol. 4912, pp. 312\u2013329. Springer, Heidelberg (2008)"},{"key":"22_CR74","doi-asserted-by":"crossref","unstructured":"Rusinowitch, M., Turuani, M.: Protocol insecurity with finite number of sessions is np-complete. In: 14th IEEE Computer Security Foundations Workshop (CSFW-14 2001), 11\u201313 June 2001, Cape Breton, Nova Scotia, Canada, p. 174. IEEE Computer Society (2001)","DOI":"10.1109\/CSFW.2001.930145"},{"issue":"4","key":"22_CR75","doi-asserted-by":"publisher","first-page":"662","DOI":"10.1109\/TIFS.2009.2033233","volume":"4","author":"PYA Ryan","year":"2009","unstructured":"Ryan, P.Y.A., Bismark, D., Heather, J., Schneider, S., Xia, Z.: Pr\u00eat \u00e0 voter: a voter-verifiable voting system. IEEE Trans. Inf. Forensics Secur. 4(4), 662\u2013673 (2009)","journal-title":"IEEE Trans. Inf. Forensics Secur."},{"key":"22_CR76","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"162","DOI":"10.1007\/978-3-319-11851-2_11","volume-title":"Security and Trust Management","author":"S Santiago","year":"2014","unstructured":"Santiago, S., Escobar, S., Meadows, C., Meseguer, J.: A formal definition of protocol indistinguishability and its verification using Maude-NPA. In: Mauw, S., Jensen, C.D. (eds.) STM 2014. LNCS, vol. 8743, pp. 162\u2013177. Springer, Heidelberg (2014)"},{"issue":"2","key":"22_CR77","first-page":"103","volume":"19","author":"S Schneider","year":"2014","unstructured":"Schneider, S., Teague, V., Culnane, C., Heather, J.: Special section on vote-id 2013. J. Inf. Sec. Appl. 19(2), 103\u2013104 (2014)","journal-title":"J. Inf. Sec. Appl."},{"key":"22_CR78","unstructured":"SET Secure Electronic Transactions LLC. SET Secure Electronic Transactions, Version 1.0 (2002). http:\/\/www.exelana.com\/set\/"},{"key":"22_CR79","unstructured":"Shoup, V.: Sequences of games: a tool for taming complexity in security proofs. IACR Cryptology ePrint Archive 2004:332 (2004)"},{"issue":"1","key":"22_CR80","doi-asserted-by":"publisher","first-page":"191","DOI":"10.3233\/JCS-1999-72-304","volume":"7","author":"JF Thayer","year":"1999","unstructured":"Thayer, J.F., Herzog, J.C., Guttman, J.D.: Strand spaces: proving security protocols correct. J. Comput. Secur. 7(1), 191\u2013230 (1999)","journal-title":"J. Comput. Secur."},{"key":"22_CR81","unstructured":"Tor Project. The Tor Project: Anonymity Online. https:\/\/www.torproject.org\/"},{"key":"22_CR82","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/11539452_19","volume-title":"CONCUR 2005 \u2013 Concurrency Theory","author":"T Truderung","year":"2005","unstructured":"Truderung, T.: Selecting theories and recursive protocols. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 217\u2013232. Springer, Heidelberg (2005)"},{"key":"22_CR83","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/11535218_19","volume-title":"Advances in Cryptology \u2013 CRYPTO 2005","author":"S Vaudenay","year":"2005","unstructured":"Vaudenay, S.: Secure communications over insecure channels based on short authenticated strings. In: Shoup, V. (ed.) CRYPTO 2005. LNCS, vol. 3621, pp. 309\u2013326. Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","Logic, Rewriting, and Concurrency"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-23165-5_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T04:40:09Z","timestamp":1748580009000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-23165-5_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319231648","9783319231655"],"references-count":83,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-23165-5_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"27 August 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}