{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T04:14:31Z","timestamp":1748751271271,"version":"3.41.0"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319287652"},{"type":"electronic","value":"9783319287669"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-28766-9_7","type":"book-chapter","created":{"date-parts":[[2016,1,4]],"date-time":"2016-01-04T12:09:44Z","timestamp":1451909384000},"page":"95-111","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Disjunctive Information Flow for Communicating Processes"],"prefix":"10.1007","author":[{"given":"Ximeng","family":"Li","sequence":"first","affiliation":[]},{"given":"Flemming","family":"Nielson","sequence":"additional","affiliation":[]},{"given":"Hanne Riis","family":"Nielson","sequence":"additional","affiliation":[]},{"given":"Xinyu","family":"Feng","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,1,5]]},"reference":[{"key":"7_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/978-3-642-28641-4_20","volume-title":"Principles of Security and Trust","author":"T Amtoft","year":"2012","unstructured":"Amtoft, T., Dodds, J., Zhang, Z., Appel, A., Beringer, L., Hatcliff, J., Ou, X., Cousino, A.: A certificate infrastructure for machine-checked proofs of conditional information flow. In: Degano, P., Guttman, J.D. (eds.) Principles of Security and Trust. LNCS, vol. 7215, pp. 369\u2013389. Springer, Heidelberg (2012)"},{"issue":"4","key":"7_CR2","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1145\/357146.357150","volume":"3","author":"KR Apt","year":"1981","unstructured":"Apt, K.R.: Ten years of Hoare\u2019s logic: A survey - part 1. ACM Trans. Program. Lang. Syst. 3(4), 431\u2013483 (1981)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"7_CR3","doi-asserted-by":"crossref","unstructured":"Austin, T.H., Flanagan, C.: Efficient purely-dynamic information flow analysis. In: PLAS 2009, pp. 113\u2013124 (2009)","DOI":"10.1145\/1554339.1554353"},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"Besson, F., Bielova, N., Jensen, T.: Hybrid information flow monitoring against web tracking. In: CSF 2013 (2013)","DOI":"10.1109\/CSF.2013.23"},{"issue":"1","key":"7_CR5","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. Theoret. Comput. Sci. 281(1), 109\u2013130 (2002)","journal-title":"Theoret. Comput. Sci."},{"issue":"1","key":"7_CR6","doi-asserted-by":"crossref","first-page":"431","DOI":"10.1145\/1707801.1706349","volume":"45","author":"Niklas Broberg","year":"2010","unstructured":"Broberg, N., Sands, D.: Paralocks: role-based informationflow control and beyond. In: POPL 2010, pp. 431\u2013444 (2010)","journal-title":"ACM SIGPLAN Notices"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"Clarkson, M.R., Chong, S., Myers, A.C.: Civitas: Toward a secure voting system. In: S&P 2008, pp. 354\u2013368 (2008)","DOI":"10.1109\/SP.2008.32"},{"key":"7_CR8","doi-asserted-by":"crossref","unstructured":"Cohen, E.S.: Information transmission in computational systems. In: SOSP 1977 (1977)","DOI":"10.1145\/800214.806556"},{"key":"7_CR9","unstructured":"The Coq Proof Assistant. http:\/\/coq.inria.fr"},{"issue":"1","key":"7_CR10","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1145\/1111320.1111044","volume":"41","author":"Mads Dam","year":"2006","unstructured":"Dam, M.: Decidability and proof systems for language-based noninterference relations. In: POPL 2006 (2006)","journal-title":"ACM SIGPLAN Notices"},{"issue":"7","key":"7_CR11","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1145\/359636.359712","volume":"20","author":"DE Denning","year":"1977","unstructured":"Denning, D.E., Denning, P.J.: Certification of programs for secure information flow. Commun. ACM 20(7), 504\u2013513 (1977)","journal-title":"Commun. ACM"},{"key":"7_CR12","doi-asserted-by":"crossref","unstructured":"Eggert, S., van der Meyden, R., Schnoor, H., Wilke, T.: The complexity of intransitive noninterference. In: S&P 2011, pp. 196\u2013211 (2011)","DOI":"10.1109\/SP.2011.30"},{"issue":"2","key":"7_CR13","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1093\/comjnl\/17.2.143","volume":"17","author":"JS Fenton","year":"1974","unstructured":"Fenton, J.S.: Memoryless subsystems. Comput. J. 17(2), 143\u2013147 (1974)","journal-title":"Comput. J."},{"key":"7_CR14","unstructured":"Focardi, R., Rossi, S.: Information flow security in dynamic contexts. In: (CSFW 2002), pp. 307\u2013319 (2002)"},{"key":"7_CR15","doi-asserted-by":"crossref","unstructured":"Hedin, D., Birgisson, A., Bello, L., Sabelfeld, A.: JSFlow: tracking information flow in javascript and its APIs. In: SAC 2014, pp. 1663\u20131671 (2014)","DOI":"10.1145\/2554850.2554909"},{"key":"7_CR16","unstructured":"Hedin, D., Sabelfeld, A.: A perspective on information-flow control. In: Software Safety and Security - Tools for Analysis and Verification, pp. 319\u2013347 (2012)"},{"key":"7_CR17","unstructured":"Jones, C.B.: Development Methods for Computer Programs including a Notion of Interference. Ph.D. thesis, Oxford University, June 1981"},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"Jovanovic, N., Kruegel, C., Kirda, E.: Pixy: A static analysis tool for detecting web application vulnerabilities, p. 6 (2006)","DOI":"10.1109\/SP.2006.29"},{"issue":"4\u20135","key":"7_CR19","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/s00236-005-0179-x","volume":"42","author":"N Kobayashi","year":"2005","unstructured":"Kobayashi, N.: Type-based information flow analysis for the pi-calculus. Acta Inf. 42(4\u20135), 291\u2013347 (2005)","journal-title":"Acta Inf."},{"key":"7_CR20","doi-asserted-by":"crossref","unstructured":"Louren\u00e7o, L., Caires, L.: Dependent information flow types. In: POPL 2015 (2015)","DOI":"10.1145\/2676726.2676994"},{"issue":"4","key":"7_CR21","doi-asserted-by":"crossref","first-page":"615","DOI":"10.3233\/JCS-2003-11406","volume":"11","author":"H Mantel","year":"2003","unstructured":"Mantel, H., Sabelfeld, A.: A unifying approach to the security of distributed and multi-threaded programs. J. Comput. Secur. 11(4), 615\u2013676 (2003)","journal-title":"J. Comput. Secur."},{"key":"7_CR22","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. 6345, pp. 116\u2013133. Springer, Heidelberg (2010)"},{"key":"7_CR23","volume-title":"Communication and Concurrency","author":"R Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency, vol. 84. Prentice hall, Upper Saddle River (1989)"},{"key":"7_CR24","doi-asserted-by":"crossref","unstructured":"Rafnsson, W., Sabelfeld, A.: Compositional information-flow security for interactive systems. In: CSF 2014, pp. 277\u2013292 (2014)","DOI":"10.1109\/CSF.2014.27"},{"key":"7_CR25","unstructured":"Rushby, J.: Separation and integration in MILS (the MILS constitution). Computer Science Laboratory SRI International, Technical Report (2008)"},{"key":"7_CR26","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. 2890, pp. 260\u2013274. Springer, Heidelberg (2004)"},{"issue":"1","key":"7_CR27","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 J. Sel. Areas Commun. 21(1), 5\u201319 (2003)","journal-title":"IEEE J. Sel. Areas Commun."},{"key":"7_CR28","doi-asserted-by":"crossref","unstructured":"Sabelfeld, A., Sands, D.: Probabilistic noninterference for multi-threaded programs. In: CSFW 2000, pp. 200\u2013214 (2000)","DOI":"10.1109\/CSFW.2000.856937"},{"issue":"6","key":"7_CR29","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. J. Comput. Secur. 14(6), 591\u2013623 (2006)","journal-title":"J. Comput. Secur."},{"key":"7_CR30","doi-asserted-by":"crossref","unstructured":"Smith, G., Volpano, D.M.: Secure information flow in a multi-threaded imperative language. In: POPL 1998, pp. 355\u2013364 (1998)","DOI":"10.1145\/268946.268975"},{"key":"7_CR31","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1016\/j.tcs.2012.10.047","volume":"467","author":"R Meyden van der","year":"2013","unstructured":"van der Meyden, R., Zhang, C.: Information flow in systems with schedulers, part I: definitions. Theor. Comput. Sci. 467, 68\u201388 (2013)","journal-title":"Theor. Comput. Sci."},{"issue":"2\/3","key":"7_CR32","doi-asserted-by":"crossref","first-page":"167","DOI":"10.3233\/JCS-1996-42-304","volume":"4","author":"DM Volpano","year":"1996","unstructured":"Volpano, D.M., Irvine, C.E., Smith, G.: A sound type system for secure flow analysis. J. Comput. Secur. 4(2\/3), 167\u2013188 (1996)","journal-title":"J. Comput. Secur."}],"container-title":["Lecture Notes in Computer Science","Trustworthy Global Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-28766-9_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T00:57:05Z","timestamp":1748739425000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-28766-9_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319287652","9783319287669"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-28766-9_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"5 January 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}