On formal languages for sequences of authorization transformations

In a multi-user, information-sharing computer systems, authorization policy is needed to ensure that the information flows in the desired way and to prevent illegal access to the system resource. Usually such policy has a temporal property. That is, it needs to be updated to capture the changing requirements of applications, systems and users. These updates are implemented via transformation of authorization policies. In this paper, we propose two high-level formal languages L and L ^d to specify the transformation of authorizations in secure computer systems. L is a simple language that can be used to specify a sequence of authorization transformations. Though it has a simple syntax and semantics, we show that L is expressive enough to specify some well-known examples of authorization transformations. Language L ^d is an augmentation ofL which includes default propositions within the domain description of authorization policies. However, the semantics of L ^d is not just a simple extension of the semantics of L. We show that L ^d is more expressive than L in that constraints, causal and inherited authorizations, and general default authorizations can be specified.