M.M. Ayachit and H. Xu (USA)
XML firewall, web services, role-based access control (RBAC), Petri net model, formal verification
An XML firewall differs from a conventional firewall because its major task is to control access to web services rather than to filter untrusted addresses. An XML firewall can effectively protect web services from being attacked by inspecting a complete XML message including its head and data segments, and rejecting unauthorized web services invocation. In this paper, we propose a formal XML firewall security model using role-based access control (RBAC). Our proposed model supports user authentication and user authorization according to information stored in a user database and a policy database associated with an XML firewall. The formal model is designed compositionally using Petri nets, which can serve as a high-level design for XML firewall implementation. The key components of our compositional security model are the application model and the XML firewall model. To illustrate the advantages of our formal approach, we use an existing Petri net tool to verify some key properties of our model, such as boundedness and liveness.
Important Links:
Go Back
