Formal Verification of Usage Control Models : A Case Study of UseCON Using TLA+
- Submitting institution
-
The University of Lancaster
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 241304353
- Type
- E - Conference contribution
- DOI
-
10.4204/EPTCS.272.5
- Title of conference / published proceedings
- Proceedings of the 1st International Workshop on Methods and Tools for Rigorous System Design (MeTRiD 2018)
- First page
- 52
- Volume
- 272
- Issue
- -
- ISSN
- 2075-2180
- Open access status
- Compliant
- Month of publication
- April
- Year of publication
- 2018
- URL
-
https://arxiv.org/abs/1806.09848v1
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
2
- Research group(s)
-
I - Security
- Citation count
- 6
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- This paper elaborates on a case study to demonstrate how to specify a usage control model supporting concepts such as attribute mutability and continuity of decision, and formally verify its management procedures using model checking. This work anticipates shedding light to the formal verification of usage or access control models, which can be beneficial when considering their application in complex systems (e.g., the Cloud). An extended version of this work has been invited for submission at Springer’s ‘International Journal on Software Tools for Technology Transfer’. This paper resulted in a collaboration with a computer scientist at NASA Ames Research Center.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -
