Accepted author manuscript, 0.99 MB, PDF document
Available under license: CC BY-NC: Creative Commons Attribution-NonCommercial 4.0 International License
Final published version
Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSN › Conference contribution/Paper › peer-review
Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSN › Conference contribution/Paper › peer-review
}
TY - GEN
T1 - Formal Verification of Usage Control Models
T2 - International Workshop on Methods and Tools for Rigorous System Design
AU - Gouglidis, Antonios
AU - Grompanopoulos, Christos
AU - Mavridou, Anastasia
N1 - Conference code: 1
PY - 2018/6/25
Y1 - 2018/6/25
N2 - Usage control models provide an integration of access control, digital rights, and trust management. To achieve this integration, usage control models support additional concepts such as attribute mutability and continuity of decision. However, these concepts may introduce an additional level of complexity to the underlying model, rendering its definition a cumbersome and prone to errors process. Applying a formal verification technique allows for a rigorous analysis of the interactions amongst the components, and thus for formal guarantees in respect of the correctness of a model. In this paper, we elaborate on a case study, where we express the high-level functional model of the UseCON usage control model in the TLA+ formal specification language, and verify its correctness for <=12 uses in both of its supporting authorisation models.
AB - Usage control models provide an integration of access control, digital rights, and trust management. To achieve this integration, usage control models support additional concepts such as attribute mutability and continuity of decision. However, these concepts may introduce an additional level of complexity to the underlying model, rendering its definition a cumbersome and prone to errors process. Applying a formal verification technique allows for a rigorous analysis of the interactions amongst the components, and thus for formal guarantees in respect of the correctness of a model. In this paper, we elaborate on a case study, where we express the high-level functional model of the UseCON usage control model in the TLA+ formal specification language, and verify its correctness for <=12 uses in both of its supporting authorisation models.
U2 - 10.4204/EPTCS.272.5
DO - 10.4204/EPTCS.272.5
M3 - Conference contribution/Paper
T3 - EPTCS
SP - 52
EP - 64
BT - Proceedings of the 1st International Workshop on Methods and Tools for Rigorous System Design (MeTRiD 2018)
A2 - Bliudze, Simon
A2 - Bensalem, Saddek
PB - EPTCS
Y2 - 10 April 2018
ER -