Formal model and policy specification of usage control

The recent usage control model (UCON) is a foundation for next-generation access control models with distinguishing properties of decision continuity and attribute mutability. A usage control decision is determined by combining authorizations, obligations, and conditions, presented as UCON ABC core models by Park and Sandhu. Based on these core aspects, we develop a formal model and logical specification of UCON with an extension of Lamport's temporal logic of actions (TLA). The building blocks of this model include: (1) a set of sequences of system states based on the attributes of subjects, objects, and the system, (2) authorization predicates based on subject and object attributes, (3) usage control actions to update attributes and accessing status of a usage process, (4) obligation actions, and (5) condition predicates based on system attributes. A usage control policy is defined as a set of temporal logic formulas that are satisfied as the system state changes. A fixed set of scheme rules is defined to specify general UCON policies with the properties of soundness and completeness. We show the flexibility and expressive capability of this formal model by specifying the core models of UCON and some applications. © 2005 ACM.