Compliance verification algorithm for computer systems security policies

Abstract

This paper proposes an algebraic formalism and a dedicated logic for computer systems and security policies specifications. A tableaubased proof system is then developed for assessing whether policies are satisfied for a given model of a computer system. A practical example and an implementation within a theorem prover show the effectiveness of our specification and verification technique.