{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,3]],"date-time":"2026-04-03T23:14:54Z","timestamp":1775258094419,"version":"3.50.1"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030019495","type":"print"},{"value":"9783030019501","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-030-01950-1_37","type":"book-chapter","created":{"date-parts":[[2018,10,25]],"date-time":"2018-10-25T19:16:51Z","timestamp":1540495011000},"page":"629-646","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Automated Verification of Noninterference Property"],"prefix":"10.1007","author":[{"given":"Fan","family":"Zhang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cong","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mingdi","family":"Xu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xiaoli","family":"Liu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fangning","family":"Hu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"HanChieh","family":"Chao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,10,26]]},"reference":[{"key":"37_CR1","doi-asserted-by":"crossref","unstructured":"Goguen, J., Meseguer, J.: Security policies and security models. In: Proceedings of IEEE Symposium on Security and Privacy, pp. 11\u201320. IEEE, Oakland (1982)","DOI":"10.1109\/SP.1982.10014"},{"issue":"2","key":"37_CR2","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1109\/TSE.1987.226478","volume":"SE-13","author":"J Haigh","year":"1987","unstructured":"Haigh, J., Young, W.: Extending the noninterference version of MLS for SAT. IEEE Trans. Softw. Eng. SE-13(2), 141\u2013150 (1987)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"37_CR3","unstructured":"Rushby, J.: Noninterference, transitivity, and channel control security policies. SRI International. Technical report CSL-92-02, December 1992. http:\/\/www.csl.sri.com\/papers\/csl-92-2\/"},{"issue":"5","key":"37_CR4","doi-asserted-by":"publisher","first-page":"948","DOI":"10.1109\/TSMCB.2005.847749","volume":"35","author":"N Hadj-Alouane","year":"2005","unstructured":"Hadj-Alouane, N., Lafrance, S., Lin, F., Mullins, J., Yeddes, M.: On the verification of intransitive noninterference in multilevel security. IEEE Trans. on Syst. Man Cybern. Part B 35(5), 948\u2013958 (2005)","journal-title":"IEEE Trans. on Syst. Man Cybern. Part B"},{"key":"37_CR5","doi-asserted-by":"crossref","unstructured":"Eggert, S., Meyden, R.V.D., Schnoor, H., Wilke, T.: The complexity of intransitive noninterference. In: Proceedings of the IEEE Symposium on Security and Privacy, pp. 196\u2013211. IEEE, Oakland (2011)","DOI":"10.1109\/SP.2011.30"},{"issue":"10","key":"37_CR6","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1016\/j.entcs.2006.11.002","volume":"168","author":"RVD Meyden","year":"2007","unstructured":"Meyden, R.V.D., Zhang, C.: Algorithmic verification of noninterference properties. Electr. Notes Theor. Comput. Sci. 168(10), 61\u201375 (2007)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"issue":"1","key":"37_CR7","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1016\/j.entcs.2005.06.005","volume":"135","author":"D D\u2019Souza","year":"2005","unstructured":"D\u2019Souza, D., Raghavendra, K.R., Sprick, B.: An automata based approach for verifying information flow properties. Electr. Notes Theor. Comput. Sci. 135(1), 39\u201358 (2005)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"37_CR8","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/3-540-45608-2_6","volume-title":"Foundations of Security Analysis and Design 2000","author":"R Focardi","year":"2000","unstructured":"Focardi, R., Gorrieri, R.: Classification of security properties (part I: information flow). In: Focardi, R., Gorrieri, R. (eds.) Foundations of Security Analysis and Design 2000. LNCS, vol. 2171, pp. 331\u2013396. Springer, Heidelberg (2000)"},{"key":"37_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-45608-2_1","volume-title":"Foundations of Security Analysis and Design","author":"PYA Ryan","year":"2001","unstructured":"Ryan, P.Y.A.: Mathematical models of computer security. In: Focardi, R., Gorrieri, R. (eds.) FOSAD 2000. LNCS, vol. 2171, pp. 1\u201362. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45608-2_1"},{"key":"37_CR10","doi-asserted-by":"crossref","unstructured":"Wittbold, J.T., Johnson, D.M.: Information flow in nondeterministic systems. In: IEEE Symposium on Security and Privacy, pp. 144\u2013161. IEEE, Oakland (1990)","DOI":"10.1109\/RISP.1990.63846"},{"key":"37_CR11","doi-asserted-by":"crossref","unstructured":"McCullough, D.: Noninterference and the composability of security properties. In: IEEE Symposium on Security and Privacy, pp. 177\u2013186. IEEE, Oakland (1988)","DOI":"10.1109\/SECPRI.1988.8110"},{"key":"37_CR12","unstructured":"Mantel, H.: A uniform framework for the formal specification and verification of information flow security. Ph.D. dissertation, Universitat des Saarlandes (2003)"},{"key":"37_CR13","doi-asserted-by":"crossref","unstructured":"Roscoe, A.W., Goldsmith, M.H.: What is intransitive noninterference? In: IEEE Computer Security Foundations Workshop, pp. 228\u2013238. IEEE, Mordano (1999)","DOI":"10.1109\/CSFW.1999.779776"},{"key":"37_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/978-3-540-30108-0_14","volume-title":"Computer Security \u2013 ESORICS 2004","author":"D Oheimb","year":"2004","unstructured":"Oheimb, D.: Information flow control revisited: noninfluence = noninterference + nonleakage. In: Samarati, P., Ryan, P., Gollmann, D., Molva, R. (eds.) ESORICS 2004. LNCS, vol. 3193, pp. 225\u2013243. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30108-0_14"},{"key":"37_CR15","doi-asserted-by":"crossref","unstructured":"Engelhardt, K., Meyden, R.V.D., Zhang, C.: Intransitive noninterference in nondeterministic systems. In: Proceedings of ACM Conference on Computer and Communications Security, pp. 869\u2013880. ACM, Raleigh (2012)","DOI":"10.1145\/2382196.2382288"},{"key":"37_CR16","doi-asserted-by":"crossref","unstructured":"Murray, T., et al.: seL4: from general purpose to a proof of information flow enforcement. In: IEEE Symposium on Security and Privacy, pp. 415\u2013429. IEEE, Oakland (2013)","DOI":"10.1109\/SP.2013.35"},{"key":"37_CR17","doi-asserted-by":"crossref","unstructured":"Dam, M., Guanciale, R., Schwarz, O.: Formal verification of information flow security for a simple arm-based separation kernel. In: Proceedings of ACM Conference on Computer and Communications Security, pp. 223\u2013234. ACM, Berlin (2013)","DOI":"10.1145\/2508859.2516702"},{"key":"37_CR18","doi-asserted-by":"crossref","unstructured":"Ko, C., Redmond, T.: Noninterference and intrusion detection. In: IEEE Symp. on Security and Privacy, pp:177. IEEE, Oakland (2002)","DOI":"10.1109\/SECPRI.2002.1004370"},{"key":"37_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-642-35308-6_12","volume-title":"Certified Programs and Proofs","author":"T Murray","year":"2012","unstructured":"Murray, T., Matichuk, D., Brassil, M., Gammie, P., Klein, G.: Noninterference for operating system kernels. In: Hawblitzel, C., Miller, D. (eds.) CPP 2012. LNCS, vol. 7679, pp. 126\u2013142. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-35308-6_12"},{"key":"37_CR20","doi-asserted-by":"crossref","unstructured":"Krohn, M., Tromer, E.: Noninterference for a practical DIFC-based operating system. In: IEEE Symposium on Security and Privacy, pp. 61\u201376. IEEE, Oakland (2009)","DOI":"10.1109\/SP.2009.23"},{"issue":"9","key":"37_CR21","doi-asserted-by":"publisher","first-page":"550","DOI":"10.1109\/32.629493","volume":"23","author":"R Focardi","year":"1997","unstructured":"Focardi, R., Gorrieri, R.: The compositional security checker: a tool for the verification of information flow security properties. IEEE Trans. Softw. Eng. 23(9), 550\u2013572 (1997)","journal-title":"IEEE Trans. Softw. Eng."}],"container-title":["Lecture Notes in Computer Science","Information and Communications Security"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-01950-1_37","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,3]],"date-time":"2026-04-03T21:51:54Z","timestamp":1775253114000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-01950-1_37"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783030019495","9783030019501"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-01950-1_37","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"26 October 2018","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICICS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Information and Communications Security","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lille","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 October 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31 October 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"icics2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/conference.imt-lille-douai.fr\/icics2018\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}