Policy algebras for access control the predicate case

ABSTRACT

This paper deals with the algebra used to compose access control policies of collaborating organizations. To maintain a conceptual coherence and to have a common basis for comparison, we seek a framework that can be viewed at different levels of abstraction. In [21, 22], we presented a propositional version of the algebra that can support algebraic manipulations of uninterpreted policies. This paper extends the algebra to many sorted first order predicate case. The predicate version can be used to reason about first order properties of security policies from their components. We show how to compose and reason about security properties such as those used in role based access control models usually specified using second order (set) quantifiers in languages (see RCL2000 [1]). We also show how different application specific notions of consistency and completeness can be formulated as sentences in our many sorted first order logic and propose a Hoare calculus to reason about them.

REFERENCES

• 1: Gail-Joon Ahn , Ravi Sandhu, Role-based authorization constraints specification, ACM Transactions on Information and System Security (TISSEC), v.3 n.4, p.207-226, Nov. 2000 [doi>10.1145/382912.382913]
• 2: B. Alpern and F. B. Schneider. Defining liveness. Information Processing Letters, 21(4):181--185, October 1985.
• 3: B. Alpern and F. B. Schneider. Recognizing safety and liveness. Distributed Computing, 2:117--126, 1987.
• 4: Yun Bai , Vijay Varadharajan, A Logic For State Transformations in Authorization Policies, Proceedings of the 10th Computer Security Foundations Workshop (CSFW '97), p.173, June 10-12, 1997
• 5: J. Barwise and S. Feffermann. Model Theoretic Logics. Springer-Verlag, 1985.
• 6: Piero Bonatti , Sabrina de Capitani di Vimercati , Pierangela Samarati, A modular approach to composing access control policies, Proceedings of the 7th ACM conference on Computer and communications security, p.164-173, November 01-04, 2000, Athens, Greece [doi>10.1145/352600.352623]
• 7: S. A. Cook. Soundness and completeness of an axiom system for program verfication. SIAM Journal on Computing, pages 79--90, 1978.
• 8: J. Dobson and J. McDermid. A framework for expressing models of security policy. In Proceedings of IEEE Symposium on Security and Privacy, pages 229--239, May 1989.
• 9: H. B. Enderton. Mathematical Introduction to Logic. Harcourt Academic Press, 2001.
• 10: David Gries, The Science of Programming, Springer-Verlag New York, Inc., Secaucus, NJ, 1987
• 11: David Harel , Jerzy Tiuryn , Dexter Kozen, Dynamic Logic, MIT Press, Cambridge, MA, 2000
• 12: Elisa Bertino , Sushil Jajodia , Pierangela Samarati, A flexible authorization mechanism for relational data management systems, ACM Transactions on Information Systems (TOIS), v.17 n.2, p.101-140, April 1999 [doi>10.1145/306686.306687]
• 13: 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]
• 14: Jacques Leockx , Kurt Sieber , Ryan D. Stansifer, The foundations of program verification (2nd ed.), John Wiley & Sons, Inc., New York, NY, 1987
• 15: John McLean, A General Theory of Composition for Trace Sets Closed under Selective Interleaving Functions, Proceedings of the 1994 IEEE Symposium on Security and Privacy, p.79, May 16-18, 1994
• 16: John McLean, A General Theory of Composition for a Class of "Possibilistic" Properties, IEEE Transactions on Software Engineering, v.22 n.1, p.53-67, January 1996 [doi>10.1109/32.481534]
• 17: J. McLean. Algebra of security. In Proc. IEEE Symp. on Security and Privacy, pages 2--7, Oakland, CA, May 1998.
• 18: 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]
• 19: Ravi Sandhu , Venkata Bhamidipati , Qamar Munawer, The ARBAC97 model for role-based administration of roles, ACM Transactions on Information and System Security (TISSEC), v.2 n.1, p.105-135, Feb. 1999 [doi>10.1145/300830.300839]
• 20: Fred B. Schneider, Enforceable Security Policies, Cornell University, Ithaca, NY, 1998
• 21: Duminda Wijesekera , Sushil Jajodia, Policy algebras for access control: the propositional case, Proceedings of the 8th ACM conference on Computer and Communications Security, November 05-08, 2001, Philadelphia, PA, USA [doi>10.1145/501983.501990]
• 22: Duminda Wijesekera , Sushil Jajodia, A propositional policy algebra for access control, ACM Transactions on Information and System Security (TISSEC), v.6 n.2, p.286-325, May 2003 [doi>10.1145/762476.762481]