Secure EHR access in the cloud: an alloy-based formalization of ABAC in collaborative and non-collaborative models

The approach proposed in this article integrates the Attribute-Based Access Control (ABAC) ‎model and the Alloy modeling tool to enhance security in cloud environments, whet alher ‎collaborative or non-collaborative. Cloud computing facilitates data management, particularly ‎in collaborative environments that promote teamwork, but this increased flexibility introduces ‎more complex security challenges. In contrast, non-collaborative environments offer stricter ‎access control, thereby improving security while limiting the flexibility of interactions. The ‎ABAC model allows for the definition of fine-grained access policies based on user roles, ‎context, and data sensitivity, making it an ideal solution for protecting Electronic Health ‎Records (EHR). With dynamic access management, only authorized individuals can view or ‎manipulate sensitive data. The use of Alloy enables the formalization and testing of these ‎security policies by simulating different access scenarios to verify the consistency of the rules ‎and understand the trade-offs bet alween security and flexibility. Thus, the combination of ‎ABAC and Alloy provides a robust solution for managing access in complex cloud ‎environments while ensuring optimal protection of sensitive data.‎