Automata model for verifying attibuted-based access control policy in systems with a finite number of objects

In this paper, we use a finite-automata model of attribute-based access control policies. The correctness of a policy is defined as a variation of the reachability problem for an infinite transition system induced by the policy. The problem of correctness validation for a given policy is shown decidable for information systems with a bounded number of objects.