Security policy specification in logic

We show how clausal form logic may be used to protect the information contained in a computer system from unauthorized disclosure and modification. More specifically, we show how security policies based on discretionary access control (DAC) and mandatory access control (MAC) may be viewed as special subtheories of a clausal form theory which formulates a role-based access control (RBAC) policy. In this context, theorem-proving techniques are used to decide whether requests to access information are authorized or not.