Formal model and policy specification of usage control

TLDR

UCON provides a foundation for next‑generation access control by integrating decision continuity and attribute mutability through authorizations, obligations, and conditions. The study develops a formal model and logical specification of UCON extending Lamport's temporal logic of actions. The model comprises state sequences of subject, object, and system attributes; authorization, obligation, and condition predicates; usage control actions that update attributes and access status; and a set of temporal logic formulas defining policies, with scheme rules ensuring soundness and completeness. We demonstrate the model’s flexibility and expressive capability by specifying UCON core models and various applications.

Abstract

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.