{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,12]],"date-time":"2026-02-12T11:36:25Z","timestamp":1770896185574,"version":"3.50.1"},"reference-count":82,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2020,7,16]],"date-time":"2020-07-16T00:00:00Z","timestamp":1594857600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2020,7,16]],"date-time":"2020-07-16T00:00:00Z","timestamp":1594857600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100000858","name":"University of Sheffield","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100000858","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2021,2]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present a case study in formally verified security for realistic systems: the information flow security verification of the functional kernel of a web application, the CoCon conference management system. We use the Isabelle theorem prover to specify and verify fine-grained confidentiality properties, as well as complementary safety and \u201ctraceback\u201d properties. The challenges posed by this development in terms of expressiveness have led to <jats:italic>bounded-deducibility security<\/jats:italic>, a novel security model and verification method generally applicable to systems describable as input\/output automata.\n<\/jats:p>","DOI":"10.1007\/s10817-020-09566-9","type":"journal-article","created":{"date-parts":[[2020,7,16]],"date-time":"2020-07-16T02:02:23Z","timestamp":1594864943000},"page":"321-356","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["CoCon: A Conference Management System with Formally Verified Document Confidentiality"],"prefix":"10.1007","volume":"65","author":[{"given":"Andrei","family":"Popescu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"Lammich","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ping","family":"Hou","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,7,16]]},"reference":[{"key":"9566_CR1","doi-asserted-by":"crossref","unstructured":"Arapinis, M., Bursuc, S., Ryan, M.: Privacy supporting cloud computing: confichair, a case study. In: POST, pp. 89\u2013108 (2012)","DOI":"10.1007\/978-3-642-28641-4_6"},{"key":"9566_CR2","doi-asserted-by":"crossref","unstructured":"Askarov, A., Chong, S.: Learning is change in knowledge: knowledge-based security for dynamic policies. In: CSF, pp. 308\u2013322 (2012)","DOI":"10.1109\/CSF.2012.31"},{"key":"9566_CR3","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-7(3:17)2011","author":"A Askarov","year":"2011","unstructured":"Askarov, A., Myers, A.C.: Attacker control and impact for confidentiality and integrity. Log. Methods Comput. Sci. (2011). https:\/\/doi.org\/10.2168\/LMCS-7(3:17)2011","journal-title":"Log. Methods Comput. Sci."},{"key":"9566_CR4","doi-asserted-by":"crossref","unstructured":"Askarov, A., Sabelfeld, A.: Gradual release: unifying declassification, encryption and key release policies. In: IEEE Symposium on Security and Privacy, pp. 207\u2013221 (2007)","DOI":"10.1109\/SP.2007.22"},{"key":"9566_CR5","doi-asserted-by":"crossref","unstructured":"Askarov, A., Sabelfeld, A.: Tight enforcement of information-release policies for dynamic languages. In: CSF, pp. 43\u201359 (2009)","DOI":"10.1109\/CSF.2009.22"},{"key":"9566_CR6","doi-asserted-by":"crossref","unstructured":"Bauerei\u00df, T., Pesenti Gritti, A., Popescu, A., Raimondi, F.: CoSMeDis: a distributed social media platform with formally verified confidentiality guarantees. In: IEEE Symposium on Security and Privacy, pp. 729\u2013748 (2017)","DOI":"10.1109\/SP.2017.24"},{"issue":"1\u20134","key":"9566_CR7","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/s10817-017-9443-3","volume":"61","author":"T Bauerei\u00df","year":"2018","unstructured":"Bauerei\u00df, T., Pesenti Gritti, A., Popescu, A., Raimondi, F.: CoSMed: a confidentiality-verified social media platform. J. Autom. Reason. 61(1\u20134), 113\u2013139 (2018)","journal-title":"J. Autom. Reason."},{"key":"9566_CR8","doi-asserted-by":"crossref","unstructured":"Bell, E.D., La Padula, J.L.: Secure computer system: unified exposition and multics interpretation, 1975. Technical Report MTR-2997, MITRE, Bedford, MA","DOI":"10.21236\/ADA023588"},{"key":"9566_CR9","doi-asserted-by":"crossref","unstructured":"Bichhawat, A., Rajani, V., Garg, D., Hammer, C.: Information flow control in WebKit\u2019s JavaScript bytecode. In: POST, pp. 159\u2013178 (2014)","DOI":"10.1007\/978-3-642-54792-8_9"},{"key":"9566_CR10","unstructured":"Blanchet, B., Abadi, M., Fournet, C.: Automated verification of selected equivalences for security protocols. In: LICS, pp. 331\u2013340 (2005)"},{"key":"9566_CR11","series-title":"Lecture Notes in Computer Science","volume-title":"Interactive Theorem Proving: 7th International Conference, ITP 2016, Nancy, France, August 22\u201325, 2016, Proceedings","year":"2016","unstructured":"Blanchette, J.C., Merz, S. (eds.): Interactive Theorem Proving: 7th International Conference, ITP 2016, Nancy, France, August 22\u201325, 2016, Proceedings. Lecture Notes in Computer Science, vol. 9807. Springer, Berlin (2016)"},{"issue":"4\u20135","key":"9566_CR12","doi-asserted-by":"publisher","first-page":"323","DOI":"10.3233\/JCS-15791","volume":"25","author":"N Broberg","year":"2017","unstructured":"Broberg, N., van Delft, B., Sands, D.: Paragon: practical programming with information flow control. J. Comput. Secur. 25(4\u20135), 323\u2013365 (2017)","journal-title":"J. Comput. Secur."},{"key":"9566_CR13","doi-asserted-by":"crossref","unstructured":"Chlipala, A.: Ur\/Web: a simple model for programming the web. In: POPL, pp. 153\u2013165 (2015)","DOI":"10.1145\/2775051.2677004"},{"key":"9566_CR14","doi-asserted-by":"crossref","unstructured":"Chugh, R., Meister, J.A., Jhala, R., Lerner, S.: Staged information flow for Javascript. In: PLDI, pp. 50\u201362 (2009)","DOI":"10.1145\/1543135.1542483"},{"key":"9566_CR15","doi-asserted-by":"crossref","unstructured":"Clarkson, M.R., Finkbeiner, B., Koleini, M., Micinski, K.K., Rabe, M.N., S\u00e1nchez, C.: Temporal logics for hyperproperties. In: POST, pp. 265\u2013284 (2014)","DOI":"10.1007\/978-3-642-54792-8_15"},{"key":"9566_CR16","doi-asserted-by":"crossref","unstructured":"Cohen, E.S.: Information transmission in computational systems. In: SOSP, pp. 133\u2013139 (1977)","DOI":"10.1145\/1067625.806556"},{"key":"9566_CR17","doi-asserted-by":"crossref","unstructured":"Dam, M., Guanciale, R., Khakpour, N., Nemati, H., Schwarz, O.: Formal verification of information flow security for a simple ARM-based separation kernel. In: CCS, pp. 223\u2013234 (2013)","DOI":"10.1145\/2508859.2516702"},{"issue":"6","key":"9566_CR18","doi-asserted-by":"publisher","first-page":"689","DOI":"10.3233\/JCS-15784","volume":"24","author":"AA de Amorim","year":"2016","unstructured":"de Amorim, A.A., Collins, N., DeHon, A., Demange, D., Hritcu, C., Pichardie, D., Pierce, B.C., Pollack, R., Tolmach, A.: A verified information-flow architecture. J. Comput. Secur. 24(6), 689\u2013734 (2016)","journal-title":"J. Comput. Secur."},{"key":"9566_CR19","series-title":"Lecture Notes in Computer Science","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods\u201424th International Conference, TABLEAUX 2015, Wroc\u0142aw, Poland, September 21\u201324, 2015. Proceedings","year":"2015","unstructured":"de Nivelle, H. (ed.): Automated Reasoning with Analytic Tableaux and Related Methods\u201424th International Conference, TABLEAUX 2015, Wroc\u0142aw, Poland, September 21\u201324, 2015. Proceedings. Lecture Notes in Computer Science, vol. 9323. Springer, Berlin (2015)"},{"key":"9566_CR20","doi-asserted-by":"crossref","unstructured":"Dimitrova, R., Finkbeiner, B., Kov\u00e1cs, M., Rabe, M.N., Seidl, H.: Model checking information flow in reactive systems. In: VMCAI, pp. 169\u2013185 (2012)","DOI":"10.1007\/978-3-642-27940-9_12"},{"key":"9566_CR21","doi-asserted-by":"crossref","unstructured":"Esparza, J., Lammich, P., Neumann, R., Nipkow, T., Schimpf, A., Smaus, J.: A fully verified executable LTL model checker. In: CAV, pp. 463\u2013478 (2013)","DOI":"10.1007\/978-3-642-39799-8_31"},{"key":"9566_CR22","doi-asserted-by":"crossref","unstructured":"Finkbeiner, B., Rabe, M.N., S\u00e1nchez, C.: Algorithms for model checking hyperltl and hyperctl $$^*$$. In: CAV, pp. 30\u201348","DOI":"10.1007\/978-3-319-21690-4_3"},{"key":"9566_CR23","doi-asserted-by":"crossref","unstructured":"Focardi, R., Gorrieri, R.: Classification of security properties (part I: information flow). In: FOSAD, pp. 331\u2013396 (2000)","DOI":"10.1007\/3-540-45608-2_6"},{"issue":"4\u20135","key":"9566_CR24","doi-asserted-by":"publisher","first-page":"427","DOI":"10.3233\/JCS-15801","volume":"25","author":"DB Giffin","year":"2017","unstructured":"Giffin, D.B., Levy, A., Stefan, D., Terei, D., Mazi\u00e8res, D., Mitchell, J.C., Russo, A.: Hails: protecting data privacy in untrusted web applications. J. Comput. Secur. 25(4\u20135), 427\u2013461 (2017)","journal-title":"J. Comput. Secur."},{"key":"9566_CR25","doi-asserted-by":"crossref","unstructured":"Goguen, J.A., Meseguer, J.: Security policies and security models. In: IEEE Symposium on Security and Privacy, pp. 11\u201320 (1982)","DOI":"10.1109\/SP.1982.10014"},{"key":"9566_CR26","doi-asserted-by":"crossref","unstructured":"Goguen, J.A., Meseguer, J.: Unwinding and inference control. In: IEEE Symposium on Security and Privacy, pp. 75\u201387 (1984)","DOI":"10.1109\/SP.1984.10019"},{"key":"9566_CR27","volume-title":"Computer Security","author":"D Gollmann","year":"2005","unstructured":"Gollmann, D.: Computer Security, 2nd edn. Wiley, New York (2005)","edition":"2"},{"key":"9566_CR28","doi-asserted-by":"crossref","unstructured":"Greiner, S., Grahl, D.: Non-interference with what-declassification in component-based systems. In: CSF, pp. 253\u2013267. IEEE Computer Society (2016)","DOI":"10.1109\/CSF.2016.25"},{"key":"9566_CR29","unstructured":"Groef, W.D., Devriese, D., Nikiforakis, N., Piessens, F.: FlowFox: a web browser with flexible and precise information flow control. In: CCS, pp. 748\u2013759 (2012)"},{"key":"9566_CR30","doi-asserted-by":"crossref","unstructured":"Guttman, J.D., Rowe, P.D.: A cut principle for information flow. In: Fournet, C., Hicks, M.W., Vigan\u00f2, L. (eds.) IEEE 28th Computer Security Foundations Symposium, CSF 2015, Verona, Italy, 13\u201317 July 2015, pp. 107\u2013121. IEEE (2015)","DOI":"10.1109\/CSF.2015.15"},{"key":"9566_CR31","unstructured":"Haftmann, F.: Code generation from specifications in higher-order logic. Ph.D. thesis, Technische Universit\u00e4t M\u00fcnchen (2009)"},{"key":"9566_CR32","first-page":"103","volume":"2010","author":"F Haftmann","year":"2010","unstructured":"Haftmann, F., Nipkow, T.: Code generation via higher-order rewrite systems. FLOPS 2010, 103\u2013117 (2010)","journal-title":"FLOPS"},{"issue":"1","key":"9566_CR33","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1410234.1410239","volume":"12","author":"JY Halpern","year":"2008","unstructured":"Halpern, J.Y., O\u2019Neill, K.R.: Secrecy in multiagent systems. ACM Trans. Inf. Syst. Secur. 12(1), 1\u201347 (2008)","journal-title":"ACM Trans. Inf. Syst. Secur."},{"key":"9566_CR34","doi-asserted-by":"crossref","unstructured":"Hardin, D.S., Smith, E.W., Young, W.D.: A robust machine code proof framework for highly secure applications. In: Manolios, P., Wilding, M. (eds.) ACL2, pp. 11\u201320 (2006)","DOI":"10.1145\/1217975.1217978"},{"key":"9566_CR35","unstructured":"Hawblitzel, C., Howell, J., Lorch, J.R., Narayan, A., Parno, B., Zhang, D., Zill, B.: Ironclad apps: end-to-end security via automated full-system verification. In: USENIX, pp. 165\u2013181 (2014)"},{"key":"9566_CR36","unstructured":"Hou, P., Lammich, P., Popescu, A.: This paper\u2019s website. http:\/\/andreipopescu.uk\/papers\/CoConExtended.html"},{"key":"9566_CR37","unstructured":"Jang, D., Tatlock, Z., Lerner, S.: Establishing browser security guarantees through formal shim verification. In: USENIX Security, pp. 113\u2013128 (2012)"},{"key":"9566_CR38","unstructured":"Jif: Java + information flow, 2014. http:\/\/www.cs.cornell.edu\/jif"},{"key":"9566_CR39","doi-asserted-by":"crossref","unstructured":"Kanav, S., Lammich, P., Popescu, A.: A conference management system with verified document confidentiality. In: CAV, pp. 167\u2013183 (2014)","DOI":"10.1007\/978-3-319-08867-9_11"},{"issue":"6","key":"9566_CR40","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1743546.1743574","volume":"53","author":"G Klein","year":"2010","unstructured":"Klein, G., Andronick, J., Elphinstone, K., Heiser, G., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: Formal verification of an operating-system kernel. Commun. ACM 53(6), 107\u2013115 (2010)","journal-title":"Commun. ACM"},{"key":"9566_CR41","doi-asserted-by":"crossref","unstructured":"Kozyri, E., Arden, O., Myers, A.C., Schneider, F.B.: JRIF: reactive information flow control for java. In: Foundations of Security, Protocols, and Equational Reasoning\u2014Essays Dedicated to Catherine A. Meadows, pp. 70\u201388 (2019)","DOI":"10.1007\/978-3-030-19052-1_7"},{"key":"9566_CR42","doi-asserted-by":"crossref","unstructured":"Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: CakeML: a verified implementation of ML. In: POPL, pp. 179\u2013192 (2014)","DOI":"10.1145\/2578855.2535841"},{"issue":"1","key":"9566_CR43","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1145\/775265.775268","volume":"8","author":"BW Lampson","year":"1974","unstructured":"Lampson, B.W.: Protection. Oper. Syst. Rev. 8(1), 18\u201324 (1974)","journal-title":"Oper. Syst. Rev."},{"issue":"7","key":"9566_CR44","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"issue":"4\u20135","key":"9566_CR45","doi-asserted-by":"publisher","first-page":"367","DOI":"10.3233\/JCS-15805","volume":"25","author":"J Liu","year":"2017","unstructured":"Liu, J., Arden, O., George, M.D., Myers, A.C.: Fabric: building open distributed systems securely by construction. J. Comput. Secur. 25(4\u20135), 367\u2013426 (2017)","journal-title":"J. Comput. Secur."},{"key":"9566_CR46","doi-asserted-by":"crossref","unstructured":"Lochbihler, A.: Java and the Java memory model\u2014a unified, machine-checked formalisation. In: ESOP, pp. 497\u2013517 (2012)","DOI":"10.1007\/978-3-642-28869-2_25"},{"key":"9566_CR47","doi-asserted-by":"crossref","unstructured":"Mantel, H.: Information flow control and applications\u2014bridging a gap. In: FME, pp. 153\u2013172 (2001)","DOI":"10.1007\/3-540-45251-6_9"},{"key":"9566_CR48","unstructured":"Mantel, H.: A uniform framework for the formal specification and verification of information flow security. Ph.D. thesis, University of Saarbr\u00fccken (2003)"},{"key":"9566_CR49","doi-asserted-by":"crossref","unstructured":"Mantel, H.: Information flow and noninterference. In: Encyclopedia of Cryptography and Security (2nd Ed.), pp. 605\u2013607 (2011)","DOI":"10.1007\/978-1-4419-5906-5_874"},{"key":"9566_CR50","doi-asserted-by":"crossref","unstructured":"McCullough, D.: Specifications for multi-level security and a hook-up property. In: IEEE Symposium on Security and Privacy (1987)","DOI":"10.1109\/SP.1987.10009"},{"key":"9566_CR51","unstructured":"McLean, J.: A general theory of composition for trace sets closed under selective interleaving functions. In: Proceedings of the IEEE Symposium on Security and Privacy, pp. 79\u201393 (1994)"},{"key":"9566_CR52","unstructured":"McLean, J.: Security models. In: Encyclopedia of Software Engineering (1994)"},{"key":"9566_CR53","unstructured":"Mehta, A., Elnikety, E., Harvey, K., Garg, D., Druschel, P.: Qapla: policy compliance for database-backed systems. In: USENIX Security, pp. 1463\u20131479 (2017)"},{"key":"9566_CR54","volume-title":"Communication and Concurrency","author":"R Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. Prentice Hall, Upper Saddle River (1989)"},{"issue":"9","key":"9566_CR55","doi-asserted-by":"publisher","first-page":"913","DOI":"10.1109\/12.713311","volume":"47","author":"JS Moore","year":"1998","unstructured":"Moore, J.S., Lynch, T.W., Kaufmann, M.: A mechanically checked proof of the amd5$${}_{\\text{ k }}$$86$${}^{\\text{ tm }}$$ floating point division program. IEEE Trans. Comput. 47(9), 913\u2013926 (1998)","journal-title":"IEEE Trans. Comput."},{"key":"9566_CR56","doi-asserted-by":"crossref","unstructured":"Murray, T.C., Matichuk, D., Brassil, M., Gammie, P., Bourke, T., Seefried, S., Lewis, C., Gao, X., Klein, G.: seL4: From general purpose to a proof of information flow enforcement. In: Security and Privacy, pp. 415\u2013429 (2013)","DOI":"10.1109\/SP.2013.35"},{"key":"9566_CR57","doi-asserted-by":"crossref","unstructured":"Murray, T.C., Matichuk, D., Brassil, M., Gammie, P., Klein, G.: Noninterference for operating system kernels. In: CPP, pp. 126\u2013142 (2012)","DOI":"10.1007\/978-3-642-35308-6_12"},{"issue":"4\u20135","key":"9566_CR58","doi-asserted-by":"publisher","first-page":"319","DOI":"10.3233\/JCS-0559","volume":"25","author":"TC Murray","year":"2017","unstructured":"Murray, T.C., Sabelfeld, A., Bauer, L.: Special issue on verified information flow security. J. Comput. Secur. 25(4\u20135), 319\u2013321 (2017)","journal-title":"J. Comput. Secur."},{"key":"9566_CR59","doi-asserted-by":"crossref","unstructured":"Murray, T.C., Sison, R., Engelhardt, K.: COVERN: a logic for compositional verification of information flow control. In: EuroS&P, pp. 16\u201330. IEEE (2018)","DOI":"10.1109\/EuroSP.2018.00010"},{"key":"9566_CR60","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10542-0","volume-title":"Concrete Semantics: With Isabelle\/HOL","author":"T Nipkow","year":"2014","unstructured":"Nipkow, T., Klein, G.: Concrete Semantics: With Isabelle\/HOL. Springer, Berlin (2014)"},{"key":"9566_CR61","series-title":"LNCS","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Berlin (2002)"},{"key":"9566_CR62","unstructured":"O\u2019Halloran, C.: A calculus of information flow. In: ESORICS, pp. 147\u2013159 (1990)"},{"issue":"9","key":"9566_CR63","doi-asserted-by":"publisher","first-page":"737","DOI":"10.1145\/359588.359597","volume":"21","author":"GJ Popek","year":"1978","unstructured":"Popek, G.J., Farber, D.A.: A model for verification of data security in operating systems. Commun. ACM 21(9), 737\u2013749 (1978)","journal-title":"Commun. ACM"},{"key":"9566_CR64","unstructured":"Rabe, M.N., Lammich, P., Popescu, A.: A shallow embedding of hyperctl. Archive of Formal Proofs, 2014 (2014)"},{"key":"9566_CR65","unstructured":"Reliably Secure software systems (RS3): priority program of the German research foundation (DFG), (2019). https:\/\/www.spp-rs3.de"},{"key":"9566_CR66","volume-title":"Reasoning About Knowledge","author":"YM Ronald Fagin","year":"2003","unstructured":"Ronald Fagin, Y.M., Halpern, J.Y., Vardi, M.: Reasoning About Knowledge. MIT Press, Cambridge (2003)"},{"key":"9566_CR67","unstructured":"Rushby, J.: Noninterference, transitivity, and channel-control security policies. Technical report, Dec (1992)"},{"key":"9566_CR68","doi-asserted-by":"crossref","unstructured":"Ryan, P.Y.A.: Mathematical models of computer security. In: FOSAD, pp. 1\u201362 (2000)","DOI":"10.1007\/3-540-45608-2_1"},{"issue":"1","key":"9566_CR69","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 J. Sel. Areas Commun. 21(1), 5\u201319 (2003)","journal-title":"IEEE J. Sel. Areas Commun."},{"key":"9566_CR70","doi-asserted-by":"crossref","unstructured":"Sabelfeld, A., Myers, A.C.: A model for delimited information release. In: ISSS, pp. 174\u2013191 (2003)","DOI":"10.1007\/978-3-540-37621-7_9"},{"issue":"5","key":"9566_CR71","doi-asserted-by":"publisher","first-page":"517","DOI":"10.3233\/JCS-2009-0352","volume":"17","author":"A Sabelfeld","year":"2009","unstructured":"Sabelfeld, A., Sands, D.: Declassification: dimensions and principles. J. Comput. Secur. 17(5), 517\u2013548 (2009)","journal-title":"J. Comput. Secur."},{"issue":"5","key":"9566_CR72","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1017\/S0960129598002527","volume":"8","author":"D Sangiorgi","year":"1998","unstructured":"Sangiorgi, D.: On the bisimulation proof method. Math. Struct. Comput. Sci. 8(5), 447\u2013479 (1998)","journal-title":"Math. Struct. Comput. Sci."},{"key":"9566_CR73","unstructured":"SPARK, 2014. http:\/\/www.spark-2014.org"},{"key":"9566_CR74","unstructured":"Sutherland, D.: A model of information. In: 9th National Security Conference, pp. 175\u2013183 (1986)"},{"key":"9566_CR75","unstructured":"The Redis System. https:\/\/redis.io, 2019"},{"key":"9566_CR76","unstructured":"The EasyChair conference system, 2014. http:\/\/easychair.org"},{"key":"9566_CR77","unstructured":"The HotCRP conference management system, 2014. http:\/\/read.seas.harvard.edu\/~kohler\/hotcrp"},{"key":"9566_CR78","unstructured":"The Scalatra Web Framework, 2019. http:\/\/scalatra.org\/"},{"key":"9566_CR79","doi-asserted-by":"crossref","unstructured":"Wimmer, S., Lammich, P.: Verified model checking of timed automata. In: TACAS, pp. 61\u201378 (2018)","DOI":"10.1007\/978-3-319-89960-2_4"},{"issue":"4","key":"9566_CR80","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1002\/sec.574","volume":"9","author":"Z Xiao","year":"2016","unstructured":"Xiao, Z., Kathiresshan, N., Xiao, Y.: A survey of accountability in computer networks and distributed systems. Secur. Commun. Netw. 9(4), 290\u2013315 (2016)","journal-title":"Secur. Commun. Netw."},{"key":"9566_CR81","doi-asserted-by":"crossref","unstructured":"Yang, J., Yessenov, K., Solar-Lezama, A.: A language for automatically enforcing privacy policies. In: POPL, pp. 85\u201396 (2012)","DOI":"10.1145\/2103621.2103669"},{"key":"9566_CR82","unstructured":"Zdancewic, S., Myers, A.C.: Robust declassification. In: CSFW, pp. 15\u201323 (2001)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-020-09566-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-020-09566-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-020-09566-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,15]],"date-time":"2021-07-15T23:47:02Z","timestamp":1626392822000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-020-09566-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,7,16]]},"references-count":82,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2021,2]]}},"alternative-id":["9566"],"URL":"https:\/\/doi.org\/10.1007\/s10817-020-09566-9","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,7,16]]},"assertion":[{"value":"26 September 2018","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"23 May 2020","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"16 July 2020","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}