{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T22:35:37Z","timestamp":1725921337050},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319712369"},{"type":"electronic","value":"9783319712376"}],"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-71237-6_3","type":"book-chapter","created":{"date-parts":[[2017,11,18]],"date-time":"2017-11-18T01:13:02Z","timestamp":1510967582000},"page":"45-66","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Taming Message-Passing Communication in Compositional Reasoning About Confidentiality"],"prefix":"10.1007","author":[{"given":"Ximeng","family":"Li","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Heiko","family":"Mantel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Markus","family":"Tasch","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,11,19]]},"reference":[{"key":"3_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-642-12459-4_10","volume-title":"Formal Aspects in Security and Trust","author":"R Alp\u00edzar","year":"2010","unstructured":"Alp\u00edzar, R., Smith, G.: Secure information flow for distributed systems. In: Degano, P., Guttman, J.D. (eds.) FAST 2009. LNCS, vol. 5983, pp. 126\u2013140. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-12459-4_10"},{"key":"3_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/978-3-540-68237-0","volume-title":"FM 2008: Formal Methods","author":"T Amtoft","year":"2008","unstructured":"Amtoft, T., Hatcliff, J., Rodr\u00edguez, E., Robby, H.J., Greve, D.: Specification and checking of software contracts for conditional information flow. In: Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 229\u2013245. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-68237-0"},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"Askarov, A., Chong, S., Mantel, H.: Hybrid monitors for concurrent noninterference. In: CSF 2015, pp. 137\u2013151 (2015)","DOI":"10.1109\/CSF.2015.17"},{"key":"3_CR4","doi-asserted-by":"crossref","unstructured":"Askarov, A., Sabelfeld, A.: Gradual release: unifying declassification, encryption and key release policies. In: S&P 2007, pp. 207\u2013221 (2007)","DOI":"10.1109\/SP.2007.22"},{"key":"3_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/978-3-642-15375-4_17","volume-title":"CONCUR 2010 - Concurrency Theory","author":"S Capecchi","year":"2010","unstructured":"Capecchi, S., Castellani, I., Dezani-Ciancaglini, M., Rezk, T.: Session types for access and information flow control. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 237\u2013252. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15375-4_17"},{"issue":"6","key":"3_CR6","doi-asserted-by":"crossref","first-page":"1157","DOI":"10.3233\/JCS-2009-0393","volume":"18","author":"MR Clarkson","year":"2010","unstructured":"Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur. 18(6), 1157\u20131210 (2010)","journal-title":"J. Comput. Secur."},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"Focardi, R., Centenaro, M.: Information flow security of multi-threaded distributed programs. In: PLAS 2008, pp. 113\u2013124 (2008)","DOI":"10.1145\/1375696.1375711"},{"key":"3_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. 2171, pp. 331\u2013396. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45608-2_6"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Goguen, J.A., Meseguer, J.: Security policies and security models. In: S&P 1982. IEEE Computer Society (1982)","DOI":"10.1109\/SP.1982.10014"},{"key":"3_CR10","doi-asserted-by":"crossref","unstructured":"Greiner, S., Grahl, D.: Non-interference with what-declassification in component-based systems. In: CSF 2016, pp. 253\u2013267 (2016)","DOI":"10.1109\/CSF.2016.25"},{"key":"3_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1007\/3-540-46425-5_12","volume-title":"Programming Languages and Systems","author":"K Honda","year":"2000","unstructured":"Honda, K., Vasconcelos, V., Yoshida, N.: Secure information flow as typed process behaviour. In: Smolka, G. (ed.) ESOP 2000. LNCS, vol. 1782, pp. 180\u2013199. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-46425-5_12"},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"Hunt, S., Sands, D.: On flow-sensitive security types. In: POPL 2006, pp. 79\u201390 (2006)","DOI":"10.1145\/1111037.1111045"},{"key":"3_CR13","unstructured":"Jones, C.B.: Development methods for computer programs including a notion of interference. Oxford University Computing Laboratory (1981)"},{"issue":"4\u20135","key":"3_CR14","doi-asserted-by":"crossref","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."},{"issue":"2","key":"3_CR15","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1109\/TSE.1977.229904","volume":"3","author":"L Lamport","year":"1977","unstructured":"Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. Softw. Eng. 3(2), 125\u2013143 (1977)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"3_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/978-3-319-28766-9_7","volume-title":"Trustworthy Global Computing","author":"X Li","year":"2016","unstructured":"Li, X., Nielson, F., Nielson, H.R., Feng, X.: Disjunctive information flow for communicating processes. In: Ganty, P., Loreti, M. (eds.) TGC 2015. LNCS, vol. 9533, pp. 95\u2013111. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-28766-9_7"},{"key":"3_CR17","doi-asserted-by":"crossref","first-page":"605","DOI":"10.1007\/978-1-4419-5906-5_874","volume-title":"Encyclopedia of Cryptography and Security","author":"H Mantel","year":"2011","unstructured":"Mantel, H.: Information flow and noninterference. In: van Tilborg, H.C.A., Jajodia, S. (eds.) Encyclopedia of Cryptography and Security, 2nd edn, pp. 605\u2013607. Springer, New York (2011)","edition":"2"},{"key":"3_CR18","doi-asserted-by":"crossref","unstructured":"Mantel, H., M\u00fcller-Olm, M., Perner, M., Wenner, A.: Using dynamic pushdown networks to automate a modular information-flow analysis. In: LOPSTR 2015 (2015)","DOI":"10.1007\/978-3-319-27436-2_12"},{"key":"3_CR19","doi-asserted-by":"crossref","unstructured":"Mantel, H., Sands, D., Sudbrock, H.: Assumptions and guarantees for compositional noninterference. In: CSF 2011, pp. 218\u2013232 (2011)","DOI":"10.1109\/CSF.2011.22"},{"key":"3_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/10722468_16","volume-title":"SPIN Model Checking and Software Verification","author":"M Martel","year":"2000","unstructured":"Martel, M., Gengler, M.: Communication topology analysis for concurrent programs. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, pp. 265\u2013286. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/10722468_16"},{"issue":"6","key":"3_CR21","doi-asserted-by":"crossref","first-page":"563","DOI":"10.1109\/32.55085","volume":"16","author":"D McCullough","year":"1990","unstructured":"McCullough, D.: A hookup theorem for multilevel security. IEEE Trans. Softw. Eng. 16(6), 563\u2013568 (1990)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"3_CR22","doi-asserted-by":"crossref","unstructured":"Murray, T.C., Sison, R., Pierzchalski, E., Rizkallah, C.: Compositional verification and refinement of concurrent value-dependent noninterference. In: CSF 2016 (2016)","DOI":"10.1109\/CSF.2016.36"},{"key":"3_CR23","doi-asserted-by":"crossref","unstructured":"Myers, A.C., Liskov, B.: A decentralized model for information flow control. In: SOSP 1997, pp. 129\u2013142 (1997)","DOI":"10.1145\/268998.266669"},{"key":"3_CR24","doi-asserted-by":"crossref","unstructured":"Rafnsson, W., Hedin, D., Sabelfeld, A.: Securing interactive programs. In: CSF 2012, pp. 293\u2013307 (2012)","DOI":"10.1109\/CSF.2012.15"},{"key":"3_CR25","doi-asserted-by":"crossref","unstructured":"Sabelfeld, A., Mantel, H.: Securing communication in a concurrent language. In: SAS 2002, pp. 376\u2013394 (2002)","DOI":"10.1007\/3-540-45789-5_27"},{"issue":"1","key":"3_CR26","doi-asserted-by":"crossref","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":"3_CR27","volume-title":"Distributed Systems - Principles and Paradigms","author":"AS Tanenbaum","year":"2007","unstructured":"Tanenbaum, A.S., van Steen, M.: Distributed Systems - Principles and Paradigms, 2nd edn. Prentice-Hall Inc., Upper Saddle River (2007)","edition":"2"},{"issue":"2\/3","key":"3_CR28","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."},{"key":"3_CR29","doi-asserted-by":"crossref","unstructured":"Zdancewic, S., Myers, A.C.: Observational determinism for concurrent program security. In: CSFW 2003, pp. 29\u201343 (2003)","DOI":"10.1109\/CSFW.2003.1212703"},{"issue":"2\u20133","key":"3_CR30","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1007\/s10207-007-0019-9","volume":"6","author":"L Zheng","year":"2007","unstructured":"Zheng, L., Myers, A.C.: Dynamic security labels and static information flow control. Int. J. Inf. Sec. 6(2\u20133), 67\u201384 (2007)","journal-title":"Int. J. Inf. Sec."}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-71237-6_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,10,22]],"date-time":"2020-10-22T03:16:11Z","timestamp":1603336571000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-71237-6_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319712369","9783319712376"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-71237-6_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}