{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:48:58Z","timestamp":1740098938778,"version":"3.37.3"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319694825"},{"type":"electronic","value":"9783319694832"}],"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":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-69483-2_17","type":"book-chapter","created":{"date-parts":[[2017,10,16]],"date-time":"2017-10-16T11:34:48Z","timestamp":1508153688000},"page":"283-299","source":"Crossref","is-referenced-by-count":0,"title":["Formal Analysis of Information Flow in HOL"],"prefix":"10.1007","author":[{"given":"Ghassen","family":"Helali","sequence":"first","affiliation":[]},{"given":"Sofi\u00e8ne","family":"Tahar","sequence":"additional","affiliation":[]},{"given":"Osman","family":"Hasan","sequence":"additional","affiliation":[]},{"given":"Tsvetan","family":"Dunchev","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,10,17]]},"reference":[{"key":"17_CR1","unstructured":"HOL4, hol.sourceforge.net (2017)"},{"key":"17_CR2","doi-asserted-by":"crossref","unstructured":"Alvim, M.S., Chatzikokolakis, K., Palamidessi, C., Smith, G.: Measuring information leakage using generalized gain functions. In: IEEE Symposium on Computer Security Foundations, pp. 265\u2013279 (2012)","DOI":"10.1109\/CSF.2012.26"},{"issue":"1","key":"17_CR3","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1016\/S0165-0114(01)00245-7","volume":"132","author":"S Andrea","year":"2002","unstructured":"Andrea, S.: Possibilistic information theory: a coding theoretic approach. Fuzzy Sets Syst. 132(1), 11\u201332 (2002)","journal-title":"Fuzzy Sets Syst."},{"issue":"5\u20136","key":"17_CR4","doi-asserted-by":"crossref","first-page":"432","DOI":"10.26421\/QIC12.5-6-4","volume":"12","author":"NJ Beaudry","year":"2012","unstructured":"Beaudry, N.J., Renner, R.: An intuitive proof of the data processing inequality. Quantum Inform. Comput. 12(5\u20136), 432\u2013441 (2012)","journal-title":"Quantum Inform. Comput."},{"key":"17_CR5","unstructured":"Chung, K.L.: Markov Chains with Stationary Transition Probabilities (1967)"},{"key":"17_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/3-540-44702-4_4","volume-title":"Designing Privacy Enhancing Technologies","author":"I Clarke","year":"2001","unstructured":"Clarke, I., Sandberg, O., Wiley, B., Hong, T.W.: Freenet: a distributed anonymous information storage and retrieval system. In: Federrath, H. (ed.) Designing Privacy Enhancing Technologies. LNCS, vol. 2009, pp. 46\u201366. Springer, Heidelberg (2001). doi: 10.1007\/3-540-44702-4_4"},{"key":"17_CR7","doi-asserted-by":"crossref","unstructured":"Clarkson, M.R., Chong, S., Myers, A.C.: Civitas: toward a secure voting system. In: IEEE Symposium on Security and Privacy, pp. 354\u2013368. IEEE Computer Society (2008)","DOI":"10.1109\/SP.2008.32"},{"key":"17_CR8","unstructured":"Coble, A.R.: Anonymity, Information, and Machine-Assisted Proof. Ph.D. thesis, King\u2019s College, University of Cambridge, UK (2010)"},{"key":"17_CR9","doi-asserted-by":"crossref","unstructured":"Cover, T.M., Thomas, J.: Entropy, relative entropy and mutual information. In: Elements of Information Theory. Wiley-Interscience (1991)","DOI":"10.1002\/0471200611.ch2"},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"Dubois, D., Nguyen, H.T., Prade, H.: Possibility theory, probability and fuzzy sets: misunderstandings, bridges and gaps. In: Dubois, D., Prade, H. (eds.) Fundamentals of Fuzzy Sets. The Handbooks of Fuzzy Sets Series, pp. 343\u2013438. Kluwer, Boston (2000)","DOI":"10.1007\/978-1-4615-4429-6_8"},{"issue":"3","key":"17_CR11","doi-asserted-by":"crossref","first-page":"483","DOI":"10.3233\/JCS-2005-13305","volume":"13","author":"J Halpern","year":"2005","unstructured":"Halpern, J., O\u2019Neill, K.: Anonymity and information hiding in multiagent systems. J. Comput. Secur. 13(3), 483\u2013514 (2005)","journal-title":"J. Comput. Secur."},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"Hasan, O., Tahar, S.: Formal verification methods. In: Encyclopedia of Information Science and Technology, pp. 7162\u20137170. IGI Global Pub. (2015)","DOI":"10.4018\/978-1-4666-5888-2.ch705"},{"key":"17_CR13","unstructured":"Helali, G., Dunchev, C., Hasan, O., Tahar, S.: Towards The Quantitative Analysis of Information Flow in HOL, HOL4 code (2017). http:\/\/hvg.ece.concordia.ca\/projects\/prob-it\/gainMinEntropy.php"},{"key":"17_CR14","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 Moura, J. (eds.) SBMF 2013. LNCS, vol. 8195, pp. 131\u2013146. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-41071-0_10"},{"key":"17_CR15","unstructured":"H\u00f6lzl, J.: Construction and Stochastic Applications of Measure Spaces in Higher-Order Logic. Ph.D. thesis, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen, Germany (2012)"},{"key":"17_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-642-22863-6_12","volume-title":"Interactive Theorem Proving","author":"J H\u00f6lzl","year":"2011","unstructured":"H\u00f6lzl, J., Heller, A.: Three chapters of measure theory in Isabelle\/HOL. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol. 6898, pp. 135\u2013151. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-22863-6_12"},{"key":"17_CR17","unstructured":"Hua, J., Jing, Y.: On-line payment and security of e-commerce. In: International Conference on Computer Engineering and Applications, pp. 545\u2013550. CEA, WSEAS (2007)"},{"key":"17_CR18","unstructured":"Jebara, T., Pentland, A.: On Reversing Jensen\u2019s Inequality. In: Advances in Neural Information Processing Systems 13. MIT Press (2000)"},{"issue":"2\u20134","key":"17_CR19","doi-asserted-by":"crossref","first-page":"378","DOI":"10.1016\/j.ic.2007.07.003","volume":"206","author":"K Chatzikokolakis","year":"2008","unstructured":"Chatzikokolakis, K., Palamidessi, C., Panangaden, P.: Anonymity protocols as noisy channels. Inf. Comput. 206(2\u20134), 378\u2013401 (2008)","journal-title":"Inf. Comput."},{"key":"17_CR20","unstructured":"Liu, L.: Formalization of Discrete-time Markov Chains in HOL. Ph.D. thesis, Dept. of Electrical and Computer Engineering, Concordia University, Canada (2013)"},{"key":"17_CR21","unstructured":"Mhamdi, T.: Information-Theoretic Analysis using Theorem Proving. Ph.D. thesis, Dept. of Electrical and Computer Engineering, Concordia University, Canada (2012)"},{"key":"17_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-642-22863-6_18","volume-title":"Interactive Theorem Proving","author":"T Mhamdi","year":"2011","unstructured":"Mhamdi, T., Hasan, O., Tahar, S.: Formalization of entropy measures in HOL. In: Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol. 6898, pp. 233\u2013248. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-22863-6_18"},{"key":"17_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/978-3-642-34281-3_11","volume-title":"Formal Methods and Software Engineering","author":"T Mhamdi","year":"2012","unstructured":"Mhamdi, T., Hasan, O., Tahar, S.: Quantitative analysis of information flow using theorem proving. In: Aoki, T., Taguchi, K. (eds.) ICFEM 2012. LNCS, vol. 7635, pp. 119\u2013134. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-34281-3_11"},{"key":"17_CR24","doi-asserted-by":"crossref","unstructured":"Mhamdi, T., Hasan, O., Tahar, S.: Formalization of measure theory and lebesgue integration for probabilistic analysis in HOL. ACM Trans. Embedded Comput. Syst. 12(1) (2013)","DOI":"10.1145\/2406336.2406349"},{"issue":"1","key":"17_CR25","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."},{"key":"17_CR26","unstructured":"R\u00e9nyi, A.: On measures of entropy and information. In: Berkeley Symposium on Mathematics, Statistics and Probability, pp. 547\u2013561 (1961)"},{"key":"17_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/978-3-642-15640-3_7","volume-title":"Trustworthly Global Computing","author":"V Sassone","year":"2010","unstructured":"Sassone, V., ElSalamouny, E., Hamadou, S.: Trust in crowds: probabilistic behaviour in anonymity protocols. In: Wirsing, M., Hofmann, M., Rauschmayer, A. (eds.) TGC 2010. LNCS, vol. 6084, pp. 88\u2013102. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-15640-3_7"},{"key":"17_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1007\/3-540-61770-1_38","volume-title":"Computer Security \u2014 ESORICS 96","author":"S Schneider","year":"1996","unstructured":"Schneider, S., Sidiropoulos, A.: CSP and anonymity. In: Bertino, E., Kurth, H., Martella, G., Montolivo, E. (eds.) ESORICS 1996. LNCS, vol. 1146, pp. 198\u2013218. Springer, Heidelberg (1996). doi: 10.1007\/3-540-61770-1_38"},{"key":"17_CR29","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). doi: 10.1007\/978-3-642-00596-1_21"},{"key":"17_CR30","doi-asserted-by":"crossref","unstructured":"Smith, G.: Quantifying information flow using min-entropy. In: IEEE International Conference on Quantitative Evaluation of Systems, pp. 159\u2013167 (2011)","DOI":"10.1109\/QEST.2011.31"},{"key":"17_CR31","doi-asserted-by":"crossref","unstructured":"Syverson, P., Goldschlag, D., Reed, M.: Anonymous connections and onion routing. In: IEEE Symposium on Security and Privacy, Oackland, California, pp. 44\u201354 (1997)","DOI":"10.1109\/SECPRI.1997.601314"},{"key":"17_CR32","unstructured":"Trevathan, J.: Privacy and Security in Online Auctions. Ph.D. thesis, School of Mathematics, Physics and Information Technology, James Cook University, Australia (2007)"}],"container-title":["Lecture Notes in Computer Science","Dependable Software Engineering. Theories, Tools, and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-69483-2_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,4]],"date-time":"2022-08-04T18:02:52Z","timestamp":1659636172000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-69483-2_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319694825","9783319694832"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-69483-2_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}