Formal Verification of Access Control Policies

Abstract

The primary purpose of security mechanisms in a system is to control access to information. Access control is the process of limiting
access to the resources of a system to authorized users, programs, processes, or other systems. In this paper we illustrate different access control
techniques and models that have been proposed in the literature and model checking approach to verify the properties of models. Model
checking approach first expresses access control models in the specification language of a model checker. It expresses generic access control
properties in temporal logic formulas and then uses the model checker to verify these properties for the access control models and generate the
counter example for those properties which is not true in the specified model. We use NuSMV model checker tool. We present a case study of a
health care system. The goal of our paper is to give a general approach for verification of a health care system using model checking.

 

 

Keywords: Access Control; RBAC,Model Checking;NUSMV;LTL;CTL;