{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,22]],"date-time":"2025-08-22T04:56:42Z","timestamp":1755838602528,"version":"3.41.0"},"reference-count":40,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2017,11,1]],"date-time":"2017-11-01T00:00:00Z","timestamp":1509494400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,11,1]],"date-time":"2017-11-01T00:00:00Z","timestamp":1509494400000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100000923","name":"Australian Research Council","doi-asserted-by":"publisher","award":["DP1097203"],"award-info":[{"award-number":["DP1097203"]}],"id":[{"id":"10.13039\/501100000923","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2017,11]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The paper studies dynamic information flow security policies in an automaton-based model. Two semantic interpretations of such policies are developed, both of which generalize the notion of TA-security [van der Meyden ESORICS 2007] for static intransitive noninterference policies. One of the interpretations focuses on information flows permitted by policy edges, the other focuses on prohibitions implied by absence of policy edges. In general, the two interpretations differ, but necessary and sufficient conditions are identified for the two interpretations to be equivalent. Sound and complete proof techniques are developed for both interpretations. Two applications of the theory are presented. The first is a general result showing that access control mechanisms are able to enforce a dynamic information flow policy. The second is a simple capability system motivated by the Flume operating system.<\/jats:p>","DOI":"10.1007\/s00165-017-0430-6","type":"journal-article","created":{"date-parts":[[2017,6,6]],"date-time":"2017-06-06T08:28:54Z","timestamp":1496737734000},"page":"1087-1120","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Dynamic intransitive noninterference revisited"],"prefix":"10.1145","volume":"29","author":[{"given":"Sebastian","family":"Eggert","sequence":"first","affiliation":[{"name":"Institut f\u00fcr Informatik, Kiel University, Kiel, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9243-0571","authenticated-orcid":false,"given":"Ron","family":"van der Meyden","sequence":"additional","affiliation":[{"name":"School of Computer Science and Engineering, UNSW Australia, 2052, Sydney, NSW, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Askarov A Chong S (2012) Learning is change in knowledge: knowledge-based security for dynamic policies. In: Chong S (ed) CSF. IEEE pp 308\u2013322","DOI":"10.1109\/CSF.2012.31"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Askarov A Sabelfeld A (2007) Localized delimited release: combining the what and where dimensions of information release. In: Proceedings of workshop on programming languages and analysis for security pp 53\u201360","DOI":"10.1145\/1255329.1255339"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Boettcher C DeLong R Rushby J Sifre W (2008) The MILS component integration approach to secure information sharing. In: Proceedings of 27th IEEE\/AIAA digital avionics systems conference pp 1.C.2\u20131\u20131.C.2\u201314 October 2008","DOI":"10.1109\/DASC.2008.4702758"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Banerjee A Naumann DA Rosenberg S (2008) Expressive declassification policies and modular static enforcement. In: IEEE symposium on security and privacy. IEEE Computer Society pp 339\u2013353","DOI":"10.1109\/SP.2008.20"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Bytschkow D Quilbeuf J Igna G Ruess H (2014) Distributed MILS architectural approach for secure smart grids. In: Smart grid security\u2014second international workshop SmartGridSec 2014 Munich Germany February 26 2014 Revised Selected Papers pp 16\u201329","DOI":"10.1007\/978-3-319-10329-7_2"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Broberg N Sands D (2006) Flow locks: towards a core calculus for dynamic flow policies. In: Sestoft P (ed) ESOP volume 3924 of Lecture notes in computer science. Springer pp 180\u2013196","DOI":"10.1007\/11693024_13"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Broberg N Sands D (2009) Flow-sensitive semantics for dynamic information flow policies. In: PLAS pp 101\u2013112","DOI":"10.1145\/1554339.1554352"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Broberg N van Delft B Sands D (2015) The anatomy and facets of dynamic policies. In: IEEE 28th computer security foundations symposium CSF 2015 Verona Italy 13\u201317 July 2015 pp 122\u2013136","DOI":"10.1109\/CSF.2015.16"},{"key":"e_1_2_1_2_9_2","unstructured":"Clark D Hunt S (2008) Non-interference for deterministic interactive programs. In: Formal aspects in security and trust 5th international workshop FAST 2008 Malaga Spain October 9\u201310 2008 Revised Selected Papers pp 50\u201366"},{"key":"e_1_2_1_2_10_2","unstructured":"Cheung L (2006) Reconciling nondetermistic and probabilistic choices. Ph.D. thesis IPA Radboud University Nijmegen"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Chong S Myers AC (2004) Security policies for downgrading. In: Proceedings of the 11th ACM conference on computer and communications security CCS 2004 Washington DC USA October 25\u201329 2004 pp 198\u2013209","DOI":"10.1145\/1030083.1030110"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Cohen ES (1977) Information transmission in computational systems. In: SOSP pp 133\u2013139","DOI":"10.1145\/1067625.806556"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Eggert S Schnoor H Wilke T (2013) Noninterference with local policies. In: Chatterjee K Sgall J (ed) MFCS volume 8087 of Lecture notes in computer science. Springer pp 337\u2013348","DOI":"10.1007\/978-3-642-40313-2_31"},{"key":"e_1_2_1_2_14_2","unstructured":"Eggert S van der Meyden R Schnoor H Wilke T (2013) Complexity and unwinding for intransitive noninterference. CoRR. arXiv:1308.1204"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Engelhardt K van der Meyden R Zhang C (2012) Intransitive noninterference in nondeterministic systems. In: ACM conference on computer and communications security pp 869\u2013880","DOI":"10.1145\/2382196.2382288"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Fagin R Halpern JY Moses Y Vardi MY (1995) Reasoning about knowledge. MIT-Press London","DOI":"10.7551\/mitpress\/5803.001.0001"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Goguen JA Meseguer J (1982) Security policies and security models. In: IEEE symposium on security and privacy pp 11\u201320","DOI":"10.1109\/SP.1982.10014"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Goguen JA Meseguer J (1984) Unwinding and inference control. In: IEEE symposium on security and privacy","DOI":"10.1109\/SP.1984.10019"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Heitmeyer CL Archer M Leonard EI McLean JD (2006) Formal specification and verification of data separation in a separation kernel for an embedded system. In: Proceedings of the 13th ACM conference on computer and communications security CCS pp 346\u2013355","DOI":"10.1145\/1180405.1180448"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(96)00019-6"},{"key":"e_1_2_1_2_21_2","unstructured":"Hicks M Tse S Hicks B Zdancewic S (2005) Dynamic updating of information-flow policies. In: Proceedings of foundations of computer security workshop (FCS)"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1987.226478"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Krohn M Tromer E (2009) Noninterference for a practical DIFC-based operating system. In: IEEE symposium on security and privacy pp 61\u201376","DOI":"10.1109\/SP.2009.23"},{"key":"e_1_2_1_2_24_2","unstructured":"Leslie R (2006) Dynamic intransitive noninterference. In: Proceedings of IEEE international symposium on secure software engineering"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2009-0355"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Myers AC Liskov B (1997) A decentralized model for information flow control. In: Proceedings of the sixteenth ACM symposium on operating systems principles SOSP \u201997 pp 129\u2013142 New York NY USA 1997. ACM","DOI":"10.1145\/268998.266669"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Murray T Matichuk D Brassil M Gammie P Klein G (2012) Noninterference for operating system kernels. In: Hawblitzel C Miller D (eds) Certified programs and proofs volume 7679 of Lecture notes in computer science pp 126\u2013142. Springer Berlin Heidelberg","DOI":"10.1007\/978-3-642-35308-6_12"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.09.003"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Mantel H Sands D (2004) Controlled declassification based on intransitive noninterference. In: Proceedings of Asian symposioum on Programming Languages and Systems volume 3302 of LNCS. Springer November 2004 pp 129\u2013145","DOI":"10.1007\/978-3-540-30477-7_9"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Martin W White P Taylor FS Goldberg A (2000) Formal construction of the mathematically analyzed separation kernel. In: IEEE Computer Society Press (ed) Proceedings of 15th IEEE conference on automated software engineering","DOI":"10.1109\/ASE.2000.873658"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"Roscoe AW Goldsmith MH (1999) What is intransitive noninterference? In: IEEE computer security foundations workshop pp 228\u2013238","DOI":"10.1109\/CSFW.1999.779776"},{"key":"e_1_2_1_2_32_2","unstructured":"Rushby J (1992) Noninterference transitivity and channel-control security policies. Technical report CSL-92-02 SRI International"},{"key":"e_1_2_1_2_33_2","unstructured":"Swamy N Hicks M Tse S Zdancewic S (2006) Managing policy updates in security-typed languages. In: 19th IEEE computer security foundations workshop (CSFW-19 2006) 5\u20137 July 2006 Venice Italy pp 202\u2013216"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"publisher","DOI":"10.5555\/773069.773072"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"publisher","DOI":"10.5555\/1662658.1662659"},{"key":"e_1_2_1_2_36_2","unstructured":"Vanfleet WM Beckworth RW Calloni B Luke JA Taylor C Uchenick G (2005) MILS: architecture for high assurance embedded computing. Crosstalk: J Defence Eng"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"crossref","unstructured":"van Delft B Hunt S Sands D (2015) Very static enforcement of dynamic policies. In: Proceedings of principles of security and Trust\u20144th international conference POST pp 32\u201352","DOI":"10.1007\/978-3-662-46666-7_3"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"crossref","unstructured":"van der Meyden R (2015) What indeed is intransitive noninterference? J Comput Secur 23(2):197\u2013228 2015. An earlier version of this work appeared in ESORICS\u201907","DOI":"10.3233\/JCS-140516"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"crossref","unstructured":"Vandebogart S Efstathopoulos P Kohler E Krohn M Frey C Ziegler D Kaashoek F Morris R Mazi\u00e8res D (2007) Labels and event processes in the Asbestos operating system. ACM Trans Comput Syst 25(4)","DOI":"10.1145\/1314299.1314302"},{"key":"e_1_2_1_2_40_2","unstructured":"Zeldovich N Boyd-Wickizer S Kohler E Mazi\u00e8res D (2006) Making information flow explicit in HiStar. In: 7th symposium on operating systems design and implementation (OSDI \u201906) November 6\u20138 Seattle WA USA pp 263\u2013278"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-017-0430-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-017-0430-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-017-0430-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-017-0430-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T00:24:03Z","timestamp":1750292643000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-017-0430-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,11]]},"references-count":40,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2017,11]]}},"alternative-id":["10.1007\/s00165-017-0430-6"],"URL":"https:\/\/doi.org\/10.1007\/s00165-017-0430-6","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2017,11]]},"assertion":[{"value":"21 January 2016","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"4 April 2017","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"6 June 2017","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}