Using a Process Algebraic Approach of VerifyingAccess Control in XML-based Healthcare Systems

摘要

Healthcare information and its secure management has become an active research topic along with anincrease in the usage of XML documents and the importance of access control in maintaining patient records.In this paper, we present a methodology to describe a formal specification for an authorized view of an XMLbasedhealthcare system having a schema-level access control by assigning well-established concurrencysemantics to the system. To achieve this goal, we translate the semantics of the schema, query, access controlfor XML-based health records, and XPath expressions, into a CSP-like process algebra language through anillustrative example. Finally, our experimental results show the possibility to reason about securityproperties of an XML-based access control model with the support of automated model checking tools,because it provides the formal semantics for access control policies and XML documents with the treestructure.