Verification of SGAC access control policies using alloy and ProB

Nghi Huynh, Marc Frappier, Amel Mammar, Regine Laleau

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

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.

Original languageEnglish
Title of host publicationProceedings - IEEE 18th International Symposium on High Assurance Systems Engineering, HASE 2017
PublisherIEEE Computer Society
Pages120-123
Number of pages4
ISBN (Electronic)9781509046355
DOIs
Publication statusPublished - 25 Apr 2017
Event18th IEEE International Symposium on High Assurance Systems Engineering, HASE 2017 - Singapore, Singapore
Duration: 12 Jan 201714 Jan 2017

Publication series

NameProceedings of IEEE International Symposium on High Assurance Systems Engineering
ISSN (Print)1530-2059

Conference

Conference18th IEEE International Symposium on High Assurance Systems Engineering, HASE 2017
Country/TerritorySingapore
CitySingapore
Period12/01/1714/01/17

Keywords

  • Access control
  • Alloy
  • Consent management
  • Formal model
  • Healthcare
  • ProB
  • Verification

Fingerprint

Dive into the research topics of 'Verification of SGAC access control policies using alloy and ProB'. Together they form a unique fingerprint.

Cite this