Verification of Interoperability Security Policies by Model Checking

Access control policies are the key point for a secured interaction in business community. In general, an information system has to include an interoperability access control security policy to regulate the access from other systems to its resources. The security policy specifies a set of rules that defines the privileges of any subject accessing to the information system resources. In this paper we provide an approach to verify the correctness of contextual based interoperability access control security policies which are integrated in a system model. Security rules are initially described using the organization to organization model (O2O). We first propose an approach to transform O2O security rules to the well known Linear Temporal Logic (LTL). In order to instantiate the LTL formulae from a set of O2O security rules, we provided a mapping between the elements of the O2O security rule and the elements of the functional model in which the security rules are integrated. The resulted LTL formulae are used to verify the correctness of the security rules by model checking.