A verification for PDAC model by policy language

In the previous works, we have designed and implemented a distributed access control model using a reputation mechanism. The implementation was tested with a series of random executions to prove that the system is correct and behaves as desired. But to obtain confidence in the behavior of such a system, we must verify it more rigorously. In this paper, we define a logic which enables us to express and prove properties of the capability-based access control. We give three axioms, which is the basis in logic soundness proof firstly. And then a series of inference rules are introduced, followed by soundness proof of this logic. Based on this logic, we conclude the properties of PDAC model that we are interested in, state and prove them. By thoroughly verification, we believe that PDAC model behaves as desired.