{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,28]],"date-time":"2025-05-28T04:21:20Z","timestamp":1748406080811,"version":"3.41.0"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319184661"},{"type":"electronic","value":"9783319184678"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","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":[[2015]]},"DOI":"10.1007\/978-3-319-18467-8_6","type":"book-chapter","created":{"date-parts":[[2015,5,8]],"date-time":"2015-05-08T12:12:03Z","timestamp":1431087123000},"page":"82-93","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Verifying Observational Determinism"],"prefix":"10.1007","author":[{"given":"Jaber","family":"Karimpour","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ayaz","family":"Isazadeh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ali A.","family":"Noroozi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,5,9]]},"reference":[{"key":"6_CR1","unstructured":"Balliu, M.: Logics for information flow security: from specification to verification (2014)"},{"key":"6_CR2","doi-asserted-by":"crossref","unstructured":"Smith, G.: Principles of secure information flow analysis. In: Malware Detection, pp. 291\u2013307. Springer, US (2007)","DOI":"10.1007\/978-0-387-44599-1_13"},{"issue":"1","key":"6_CR3","doi-asserted-by":"publisher","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 Journal on Selected Areas in Communications 21(1), 5\u201319 (2003)","journal-title":"IEEE Journal on Selected Areas in Communications"},{"issue":"5","key":"6_CR4","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1145\/360051.360056","volume":"19","author":"D Denning","year":"1976","unstructured":"Denning, D.: A lattice model of secure information flow. Communications of the ACM 19(5), 236\u2013243 (1976)","journal-title":"Communications of the ACM"},{"key":"6_CR5","unstructured":"Zdancewic, S., Myers, A.C.: Observational determinism for concurrent program security. In: Computer Security Foundations Workshop, Proceedings. 16th IEEE (2003)"},{"issue":"1","key":"6_CR6","doi-asserted-by":"crossref","first-page":"37","DOI":"10.3233\/JCS-1992-1103","volume":"1","author":"J McLean","year":"1992","unstructured":"McLean, J.: Proving noninterference and functional correctness using traces. Journal of Computer security 1(1), 37\u201357 (1992)","journal-title":"Journal of Computer security"},{"key":"6_CR7","unstructured":"Roscoe, A.W.: CSP and determinism in security modelling. In: IEEE Symposium on Security and Privacy, Proceedings (1995)"},{"key":"6_CR8","unstructured":"Huisman, M., Worah, P., Sunesen, K.: A temporal logic characterisation of observational determinism. In: Computer Security Foundations Workshop, 19th IEEE (2006)"},{"key":"6_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/978-3-642-54792-8_15","volume-title":"Principles of Security and Trust","author":"MR Clarkson","year":"2014","unstructured":"Clarkson, M.R., Finkbeiner, B., Koleini, M., Micinski, K.K., Rabe, M.N., S\u00e1nchez, C.: Temporal logics for hyperproperties. In: Abadi, M., Kremer, S. (eds.) POST 2014 (ETAPS 2014). LNCS, vol. 8414, pp. 265\u2013284. Springer, Heidelberg (2014)"},{"key":"6_CR10","volume-title":"Principles of model checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of model checking, vol. 26202649. MIT press, Cambridge (2008)"},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"Terauchi, T.: A type System for observational determinism. In: Computer Security Foundations, pp. 287\u2013300 (2008)","DOI":"10.1109\/CSF.2008.9"},{"key":"6_CR12","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0032063","volume-title":"An Efficient Algorithm for Branching Bisimulation and Stuttering Equivalence","author":"JF Groote","year":"1990","unstructured":"Groote, J.F., Vaandrager, F.: An Efficient Algorithm for Branching Bisimulation and Stuttering Equivalence. Springer, Berlin Heidelberg (1990)"},{"issue":"9","key":"6_CR13","doi-asserted-by":"publisher","first-page":"1401","DOI":"10.1109\/9.948467","volume":"46","author":"A Chutinan","year":"2001","unstructured":"Chutinan, A., Krogh, B.H.: Verification of infinite-state dynamic systems using approximate quotient transition systems. IEEE Transactions on Automatic Control 46(9), 1401\u20131410 (2001)","journal-title":"IEEE Transactions on Automatic Control"},{"key":"6_CR14","unstructured":"Ngo, T.M.: Qualitative and quantitative information flow analysis for multi-thread programs. University of Twente (2014)"},{"key":"6_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-642-27375-9_9","volume-title":"Theory of Security and Applications","author":"M Huisman","year":"2012","unstructured":"Huisman, M., Blondeel, H.-C.: Model-checking secure information flow for multi-threaded programs. In: M\u00f6dersheim, S., Palamidessi, C. (eds.) TOSCA 2011. LNCS, vol. 6993, pp. 148\u2013165. Springer, Heidelberg (2012)"},{"issue":"2","key":"6_CR16","doi-asserted-by":"crossref","first-page":"269","DOI":"10.3233\/JCS-130492","volume":"22","author":"TM Ngo","year":"2014","unstructured":"Ngo, T.M., Stoelinga, M., Huisman, M.: Effective verification of confidentiality for multi-threaded programs. Journal of Computer Security 22(2), 269\u2013300 (2014)","journal-title":"Journal of Computer Security"},{"issue":"2","key":"6_CR17","doi-asserted-by":"crossref","first-page":"167","DOI":"10.3233\/JCS-1996-42-304","volume":"4","author":"D Volpano","year":"1996","unstructured":"Volpano, D., Irvine, C., Smith, G.: A sound type system for secure flow analysis. Journal of computer security 4(2), 167\u2013187 (1996)","journal-title":"Journal of computer security"},{"key":"6_CR18","doi-asserted-by":"crossref","unstructured":"Smith, G., Volpano, D.: Secure information flow in a multi-threaded imperative language. In: Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 355\u2013364. ACM (1998)","DOI":"10.1145\/268946.268975"},{"issue":"06","key":"6_CR19","doi-asserted-by":"publisher","first-page":"1207","DOI":"10.1017\/S0960129511000193","volume":"21","author":"G Barthe","year":"2011","unstructured":"Barthe, G., D\u2019argenio, P.R., Rezk, T.: Secure information flow by self-composition. Mathematical Structures in Computer Science 21(06), 1207\u20131252 (2011)","journal-title":"Mathematical Structures in Computer Science"},{"key":"6_CR20","doi-asserted-by":"crossref","unstructured":"McLean, J.: A general theory of composition for trace sets closed under selective interleaving functions. In: IEEE Computer Society Symposium on Research in Security and Privacy, Proceedings, pp. 79\u201393 (1994)","DOI":"10.1109\/RISP.1994.296590"},{"issue":"6","key":"6_CR21","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. Journal of Computer Security 18(6), 1157\u20131210 (2010)","journal-title":"Journal of Computer Security"},{"key":"6_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-69850-0_1","volume-title":"25 Years of Model Checking","author":"EM Clarke","year":"2008","unstructured":"Clarke, E.M.: The Birth of Model Checking. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking. LNCS, vol. 5000, pp. 1\u201326. Springer, Heidelberg (2008)"},{"key":"6_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/978-3-540-69850-0_2","volume-title":"25 Years of Model Checking","author":"EA Emerson","year":"2008","unstructured":"Emerson, E.A.: The beginning of model checking: a personal perspective. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking. LNCS, vol. 5000, pp. 27\u201345. Springer, Heidelberg (2008)"},{"key":"6_CR24","unstructured":"Finkbeiner, B., Rabe, M.N., Snchez, C.: A temporal logic for hyperproperties. In: arXiv preprint arXiv:1306.6657 (2013)"},{"key":"6_CR25","doi-asserted-by":"crossref","unstructured":"Dimitrova, R., Finkbeiner, B., Kovcs, M., Rabe, M.N., Seidl, H.: Model checking information flow in reactive systems. In: Verification, Model Checking, and Abstract Interpretation, pp. 169\u2013185. Springer, Berlin Heidelberg (2012)","DOI":"10.1007\/978-3-642-27940-9_12"},{"key":"6_CR26","doi-asserted-by":"crossref","unstructured":"Mantel, H.: Unwinding possibilistic security properties. In: Computer Security-ESORICS 2000, pp. 238\u2013254. Springer, Berlin Heidelberg (2000)","DOI":"10.1007\/10722599_15"},{"issue":"1","key":"6_CR27","doi-asserted-by":"crossref","first-page":"101","DOI":"10.3233\/JCS-2010-0400","volume":"19","author":"D D\u2019Souza","year":"2011","unstructured":"D\u2019Souza, D., Holla, R., Raghavendra, K.R., Sprick, B.: Model-checking trace-based information flow properties. Journal of Computer Security 19(1), 101\u2013138 (2011)","journal-title":"Journal of Computer Security"}],"container-title":["IFIP Advances in Information and Communication Technology","ICT Systems Security and Privacy Protection"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-18467-8_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,27]],"date-time":"2025-05-27T21:22:26Z","timestamp":1748380946000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-18467-8_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319184661","9783319184678"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-18467-8_6","relation":{},"ISSN":["1868-4238","1868-422X"],"issn-type":[{"type":"print","value":"1868-4238"},{"type":"electronic","value":"1868-422X"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"9 May 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}