Specifying and Verifying Organizational Security Properties in First-Order Logic

Christoph Brandt, Jens Otten, Christoph Kreitz.

Verification, Induction, Termination Analysis, LNCS 6463, pp. 38-53, Springer Verlag, 2010.


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.

PS Version PDF Version   (Preprint) BACK
Back to overview of papers

Bibtex Entry

@InProceedings{inp:BrandtOttenKreitz10a, author = "Christoph Brandt and Jens Otten and Christoph Kreitz", title = "Specifying and Verifying Organizational Security Properties in First-Order Logic", booktitle = "Verification, Induction, Termination Analysis", year = "2010", editor = "Simon Siegler and Nathan Wasser", volume = "6463", series = "Lecture Notes in Computer Science", pages = "38--53", publisher = "Springer Verlag" }