Automated Symbolic Analysis of ARBAC-Policies (Extended Version)

TL;DR

This paper introduces a symbolic, parametric analysis framework for ARBAC policies that can handle an unbounded number of users and roles, improving scalability over existing bounded methods.

Contribution

It presents a novel automated security analysis technique for ARBAC policies using first-order logic and theorem proving, capable of analyzing infinite state systems.

Findings

Preliminary experiments show promising scalability.

The framework effectively handles unbounded users and roles.

It adapts model checking techniques for infinite state systems.

Abstract

One of the most widespread framework for the management of access-control policies is Administrative Role Based Access Control (ARBAC). Several automated analysis techniques have been proposed to help maintaining desirable security properties of ARBAC policies. One limitation of many available techniques is that the sets of users and roles are bounded. In this paper, we propose a symbolic framework to overcome this difficulty. We design an automated security analysis technique, parametric in the number of users and roles, by adapting recent methods for model checking infinite state systems that use first-order logic and state-of-the-art theorem proving techniques. Preliminary experiments with a prototype implementations seem to confirm the scalability of our technique.