A first step towards formal verification of security policy properties for RBAC

Considering the current expansion of IT-infrastructure, the security of the data inside this infrastructure becomes increasingly important. Therefore, assuring certain security properties of IT-systems by formal methods is desirable. So far in security, formal methods have mostly been used to prove properties of security protocols. However, access control is an indispensable part of security inside a given IT-system, which has not yet been sufficiently examined using formal methods. The paper presents an example of a RBAC security policy having the dual control property. This is proved in a first-order linear temporal logic (LTL) that has been embedded in the theorem prover Isabelle/HOL by the authors. Thus, the correctness of the proof is assured by Isabelle/HOL. The authors consider first-order LTL a good formalism for expressing RBAC authorisation constraints and deriving properties from given RBAC security policies. Furthermore, it might also be applied to safety-related issues in similar manner.