Specifying and verifying organizational security properties in first-order logic

In certain critical cases the data flow between business departments in banking organizations has to respect security policies known as Chinese Wall or Bell-La Padula. We show that these policies can be represented by formal requirements and constraints in first-order logic. By additionally providing a formal model for the flow of data between business departments we demonstrate how security policies can be applied to a concrete organizational setting and checked with a first-order theorem prover. Our approach can be applied without requiring a deep formal expertise and it therefore promises a high potential of usability in the business.