Verification of SGAC Access Control Policies Using Alloy and ProB

This paper investigates the verification ofaccess control policies for SGAC, a new healthcare access-control model, using Alloy and ProB, two first orderlogic model checkers based on distinct technologies.SGAC supports permission and prohibition, ruleinheritance among subjects and resources and conf...

Full description

Saved in:
Bibliographic Details
Main Authors: Huynh, Nghi, Frappier, Marc, Mammar, Amel, Laleau, Regine
Format: Conference Proceeding
Language:English
Subjects:
Access control
Alloy
consent management
Context
formal model
healthcare
Hospitals
Metals
Modeling
Privacy
ProB
verification
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:This paper investigates the verification ofaccess control policies for SGAC, a new healthcare access-control model, using Alloy and ProB, two first orderlogic model checkers based on distinct technologies.SGAC supports permission and prohibition, ruleinheritance among subjects and resources and conflictsresolution. In order to protect patient privacy while ensuringeffective caregiving in safety-critical situations, we check different properties such as accessibility, ineffectiverule detection. Our performance results showthat ProB performs two orders of magnitude betterthan Alloy. Results are promising enough to considerProB for verifying patient policies in SGAC.
ISSN:1530-2059
2640-7507
DOI:10.1109/HASE.2017.24