Formal Semantics for Attribute Access and Usage Control


Modern security architectures rely on sophisticated usage control mechanisms that control access and usage of resources. It is a major challenge to ensure that these usage control mechanisms behave as intended. This project develops methods for the formalization, verification, and analysis of a continuous usage control system.

Project description

The project develops analysis and verification methods for modern continuous usage control systems deployed in cloud, edge, and IoT environments. To make the analysis of usage control possible, we develop a formal specification of the intendent system behavior and use it to develop methods for verification and analysis.

There are three main goals:

  • Formalization: Define a clear and rigorous specification for policies and continuous usage control.
  • Verification: Develop a monitoring approach for verifying that usage control systems correctly implement the specification.
  • Analysis: Support the correct use of usage control systems with automated policy analysis methods that may be used to assist writing and maintaining policies.

Research contribution

The formal specification of usage control provides the basis that makes automated analysis and verification possible. The project extends the scope of the formal semantics of access control systems, particularly by capturing models of continuous usage control. It applies the results to develop a monitoring method for verifying that usage control policies are enforced correctly. It develops new automated methods for analyzing properties of policies statically before they are deployed.

Project duration

01.11.2021 – 31.05.2023

Project partner