Theorem proving for modeling and conflict checking of authorization policies

For large information systems with many entities, defining and verifying information security policies manually is error-prone and cumbersome. An automated analysis is necessary to ensure that the policies are conflict-free when defined at first and as new authorization terms are added and removed. Graph theory and logic based approaches have been previously used for formal definition and conflict checking of policies. Theorem proving has been used in cryptographic protocol and secure system verification. In this case study the use of theorem proving for definition and verification of security policies is investigated using the Coq theorem proving tool.