Work-Based Access Control Model for Cooperative Healthcare Environments: Formal Specification and Verification

In this study, an access control model for cooperative healthcare environments is presented. A work-based access control (WBAC) model is proposed by introducing the concept of team role classification based on Belbin team role theory and modifying the user-role assignment model from previous work. Roles are used in conjunction with team roles to handle access control in dynamic collaborative environments. To evaluate and analyze the security, efficiency, and practicality of the proposed model, we first formalize the model (events and policies), define the basic element set and relations in the WBAC model, present the WBAC authorization constraints, and define the WBAC access control decision function. Second, we evaluate the model's security and manageability validity to ensure that the security and management requirements of our WBAC model are met. Finally, we evaluate the performance of the proposed model and compare it with relevant existing models. Verification indicates that WBAC is flexible, easy to manage and meets our expectation of allowing fine-grained access control, and it enhances the practicability of access control in dynamic collaboration environments.