{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T18:05:45Z","timestamp":1743098745142,"version":"3.40.3"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319708478"},{"type":"electronic","value":"9783319708485"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-70848-5_10","type":"book-chapter","created":{"date-parts":[[2017,11,10]],"date-time":"2017-11-10T10:43:26Z","timestamp":1510310606000},"page":"142-158","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Formal Analysis of the Information Leakage of the DC-Nets and Crowds Anonymity Protocols"],"prefix":"10.1007","author":[{"given":"Arthur","family":"Am\u00e9rico","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Artur","family":"Vaz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"M\u00e1rio S.","family":"Alvim","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"S\u00e9rgio V. A.","family":"Campos","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Annabelle","family":"McIver","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,11,11]]},"reference":[{"key":"10_CR1","unstructured":"PRISM: A Probabilistic Symbolic Model Checker. www.prismmodelchecker.org\/"},{"key":"10_CR2","unstructured":"http:\/\/homepages.dcc.ufmg.br\/~arturvaz\/sbmf\/"},{"key":"10_CR3","doi-asserted-by":"crossref","unstructured":"Alvim, M.S., Chatzikokolakis, K., McIver, A., Morgan, C., Palamidessi, C., Smith, G.: Additive and multiplicative notions of leakage, and their capacities. In: Proceedings of CSF, pp. 308\u2013322. IEEE (2014)","DOI":"10.1109\/CSF.2014.29"},{"key":"10_CR4","doi-asserted-by":"crossref","unstructured":"Alvim, M.S., Chatzikokolakis, K., McIver, A., Morgan, C., Palamidessi, C., Smith, G.: Axioms for information leakage. In: Proceedings of CSF, pp. 77\u201392 (2016)","DOI":"10.1109\/CSF.2016.13"},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"Alvim, M.S., Chatzikokolakis, K., Palamidessi, C., Smith, G.: Measuring information leakage using generalized gain functions. In: Proceedings of CSF, pp. 265\u2013279 (2012)","DOI":"10.1109\/CSF.2012.26"},{"key":"10_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1007\/978-3-642-12002-2_32","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"ME Andr\u00e9s","year":"2010","unstructured":"Andr\u00e9s, M.E., Palamidessi, C., Rossum, P., Smith, G.: Computing the leakage of information-hiding systems. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 373\u2013389. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-12002-2_32"},{"key":"10_CR7","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. The MIT Press (2008)"},{"issue":"4:5","key":"10_CR8","first-page":"1","volume":"11","author":"M Boreale","year":"2015","unstructured":"Boreale, M., Pampaloni, F.: Quantitative information flow under generic leakage functions and adaptive adversaries. Logical Methods Comput. Sci. 11(4:5), 1\u201331 (2015)","journal-title":"Logical Methods Comput. Sci."},{"key":"10_CR9","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1016\/j.entcs.2009.07.085","volume":"249","author":"C Braun","year":"2009","unstructured":"Braun, C., Chatzikokolakis, K., Palamidessi, C.: Quantitative notions of leakage for one-try attacks. Electron. Theoret. Comput. Sci. 249, 75\u201391 (2009)","journal-title":"Electron. Theoret. Comput. Sci."},{"key":"10_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"390","DOI":"10.1007\/978-3-642-12002-2_33","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K Chatzikokolakis","year":"2010","unstructured":"Chatzikokolakis, K., Chothia, T., Guha, A.: Statistical measurement of information leakage. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 390\u2013404. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-12002-2_33"},{"issue":"5","key":"10_CR11","doi-asserted-by":"crossref","first-page":"531","DOI":"10.3233\/JCS-2008-0333","volume":"16","author":"K Chatzikokolakis","year":"2008","unstructured":"Chatzikokolakis, K., Palamidessi, C., Panangaden, P.: On the Bayes risk in information-hiding protocols. J. Comp. Security 16(5), 531\u2013571 (2008)","journal-title":"J. Comp. Security"},{"issue":"1","key":"10_CR12","doi-asserted-by":"crossref","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. Cryptology 1(1), 65\u201375 (1988)","journal-title":"J. Cryptology"},{"key":"10_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/978-3-319-11212-1_13","volume-title":"Computer Security - ESORICS 2014","author":"T Chothia","year":"2014","unstructured":"Chothia, T., Kawamoto, Y., Novakovic, C.: LeakWatch: estimating information leakage from Java Programs. In: Kuty\u0142owski, M., Vaidya, J. (eds.) ESORICS 2014. LNCS, vol. 8713, pp. 219\u2013236. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11212-1_13"},{"key":"10_CR14","doi-asserted-by":"crossref","unstructured":"Chothia, T., Kawamoto, Y., Novakovic, C., Parker, D.: Probabilistic point-to-point information leakage. In: Proceedings of CSF, pp. 193\u2013205. IEEE Computer Society (2013)","DOI":"10.1109\/CSF.2013.20"},{"issue":"2","key":"10_CR15","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1093\/logcom\/exi009","volume":"18","author":"D Clark","year":"2005","unstructured":"Clark, D., Hunt, S., Malacaria, P.: Quantitative information flow, relations and polymorphic types. J. Logic Comput. 18(2), 181\u2013199 (2005)","journal-title":"J. Logic Comput."},{"issue":"3","key":"10_CR16","doi-asserted-by":"crossref","first-page":"321","DOI":"10.3233\/JCS-2007-15302","volume":"15","author":"D Clark","year":"2007","unstructured":"Clark, D., Hunt, S., Malacaria, P.: A static analysis for quantifying information flow in a simple imperative language. J. Comp. Security 15(3), 321\u2013371 (2007)","journal-title":"J. Comp. Security"},{"key":"10_CR17","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1016\/j.ic.2013.03.005","volume":"226","author":"B Espinoza","year":"2013","unstructured":"Espinoza, B., Smith, G.: Min-entropy as a resource. Inf. Comp. 226, 57\u201375 (2013)","journal-title":"Inf. Comp."},{"issue":"5","key":"10_CR18","doi-asserted-by":"crossref","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H Hansson","year":"1994","unstructured":"Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects Comput. 6(5), 512\u2013535 (1994)","journal-title":"Formal Aspects Comput."},{"key":"10_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-642-41071-0_10","volume-title":"Formal Methods: Foundations and Applications","author":"G Helali","year":"2013","unstructured":"Helali, G., Hasan, O., Tahar, S.: Formal analysis of information flow using min-entropy and belief min-entropy. In: Iyoda, J., de Leonardo, M. (eds.) SBMF 2013. LNCS, vol. 8195, pp. 131\u2013146. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-41071-0_10"},{"key":"10_CR20","doi-asserted-by":"crossref","unstructured":"Heusser, J., Malacaria, P.: Quantifying information leaks in software. In: Proceedings of ACSAC, pp. 261\u2013269. ACM (2010)","DOI":"10.1145\/1920261.1920300"},{"key":"10_CR21","doi-asserted-by":"crossref","unstructured":"H\u00f6lzl, J., Nipkow, T.: Interactive verification of Markov Chains: two distributed protocol case studies, p. 103 (2012)","DOI":"10.4204\/EPTCS.103.2"},{"key":"10_CR22","doi-asserted-by":"crossref","unstructured":"K\u00f6pf, B., Basin, D.A.: An information-theoretic model for adaptive side-channel attacks. In: Proceedings of CCS, pp. 286\u2013296. ACM (2007)","DOI":"10.1145\/1315245.1315282"},{"key":"10_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"564","DOI":"10.1007\/978-3-642-31424-7_40","volume-title":"Computer Aided Verification","author":"B K\u00f6pf","year":"2012","unstructured":"K\u00f6pf, B., Mauborgne, L., Ochoa, M.: Automatic quantification of cache side-channels. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 564\u2013580. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_40"},{"key":"10_CR24","doi-asserted-by":"crossref","unstructured":"K\u00f6pf, B., Rybalchenko, A.: Approximation and randomization for quantitative information-flow analysis. In: Proceedings of CSF, pp. 3\u201314. IEEE (2010)","DOI":"10.1109\/CSF.2010.8"},{"key":"10_CR25","doi-asserted-by":"crossref","unstructured":"Massey, J.L.: Guessing and entropy. In: Proceedings of the IEEE International Symposium on Information Theory, p. 204. IEEE (1994)","DOI":"10.1109\/ISIT.1994.394764"},{"key":"10_CR26","doi-asserted-by":"crossref","unstructured":"McCamant, S., Ernst, M.D.: Quantitative information flow as network flow capacity. In: Proceedings of SIGPLAN, Tucson, AZ, USA, 9\u201311 June 2008, pp. 193\u2013205 (2008)","DOI":"10.1145\/1375581.1375606"},{"key":"10_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-642-14162-1_19","volume-title":"Automata, Languages and Programming","author":"A McIver","year":"2010","unstructured":"McIver, A., Meinicke, L., Morgan, C.: Compositional closure for Bayes risk in probabilistic noninterference. In: Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf der Heide, F., Spirakis, P.G. (eds.) ICALP 2010. LNCS, vol. 6199, pp. 223\u2013235. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14162-1_19"},{"key":"10_CR28","doi-asserted-by":"crossref","unstructured":"McIver, A., Morgan, C., Rabehaja, T.M.: Abstract hidden Markov Models: a monadic account of quantitative information flow. In: Proceedings of LICS, pp. 597\u2013608 (2015)","DOI":"10.1109\/LICS.2015.61"},{"key":"10_CR29","unstructured":"Morgan, C.: A Haskell program to compute hyper distributions for measuring information leakage (2017). http:\/\/www.cse.unsw.edu.au\/~carrollm\/Hypers170731.zip"},{"key":"10_CR30","unstructured":"Novakovic, C.: Computing and estimating information leakage with a quantitative point-to-point information flow model. PhD thesis, Birmingham University, UK (2014)"},{"key":"10_CR31","unstructured":"Parker, D.: Implementation of symbolic model checking for probabilistic systems. PhD thesis, University of Birmingham (2002)"},{"key":"10_CR32","doi-asserted-by":"crossref","unstructured":"Phan, Q., Malacaria, P., Pasareanu, C.S., d\u2019Amorim, M.: Quantifying information leaks using reliability analysis. In: Proceedings of SPIN, pp. 105\u2013108 (2014)","DOI":"10.1145\/2632362.2632367"},{"issue":"1","key":"10_CR33","doi-asserted-by":"crossref","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. Inform. Syst. Secur. 1(1), 66\u201392 (1998)","journal-title":"ACM Trans. Inform. Syst. Secur."},{"issue":"379\u2013423","key":"10_CR34","first-page":"625","volume":"27","author":"CE Shannon","year":"1948","unstructured":"Shannon, C.E.: A mathematical theory of communication. Bell Syst. Tech. J. 27(379\u2013423), 625\u201356 (1948)","journal-title":"Bell Syst. Tech. J."},{"key":"10_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1007\/978-3-642-00596-1_21","volume-title":"Foundations of Software Science and Computational Structures","author":"G Smith","year":"2009","unstructured":"Smith, G.: On the foundations of quantitative information flow. In: Alfaro, L. (ed.) FoSSaCS 2009. LNCS, vol. 5504, pp. 288\u2013302. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-00596-1_21"},{"key":"10_CR36","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1016\/j.tcs.2013.07.031","volume":"538","author":"H Yasuoka","year":"2014","unstructured":"Yasuoka, H., Terauchi, T.: Quantitative information flow as safety and liveness hyperproperties. Theor. Comp. Sci. 538, 167\u2013182 (2014)","journal-title":"Theor. Comp. Sci."}],"container-title":["Lecture Notes in Computer Science","Formal Methods: Foundations and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-70848-5_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,5]],"date-time":"2019-10-05T20:37:03Z","timestamp":1570307823000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-70848-5_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319708478","9783319708485"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-70848-5_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}