Home > Research > Publications & Outputs > Specifying and Verifying Usage Control Models a...

Electronic data

  • STTT UseCON TLA

    Rights statement: The final publication is available at Springer via http://dx.doi.org/10.1007/s10009-020-00600-0

    Accepted author manuscript, 818 KB, PDF document

    Available under license: CC BY-NC: Creative Commons Attribution-NonCommercial 4.0 International License

Links

Text available via DOI:

View graph of relations

Specifying and Verifying Usage Control Models and Policies in TLA+

Research output: Contribution to Journal/MagazineJournal articlepeer-review

Published
Close
<mark>Journal publication date</mark>31/10/2021
<mark>Journal</mark>International Journal on Software Tools for Technology Transfer
Issue number5
Volume23
Pages (from-to)685-700
Publication StatusPublished
Early online date8/01/21
<mark>Original language</mark>English

Abstract

Novel computing paradigms, e.g., the Cloud, introduce new requirements with regard to access control such as utilization of historical information and continuity of decision. However, these concepts may introduce an additional level of complexity to the underpinning model, rendering its definition and verification a cumbersome and prone to errors process. Using a formal language to specify a model and formally verify it may lead to a rigorous definition of the interactions amongst its components, and the provision of formal guarantees for its correctness. In this paper, we consider a case study where we specify a formal model in TLA+ for both a policy-neutral and policy-specific UseCON usage control model. Through that, we anticipate to shed light in the analysis and verification of usage control models and policies by sharing our experience when using TLA+ specific tools.

Bibliographic note

The final publication is available at Springer via http://dx.doi.org/10.1007/s10009-020-00600-0