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 First-Order 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 sourc...