Static verification of access control model for AXML documents

Abstract

Reasoning about the access control model for AXML documents is a non-trivial topic because of its own challenging issues: the hierarchical nature of XML with embedded service call and query transformation. In this paper, we present a methodology to specify an access control model (GUPster) for AXML (Active XML) documents by translating a query, schema, and access control policy in CSP language. Then, we show how to verify access control policies of AXML documents, by illustrating the running example, with the FDR model checker. Finally, the examples demonstrate that our automated static verification is efficient to analyze security problems, not only whether the policies give legitimate users enough permissions to read data, but also whether the policies prevent unauthorized users from reading sensitive data. © Springer-Verlag Berlin Heidelberg 2007.