{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,22]],"date-time":"2025-04-22T05:47:27Z","timestamp":1745300847050,"version":"3.37.3"},"reference-count":34,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2020,7,27]],"date-time":"2020-07-27T00:00:00Z","timestamp":1595808000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,7,27]],"date-time":"2020-07-27T00:00:00Z","timestamp":1595808000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2021,4]]},"DOI":"10.1007\/s10817-020-09577-6","type":"journal-article","created":{"date-parts":[[2020,7,27]],"date-time":"2020-07-27T12:02:40Z","timestamp":1595851360000},"page":"463-478","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":14,"title":["Automated Proof of Bell\u2013LaPadula Security Properties"],"prefix":"10.1007","volume":"65","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9163-2609","authenticated-orcid":false,"given":"Maximiliano","family":"Cristi\u00e1","sequence":"first","affiliation":[]},{"given":"Gianfranco","family":"Rossi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,7,27]]},"reference":[{"key":"9577_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book: Assigning Programs to Meanings","author":"JR Abrial","year":"1996","unstructured":"Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, New York (1996)"},{"key":"9577_CR2","unstructured":"Anderson, J.P.: Computer security technology planning study. Techreport ESD-TR-73-51, Vol II, Deputy for Command and Management Systems, HQ Electronic Systems Division (AFSC) (1972). http:\/\/seclab.cs.ucdavis.edu\/projects\/history\/papers\/ande72.pdf"},{"issue":"1","key":"9577_CR3","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10817-017-9441-5","volume":"63","author":"G Barthe","year":"2019","unstructured":"Barthe, G., Betarte, G., Campo, J.D., Luna, C.: System-level non-interference of constant-time cryptography. Part I: model. J. Autom. Reason. 63(1), 1\u201351 (2019). https:\/\/doi.org\/10.1007\/s10817-017-9441-5","journal-title":"J. Autom. Reason."},{"issue":"6","key":"9577_CR4","doi-asserted-by":"publisher","first-page":"881","DOI":"10.3233\/JCS-130476","volume":"21","author":"G Barthe","year":"2013","unstructured":"Barthe, G., Gr\u00e9goire, B., Heraud, S., Olmedo, F., B\u00e9guelin, S.Z.: Verified indifferentiable hashing into elliptic curves. J. Comput. Secur. 21(6), 881\u2013917 (2013). https:\/\/doi.org\/10.3233\/JCS-130476","journal-title":"J. Comput. Secur."},{"key":"9577_CR5","doi-asserted-by":"publisher","first-page":"727","DOI":"10.1007\/978-3-319-10575-8_22","volume-title":"Handbook of Model Checking","author":"DA Basin","year":"2018","unstructured":"Basin, D.A., Cremers, C., Meadows, C.A.: Model checking security protocols. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 727\u2013762. Springer, Berlin (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_22"},{"key":"9577_CR6","unstructured":"Bell, D.E., LaPadula, L.: Secure Computer Systems: Mathematical Foundations. MTR 2547, The MITRE Corporation, McLean (1973)"},{"key":"9577_CR7","unstructured":"Bell, D.E., LaPadula, L.: Secure Computer Systems: Mathematical Model. ESD-TR 73-278, The MITRE Corporation, McLean (1973)"},{"key":"9577_CR8","doi-asserted-by":"publisher","unstructured":"Bonichon, R., Delahaye, D., Doligez, D.: Zenon: an extensible automated theorem prover producing checkable proofs. In: Dershowitz, N., Voronkov, A. (eds.) 14th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2007, Yerevan, Armenia, October 15\u201319, 2007, Proceedings. Lecture Notes in Computer Science, vol. 4790, pp. 151\u2013165. Springer (2007). https:\/\/doi.org\/10.1007\/978-3-540-75560-9_13","DOI":"10.1007\/978-3-540-75560-9_13"},{"key":"9577_CR9","unstructured":"Coq Development Team: The Coq Proof Assistant Reference Manual, Version 8.8.1. LogiCal Project, Palaiseau, France (2018)"},{"key":"9577_CR10","unstructured":"Cristi\u00e1, M.: Formal verification of an extension of a secure, compatible UNIX file system. In: Anales de la XXIX Conferencia Latinoamericana de Inform\u00e1tica. CLEI, La Paz, Bolivia (2003)"},{"key":"9577_CR11","doi-asserted-by":"publisher","unstructured":"Cristi\u00e1, M., Rossi, G.: A decision procedure for restricted intensional sets. In: de\u00a0Moura, L. (ed.) Automated Deduction\u2014CADE 26\u201426th International Conference on Automated Deduction, Gothenburg, Sweden, August 6\u201311, 2017, Proceedings. Lecture Notes in Computer Science, vol. 10395, pp. 185\u2013201. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-63046-5_12","DOI":"10.1007\/978-3-319-63046-5_12"},{"key":"9577_CR12","doi-asserted-by":"publisher","unstructured":"Cristi\u00e1, M., Rossi, G.: A set solver for finite set relation algebra. In: Desharnais, J., Guttmann, W., Joosten, S. (eds.) Relational and Algebraic Methods in Computer Science\u201417th International Conference, RAMiCS 2018, Groningen, The Netherlands, October 29\u2013November 1, 2018, Proceedings. Lecture Notes in Computer Science, vol. 11194, pp. 333\u2013349. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-030-02149-8_20","DOI":"10.1007\/978-3-030-02149-8_20"},{"key":"9577_CR13","unstructured":"Cristi\u00e1, M., Rossi, G.: Automated reasoning with restricted intensional sets (2019). CoRR arXiv:1910.09118"},{"issue":"2","key":"9577_CR14","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/s10817-019-09520-4","volume":"64","author":"M Cristi\u00e1","year":"2020","unstructured":"Cristi\u00e1, M., Rossi, G.: Solving quantifier-free first-order constraints over finite sets and binary relations. J. Autom. Reason. 64(2), 295\u2013330 (2020). https:\/\/doi.org\/10.1007\/s10817-019-09520-4","journal-title":"J. Autom. Reason."},{"key":"9577_CR15","first-page":"229","volume-title":"SEFM. Lecture Notes in Computer Science","author":"M Cristi\u00e1","year":"2013","unstructured":"Cristi\u00e1, M., Rossi, G., Frydman, C.S.: log as a test case generator for the Test Template Framework. In: Hierons, R.M., Merayo, M.G., Bravetti, M. (eds.) SEFM. Lecture Notes in Computer Science, vol. 8137, pp. 229\u2013243. Springer, Berlin (2013)"},{"key":"9577_CR16","unstructured":"D\u00e9n\u00e8s, M., Hritcu, C., Lampropoulos, L., Paraskevopoulou, Z., Pierce, B.C.: Quickchick: property-based testing for Coq. In: The Coq Workshop (2014)"},{"key":"9577_CR17","doi-asserted-by":"publisher","unstructured":"Devyanin, P.N., Khoroshilov, A.V., Kuliamin, V.V., Petrenko, A.K., Shchepetkov, I.V.: Formal verification of OS security model with alloy and event-b. In: Ameur, Y.A., Schewe, K. (eds.) Abstract State Machines, Alloy, B, TLA, VDM, and Z\u20144th International Conference, ABZ 2014, Toulouse, France, June 2\u20136, 2014. Proceedings. Lecture Notes in Computer Science, vol. 8477, pp. 309\u2013313. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-662-43652-3_30","DOI":"10.1007\/978-3-662-43652-3_30"},{"key":"9577_CR18","doi-asserted-by":"publisher","unstructured":"Doligez, D., Jaume, M., Rioboo, R.: Development of secured systems by mixing programs, specifications and proofs in an object-oriented programming environment: a case study within the focalize environment. In: Maffeis, S., Rezk, T. (eds.) Proceedings of the 2012 Workshop on Programming Languages and Analysis for Security, PLAS 2012, Beijing, China, 15 June, 2012, p.\u00a09. ACM (2012). https:\/\/doi.org\/10.1145\/2336717.2336726","DOI":"10.1145\/2336717.2336726"},{"issue":"5","key":"9577_CR19","doi-asserted-by":"publisher","first-page":"861","DOI":"10.1145\/365151.365169","volume":"22","author":"A Dovier","year":"2000","unstructured":"Dovier, A., Piazza, C., Pontelli, E., Rossi, G.: Sets and constraint logic programming. ACM Trans. Program. Lang. Syst. 22(5), 861\u2013931 (2000)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"6","key":"9577_CR20","doi-asserted-by":"publisher","first-page":"645","DOI":"10.1017\/S1471068406002730","volume":"6","author":"A Dovier","year":"2006","unstructured":"Dovier, A., Pontelli, E., Rossi, G.: Set unification. Theory Pract. Log Program. 6(6), 645\u2013701 (2006). https:\/\/doi.org\/10.1017\/S1471068406002730","journal-title":"Theory Pract. Log Program."},{"key":"9577_CR21","volume-title":"Building a Secure Computer System","author":"M Gasser","year":"1988","unstructured":"Gasser, M.: Building a Secure Computer System. Van Nostrand Reinhold Co., New York (1988)"},{"key":"9577_CR22","doi-asserted-by":"publisher","unstructured":"Goguen, J.A., Meseguer, J.: Security policies and security models. In: 1982 IEEE Symposium on Security and Privacy, Oakland, CA, USA, April 26\u201328, 1982, pp. 11\u201320. IEEE Computer Society (1982). https:\/\/doi.org\/10.1109\/SP.1982.10014","DOI":"10.1109\/SP.1982.10014"},{"key":"9577_CR23","doi-asserted-by":"publisher","unstructured":"Haraty, R.A., Naous, M.: Role-based access control modeling and validation. In: 2013 IEEE Symposium on Computers and Communications, ISCC 2013, Split, Croatia, 7\u201310 July, 2013, pp. 61\u201366. IEEE Computer Society (2013). https:\/\/doi.org\/10.1109\/ISCC.2013.6754925","DOI":"10.1109\/ISCC.2013.6754925"},{"issue":"2","key":"9577_CR24","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1109\/MAHC.2015.27","volume":"37","author":"SB Lipner","year":"2015","unstructured":"Lipner, S.B.: The birth and death of the orange book. IEEE Ann. Hist. Comput. 37(2), 19\u201331 (2015). https:\/\/doi.org\/10.1109\/MAHC.2015.27","journal-title":"IEEE Ann. Hist. Comput."},{"issue":"2","key":"9577_CR25","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1016\/0020-0190(85)90065-1","volume":"20","author":"J McLean","year":"1985","unstructured":"McLean, J.: A comment on the \u2019basic security theorem\u2019 of bell and lapadula. Inf. Process. Lett. 20(2), 67\u201370 (1985). https:\/\/doi.org\/10.1016\/0020-0190(85)90065-1","journal-title":"Inf. Process. Lett."},{"key":"9577_CR26","doi-asserted-by":"publisher","unstructured":"McLean, J.: Twenty years of formal methods. In: 1999 IEEE Symposium on Security and Privacy, Oakland, California, USA, May 9\u201312, 1999, pp. 115\u2013116. IEEE Computer Society (1999). https:\/\/doi.org\/10.1109\/SECPRI.1999.766907","DOI":"10.1109\/SECPRI.1999.766907"},{"key":"9577_CR27","doi-asserted-by":"publisher","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: 2013 IEEE Symposium on Security and Privacy, SP 2013, Berkeley, CA, USA, May 19\u201322, 2013, pp. 415\u2013429. IEEE Computer Society (2013). https:\/\/doi.org\/10.1109\/SP.2013.35","DOI":"10.1109\/SP.2013.35"},{"key":"9577_CR28","doi-asserted-by":"publisher","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL\u2014A Proof Assistant for Higher-Order Logic, Lecture Notes in Computer Science, vol. 2283. Springer (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9","DOI":"10.1007\/3-540-45949-9"},{"key":"9577_CR29","unstructured":"Rossi, G.: $$\\{log\\}$$ (2008). http:\/\/people.dmi.unipr.it\/gianfranco.rossi\/setlog.Home.html"},{"issue":"1","key":"9577_CR30","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1109\/JSAC.2002.806121","volume":"21","author":"A Sabelfeld","year":"2006","unstructured":"Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE J. Sel. A. Commun. 21(1), 5\u201319 (2006). https:\/\/doi.org\/10.1109\/JSAC.2002.806121","journal-title":"IEEE J. Sel. A. Commun."},{"key":"9577_CR31","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4613-9575-1","volume-title":"Programming with Sets\u2014An Introduction to SETL. Texts and Monographs in Computer Science","author":"JT Schwartz","year":"1986","unstructured":"Schwartz, J.T., Dewar, R.B.K., Dubinsky, E., Schonberg, E.: Programming with Sets\u2014An Introduction to SETL. Texts and Monographs in Computer Science. Springer, Berlin (1986). https:\/\/doi.org\/10.1007\/978-1-4613-9575-1"},{"key":"9577_CR32","volume-title":"The Z Notation: A Reference Manual","author":"JM Spivey","year":"1992","unstructured":"Spivey, J.M.: The Z Notation: A Reference Manual. Prentice Hall International (UK) Ltd., Hertfordshire (1992)"},{"key":"9577_CR33","doi-asserted-by":"publisher","unstructured":"Stasiak, A., Zielinski, Z.: An approach to automated verification of multi-level security system models. In: Zamojski, W., Mazurkiewicz, J., Sugier, J., Walkowiak, T., Kacprzyk, J. (eds.) New Results in Dependability and Computer Systems\u2014Proceedings of the 8th International Conference on Dependability and Complex Systems DepCoS-RELCOMEX, September 9\u201313, 2013, Brun\u00f3w, Poland. Advances in Intelligent Systems and Computing, vol. 224, pp. 375\u2013388. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-319-00945-2_34","DOI":"10.1007\/978-3-319-00945-2_34"},{"key":"9577_CR34","doi-asserted-by":"publisher","unstructured":"von Oheimb, D.: Information flow control revisited: Noninfluence = noninterference + nonleakage. In: Samarati, P., Ryan, P.Y.A., Gollmann, D., Molva, R. (eds.) 9th European Symposium on Research Computer Security\u2014ESORICS 2004, Sophia Antipolis, France, September 13\u201315, 2004, Proceedings. Lecture Notes in Computer Science, vol. 3193, pp. 225\u2013243. Springer (2004). https:\/\/doi.org\/10.1007\/978-3-540-30108-0_14","DOI":"10.1007\/978-3-540-30108-0_14"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-020-09577-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-020-09577-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-020-09577-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,26]],"date-time":"2021-07-26T23:32:19Z","timestamp":1627342339000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-020-09577-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,7,27]]},"references-count":34,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2021,4]]}},"alternative-id":["9577"],"URL":"https:\/\/doi.org\/10.1007\/s10817-020-09577-6","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2020,7,27]]},"assertion":[{"value":"10 December 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"16 July 2020","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"27 July 2020","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}