Formal Specification and Integration of Distributed Security Policies

TL;DR

This paper introduces SePL, a formal language for specifying and integrating distributed security policies, with a semantics that is environment-independent and includes formalization of XACML policy algorithms.

Contribution

It presents SePL, a novel formal language with a denotational semantics for security policies, and formalizes part of XACML for Web security policy integration.

Findings

SePL is complete with respect to set theory.

Provides a formal semantics for XACML combining algorithms.

Enables rigorous policy specification and integration.

Abstract

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.