Security policy validation using temporal executable specifications

Security policies constitute the core of protecting information systems. Validation tools should therefore be developed to check whether a version of a specific security policy conforms to the required security properties. This paper proposes a validation framework for security policies where: (1) algebraic specifications are used to build abstract views about the security policy, (2) an executable security policy can be extracted from the algebraic representation, and (3) syntactical (resp. sematic) verification of the executable (resp. algebraic) security policy is performed.