An approach to correctness of security and operational business policies

In this paper we have proposed an approach to describing security and operational business policies and verifying their correctness with respect to a set of properties. The method is based on the REA business modeling language to construct definitions of security and operational business rules. Once the rules are created their representations are combined into policies and policy sets using state machines.