{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,25]],"date-time":"2026-02-25T15:13:27Z","timestamp":1772032407013,"version":"3.50.1"},"reference-count":11,"publisher":"Open Publishing Association","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electron. Proc. Theor. Comput. Sci.","EPTCS"],"DOI":"10.4204\/eptcs.272.5","type":"journal-article","created":{"date-parts":[[2018,6,25]],"date-time":"2018-06-25T08:47:06Z","timestamp":1529916426000},"page":"52-64","source":"Crossref","is-referenced-by-count":4,"title":["Formal Verification of Usage Control Models: A Case Study of UseCON Using TLA+"],"prefix":"10.4204","volume":"272","author":[{"given":"Antonios","family":"Gouglidis","sequence":"first","affiliation":[{"name":"School of Computing and Communications, Lancaster University, Lancaster, UK"}]},{"given":"Christos","family":"Grompanopoulos","sequence":"additional","affiliation":[{"name":"Department of Mechanical Engineering, University of Western Macedonia, Kozani, Greece"}]},{"given":"Anastasia","family":"Mavridou","sequence":"additional","affiliation":[{"name":"Institute for Software Integrated Systems, Vanderbilt University, Nashville, TN, USA"}]}],"member":"2720","published-online":{"date-parts":[[2018,6,25]]},"reference":[{"key":"TLATools","volume-title":"TLA+ Tools","author":"Corporation"},{"issue":"2","key":"gouglidis2014security","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/s10207-013-0205-x","article-title":"Security policy verification for multi-domains in cloud systems","volume":"13","author":"Gouglidis","year":"2014","journal-title":"Int. J. Inf. Sec."},{"key":"grompanopoulos2012use","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/978-3-642-38004-4_6","article-title":"A Use-Based Approach for Enhancing UCON","volume-title":"Security and Trust Management - 8th International Workshop, STM 2012, Pisa, Italy, September 13-14, 2012, Revised Selected Papers","author":"Grompanopoulos","year":"2012"},{"key":"hu2017verification","doi-asserted-by":"publisher","DOI":"10.6028\/NIST.SP.800-192","article-title":"Verification and Test Methods for Access Control Policies\/Models","volume":"800-192","author":"Hu","year":"2017","journal-title":"NIST Special Publication"},{"key":"Lamport2002","volume-title":"Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers","author":"Lamport","year":"2002"},{"issue":"2","key":"lazouski2010usage","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1016\/j.cosrev.2010.02.002","article-title":"Usage control in computer security: A survey","volume":"4","author":"Lazouski","year":"2010","journal-title":"Computer Science Review"},{"key":"mavridou2016architecture","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/978-3-319-57666-4_16","article-title":"Architecture-Based Design: A Satellite On-Board Software Case Study","volume-title":"Formal Aspects of Component Software - 13th International Conference, FACS 2016, Besan\u00e7on, France, October 19-21, 2016, Revised Selected Papers","author":"Mavridou","year":"2016"},{"issue":"1","key":"Park2004","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1145\/984334.984339","article-title":"The UCON_\\voidb@x ABC usage control model","volume":"7","author":"Park","year":"2004","journal-title":"ACM Trans. Inf. Syst. Secur."},{"key":"said2014model","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-54848-2_1","article-title":"Model-Driven Information Flow Security for Component-Based Systems","volume-title":"From Programs to Systems. The Systems perspective in Computing - ETAPS Workshop, FPS 2014, in Honor of Joseph Sifakis, Grenoble, France, April 6, 2014. Proceedings","author":"Said","year":"2014"},{"issue":"1","key":"zhang2008toward","doi-asserted-by":"publisher","DOI":"10.1145\/1330295.1330298","article-title":"Toward a Usage-Based Security Framework for Collaborative Computing Systems","volume":"11","author":"Zhang","year":"2008","journal-title":"ACM Trans. Inf. Syst. Secur."},{"key":"Zhang2004","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/990036.990038","article-title":"A logical specification for usage control","volume-title":"9th ACM Symposium on Access Control Models and Technologies, SACMAT 2004, Yorktown Heights, New York, USA, June 2-4, 2004, Proceedings","author":"Zhang","year":"2004"}],"container-title":["Electronic Proceedings in Theoretical Computer Science"],"original-title":[],"language":"en","deposited":{"date-parts":[[2019,11,20]],"date-time":"2019-11-20T05:05:35Z","timestamp":1574226335000},"score":1,"resource":{"primary":{"URL":"http:\/\/arxiv.org\/abs\/1806.09848v1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,6,25]]},"references-count":11,"URL":"https:\/\/doi.org\/10.4204\/eptcs.272.5","relation":{},"ISSN":["2075-2180"],"issn-type":[{"value":"2075-2180","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,6,25]]}}}