ABSTRACT. The RBAC challenge paper describes a dynamic system for role based access control. In this position paper, we take a theoretical perspective on the problem. The questions we asked ourselves were of the following kind: how much of the RBAC domain can be formally specified in first order logic extended with inductive definitions and aggregates (FO(.))? How much of the RBAC system can be analyzed on the basis of this formal specification? What functionalities of the RBAC system can be executed by applying suitable forms of inference on the formal specification? What forms of inference are needed for that?