Formal Specification of Concurrent Enforcement UCON Model with CTL Logic.

Usage Control (UCON) model has been considered as the next generation access control model, its distinguishing properties of attribute mutability and decision continuity were more suit for dynamic and open network environment. Just a single usage process was described in form of a state diagram in early formalization, it make it difficult to reason about the interactions of several concurrent usage control process. There were have many formal specifications of Usage Control model. But that formalization all are ambiguous about the interactions of several concurrent usage control process. In this paper we introduced the formal description of UCONABC model and presented an alternative formalization of UCON using extended Computation Tree Logic (CTL) as the underlying formalism. The branching-time character of CTL makes it more naturally on the specification of concurrent enforcement and makes specify the usage control security policy better.