Formal model and policy specification of usage control

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.

REFERENCES

• 1: Bell, D. E. and LaPadula, L. J. 1975. Secure computer systems: Mathematical foundations and model. Mitre Corp. Report No.M74-244, Bedford, MA.
• 2: Elisa Bertino , Claudio Bettini , Pierangela Samarati, A temporal authorization model, Proceedings of the 2nd ACM Conference on Computer and communications security, p.126-135, November 1994, Fairfax, Virginia, United States [doi>10.1145/191177.191202]
• 3: Elisa Bertino , Claudio Bettini , Elena Ferrari , Pierangela Samarati, A Temporal Access Control Mechanism for Database Systems, IEEE Transactions on Knowledge and Data Engineering, v.8 n.1, p.67-80, February 1996 [doi>10.1109/69.485637]
• 4: Elisa Bertino , Claudio Bettini , Elena Ferrari , Pierangela Samarati, An access control model supporting periodicity constraints and temporal reasoning, ACM Transactions on Database Systems (TODS), v.23 n.3, p.231-285, Sept. 1998 [doi>10.1145/293910.293151]
• 5: Elisa Bertino , Barbara Catania , Elena Ferrari , Paolo Perlasca, A logical framework for reasoning about access control models, Proceedings of the sixth ACM symposium on Access control models and technologies, p.41-52, May 2001, Chantilly, Virginia, United States [doi>10.1145/373256.373261]
• 6: C. Bettini , S. Jajodia , X. Wang , D. Wijesekera, Obligation Monitoring in Policy Management, Proceedings of the 3rd International Workshop on Policies for Distributed Systems and Networks (POLICY'02), p.2, June 05-07, 2002
• 7: 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.
• 8: Brewer, D. and Nash, M. 1988. The chinese wall security policy. In Proceedings of the IEEE Symposium on Research in Security and Privacy.
• 9: Jan Chomicki , Jorge Lobo, Monitors for History-Based Policies, Proceedings of the International Workshop on Policies for Distributed Systems and Networks, p.57-72, January 29-31, 2001
• 10: Nicodemos Damianou , Naranker Dulay , Emil Lupu , Morris Sloman, The Ponder Policy Specification Language, Proceedings of the International Workshop on Policies for Distributed Systems and Networks, p.18-38, January 29-31, 2001
• 11: Dorothy E. Denning, A lattice model of secure information flow, Communications of the ACM, v.19 n.5, p.236-243, May 1976 [doi>10.1145/360051.360056]
• 12: Avigdor Gal , Vijayalakshmi Atluri, An authorization model for temporal data, Proceedings of the 7th ACM conference on Computer and communications security, p.144-153, November 01-04, 2000, Athens, Greece [doi>10.1145/352600.352621]
• 13: Michael R. Hansen , Robin Sharp, Using interval logics for temporal analysis of security protocols, Proceedings of the 2003 ACM workshop on Formal methods in security engineering, p.24-31, October 30, 2003, Washington, D.C. [doi>10.1145/1035429.1035432]
• 14: Sushil Jajodia , Pierangela Samarati , V. S. Subrahmanian, A Logical Language for Expressing Authorizations, Proceedings of the 1997 IEEE Symposium on Security and Privacy, p.31, May 04-07, 1997
• 15: Sushil Jajodia , Pierangela Samarati , Maria Luisa Sapino , V. S. Subrahmanian, Flexible support for multiple access control policies, ACM Transactions on Database Systems (TODS), v.26 n.2, p.214-260, June 2001 [doi>10.1145/383891.383894]
• 16: James B. D. Joshi , Basit Shafiq , Arif Ghafoor , Elisa Bertino, Dependencies and separation of duty constraints in GTRBAC, Proceedings of the eighth ACM symposium on Access control models and technologies, June 02-03, 2003, Como, Italy [doi>10.1145/775412.775420]
• 17: James B. D. Joshi , Elisa Bertino , Usman Latif , Arif Ghafoor, A Generalized Temporal Role-Based Access Control Model, IEEE Transactions on Knowledge and Data Engineering, v.17 n.1, p.4-23, January 2005 [doi>10.1109/TKDE.2005.1]
• 18: Leslie Lamport, The temporal logic of actions, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.3, p.872-923, May 1994 [doi>10.1145/177492.177726]
• 19: Zohar Manna , Amir Pnueli, The temporal logic of reactive and concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1992
• 20: Jaehong Park , Ravi Sandhu, The UCON_ABC usage control model, ACM Transactions on Information and System Security (TISSEC), v.7 n.1, p.128-174, February 2004 [doi>10.1145/984334.984339]
• 21: 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.
• 22: Ravi S. Sandhu, Lattice-Based Access Control Models, Computer, v.26 n.11, p.9-19, November 1993 [doi>10.1109/2.241422]
• 23: 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.
• 24: Ravi S. Sandhu , Edward J. Coyne , Hal L. Feinstein , Charles E. Youman, Role-Based Access Control Models, Computer, v.29 n.2, p.38-47, February 1996 [doi>10.1109/2.485845]
• 25: François Siewe , Antonio Cau , Hussein Zedan, A compositional framework for access control policies enforcement, Proceedings of the 2003 ACM workshop on Formal methods in security engineering, p.32-42, October 30, 2003, Washington, D.C. [doi>10.1145/1035429.1035433]
• 26: Richard Simon , Mary Ellen Zurko, Separation of Duty in Role-based Environments, Proceedings of the 10th Computer Security Foundations Workshop (CSFW '97), p.183, June 10-12, 1997

INDEX TERMS

Primary Classification:
  D. Software
  D.4 OPERATING SYSTEMS
      D.4.6 Security and Protection
          Subjects: Access controls

Additional Classification:
  K. Computing Milieux
  K.6 MANAGEMENT OF COMPUTING AND INFORMATION SYSTEMS
      K.6.5 Security and Protection (D.4.6, K.4.2)
          Subjects: Unauthorized access (e.g., hacking, phreaking)

Keywords:
Access control, formal specification, security policy, usage control