Towards Integrated Modelling of Dynamic Access Control with UML and Event-B

TL;DR

This paper proposes a combined graphical and formal modelling approach using UML and Event-B to specify and verify dynamic, state-dependent access control in systems, illustrated through a reporting management case study.

Contribution

It introduces a novel integration of UML and Event-B for modeling and verifying dynamic access control mechanisms, addressing the limitations of static RBAC models.

Findings

Successful modeling of dynamic access rights

Verification of system dependability through formal methods

Enhanced expressiveness in access control specifications

Abstract

Role-Based Access Control (RBAC) is a popular authorization model used to manage data-access constraints in a wide range of systems. RBAC usually defines the static view on the access rights. However, to ensure dependability of a system, it is often necessary to model and verify state-dependent access rights. Such a modelling allows us to explicitly define the dependencies between the system states and permissions to access and modify certain data. In this paper, we present a work-in-progress on combining graphical and formal modelling to specify and verify dynamic access control. The approach is illustrated by a case study -- a reporting management system.