Formal model and analysis of usage control

The concept of usage control (UCON) was introduced as a unified approach to capturing a number of extensions for access control models and systems. In UCON, a control decision is determined by three aspects: authorizations, obligations and conditions. Attribute mutability and decision continuity are two distinct characteristics which are presented in UCON for the first time. In this research I develop a logical model beyond the conceptual UCON model to capture the formal semantics of these key features, and then analyze the expressive power and safety properties of UCON.; Although the informal study of policy specification flexibility with UCON has been conducted in previous work, the multiple control components and unique features such as decision continuity and attribute mutability have not been formally studied. In this dissertation I develop a logical model of UCON based on an extended version of Lamport's temporal logical of actions (TLA) to formalize the state transitions in a single usage process. The model consists of predicates on subject and object attributes as authorizations, subject actions as obligations, and predicates on system attributes as conditions. With these basic terms, a usage control policy can be specified by a set of logical formulae, which are instantiated from a fixed set of scheme rules. The policy specification language is shown to be sound and complete. The flexibility of policy specification with UCON is shown by expressing policies for various applications.; To formally study the expressive power of UCON by comparing with traditional access control models, a policy-based model is developed to formalize the overall effect of a usage process. With this model, I prove that the general single-object typed access matrix (SO-TAM) model can be simulated with a UCON preA model, which is a sub-model of UCON with only pre-authorizations. The study of the expressive power shows that preA is at least as expressive as the augmented typed access matrix model (ATAM). For the expressive power of UCON pre-obligation models (preB), I prove that a general UCON preA model can be reduced to a preB model, and vice versa. This demonstrates that fundamentally these two models have the same expressive power. (Abstract shortened by UMI.)...