{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:17:24Z","timestamp":1762460244157,"version":"3.40.3"},"publisher-location":"Cham","reference-count":49,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030620769"},{"type":"electronic","value":"9783030620776"}],"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_12","type":"book-chapter","created":{"date-parts":[[2020,10,28]],"date-time":"2020-10-28T11:25:37Z","timestamp":1603884337000},"page":"167-183","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Modelchecking Safety Properties in Randomized Security Protocols"],"prefix":"10.1007","author":[{"given":"Matthew S.","family":"Bauer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rohit","family":"Chadha","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mahesh","family":"Viswanathan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,10,28]]},"reference":[{"key":"12_CR1","unstructured":"Graphviz. \n                    https:\/\/www.graphviz.org\/"},{"key":"12_CR2","doi-asserted-by":"crossref","unstructured":"Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: ACM SIGPLAN Notices, vol. 36, pp. 104\u2013115. ACM (2001)","DOI":"10.1145\/373243.360213"},{"issue":"1","key":"12_CR3","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. Theor. Comput. Sci. 367(1), 2\u201332 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"12_CR4","unstructured":"Adida, B.: Helios: web-based open-audit voting. In: USENIX Security Symposium, vol. 17, pp. 335\u2013348 (2008)"},{"issue":"1","key":"12_CR5","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10207-007-0041-y","volume":"7","author":"A Armando","year":"2008","unstructured":"Armando, A., Compagna, L.: SAT-based model-checking for security protocols analysis. Int. J. Inf. Secur. 7(1), 3\u201332 (2008)","journal-title":"Int. J. Inf. Secur."},{"key":"12_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"350","DOI":"10.1007\/978-3-319-98989-1_18","volume-title":"Computer Security","author":"G Bana","year":"2018","unstructured":"Bana, G., Chadha, R., Eeralla, A.K.: Formal analysis of vote privacy using computationally complete symbolic attacker. In: Lopez, J., Zhou, J., Soriano, M. (eds.) ESORICS 2018. LNCS, vol. 11099, pp. 350\u2013372. Springer, Cham (2018). \n                    https:\/\/doi.org\/10.1007\/978-3-319-98989-1_18"},{"key":"12_CR7","unstructured":"Bauer, M.S.: Analysis of randomized security protocols. Ph.D. thesis, University of Illinois at Urbana-Champaign (2018)"},{"key":"12_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/978-3-319-96142-2_10","volume-title":"Computer Aided Verification","author":"MS Bauer","year":"2018","unstructured":"Bauer, M.S., Chadha, R., Prasad Sistla, A., Viswanathan, M.: Model checking indistinguishability of randomized security protocols. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 117\u2013135. Springer, Cham (2018). \n                    https:\/\/doi.org\/10.1007\/978-3-319-96142-2_10"},{"key":"12_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/978-3-662-49635-0_10","volume-title":"Principles of Security and Trust","author":"MS Bauer","year":"2016","unstructured":"Bauer, M.S., Chadha, R., Viswanathan, M.: Composing protocols with randomized actions. In: Piessens, F., Vigan\u00f2, L. (eds.) POST 2016. LNCS, vol. 9635, pp. 189\u2013210. Springer, Heidelberg (2016). \n                    https:\/\/doi.org\/10.1007\/978-3-662-49635-0_10"},{"issue":"1","key":"12_CR10","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1109\/18.50372","volume":"36","author":"M Ben-Or","year":"1990","unstructured":"Ben-Or, M., Goldreich, O., Micali, S., Rivest, R.L.: A fair protocol for signing contracts. IEEE Trans. Inf. Theory 36(1), 40\u201346 (1990)","journal-title":"IEEE Trans. Inf. Theory"},{"issue":"1","key":"12_CR11","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. Algebr. Program. 75(1), 3\u201351 (2008)","journal-title":"J. Log. Algebr. Program."},{"key":"12_CR12","unstructured":"Braziunas, D.: POMDP Solution Methods. University of Toronto (2003)"},{"key":"12_CR13","unstructured":"Canetti, R., et al.: Task-structured probabilistic I\/O automata. In: Discrete Event Systems (2006)"},{"key":"12_CR14","unstructured":"Cassandra, A.R.: A survey of POMDP applications. In: Working notes of AAAI 1998 fall Symposium on Planning with Partially Observable Markov Decision Processes, vol. 1724 (1998)"},{"issue":"4","key":"12_CR15","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 protocol. ACM Trans. Comput. Log. 17(4), 1\u201332 (2016)","journal-title":"ACM Trans. Comput. Log."},{"key":"12_CR16","unstructured":"Chadha, R., Sistla, A.P., Viswanathan, M.: Model checking concurrent programs with nondeterminism and randomization. In: Foundations of Software Technology and Theoretical Computer Science, pp. 364\u2013375 (2010)"},{"key":"12_CR17","doi-asserted-by":"crossref","unstructured":"Chadha, R., Sistla, A.P., Viswanathan, M.: Verification of randomized security protocols. In: Logic in Computer Science, pp. 1\u201312. IEEE (2017)","DOI":"10.1109\/LICS.2017.8005126"},{"issue":"5","key":"12_CR18","doi-asserted-by":"publisher","first-page":"878","DOI":"10.1016\/j.jcss.2016.02.009","volume":"82","author":"K Chatterjee","year":"2016","unstructured":"Chatterjee, K., Chmel\u00edk, M., Tracol, M.: What is decidable about partially observable Markov decision processes with omega-regular objectives. J. Comput. Syst. Sci. 82(5), 878\u2013911 (2016)","journal-title":"J. Comput. Syst. Sci."},{"key":"12_CR19","doi-asserted-by":"crossref","unstructured":"Chatzikokolakis, K., Palamidessi, C.: Making random choices invisible to the scheduler. Information and Computation (2010, to appear)","DOI":"10.1016\/j.ic.2009.06.006"},{"issue":"1","key":"12_CR20","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/BF00206326","volume":"1","author":"D Chaum","year":"1988","unstructured":"Chaum, D.: The dining cryptographers problem: unconditional sender and recipient untraceability. J. Cryptol. 1(1), 65\u201375 (1988)","journal-title":"J. Cryptol."},{"key":"12_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1007\/11555827_8","volume-title":"Computer Security \u2013 ESORICS 2005","author":"D Chaum","year":"2005","unstructured":"Chaum, D., Ryan, P.Y.A., Schneider, S.: A practical voter-verifiable election scheme. In: di Vimercati, S.C., Syverson, P., Gollmann, D. (eds.) ESORICS 2005. LNCS, vol. 3679, pp. 118\u2013139. Springer, Heidelberg (2005). \n                    https:\/\/doi.org\/10.1007\/11555827_8"},{"issue":"2","key":"12_CR22","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1145\/358549.358563","volume":"24","author":"DL Chaum","year":"1981","unstructured":"Chaum, D.L.: Untraceable electronic mail, return addresses, and digital pseudonyms. Commun. ACM 24(2), 84\u201390 (1981)","journal-title":"Commun. ACM"},{"key":"12_CR23","unstructured":"Cheung, L.: Reconciling nondeterministic and probabilistic choices. Ph.D. thesis, Radboud University of Nijmegen (2006)"},{"issue":"2","key":"12_CR24","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1016\/S0304-3975(01)00359-0","volume":"285","author":"M Clavel","year":"2002","unstructured":"Clavel, M., et al.: Maude: Specification and programming in rewriting logic. Theor. Comput. Sci. 285(2), 187\u2013243 (2002)","journal-title":"Theor. Comput. Sci."},{"key":"12_CR25","doi-asserted-by":"crossref","unstructured":"Cortier, V., Delaune, S.: A method for proving observational equivalence. In: Computer Security Foundations, pp. 266\u2013276 (2009)","DOI":"10.1109\/CSF.2009.9"},{"key":"12_CR26","unstructured":"de Alfaro, L.: The verification of probabilistic systems under memoryless partial-information policies is hard. Technical report (1999)"},{"key":"12_CR27","doi-asserted-by":"publisher","unstructured":"Dehnert, C., Junges, S., Katoen, J.P., Volk, M.: A storm is coming: a modern probabilistic model checker. In: Majumdar, R., Kun\u010dak, V. (eds.) Computer Aided Verification CAV 2017. LNCS, vol. 10427, pp. 592-600. Springer, Cham (2017). \n                    https:\/\/doi.org\/10.1007\/978-3-319-63390-9_31","DOI":"10.1007\/978-3-319-63390-9_31"},{"issue":"4","key":"12_CR28","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(4), 435\u2013487 (2009)","journal-title":"J. Comput. Secur."},{"key":"12_CR29","doi-asserted-by":"crossref","unstructured":"Dingledine, R., Mathewson, N., Syverson, P.: Tor: the second-generation onion router. Technical report, DTIC Document (2004)","DOI":"10.21236\/ADA465464"},{"key":"12_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-03829-7_1","volume-title":"Foundations of Security Analysis and Design V","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-2009. LNCS, vol. 5705, pp. 1\u201350. Springer, Heidelberg (2009). \n                    https:\/\/doi.org\/10.1007\/978-3-642-03829-7_1"},{"issue":"6","key":"12_CR31","doi-asserted-by":"publisher","first-page":"637","DOI":"10.1145\/3812.3818","volume":"28","author":"S Even","year":"1985","unstructured":"Even, S., Goldreich, O., Lempel, A.: A randomized protocol for signing contracts. Commun. ACM 28(6), 637\u2013647 (1985)","journal-title":"Commun. ACM"},{"key":"12_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 \u2014 AUSCRYPT \u201992","author":"A Fujioka","year":"1993","unstructured":"Fujioka, A., Okamoto, T., Ohta, K.: A practical secret voting scheme for large scale elections. In: Seberry, J., Zheng, Y. (eds.) AUSCRYPT 1992. LNCS, vol. 718, pp. 244\u2013251. Springer, Heidelberg (1993). \n                    https:\/\/doi.org\/10.1007\/3-540-57220-1_66"},{"key":"12_CR33","unstructured":"Garcia, F.D., Van Rossum, P., Sokolova, A.: Probabilistic anonymity and admissible schedulers. arXiv preprint \n                    arXiv:0706.1019\n                    \n                   (2007)"},{"key":"12_CR34","doi-asserted-by":"crossref","unstructured":"Goldschlag, D.M., Reed, M.G., Syverson, P.F.: Hiding routing information. In: Workshop on Information Hiding, pp. 137\u2013150 (1996)","DOI":"10.1007\/3-540-61996-8_37"},{"key":"12_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"456","DOI":"10.1007\/978-3-540-24676-3_27","volume-title":"Advances in Cryptology - EUROCRYPT 2004","author":"P Golle","year":"2004","unstructured":"Golle, P., Juels, A.: Dining cryptographers revisited. In: Cachin, C., Camenisch, J.L. (eds.) EUROCRYPT 2004. LNCS, vol. 3027, pp. 456\u2013473. Springer, Heidelberg (2004). \n                    https:\/\/doi.org\/10.1007\/978-3-540-24676-3_27"},{"key":"12_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-3-540-76637-7_12","volume-title":"Programming Languages and Systems","author":"J Goubault-Larrecq","year":"2007","unstructured":"Goubault-Larrecq, J., Palamidessi, C., Troina, A.: A probabilistic applied pi\u2013calculus. In: Shao, Z. (ed.) APLAS 2007. LNCS, vol. 4807, pp. 175\u2013190. Springer, Heidelberg (2007). \n                    https:\/\/doi.org\/10.1007\/978-3-540-76637-7_12"},{"key":"12_CR37","unstructured":"Gunter, C.A., Khanna, S., Tan, K., Venkatesh, S.S.: DoS protection for reliably authenticated broadcast. In: Network and Distributed System Security (2004)"},{"key":"12_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"186","DOI":"10.1007\/978-3-540-31987-0_14","volume-title":"Programming Languages and Systems","author":"S Kremer","year":"2005","unstructured":"Kremer, S., Ryan, M.: Analysis of an electronic voting protocol in the applied pi calculus. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 186\u2013200. Springer, Heidelberg (2005). \n                    https:\/\/doi.org\/10.1007\/978-3-540-31987-0_14"},{"key":"12_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585\u2013591. Springer, Heidelberg (2011). \n                    https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47"},{"issue":"3","key":"12_CR40","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/s11241-017-9269-4","volume":"53","author":"G Norman","year":"2017","unstructured":"Norman, G., Parker, D., Zou, X.: Verification and control of partially observable probabilistic systems. Real-Time Syst. 53(3), 354\u2013402 (2017). \n                    https:\/\/doi.org\/10.1007\/s11241-017-9269-4","journal-title":"Real-Time Syst."},{"issue":"1","key":"12_CR41","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."},{"issue":"4","key":"12_CR42","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":"12_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-319-66402-6_12","volume-title":"Computer Security \u2013 ESORICS 2017","author":"MS Bauer","year":"2017","unstructured":"Bauer, M.S., Chadha, R., Viswanathan, M.: Modular verification of protocol equivalence in the presence of randomness. In: Foley, S.N., Gollmann, D., Snekkenes, E. (eds.) ESORICS 2017. LNCS, vol. 10492, pp. 187\u2013205. Springer, Cham (2017). \n                    https:\/\/doi.org\/10.1007\/978-3-319-66402-6_12"},{"issue":"3","key":"12_CR44","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1109\/MSP.2008.56","volume":"6","author":"AO Santin","year":"2008","unstructured":"Santin, A.O., Costa, R.G., Maziero, C.A.: A three-ballot-based secure electronic voting system. Secur. Priv. 6(3), 14\u201321 (2008)","journal-title":"Secur. Priv."},{"key":"12_CR45","doi-asserted-by":"crossref","unstructured":"Schmidt, B., Meier, S., Cremers, C., Basin, D.: Automated analysis of Diffie-Hellman protocols and advanced security properties. In: Computer Security Foundations, pp. 78\u201394 (2012)","DOI":"10.1109\/CSF.2012.25"},{"key":"12_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/3-540-36415-3_3","volume-title":"Information Hiding","author":"A Serjantov","year":"2003","unstructured":"Serjantov, A., Dingledine, R., Syverson, P.: From a trickle to a flood: active attacks on several mix types. In: Petitcolas, F.A.P. (ed.) IH 2002. LNCS, vol. 2578, pp. 36\u201352. Springer, Heidelberg (2003). \n                    https:\/\/doi.org\/10.1007\/3-540-36415-3_3"},{"key":"12_CR47","series-title":"IFIP \u2014 The International Federation for Information Processing","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/978-0-387-35691-4_41","volume-title":"Security and Privacy in the Age of Uncertainty","author":"A Serjantov","year":"2003","unstructured":"Serjantov, A., Newman, R.E.: On the anonymity of timed pool mixes. In: Gritzalis, D., De Capitani di Vimercati, S., Samarati, P., Katsikas, S. (eds.) SEC 2003. ITIFIP, vol. 122, pp. 427\u2013434. Springer, Boston, MA (2003). \n                    https:\/\/doi.org\/10.1007\/978-0-387-35691-4_41"},{"key":"12_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/978-3-540-39650-5_7","volume-title":"Computer Security \u2013 ESORICS 2003","author":"A Serjantov","year":"2003","unstructured":"Serjantov, A., Sewell, P.: Passive attack analysis for connection-based anonymity systems. In: Snekkenes, E., Gollmann, D. (eds.) ESORICS 2003. LNCS, vol. 2808, pp. 116\u2013131. Springer, Heidelberg (2003). \n                    https:\/\/doi.org\/10.1007\/978-3-540-39650-5_7"},{"key":"12_CR49","unstructured":"Shmatikov, V.: Probabilistic analysis of anonymity. In: Computer Security Foundations, pp. 119\u2013128. IEEE (2002)"}],"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_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,10,28]],"date-time":"2020-10-28T22:03:08Z","timestamp":1603922588000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-62077-6_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030620769","9783030620776"],"references-count":49,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-62077-6_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"28 October 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}