{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,19]],"date-time":"2025-12-19T09:27:28Z","timestamp":1766136448421,"version":"3.40.4"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319035444"},{"type":"electronic","value":"9783319035451"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"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":[[2013]]},"DOI":"10.1007\/978-3-319-03545-1_17","type":"book-chapter","created":{"date-parts":[[2013,12,9]],"date-time":"2013-12-09T16:31:48Z","timestamp":1386606708000},"page":"259-275","source":"Crossref","is-referenced-by-count":6,"title":["Formalizing Probabilistic Noninterference"],"prefix":"10.1007","author":[{"given":"Andrei","family":"Popescu","sequence":"first","affiliation":[]},{"given":"Johannes","family":"H\u00f6lzl","sequence":"additional","affiliation":[]},{"given":"Tobias","family":"Nipkow","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"17_CR1","unstructured":"The POPLmark challenge (2009), http:\/\/www.seas.upenn.edu\/~plclub\/poplmark\/"},{"issue":"8","key":"17_CR2","doi-asserted-by":"publisher","first-page":"568","DOI":"10.1016\/j.scico.2007.09.002","volume":"74","author":"P. Audebaud","year":"2009","unstructured":"Audebaud, P., Paulin-Mohring, C.: Proofs of randomized algorithms in Coq. S. of Comp. Prog.\u00a074(8), 568\u2013589 (2009)","journal-title":"S. of Comp. Prog."},{"key":"17_CR3","doi-asserted-by":"crossref","unstructured":"Barthe, G., D\u2019Argenio, P.R., Rezk, T.: Secure information flow by self-composition. In: CSFW, pp. 100\u2013114 (2004)","DOI":"10.1109\/CSFW.2004.1310735"},{"key":"17_CR4","doi-asserted-by":"crossref","unstructured":"Barthe, G., Daubignard, M., Kapron, B.M., Lakhnech, Y.: Computational indistinguishability logic. In: CCS, pp. 375\u2013386 (2010)","DOI":"10.1145\/1866307.1866350"},{"key":"17_CR5","doi-asserted-by":"crossref","unstructured":"Barthe, G., Gr\u00e9goire, B., B\u00e9guelin, S.Z.: Formal certification of code-based cryptographic proofs. In: POPL, pp. 90\u2013101 (2009)","DOI":"10.1145\/1594834.1480894"},{"key":"17_CR6","doi-asserted-by":"crossref","unstructured":"Barthe, G., Nieto, L.P.: Formally verifying information flow type systems for concurrent and thread systems. In: FMSE, pp. 13\u201322 (2004)","DOI":"10.1145\/1029133.1029136"},{"key":"17_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/11560647_24","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2005","author":"G. Boudol","year":"2005","unstructured":"Boudol, G.: On typing information flow. In: Van Hung, D., Wirsing, M. (eds.) ICTAC 2005. LNCS, vol.\u00a03722, pp. 366\u2013380. Springer, Heidelberg (2005)"},{"issue":"1-2","key":"17_CR8","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1016\/S0304-3975(02)00010-5","volume":"281","author":"G. Boudol","year":"2002","unstructured":"Boudol, G., Castellani, I.: Noninterference for concurrent programs and thread systems. Theoretical Computer Science\u00a0281(1-2), 109\u2013130 (2002)","journal-title":"Theoretical Computer Science"},{"key":"17_CR9","doi-asserted-by":"crossref","unstructured":"Cock, D.: Verifying probabilistic correctness in Isabelle with pGCL. In: SSV, pp. 167\u2013178 (2012)","DOI":"10.4204\/EPTCS.102.15"},{"key":"17_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/978-3-642-39634-2_23","volume-title":"Interactive Theorem Proving","author":"D. Cock","year":"2013","unstructured":"Cock, D.: Practical probability: Applying pGCL to lattice scheduling. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol.\u00a07998, pp. 311\u2013327. Springer, Heidelberg (2013)"},{"key":"17_CR11","unstructured":"H\u00f6lzl, J.: Analyzing discrete-time Markov chains with countable state space in Isabelle\/HOL. Draft, http:\/\/home.in.tum.de\/~hoelzl\/classifying"},{"key":"17_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/978-3-642-28756-5_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J. H\u00f6lzl","year":"2012","unstructured":"H\u00f6lzl, J., Nipkow, T.: Verifying pCTL model checking. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol.\u00a07214, pp. 347\u2013361. Springer, Heidelberg (2012)"},{"key":"17_CR13","doi-asserted-by":"crossref","unstructured":"Hurd, J., McIver, A., Morgan, C.: Probabilistic guarded commands mechanized in HOL. Theor. Comput. Sci.\u00a0346(1) (2005)","DOI":"10.1016\/j.tcs.2005.08.005"},{"key":"17_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/3-540-48256-3_11","volume-title":"Theorem Proving in Higher Order Logics","author":"F. Kamm\u00fcller","year":"1999","unstructured":"Kamm\u00fcller, F., Wenzel, M., Paulson, L.C.: Locales - a sectioning concept for Isabelle. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol.\u00a01690, pp. 149\u2013166. Springer, Heidelberg (1999)"},{"key":"17_CR15","doi-asserted-by":"crossref","unstructured":"Kemeny, J.G., Snell, J.L., Knapp, A.W.: Denumerable Markov chains, 2nd edn. Springer (1976)","DOI":"10.1007\/978-1-4684-9455-6"},{"issue":"1","key":"17_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(91)90030-6","volume":"94","author":"K.G. Larsen","year":"1991","unstructured":"Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Information and Computation\u00a094(1), 1\u201328 (1991)","journal-title":"Information and Computation"},{"key":"17_CR17","unstructured":"Mantel, H.: A uniform framework for the specification and verification of security properties. Ph.D. thesis, Univ. of Saarbr\u00fccken (2003)"},{"key":"17_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/978-3-642-15497-3_8","volume-title":"Computer Security \u2013 ESORICS 2010","author":"H. Mantel","year":"2010","unstructured":"Mantel, H., Sudbrock, H.: Flexible scheduler-independent security. In: Gritzalis, D., Preneel, B., Theoharidou, M. (eds.) ESORICS 2010. LNCS, vol.\u00a06345, pp. 116\u2013133. Springer, Heidelberg (2010)"},{"key":"17_CR19","doi-asserted-by":"crossref","unstructured":"McIver, A., Morgan, C.: Abstraction, Refinement and Proof for Probabilistic Systems. Springer (2005)","DOI":"10.1145\/1059816.1059824"},{"key":"17_CR20","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-order Logic. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)","DOI":"10.1007\/3-540-45949-9"},{"key":"17_CR21","unstructured":"Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a\u00a0practical link between automatic and interactive theorem provers. In: IWIL (2010)"},{"key":"17_CR22","unstructured":"Popescu, A., H\u00f6lzl, J.: Formal development associated with this paper, http:\/\/www21.in.tum.de\/~popescua\/prob.zip (to appear in the Archive of Formal Proofs, 2013)"},{"key":"17_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/978-3-642-35308-6_11","volume-title":"Certified Programs and Proofs","author":"A. Popescu","year":"2012","unstructured":"Popescu, A., H\u00f6lzl, J., Nipkow, T.: Proving concurrent noninterference. In: Hawblitzel, C., Miller, D. (eds.) CPP 2012. LNCS, vol.\u00a07679, pp. 109\u2013125. Springer, Heidelberg (2012)"},{"key":"17_CR24","doi-asserted-by":"crossref","unstructured":"Popescu, A., H\u00f6lzl, J., Nipkow, T.: Noninterfering schedulers - when possibilistic noninterference implies probabilistic noninterference. In: CALCO, pp. 236\u2013252 (2013)","DOI":"10.1007\/978-3-642-40206-7_18"},{"key":"17_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/978-3-540-39866-0_27","volume-title":"Perspectives of System Informatics","author":"A. Sabelfeld","year":"2004","unstructured":"Sabelfeld, A.: Confidentiality for multithreaded programs via bisimulation. In: Broy, M., Zamulin, A.V. (eds.) PSI 2003. LNCS, vol.\u00a02890, pp. 260\u2013274. Springer, Heidelberg (2004)"},{"issue":"1","key":"17_CR26","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1109\/JSAC.2002.806121","volume":"21","author":"A. Sabelfeld","year":"2003","unstructured":"Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE Journal on Selected Areas in Communications\u00a021(1), 5\u201319 (2003)","journal-title":"IEEE Journal on Selected Areas in Communications"},{"key":"17_CR27","doi-asserted-by":"crossref","unstructured":"Sabelfeld, A., Sands, D.: Probabilistic noninterference for multi-threaded programs. In: CSFW, pp. 200\u2013214 (2000)","DOI":"10.1109\/CSFW.2000.856937"},{"key":"17_CR28","doi-asserted-by":"crossref","unstructured":"Smith, G.: A new type system for secure information flow. In: CSFW, pp. 115\u2013125 (2001)","DOI":"10.1109\/CSFW.2001.930141"},{"key":"17_CR29","doi-asserted-by":"crossref","unstructured":"Smith, G.: Probabilistic noninterference through weak probabilistic bisimulation. In: CSFW, pp. 3\u201313 (2003)","DOI":"10.1109\/CSFW.2003.1212701"},{"issue":"6","key":"17_CR30","doi-asserted-by":"crossref","first-page":"591","DOI":"10.3233\/JCS-2006-14605","volume":"14","author":"G. Smith","year":"2006","unstructured":"Smith, G.: Improved typings for probabilistic noninterference in a multi-threaded language. Journal of Computer Security\u00a014(6), 591\u2013623 (2006)","journal-title":"Journal of Computer Security"},{"key":"17_CR31","doi-asserted-by":"crossref","unstructured":"Smith, G., Volpano, D.: Secure information flow in a multi-threaded imperative language. In: POPL, pp. 355\u2013364 (1998)","DOI":"10.1145\/268946.268975"},{"issue":"2,3","key":"17_CR32","doi-asserted-by":"crossref","first-page":"231","DOI":"10.3233\/JCS-1999-72-305","volume":"7","author":"D. Volpano","year":"1999","unstructured":"Volpano, D., Smith, G.: Probabilistic noninterference in a concurrent language. Journal of Computer Security\u00a07(2,3), 231\u2013253 (1999)","journal-title":"Journal of Computer Security"},{"issue":"2,3","key":"17_CR33","doi-asserted-by":"crossref","first-page":"167","DOI":"10.3233\/JCS-1996-42-304","volume":"4","author":"D. Volpano","year":"1996","unstructured":"Volpano, D., Smith, G., Irvine, C.: A sound type system for secure flow analysis. Journal of Computer Security\u00a04(2,3), 167\u2013187 (1996)","journal-title":"Journal of Computer Security"},{"key":"17_CR34","doi-asserted-by":"crossref","unstructured":"Zdancewic, S., Myers, A.C.: Observational determinism for concurrent program security. In: CSFW, pp. 29\u201343 (2003)","DOI":"10.1109\/CSFW.2003.1212703"}],"container-title":["Lecture Notes in Computer Science","Certified Programs and Proofs"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-03545-1_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T03:45:09Z","timestamp":1746071109000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-03545-1_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783319035444","9783319035451"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-03545-1_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}