Xinwen Zhang
Ravi Sandhu
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 UCONABC 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.
- Bell, D. E. and LaPadula, L. J. 1975. Secure computer systems: Mathematical foundations and model. Mitre Corp. Report No.M74-244, Bedford, MA.]]Google Scholar
- Bertino, E., Bettini, C., and Samarati, P. 1994. A temporal authorization model. In Proceedings of ACM Conference on Computer and Communication Security. ACM, New York.]] Google Scholar
- Bertino, E., Bettini, C., Ferrari, E., and Samarati, P. 1996. A temporal access control mechanism for database systems. IEEE Transactions on Knowledge and Data Engineering 8, 1 (Feb.).]] Google ScholarDigital Library
- Bertino, E., Bettini, C., Ferrari, E., and Samarati, P. 1999. An access control model supporting periodicity constraints and temporal reasoning. ACM Transaction on Database Systems 23, 3 (Sept.).]] Google Scholar
- Bertino, E., Catania, B., Ferrari, E., and Perlasca, P. 2001. A logical framework for reasoning about access control models. In Proceedings of the Sixth ACM Symposium on Access Control Models and Technologies. ACM, New York.]] Google Scholar
- Bettini, C., Jajodia, S., Wang, X. S., and Wijesekera, D. 2002a. Obligation monitoring in policy management. In Proceedings of the 3rd Internationl Workshop on Policies for Distributed Systems and Networks.]] Google Scholar
- Bettini, C., Jajodia, S., Wang, X. S., and Wijesekera, D. 2002b. Provisions and obligations in policy management and security applications. In Proceedings of the 28th VLDB Conference.]]Google Scholar
- Brewer, D. and Nash, M. 1988. The chinese wall security policy. In Proceedings of the IEEE Symposium on Research in Security and Privacy.]]Google Scholar
- Chomicki, J. and Lobo, J. 2001. Monitors for history-based policies. In Proceedings of the 2nd Internationl Workshop on Policies for Distributed Systems and Networks.]] Google Scholar
- Damianou, N., Dulay, N., Lupu, E., and Sloman, M. 2001. The ponder policy specification language. In Proceedings of the Workshop on Policies for Distributed Systems and Networks.]] Google Scholar
- Denning, D. E. 1976. A lattice model of secure information flow. Communications of the ACM 19, 5 (May).]] Google ScholarDigital Library
- Gal, A. and Atluri, V. 2000. An authorization model for temporal data. In Proceedings of the ACM Conference on Computer and Communication Security.]] Google Scholar
- Hansen, M. and Sharp, R. 2003. Using interval logics for temporal analysis of security protocols. In Proceedings of the ACM Workshop on Formal Methods in Security Engineering.]] Google Scholar
- Jajodia, S., Samarati, P., and Subrahmanian, V. S. 1997. A logical language for expressing authorizations. In Proceedings of the IEEE Symposium On Research in Security and Privacy.]] Google Scholar
- Jajodia, S., Samarati, P., Sapino, M. L., and Subrahmanian, V. S. 2001. Flexible support for multiple access control policies. ACM Transactions on Database Systems 26, 2 (June).]] Google ScholarDigital Library
- Joshi, J., Bertino, E., Shafiq, B., and Ghafoor, A. 2003. Constraints: Dependencies and separation of duty constraints in gtrbac. In Proceedings of the 8th ACM Symposium on Access Control Models and Technologies.]] Google Scholar
- Joshi, J., Bertino, E., Latif, U., and Ghafoor, A. 2005. A generalized temporal role-based access control model. IEEE Transactions on Knowledge and Data Engineering 17, 1.]] Google ScholarDigital Library
- Lamport, L. 1994. The temporal logic of actions. ACM Transactions on Programming Languages and Systems 16, 3 (May).]] Google ScholarDigital Library
- Manna, Z. and Pnueli, A. 1991. The Temporal Logic of Reactive and Concurrent Systems Specification. Springer-Verlag, New York.]] Google Scholar
- Park, J. and Sandhu, R. 2004. The UCONABC usage control model. ACM Transactions on Information and Systems Security 7, 1 (Feb.).]] Google ScholarDigital Library
- Park, J., Zhang, X., and Sandhu, R. 2004. Arrtibute mutability in usage control. In Proceedings of the Proceedings of 18th Annual IFIP WG 11.3 Working Conference on Data and Applications Security.]]Google Scholar
- Sandhu, R. 1993. Lattice-based access control models. IEEE Computer 26, 11 (Nov.).]] Google ScholarDigital Library
- Sandhu, R. and Park, J. 2003. Usage control: A vision for next generation access control. In Proceedings of the Second International Workshop on Mathematical Methods, Models and Architectures for Computer Networks Security.]]Google Scholar
- Sandhu, R., Coyne, E., Feinstein, H., and Youman, C. 1996. Role based access control models. IEEE Computer 29, 2.]] Google ScholarDigital Library
- Siewe, F., Cau, A., and Zedan, H. 2003. Compositional framework for access control policies enforcement. In Proceedings of the ACM Workshop on Formal Methods in Security Engineering.]] Google Scholar
- Simon, R. T. and Zurko, M. E. 1997. Separation of duty in role-based environments. In IEEE Computer Security Foundations Workshop.]] Google Scholar
Index Terms
- Formal model and policy specification of usage control
Recommendations
A logical specification for usage control
SACMAT '04: Proceedings of the ninth ACM symposium on Access control models and technologiesRecently 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, ...
The UCONABC usage control model
In this paper, we introduce the family of UCONABC models for usage control (UCON), which integrate Authorizations (A), oBligations (B), and Conditions (C). We call these core models because they address the essence of UCON, leaving administration, ...
A note on the formalisation of UCON
SACMAT '07: Proceedings of the 12th ACM symposium on Access control models and technologiesUsage Control (UCON) Models, similar to Access Control Models, control and govern the users' access to resources and services that are available in the system. One of the major improvements of UCON over traditional access control models is the ...
Reviews
Andre C. M. Marien
This is the latest in a series of papers about user control models (UCON), which provide a basis for next-generation access control systems. Access control in current-generation systems is static. Authorization and control are based on immutable attributes. This series of papers consider dynamic access control, and contains examples of problems requiring such an approach. The first step semi-formally describes authorizations, obligations, and conditions that are the basis for access control decisions. Temporal logic supports formal reasoning about time concepts, such as "always true," "eventually true," "has always been true," and "is true since." This type of reasoning is required in a world with mutable attributes. Lamport's temporal logic of action (TLA) provides the framework for formalizing the model and policy specifications. A fixed set of schema rules is defined to specify general UCON-policies that are subsequently proven sound and complete. The paper has 12 sections, presented in a typical academic style: an introduction; a motivating example; an introduction to UCON; an introduction to TLA; the logical model; the core authorization models of core UCON; models for obligations and conditions; a rule set that is sound and complete; the flexibility an expressive power of the model; related work; and conclusions and future work. The main contribution of this paper, according to the authors, is to formalize the UCON model with a temporal logic, while previously the model was informal and conceptual. This helps to define policies precisely, and give a precise meaning to the UCON features. Sections 6 and 10 prove that this approach is promising. A first step in understanding a user control system is understanding the scope of the proposed model. In this paper, a user control system is conceived as a system with six components: subjects and their attributes, objects and their attributes, rights, authorizations, obligations, and conditions. An authorization permits or denies access. Obligations are activities that must be performed by subjects. Conditions are environmental restrictions, unrelated to subject or object attributes. The authors point at two distinctive features of UCON: the continuity of access decisions and mutability of attributes. Decisions can be pre-decisions or ongoing decisions. Attribute updates can be pre-updates, ongoing updates, and post-updates, relative to their usage. Attribute updates can be administrator controlled or system controlled. The latter are mutable, the former are immutable as far as the system is concerned. There are three different kinds of attributes: subject, object, and system attributes. System state is a specific attribute with values initial, requested, denied, accessing, revoked, and end. There are two types of actions in UCON: user control actions and obligation actions. An update action changes the system state to a new one via an attribute update. System attributes cannot be updated. Actions are considered timeless. The transition from one system state to another is a usage control action. Actions are performed by either a subject or the system. An obligation is an action that must be performed by a subject before or during an access. The usage control decision is determined by authorizations before/during the usage, and there are no/one or more updates before and no/one or more updates during this usage. There are therefore eight core authorization models. Examples are given for each model. This uniform approach for heterogeneous existing models is refreshing, and it is well worth reading the paper just to gain an understanding and appreciation of this part. The next section provides a formal specification of general UCON models, and provides a proof of completeness and soundness. In the last core section, the authors discuss the expressivity and flexibility of the model. They include examples of role-based access control (RBAC); the Chinese Wall policy; dynamic separation of duty; the mandatory access control (MAC) policy with HIGH watermark property; and hospital information systems (HIS). Again, the approach supports a generic, concise, and clear description. Online Computing Reviews Service
Access critical reviews of Computing literature here
Become a reviewer for Computing Reviews.
Comments