A logical specification for usage control

TLDR

Usage control (UCON) is a next‑generation access control model characterized by decision continuity and attribute mutability, with decisions based on authorizations, obligations, and conditions as defined in the UCONABC core models. The authors develop a first‑order logic specification of UCON using Lamport's temporal logic of actions (TLA). The specification models a sequence of states defined by subject, object, and system attributes, state predicates, predefined authorization and obligation actions, and condition predicates, and defines temporal logic formulas that capture usage control policies. The authors demonstrate the flexibility and expressive capability of this logic model by specifying new features and core models of UCON.

Abstract

Recently presented usage control (UCON) has been considered as the next generation access control model with distinguishing properties of decision continuity and attribute mutability. Ausage control decision is determined by combining authorizations, obligations, and conditions, presented as UCONABC core models by Park and Sandhu. Based on these core aspects, we develop afirst-order logic specification of UCON with Lamport's temporallogic of actions (TLA). The building blocks of this model include:(1) a sequence of states expressed by attributes of subjects, objects, and the system, (2) state predicates on subject andobject attributes, (3) pre-defined authorization actions performed by the security system and subjects, (4) obligation actions, and(5) condition predicates on system attributes. For a UCON model we define a set of temporal logic formulas that hold as usage control policies. We show the flexibility and expressive capability of this logic model by specifying the new features and core models of UCON.