{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,19]],"date-time":"2025-12-19T09:25:54Z","timestamp":1766136354964,"version":"3.40.4"},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642353079"},{"type":"electronic","value":"9783642353086"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-35308-6_11","type":"book-chapter","created":{"date-parts":[[2012,11,8]],"date-time":"2012-11-08T03:20:18Z","timestamp":1352344818000},"page":"109-125","source":"Crossref","is-referenced-by-count":7,"title":["Proving Concurrent Noninterference"],"prefix":"10.1007","author":[{"given":"Andrei","family":"Popescu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Johannes","family":"H\u00f6lzl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tobias","family":"Nipkow","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"11_CR1","doi-asserted-by":"crossref","unstructured":"Agat, J.: Transforming out timing leaks. In: POPL, pp. 40\u201353 (2000)","DOI":"10.1145\/325694.325702"},{"key":"11_CR2","doi-asserted-by":"crossref","unstructured":"Barthe, G., D\u2019Argenio, P.R., Rezk, T.: Secure information flow by self-composition. In: IEEE Computer Security Foundations Workshop, pp. 100\u2013114 (2004)","DOI":"10.1109\/CSFW.2004.1310735"},{"key":"11_CR3","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":"11_CR4","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)"},{"key":"11_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1007\/3-540-48224-5_32","volume-title":"Automata, Languages and Programming","author":"G. Boudol","year":"2001","unstructured":"Boudol, G., Castellani, I.: Noninterference for Concurrent Programs. In: Yu, Y., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol.\u00a02076, pp. 382\u2013395. Springer, Heidelberg (2001)"},{"issue":"1-2","key":"11_CR6","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":"11_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/978-3-540-32004-3_20","volume-title":"Security in Pervasive Computing","author":"\u00c1. Darvas","year":"2005","unstructured":"Darvas, \u00c1., H\u00e4hnle, R., Sands, D.: A Theorem Proving Approach to Analysis of Secure Information Flow. In: Hutter, D., Ullmann, M. (eds.) SPC 2005. LNCS, vol.\u00a03450, pp. 193\u2013209. Springer, Heidelberg (2005)"},{"key":"11_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/3-540-45608-2_6","volume-title":"Foundations of Security Analysis and Design","author":"R. Focardi","year":"2001","unstructured":"Focardi, R., Gorrieri, R.: Classification of Security Properties (Part i: Information Flow). In: Focardi, R., Gorrieri, R. (eds.) FOSAD 2000. LNCS, vol.\u00a02171, p. 331. Springer, Heidelberg (2001)"},{"key":"11_CR9","doi-asserted-by":"crossref","unstructured":"Halpern, J.Y., O\u2019Neill, K.R.: Secrecy in multiagent systems. ACM Trans. Inf. Syst. Secur.\u00a012(1) (2008)","DOI":"10.1145\/1410234.1410239"},{"key":"11_CR10","unstructured":"Jones, C.B.: Specification and design of (parallel) programs. In: IFIP Congress 1983, pp. 321\u2013332 (1983)"},{"key":"11_CR11","doi-asserted-by":"crossref","unstructured":"Mantel, H.: On the composition of secure systems. In: IEEE Symposium on Security and Privacy, pp. 88\u2013101 (2002)","DOI":"10.1109\/SECPRI.2002.1004364"},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"Mantel, H., Sands, D., Sudbrock, H.: Assumptions and guarantees for compositional noninterference. In: CSF 2011, Cernay-la-Ville, France, pp. 218\u2013232 (2011)","DOI":"10.1109\/CSF.2011.22"},{"key":"11_CR13","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":"11_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1007\/978-3-540-71410-1_8","volume-title":"Logic-Based Program Synthesis and Transformation","author":"H. Mantel","year":"2007","unstructured":"Mantel, H., Sudbrock, H., Krau\u00dfer, T.: Combining Different Proof Techniques for Verifying Information Flow Security. In: Puebla, G. (ed.) LOPSTR 2006. LNCS, vol.\u00a04407, pp. 94\u2013110. Springer, Heidelberg (2007)"},{"key":"11_CR15","doi-asserted-by":"crossref","unstructured":"McLean, J.: A general theory of composition for trace sets closed under selective interleaving functions, pp. 79\u201393 (May 1994)","DOI":"10.1109\/RISP.1994.296590"},{"key":"11_CR16","unstructured":"Milner, R.: Communication and concurrency. Prentice Hall (1989)"},{"key":"11_CR17","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1016\/j.jlap.2004.03.009","volume":"60-61","author":"G.D. Plotkin","year":"2004","unstructured":"Plotkin, G.D.: A structural approach to operational semantics. J. Log. Algebr. Program.\u00a060-61, 17\u2013139 (2004)","journal-title":"J. Log. Algebr. Program."},{"key":"11_CR18","unstructured":"Popescu, A., H\u00f6lzl, J.: Possibilistic noninterference formalized in Isabelle\/HOL. Archive for Formal Proofs (2012), http:\/\/afp.sourceforge.net\/entries\/Possibilistic_Noninterference.shtml"},{"key":"11_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1007\/978-3-540-77505-8_10","volume-title":"Advances in Computer Science - ASIAN 2006. Secure Software and Related Issues","author":"A. Russo","year":"2008","unstructured":"Russo, A., Hughes, J., Naumann, D.A., Sabelfeld, A.: Closing Internal Timing Channels by Transformation. In: Okada, M., Satoh, I. (eds.) ASIAN 2006. LNCS, vol.\u00a04435, pp. 120\u2013135. Springer, Heidelberg (2008)"},{"key":"11_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"474","DOI":"10.1007\/978-3-540-70881-0_43","volume-title":"Perspectives of Systems Informatics","author":"A. Russo","year":"2007","unstructured":"Russo, A., Sabelfeld, A.: Security for Multithreaded Programs Under Cooperative Scheduling. In: Virbitskaite, I., Voronkov, A. (eds.) PSI 2006. LNCS, vol.\u00a04378, pp. 474\u2013480. Springer, Heidelberg (2007)"},{"key":"11_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/3-540-45575-2_22","volume-title":"Perspectives of System Informatics","author":"A. Sabelfeld","year":"2001","unstructured":"Sabelfeld, A.: The Impact of Synchronisation on Secure Information Flow in Concurrent Programs. In: Bj\u00f8rner, D., Broy, M., Zamulin, A.V. (eds.) PSI 2001. LNCS, vol.\u00a02244, pp. 225\u2013239. Springer, Heidelberg (2001)"},{"key":"11_CR22","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":"11_CR23","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":"11_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1007\/3-540-49099-X_4","volume-title":"Programming Languages and Systems","author":"A. Sabelfeld","year":"1999","unstructured":"Sabelfeld, A., Sands, D.: A Per Model of Secure Information Flow in Sequential Programs. In: Swierstra, S.D. (ed.) ESOP 1999. LNCS, vol.\u00a01576, pp. 40\u201358. Springer, Heidelberg (1999)"},{"key":"11_CR25","doi-asserted-by":"crossref","unstructured":"Sabelfeld, A., Sands, D.: Probabilistic noninterference for multi-threaded programs. In: IEEE Computer Security Foundations Workshop, pp. 200\u2013214 (2000)","DOI":"10.1109\/CSFW.2000.856937"},{"key":"11_CR26","doi-asserted-by":"crossref","unstructured":"Smith, G.: A new type system for secure information flow. In: IEEE Computer Security Foundations Workshop, pp. 115\u2013125 (2001)","DOI":"10.1109\/CSFW.2001.930141"},{"key":"11_CR27","doi-asserted-by":"crossref","unstructured":"Smith, G.: Probabilistic noninterference through weak probabilistic bisimulation. In: IEEE Computer Security Foundations Workshop, pp. 3\u201313 (2003)","DOI":"10.1109\/CSFW.2003.1212701"},{"issue":"6","key":"11_CR28","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":"11_CR29","doi-asserted-by":"crossref","unstructured":"Smith, G., Volpano, D.: Secure information flow in a multi-threaded imperative language. In: ACM Symposium on Principles of Programming Languages, pp. 355\u2013364 (1998)","DOI":"10.1145\/268946.268975"},{"issue":"2,3","key":"11_CR30","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":"11_CR31","doi-asserted-by":"crossref","unstructured":"Zdancewic, S., Myers, A.C.: Observational determinism for concurrent program security. In: IEEE Computer Security Foundations Workshop, pp. 29\u201343 (2003)","DOI":"10.1109\/CSFW.2003.1212703"}],"container-title":["Lecture Notes in Computer Science","Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-35308-6_11.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,20]],"date-time":"2025-04-20T12:19:29Z","timestamp":1745151569000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-35308-6_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642353079","9783642353086"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-35308-6_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}