{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,13]],"date-time":"2026-06-13T16:08:25Z","timestamp":1781366905279,"version":"3.54.1"},"reference-count":30,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2021,1,8]],"date-time":"2021-01-08T00:00:00Z","timestamp":1610064000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,8]],"date-time":"2021-01-08T00:00:00Z","timestamp":1610064000000},"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":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2021,10]]},"DOI":"10.1007\/s10009-020-00600-0","type":"journal-article","created":{"date-parts":[[2021,1,8]],"date-time":"2021-01-08T15:03:19Z","timestamp":1610118199000},"page":"685-700","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Specifying and verifying usage control models and policies in TLA$$^+$$"],"prefix":"10.1007","volume":"23","author":[{"given":"Christos","family":"Grompanopoulos","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Antonios","family":"Gouglidis","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Anastasia","family":"Mavridou","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2021,1,8]]},"reference":[{"key":"600_CR1","unstructured":"Andoni, A., Daniliuc, D., Khurshid, S., Marinov, D.: Evaluating the \u201csmall scope hypothesis\u201d. In: In Popl, vol.\u00a02. Citeseer (2003)"},{"key":"600_CR2","doi-asserted-by":"crossref","unstructured":"Backes, J., Bolignano, P., Cook, B., Dodge, C., Gacek, A., Luckow, K., Rungta, N., Tkachuk, O., Varming, C.: Semantic-based automated reasoning for aws access policies using smt. In: 2018 Formal Methods in Computer Aided Design (FMCAD), pp. 1\u20139. IEEE (2018)","DOI":"10.23919\/FMCAD.2018.8602994"},{"key":"600_CR3","unstructured":"Cau, A., Moszkowski, B., Zedan, H.: Interval temporal logic. https:\/\/www.cms.dmu.ac.uk\/cau\/itlhomepage\/itlhomepage.html (2006)"},{"key":"600_CR4","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: Nusmv 2: An opensource tool for symbolic model checking. In: International Conference on Computer Aided Verification, pp. 359\u2013364. Springer (2002)","DOI":"10.1007\/3-540-45657-0_29"},{"key":"600_CR5","doi-asserted-by":"crossref","unstructured":"Gouglidis, A., Grompanopoulos, C., Mavridou, A.: Formal verification of usage control models: A case study of usecon using tla+. arXiv preprint arXiv:1806.09848 (2018)","DOI":"10.4204\/EPTCS.272.5"},{"issue":"2","key":"600_CR6","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/s10207-013-0205-x","volume":"13","author":"A Gouglidis","year":"2014","unstructured":"Gouglidis, A., Mavridis, I., Hu, V.C.: Security policy verification for multi-domains in cloud systems. Int. J. Inf. Sec. 13(2), 97\u2013111 (2014). https:\/\/doi.org\/10.1007\/s10207-013-0205-x","journal-title":"Int. J. Inf. Sec."},{"key":"600_CR7","unstructured":"Grompanopoulos, C., Gouglidis, A.: UseCON specification. https:\/\/github.com\/agouglidis\/UseCON-TLA_PLUS (2020)"},{"key":"600_CR8","doi-asserted-by":"publisher","unstructured":"Grompanopoulos, C., Gouglidis, A., Mavridis, I.: A use-based approach for enhancing UCON. In: Security and Trust Management - 8th International Workshop, STM 2012, Pisa, Italy, September 13-14, 2012, Revised Selected Papers, pp. 81\u201396 (2012). https:\/\/doi.org\/10.1007\/978-3-642-38004-4_6","DOI":"10.1007\/978-3-642-38004-4_6"},{"key":"600_CR9","volume-title":"The SPIN model checker: Primer and reference manual","author":"GJ Holzmann","year":"2004","unstructured":"Holzmann, G.J.: The SPIN model checker: Primer and reference manual, vol. 1003. Addison-Wesley, Reading (2004)"},{"key":"600_CR10","doi-asserted-by":"crossref","unstructured":"Hu, V., Iorga, M., Bao, W., Li, A., Li, Q., Gouglidis, A.: General access control guidance for cloud systems. Tech. rep, National Institute of Standards and Technology (2020)","DOI":"10.6028\/NIST.SP.800-210"},{"key":"600_CR11","doi-asserted-by":"publisher","first-page":"192","DOI":"10.6028\/NIST.SP.800-192","volume":"800","author":"VC Hu","year":"2017","unstructured":"Hu, V.C., Kuhn, R., Yaga, D.: Verification and test methods for access control policies\/models. NIST Spec. Publ. 800, 192 (2017). https:\/\/doi.org\/10.6028\/NIST.SP.800-192","journal-title":"NIST Spec. Publ."},{"key":"600_CR12","volume-title":"Software Abstractions: Logic, Language, and Analysis","author":"D Jackson","year":"2012","unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT press, Cambridge (2012)"},{"key":"600_CR13","doi-asserted-by":"crossref","unstructured":"Janicke, H., Cau, A., Zedan, H.: A note on the formalisation of UCON. In: Proceedings of the 12th ACM symposium on Access control models and technologies, SACMAT \u201907, pp. 163\u2013168. ACM, New York, NY, USA (2007)","DOI":"10.1145\/1266840.1266867"},{"issue":"3","key":"600_CR14","doi-asserted-by":"publisher","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L Lamport","year":"1994","unstructured":"Lamport, L.: The temporal logic of actions. ACM Trans. Progr. Lang. Syst. (TOPLAS) 16(3), 872\u2013923 (1994)","journal-title":"ACM Trans. Progr. Lang. Syst. (TOPLAS)"},{"key":"600_CR15","volume-title":"Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers","author":"L Lamport","year":"2002","unstructured":"Lamport, L.: Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, Boston (2002)"},{"issue":"2","key":"600_CR16","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1016\/j.cosrev.2010.02.002","volume":"4","author":"A Lazouski","year":"2010","unstructured":"Lazouski, A., Martinelli, F., Mori, P.: Usage control in computer security: A survey. Comput. Sci. Rev. 4(2), 81\u201399 (2010). https:\/\/doi.org\/10.1016\/j.cosrev.2010.02.002","journal-title":"Comput. Sci. Rev."},{"issue":"5","key":"600_CR17","doi-asserted-by":"publisher","first-page":"1508","DOI":"10.1587\/transcom.E95.B.1508","volume":"95\u2013B","author":"J Lu","year":"2012","unstructured":"Lu, J., Li, R., Hu, J., Xu, D.: Static enforcement of static separation-of-duty policies in usage control authorization models. IEICE Trans. 95\u2013B(5), 1508\u20131518 (2012)","journal-title":"IEICE Trans."},{"key":"600_CR18","unstructured":"Macedo, N., Cunha, A.: Alloy meets TLA+: An exploratory study. arXiv preprint arXiv:1603.03599 (2016)"},{"issue":"7","key":"600_CR19","doi-asserted-by":"publisher","first-page":"1032","DOI":"10.1016\/j.future.2009.12.005","volume":"26","author":"F Martinelli","year":"2010","unstructured":"Martinelli, F., Mori, P.: On usage control for grid systems. Future Gener. Comput. Syst. 26(7), 1032\u20131042 (2010). https:\/\/doi.org\/10.1016\/j.future.2009.12.005","journal-title":"Future Gener. Comput. Syst."},{"key":"600_CR20","unstructured":"Oetsch, J., Prischink, M., P\u00fchrer, J., Schwengerer, M., Tompits, H.: On the small-scope hypothesis for testing answer-set programs. In: Thirteenth International Conference on the Principles of Knowledge Representation and Reasoning (2012)"},{"key":"600_CR21","doi-asserted-by":"publisher","unstructured":"Pretschner, A., Ruesch, J., Schaefer, C., Walter, T.: Formal analyses of usage control policies. In: Availability, Reliability and Security, 2009. ARES \u201909. International Conference on, pp. 98\u2013105 (2009). https:\/\/doi.org\/10.1109\/ARES.2009.100","DOI":"10.1109\/ARES.2009.100"},{"key":"600_CR22","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-642-14478-3_22","volume-title":"Recent Trends in Network Security and Applications, Communications in Computer and Information Science","author":"P Rajkumar","year":"2010","unstructured":"Rajkumar, P., Ghosh, S., Dasgupta, P.: Concurrent usage control implementation verification using the spin model checker. In: Meghanathan, N., Boumerdassi, S., Chaki, N., Nagamalai, D. (eds.) Recent Trends in Network Security and Applications, Communications in Computer and Information Science, vol. 89, pp. 214\u2013223. Springer, Berlin Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14478-3_22"},{"key":"600_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-642-34601-9_2","volume-title":"Network and System Security","author":"S Ranise","year":"2012","unstructured":"Ranise, S., Armando, A.: On the automated analysis of safety in usage control: A new decidability result. In: Xu, L., Bertino, E., Mu, Y. (eds.) Network and System Security. Lecture Notes in Computer Science, vol. 7645, pp. 15\u201328. Springer, Berlin Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-34601-9_2"},{"key":"600_CR24","doi-asserted-by":"crossref","unstructured":"Samarati, P., de\u00a0Vimercati, S.C.: Access control: Policies, models, and mechanisms. In: International School on Foundations of Security Analysis and Design, pp. 137\u2013196. Springer (2000)","DOI":"10.1007\/3-540-45608-2_3"},{"key":"600_CR25","unstructured":"Yuan, D., Luo, Y., Zhuang, X., Rodrigues, G.R., Zhao, X., Zhang, Y., Jain, P.U., Stumm, M.: Simple testing can prevent most critical failures: An analysis of production failures in distributed data-intensive systems. In: 11th $$\\{$$USENIX$$\\}$$ Symposium on Operating Systems Design and Implementation ($$\\{$$OSDI$$\\}$$ 14), pp. 249\u2013265 (2014)"},{"issue":"2","key":"600_CR26","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1145\/2185376.2185383","volume":"42","author":"P Zave","year":"2012","unstructured":"Zave, P.: Using lightweight modeling to understand chord. ACM SIGCOMM Comput. Commun. Rev. 42(2), 49\u201357 (2012)","journal-title":"ACM SIGCOMM Comput. Commun. Rev."},{"key":"600_CR27","doi-asserted-by":"publisher","unstructured":"Zhang, X., Nakae, M., Covington, M.J., Sandhu, R.S.: Toward a usage-based security framework for collaborative computing systems. ACM Trans. Inf. Syst. Secur. 11(1), 3:1\u20133:36 (2008). https:\/\/doi.org\/10.1145\/1330295.1330298","DOI":"10.1145\/1330295.1330298"},{"key":"600_CR28","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1145\/1108906.1108908","volume":"8","author":"X Zhang","year":"2005","unstructured":"Zhang, X., Parisi-Presicce, F., Sandhu, R., Park, J.: Formal model and policy specification of usage control. ACM Trans. Inf. Syst. Secur. 8, 351\u2013387 (2005)","journal-title":"ACM Trans. Inf. Syst. Secur."},{"key":"600_CR29","doi-asserted-by":"crossref","unstructured":"Zhang, X., Sandhu, R., Parisi-Presicce, F.: Safety analysis of usage control authorization models. In: Proceedings of the 2006 ACM Symposium on Information, Computer and Communications Security, ASIACCS \u201906, pp. 243\u2013254. ACM, New York, NY, USA (2006)","DOI":"10.1145\/1128817.1128853"},{"key":"600_CR30","unstructured":"Zhang, X., Sandhu, R.S., Parisi-Presicce, F.: Formal model and analysis of usage control. George Mason University, Fairfax (2006)"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-020-00600-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-020-00600-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-020-00600-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,26]],"date-time":"2021-11-26T12:06:16Z","timestamp":1637928376000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-020-00600-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,8]]},"references-count":30,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2021,10]]}},"alternative-id":["600"],"URL":"https:\/\/doi.org\/10.1007\/s10009-020-00600-0","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,1,8]]},"assertion":[{"value":"10 December 2020","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"8 January 2021","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}