  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.
