A policy language for expressing access control properties in PDAC model

An access control policy defines what is authorized, and an access control mechanism implements the policy to ensure that all accesses are in accordance with the underlying policy. Nowadays, many researcher are working for expressing access policies in a formal way. But it is still an open problem. This paper defines a policy language, which is named as PDPL to express access policies and access control properties in PDAC model [1]. This language unifies ldquoBANrdquo logic with past- and future- time temporal logic. We give the syntax and semantics of PDPL, and provided some examples with their English equivalents. This logic language can express belief and authorization in access control model. And it can deal with delegations of decision-making directly. It is easy for us to formulate the properties of interest in distributed systems of PDAC model through PDPL. This logical language is part of a formal system, and it will be used in an automatic model checker in the future.