{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,28]],"date-time":"2025-09-28T04:10:41Z","timestamp":1759032641610},"reference-count":34,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2013,1]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>A well-established specification of noninterference in CSP is that, when high-level events are appropriately abstracted, the remaining low-level view is deterministic. This is not a workable definition in Timed CSP, where many processes cannot be refined to deterministic ones. We argue that in fact \u201cdeterministic\u201d should be replaced by \u201cmaximally refined\u201d in the definition above. We show how to automate the resulting timed noninterference check within the context of the recent extension of FDR to analyse a discrete version of Timed CSP, and how an extended theory of digitisation has the potential both to create more accurate specifications and to infer when processes are noninterfering in the more usual continuous-time semantics.<\/jats:p>","DOI":"10.1007\/s00165-012-0251-6","type":"journal-article","created":{"date-parts":[[2012,6,28]],"date-time":"2012-06-28T13:55:58Z","timestamp":1340891758000},"page":"3-35","source":"Crossref","is-referenced-by-count":13,"title":["Checking noninterference in Timed CSP"],"prefix":"10.1145","volume":"25","author":[{"given":"A. W.","family":"Roscoe","sequence":"first","affiliation":[{"name":"Department of Computer Science, Oxford University, Parks Road, OX1 3QD, Oxford, UK"}]},{"given":"Jian","family":"Huang","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Oxford University, Parks Road, OX1 3QD, Oxford, UK"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","unstructured":"Allen PG (1991) A comparison of non-interference and non-deducibility using CSP. Proc CSFW. IEEE"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_2_1_2_3_2","unstructured":"Armstrong P Hopcroft PJ Roscoe AW (2012) Fairness analysis through priority. Forthcoming"},{"key":"e_1_2_1_2_4_2","unstructured":"Armstrong PJ Lowe G Ouaknine J Roscoe AW (2012) Model-checking Timed CSP. Forthcoming HOWARD (H. Barringer festschift) Easychair (pub)"},{"key":"e_1_2_1_2_5_2","first-page":"1","article-title":"A notion of non-interference for timed automata","volume":"51","author":"Barbuti R","year":"2002","journal-title":"Fundam Inform"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.5555\/2370741.2370744"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-1994\/1995-3103"},{"key":"e_1_2_1_2_8_2","unstructured":"Focardi R Gorrieri R Martinelli F (2000) Information flow analysis in a discrete-time process algebra. CSFW-13 IEEE"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2002.806122"},{"key":"e_1_2_1_2_10_2","unstructured":"Forster R (1999) Noninterference properties for nondeterministic processes. Oxford University DPhil thesis"},{"key":"e_1_2_1_2_11_2","unstructured":"Forster R Reed GM Roscoe AW (2000) The successes and failures of behavioural models. In: Millenial perspectives in computer science. Palgrave"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Goguen JA Meseguer J (1982) Security policies and security models. In: Proceedings of IEEE symposium on security and privacy","DOI":"10.1109\/SP.1982.10014"},{"key":"e_1_2_1_2_13_2","unstructured":"Graham-Cumming J (1992) The formal development of secure systems. Oxford University DPhil thesis"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Henzinger TA Manna Z Pnueli A (1992) What good are digital clocks? In: Proceedings of the nineteenth international colloquium on automata languages and programming (ICALP 92) vol 623. Springer\/LNCS Berlin pp 545\u2013558","DOI":"10.1007\/3-540-55719-9_103"},{"key":"e_1_2_1_2_15_2","unstructured":"Huang J (2010) Extending non-interference properties to the timed world. Oxford University DPhil thesis"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Huang J Roscoe AW (2006) Extending non-interference properties to the timed world. In: Proc ACM SAC","DOI":"10.1145\/1141277.1141363"},{"key":"e_1_2_1_2_17_2","unstructured":"Lazi\u0107 RS (1999) A semantic study of data independence with applications to model checking. Oxford University DPhil thesis"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.11.070"},{"key":"e_1_2_1_2_19_2","volume-title":"The thousand-and-one cryptographers. Reflections on the work of C.A.R. Hoare","author":"McIver AK","year":"2010"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Morgan CC (2006) The shadow knows: refinement of ignorance in sequential programs. Proc MPC LNCS 4014","DOI":"10.1007\/11783596_21"},{"key":"e_1_2_1_2_21_2","unstructured":"Ouaknine J (2001) Discrete analysis of continuous behaviour in real-time concurrent systems. Oxford University D.Phil thesis"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Ouaknine J (2002) Digitisation and full abstraction for dense-time model checking. TACAS Springer LNCS","DOI":"10.1007\/3-540-46002-0_4"},{"key":"e_1_2_1_2_23_2","first-page":"99","article-title":"Timed CSP = closed timed epsilon-automata","volume":"10","author":"Ouaknine J","year":"2003","journal-title":"Nord J Comput"},{"key":"e_1_2_1_2_24_2","unstructured":"Reed GM (1988) A uniform mathematical theory for real-time distributed computing. Oxford University DPhil thesis"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(88)90030-8"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(98)00214-X"},{"key":"e_1_2_1_2_27_2","unstructured":"Roscoe AW (1994) Model checking CSP. In: A classical mind: essays in honour of C.A.R. Hoare. Prentice Hall"},{"key":"e_1_2_1_2_28_2","unstructured":"Roscoe AW (1995) CSP and determinism in security modelling. Proceedings of IEEE symposium on security and privacy"},{"key":"e_1_2_1_2_29_2","unstructured":"Roscoe AW (1997) The theory and practice of concurrency. Prentice Hall"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.12.098"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84882-258-0"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"publisher","DOI":"10.5555\/2699889.2699892"},{"key":"e_1_2_1_2_33_2","unstructured":"Ryan PYA (1991) A CSP formulation of non-interference and unwinding. Cipher Winter 1991. IEEE Press"},{"key":"e_1_2_1_2_34_2","volume-title":"Concurrent and real-time systems: the CSP approach","author":"Schneider SA","year":"2000"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-012-0251-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-012-0251-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-012-0251-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:56:58Z","timestamp":1641484618000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-012-0251-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,1]]},"references-count":34,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2013,1]]}},"alternative-id":["10.1007\/s00165-012-0251-6"],"URL":"https:\/\/doi.org\/10.1007\/s00165-012-0251-6","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,1]]}}}