  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.
