Formal Specification and Integration of Distributed Security Policies
This work addresses the need for formal specification in security policy integration, particularly for web security standards like XACML, but it appears incremental as it builds on existing informal specifications.
The authors tackled the problem of formalizing and integrating distributed security policies by proposing the Security Policy Language (SePL), which includes operators for integration and has a denotational semantics independent of evaluation environments, and they proved its completeness with respect to set theory while formalizing a subset of XACML and its combining algorithms.
We propose in this paper the Security Policy Language (SePL), which is a formal language for capturing and integrating distributed security policies. The syntax of SePL includes several operators for the integration of policies and it is endowed with a denotational semantics that is a generic semantics, i.e., which is independent of any evaluation environment. We prove the completeness of SePL with respect to sets theory. Furthermore, we provide a formalization of a subset of the eXtensible Access Control Markup Language (XACML), which is the well-known standard informal specification language of Web security policies. We provide also a semantics for XACML policy combining algorithms.