Access Control Policies: Modeling and Validation

Abstract — Access control requires authorization rules and constraints. To express access control policies, several languages, such as XACML, EPAL or PONDER, are used. These languages specify which subjects can (or cannot) access sets of resources or services to perform specific actions. A user can define several access control policies and rules, but these access control languages do not offer any mechanism to avoid conflicts and inconsistencies among them. In fact, it can happen that more than a rule or a policy, with opposite decisions, is applicable in a given context. We propose a method based on first order logic modeling to detect and visualize possible conflicts within sets of access control policies expressed in XACML. We translate the model into a relational first order logic language called Alloy. Alloy allows to specify sets of predicates and assertions defining the desired properties of a system. We can then analyze interactions and conflicts among access control policies by using the Alloy Analyzer tool. I