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

Research

Associated organisational unit

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:

Keywords

View graph of relations

Specifying and Verifying Usage Control Models and Policies in TLA+

Research output: Contribution to Journal/Magazine › Journal article › peer-review

Published

Standard

Specifying and Verifying Usage Control Models and Policies in TLA+. / Grompanopoulos, Christos; Gouglidis, Antonios; Mavridou, Anastasia.
In: International Journal on Software Tools for Technology Transfer, Vol. 23, No. 5, 31.10.2021, p. 685-700.

Research output: Contribution to Journal/Magazine › Journal article › peer-review

Harvard

Grompanopoulos, C, Gouglidis, A & Mavridou, A 2021, 'Specifying and Verifying Usage Control Models and Policies in TLA+', International Journal on Software Tools for Technology Transfer, vol. 23, no. 5, pp. 685-700. https://doi.org/10.1007/s10009-020-00600-0

APA

Grompanopoulos, C., Gouglidis, A., & Mavridou, A. (2021). Specifying and Verifying Usage Control Models and Policies in TLA+. International Journal on Software Tools for Technology Transfer, 23(5), 685-700. https://doi.org/10.1007/s10009-020-00600-0

Vancouver

Grompanopoulos C, Gouglidis A, Mavridou A. Specifying and Verifying Usage Control Models and Policies in TLA+. International Journal on Software Tools for Technology Transfer. 2021 Oct 31;23(5):685-700. Epub 2021 Jan 8. doi: 10.1007/s10009-020-00600-0

Author

Grompanopoulos, Christos ; Gouglidis, Antonios ; Mavridou, Anastasia. / Specifying and Verifying Usage Control Models and Policies in TLA+. In: International Journal on Software Tools for Technology Transfer. 2021 ; Vol. 23, No. 5. pp. 685-700.

Bibtex

@article{4312835761c7479e971fbf8c98e61976,
title = "Specifying and Verifying Usage Control Models and Policies in TLA+",
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.",
keywords = "Authorization models, Concurrency, Model checking, UseCON",
author = "Christos Grompanopoulos and Antonios Gouglidis and Anastasia Mavridou",
note = "The final publication is available at Springer via http://dx.doi.org/10.1007/s10009-020-00600-0",
year = "2021",
month = oct,
day = "31",
doi = "10.1007/s10009-020-00600-0",
language = "English",
volume = "23",
pages = "685--700",
journal = "International Journal on Software Tools for Technology Transfer",
issn = "1433-2779",
publisher = "Springer Verlag",
number = "5",

}

RIS

TY - JOUR

T1 - Specifying and Verifying Usage Control Models and Policies in TLA+

AU - Grompanopoulos, Christos

AU - Gouglidis, Antonios

AU - Mavridou, Anastasia

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

PY - 2021/10/31

Y1 - 2021/10/31

N2 - 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.

AB - 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.

KW - Authorization models

KW - Concurrency

KW - Model checking

KW - UseCON

U2 - 10.1007/s10009-020-00600-0

DO - 10.1007/s10009-020-00600-0

M3 - Journal article

VL - 23

SP - 685

EP - 700

JO - International Journal on Software Tools for Technology Transfer

JF - International Journal on Software Tools for Technology Transfer

SN - 1433-2779

IS - 5

ER -