King's College London

Research portal

A formal model and correctness proof for an access control policy framework

Research output: Chapter in Book/Report/Conference proceedingConference paper

Chunhan Wu, Xingyuan Zhang, Christian Urban

Original languageEnglish
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Pages292-307
Number of pages16
Volume8307
DOIs
Publication statusPublished - 2013
Event3rd International Conference on Certified Programs and Proofs, CPP 2013 - Melbourne, VIC, Australia
Duration: 11 Dec 201313 Dec 2013

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8307 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Conference

Conference3rd International Conference on Certified Programs and Proofs, CPP 2013
CountryAustralia
CityMelbourne, VIC
Period11/12/201313/12/2013

King's Authors

Abstract

If an access control policy promises that a resource is protected in a system, how do we know it is really protected? To give an answer we formalise in this paper the Role-Compatibility Model - a framework, introduced by Ott, in which access control policies can be expressed. We also give a dynamic model determining which security related events can happen while a system is running. We prove that if a policy in this framework ensures a resource is protected, then there is really no sequence of events that would compromise the security of this resource. We also prove the opposite: if a policy does not prevent a security compromise of a resource, then there is a sequence of events that will compromise it. Consequently, a static policy check is sufficient (sound and complete) in order to guarantee or expose the security of resources before running the system. Our formal model and correctness proof are mechanised in the Isabelle/HOL theorem prover using Paulson's inductive method for reasoning about valid sequences of events. Our results apply to the Role-Compatibility Model, but can be readily adapted to other role-based access control models.

View graph of relations

© 2018 King's College London | Strand | London WC2R 2LS | England | United Kingdom | Tel +44 (0)20 7836 5454