RBAC for Healthcare-Infrastructure and data storage

TL;DR

This paper presents a formal RBAC model tailored for healthcare infrastructure, using Alloy to validate system behaviors and ensure security properties like integrity and conformance.

Contribution

It introduces a formal RBAC framework for healthcare, modeling both static and dynamic behaviors with Alloy for validation.

Findings

Validated system integrity and conformance properties

Demonstrated effective modeling of static and dynamic behaviors

Ensured security properties in healthcare access control

Abstract

Role based Access control (RBAC) is the cornerstone of security for any modern organization. In this report, we defined a health-care access control structure based on RBAC. We used Alloy formal logic modeling tool to model and validate system functions. We modeled system static and dynamic or temporal behaviours. We focused on evaluating properties such as integrity, conformance and progress.