Evaluating Access Control Policies through Model Checking

Nan Zhang, Mark Ryan, Dimitar Guelev

Research output: Contribution to journalArticlepeer-review

72 Citations (Scopus)


We present a model-checking algorithm which can be used to evaluate access control policies, and a tool which implements it. The evaluation includes not only assessing whether the policies give legitimate users enough permissions to reach their goals, but also checking whether the policies prevent intruders from reaching their malicious goals. Policies of the access control system and goals of agents must be described in the access control description and specification language introduced as RW in our earlier work. The algorithm takes a policy description and a goal as input and performs two modes of checking. In the assessing mode, the algorithm searches for strategies consisting of reading and writing steps which allow the agents to achieve their goals no matter what states the system may be driven into during the execution of the strategies. In the intrusion detection mode, a weaker notion of strategy is used, reflecting the willingness of intruders to guess the value of attributes which they cannot read.
Original languageEnglish
Pages (from-to)446-460
Number of pages15
JournalLecture Notes in Computer Science
Publication statusPublished - 1 Jan 2005
EventEighth Information Security Conference (ISC'05) -
Duration: 1 Jan 2005 → …


Dive into the research topics of 'Evaluating Access Control Policies through Model Checking'. Together they form a unique fingerprint.

Cite this