{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,2]],"date-time":"2025-04-02T22:10:25Z","timestamp":1743631825795,"version":"3.40.3"},"reference-count":24,"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><jats:p>The Shadow semantics is a qualitative model for noninterference security for sequential programs. In this paper, we first extend the Shadow semantics to Event-B, to reason about discrete transition systems with noninterference security properties. In particular, we investigate how these security properties can be specified and proved as machine invariants. Next we highlight the role of security invariants during refinement and identify some common patterns in specifying them. Finally, we propose a practical extension to the supporting<jats:italic>Rodin platform<\/jats:italic>of Event-B, with the possibility of having some properties to be<jats:italic>invariants-by-construction<\/jats:italic>.<\/jats:p>","DOI":"10.1007\/s00165-012-0256-1","type":"journal-article","created":{"date-parts":[[2012,6,28]],"date-time":"2012-06-28T16:06:42Z","timestamp":1340899602000},"page":"59-87","source":"Crossref","is-referenced-by-count":1,"title":["Security invariants in discrete transition systems"],"prefix":"10.1145","volume":"25","author":[{"given":"Thai Son","family":"Hoang","sequence":"first","affiliation":[{"name":"Institute of Information Security, ETH-Zurich, 8092, Zurich, Switzerland"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-010-0145-y"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Al-Bataineh OI van der Meyden R (2010) Abstraction for epistemic model checking of dining cryptographers-based protocols. CoRR. abs\/1010.2287","DOI":"10.1145\/2000378.2000408"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Back R-J (1989) Refinement Calculus II: parallel and reactive programs. In: deBakker JW deRoever WP Rozenberg G (eds) Stepwise refinement of distributed systems. Lecture notes in computer science vol 430 pp 67\u201393 Mook The Netherlands May 1989. Springer Berlin","DOI":"10.1007\/3-540-52559-9_61"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00206326"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Chandy K Misra J (1989) Parallel program design: a foundation. Addison-Wesley","DOI":"10.1007\/978-1-4613-9668-0_6"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Deharbe D Fontaine P Guyot Y Voisin L (2012) SMT solvers for Rodin. In: Proceedings of ABZ 2012 conference. LNCS no 7316. Springer Berlin","DOI":"10.1007\/978-3-642-30885-7_14"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Fagin R Halpern JY Moses Y Vardi MY (1995) Reasoning about knowledge. MIT","DOI":"10.7551\/mitpress\/5803.001.0001"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Hoang TS F\u00fcrst A Abrial J-R (2009) Event-b patterns and their tool support. In: Hung DV Krishnan P (eds) SEFM. IEEE Computer Society pp 210\u2013219","DOI":"10.1109\/SEFM.2009.17"},{"key":"e_1_2_1_2_11_2","unstructured":"Hoang TS McIver AK Meinicke L Morgan CC Sloane A Susatyo E (2011) Abstractions of non-interference security: probabilistic versus possibilistic. Form Asp Comp (to appear)"},{"key":"e_1_2_1_2_12_2","unstructured":"Halpern JY O\u2019Neill KR (2004) Anonymity and information hiding in multiagent systems. CoRR. cs.CR\/0402042"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/1410234.1410239"},{"issue":"1","key":"e_1_2_1_2_14_2","first-page":"215","article-title":"Comparing bdd and sat based techniques for model checking Chaum\u2019s dining cryptographers protocol","volume":"72","author":"Kacprzak M","year":"2006","journal-title":"Fundam Inform"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177726"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-007-0063-9"},{"key":"e_1_2_1_2_17_2","unstructured":"Maamria I (2012) Theory plug-in. http:\/\/wiki.event-b.org\/index.php\/Theory_Plug-in"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"McIver A Morgan CC (2009) Sums and lovers : case studies in security compositionality and refinement. In: Cavalcanti A Dams D (eds) FM. Lecture notes in computer science vol 5850. Springer Berlin pp 289\u2013304","DOI":"10.1007\/978-3-642-05089-3_19"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Morgan C (2006) The shadow knows : refinement of ignorance in sequential programs. In: Uustalu T (ed) MPC. Lecture notes in computer science vol 4014. Springer Berlin pp 359\u2013378","DOI":"10.1007\/11783596_21"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.09.003"},{"key":"e_1_2_1_2_21_2","unstructured":"Rivest R (1999) Unconditional secure commitment and oblivious transfer schemes using private channels and a trusted initializer. Technical report MIT November 1999. http:\/\/people.csail.mit.edu\/rivest\/Rivest-commitment.pdf"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jal.2005.12.010"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"van der Meyden R (2011) Two applications of epistemic logic in computer security. In: van Benthem J Gupta A Parikh R (eds) Proof computation and agency. Synthese library vol 352. Springer Berlin pp 133\u2013144","DOI":"10.1007\/978-94-007-0080-2_9"},{"key":"e_1_2_1_2_24_2","unstructured":"van der Meyden R Su K (2004) Symbolic model checking the knowledge of the dining cryptographers. In: CSFW IEEE Computer Society"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-012-0256-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-012-0256-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-012-0256-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,2]],"date-time":"2025-04-02T21:32:56Z","timestamp":1743629576000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-012-0256-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,1]]},"references-count":24,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2013,1]]}},"alternative-id":["10.1007\/s00165-012-0256-1"],"URL":"https:\/\/doi.org\/10.1007\/s00165-012-0256-1","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2013,1]]}}}