XACML has emerged as a popular access control language on the Web, but because of its rich expressiveness, it has proved difficult to analyze in an automated fashion. In this paper, we present a formalization of XACML using description logics (DL), which are a decidable fragment of FirstOrder logic. This formalization allows us to cover a more expressive subset of XACML than propositional logic-based analysis tools, and in addition we provide a new analysis service (policy redundancy). Also, mapping XACML to description logics allows us to use off-the-shelf DL reasoners for analysis tasks such as policy comparison, verification and querying. We provide empirical evaluation of a policy analysis tool that was implemented on top of open source DL reasoner Pellet. Categories and Subject Descriptors I.2.2 [Artificial Intelligence]: Automatic Programming-program verification; I.2.4 [Artificial Intelligence]: Knowledge Representation Formalisms and Methods--representation languages; H.3.5 [I...
Vladimir Kolovski, James A. Hendler, Bijan Parsia