Home > Research > Publications & Outputs > Formal Verification of Usage Control Models

Electronic data

  • pre-proceedings-formal (2)

    Accepted author manuscript, 0.99 MB, 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

Formal Verification of Usage Control Models: A Case Study of UseCON Using TLA+

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSNConference contribution/Paperpeer-review

Published
Close
Publication date25/06/2018
Host publicationProceedings of the 1st International Workshop on Methods and Tools for Rigorous System Design (MeTRiD 2018)
EditorsSimon Bliudze, Saddek Bensalem
PublisherEPTCS
Pages52-64
Number of pages13
<mark>Original language</mark>English
EventInternational Workshop on Methods and Tools for Rigorous System Design - Thessaloniki, Greece
Duration: 10/04/2018 → …
Conference number: 1
https://project.inria.fr/metrid2018/

Workshop

WorkshopInternational Workshop on Methods and Tools for Rigorous System Design
Abbreviated titleMeTRiD
Country/TerritoryGreece
CityThessaloniki
Period10/04/18 → …
Internet address

Publication series

NameEPTCS
Volume272
ISSN (Print)2075-2180

Workshop

WorkshopInternational Workshop on Methods and Tools for Rigorous System Design
Abbreviated titleMeTRiD
Country/TerritoryGreece
CityThessaloniki
Period10/04/18 → …
Internet address

Abstract

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.