Using First-Order Logic to Reason about Policies

ABSTRACT

A policy describes the conditions under which an action is permitted or forbidden. We show that a fragment of (multi-sorted) first-order logic can be used to represent and reason about policies. Because we use first-order logic, policies have a clear syntax and semantics. We show that further restricting the fragment results in a language that is still quite expressive yet is also tractable. More precisely, questions about entailment, such as “May Alice access the file?”, can be answered in time that is a low-order polynomial (indeed, almost linear in some cases), as can questions about the consistency of policy sets.

REFERENCES

• 1: Martín Abadi , Michael Burrows , Butler Lampson , Gordon Plotkin, A calculus for access control in distributed systems, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.4, p.706-734, Sept. 1993 [doi>10.1145/155183.155225]
• 2: Andrew W. Appel , Edward W. Felten, Proof-carrying authentication, Proceedings of the 6th ACM conference on Computer and communications security, p.52-62, November 01-04, 1999, Kent Ridge Digital Labs, Singapore [doi>10.1145/319709.319718]
• 3: Apple Computer, I. 2004. iTunes: Terms of sale. Available at http://www.apple.com/support/ itunes/legal/policies.html.
• 4: Moritz Y. Becker , Peter Sewell, Cassandra: Flexible Trust Management, Applied to Electronic Health Records, Proceedings of the 17th IEEE workshop on Computer Security Foundations, p.139, June 28-30, 2004 [doi>10.1109/CSFW.2004.7]
• 5: 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]
• 6: Blaze, M., Feigenbaum, J., Ioannidis, J., and Keromytis, A. 1998. The KeyNote trust management system. Available at http://www.cis.upenn.edu/~angelos/keynote.html.
• 7: Matt Blaze , Joan Feigenbaum , Jack Lacy, Decentralized Trust Management, Proceedings of the 1996 IEEE Symposium on Security and Privacy, p.164, May 06-08, 1996
• 8: Matt Blaze , Joan Feigenbaum , Martin Strauss, Compliance Checking in the PolicyMaker Trust Management System, Proceedings of the Second International Conference on Financial Cryptography, p.254-274, February 23-25, 1998
• 9: Börger, E., Grädel, E., and Gurevich, Y. 1997. The Classical Decision Problem. Perspectives of Mathematical Logic. Springer-Verlag, Berlin, Germany. 2nd printing (Universitext) 2001.
• 10: Brand, D. 1975. Proving theorems with the modification method. SIAM J. Comput. 4, 4, 412--430.
• 11: Chomicki, J., Lobo, J., and Naqvi, S. 2000. A logic programming approach to conflict resolution in policy management. In Principles of Knowledge Representation and Reasoning: Proceedings of the 9th International Conference (KR'00). 121--132.
• 12: ContentGuard. 2001. XrML: The digital rights language for trusted content and services. Available at http://www.xrml.org/.
• 13: John DeTreville, Binder, a Logic-Based Security Language, Proceedings of the 2002 IEEE Symposium on Security and Privacy, p.105, May 12-15, 2002
• 14: Ellison, C., Frantz, B., Lampson, B., Rivest, R., Thomas, B., and Ylonen, T. 1999a. Simple public key certificate. Available at http://world.std.com/~cme/spki.txt. Internet RFC 2693.
• 15: C. Ellison , B. Frantz , B. Lampson , R. Rivest , B. Thomas , T. Ylonen, SPKI Certificate Theory, RFC Editor, 1999
• 16: Enderton, H. B. 1972. A Mathematical Introduction to Logic. Academic Press, New York.
• 17: David F. Ferraiolo , John F. Barkley , D. Richard Kuhn, A role-based access control model and reference implementation within a corporate intranet, ACM Transactions on Information and System Security (TISSEC), v.2 n.1, p.34-64, Feb. 1999 [doi>10.1145/300830.300834]
• 18: Garcia-Molina, H., Ullman, J. D., and Widom, J. 2002. Database Systems: The Complete Book. Prentice Hall, New Jersey.
• 19: Janice Glasgow , Glenn Macewen , Prakash Panangaden, A logic for reasoning about security, ACM Transactions on Computer Systems (TOCS), v.10 n.3, p.226-264, Aug. 1992 [doi>10.1145/146937.146940]
• 20: Patricia P. Griffiths , Bradford W. Wade, An authorization mechanism for a relational database system, ACM Transactions on Database Systems (TODS), v.1 n.3, p.242-255, Sept. 1976 [doi>10.1145/320473.320482]
• 21: Joseph Y. Halpern , Ron van der Meyden, A logical reconstruction of SPKI, Journal of Computer Security, v.11 n.4, p.581-613, July 2003
• 22: Halpern, J. Y., van der Meyden, R., and Schneider, F. 1999. Logical foundations for trust management. Unpublished manuscript.
• 23: Halpern, J. Y. and Weissman, V. 2003. Using first-order logic to reason about policies. In Proceedings of the 16th IEEE Computer Security Foundations Workshop (CSFW'03). 187--201.
• 24: Joseph Y. Halpern , Vicky Weissman, A formal foundation for XrML, Journal of the ACM (JACM), v.55 n.1, p.1-42, February 2008 [doi>10.1145/1326554.1326558]
• 25: Michael Hitchens , Vijay Varadharajan, Tower: A Language for Role Based Access Control, Proceedings of the International Workshop on Policies for Distributed Systems and Networks, p.88-106, January 29-31, 2001
• 26: Iannella, R. 2001. ODRL: The open digital rights language initiative. Available at http://odrl.net/.
• 27: Ioannidis, Y. and Sellis, T. 1992. Supporting inconsistent rules in database systems. J. Intell. Inform. Syst. 1, 3/4, 243--270.
• 28: 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]
• 29: Trevor Jim, SD3: A Trust Management System with Certified Evaluation, Proceedings of the 2001 IEEE Symposium on Security and Privacy, p.106, May 14-16, 2001
• 30: Butler Lampson , Martín Abadi , Michael Burrows , Edward Wobber, Authentication in distributed systems: theory and practice, ACM Transactions on Computer Systems (TOCS), v.10 n.4, p.265-310, Nov. 1992 [doi>10.1145/138873.138874]
• 31: Ninghui Li , Benjamin N. Grosof , Joan Feigenbaum, Delegation logic: A logic-based approach to distributed authorization, ACM Transactions on Information and System Security (TISSEC), v.6 n.1, p.128-171, February 2003 [doi>10.1145/605434.605438]
• 32: Ninghui Li , John C. Mitchell, DATALOG with Constraints: A Foundation for Trust Management Languages, Proceedings of the 5th International Symposium on Practical Aspects of Declarative Languages, p.58-73, January 13-14, 2003
• 33: Ninghui Li , C. Mitchell, Understanding SPKI/SDSI using first-order logic, International Journal of Information Security, v.5 n.1, p.48-64, January 2006 [doi>10.1007/s10207-005-0073-0]
• 34: Ninghui Li , John C. Mitchell , William H. Winsborough, Design of a Role-Based Trust-Management Framework, Proceedings of the 2002 IEEE Symposium on Security and Privacy, p.114, May 12-15, 2002
• 35: Microsoft. 2003. Information rights management in Office Professional Edition 2003. Available at http://www.microsoft.com/office/editions/prodinfo/technologies/irm.mspx.
• 36: Moses, T. 2005. XACML: The eXtensible Access Control Markup Language, version 2.0. Available at http://www.xacml.org.
• 37: MPEG. 2004. Information technology---Multimedia framework (MPEG-21) -- Part 5: Rights Expression Language (ISO/IEC 21000-5:2004). Available at http://www.iso.ch/iso/en/.
• 38: Greg Nelson , Derek C. Oppen, Fast Decision Procedures Based on Congruence Closure, Journal of the ACM (JACM), v.27 n.2, p.356-364, April 1980 [doi>10.1145/322186.322198]
• 39: Anil Nerode , Richard Shore, Logic for Applications, Springer-Verlag New York, Inc., Secaucus, NJ, 1997
• 40: Charles P. Pfleeger, Security in computing, Prentice-Hall, Inc., Upper Saddle River, NJ, 1996
• 41: Pucella, R. and Weissman, V. 2004. A formal foundation for ODRL rights. In Workshop on Issues in the Theory of Security (WITS'04).
• 42: Rivest, R. and Lampson, B. 1996. SDSI --- A simple distributed security infrastructure. Available at http://theory.lcs.mit.edu/~cis/sdsi.html.
• 43: Robinson, G. and Wos, L. 1983. Paramodulation and theorem-proving in first-order theories with equality. In Automation of Reasoning 2: Classical Papers on Computational Logic 1967-1970, J. Siekmann and G. Wrightson, Eds. Springer, Berlin, Heidelberg, 298--313.
• 44: 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]
• 45: Daniel D. Sleator , Robert Endre Tarjan, A data structure for dynamic trees, Journal of Computer and System Sciences, v.26 n.3, p.362-391, June 1983 [doi>10.1016/0022-0000(83)90006-5]
• 46: Stockmeyer, L. J. 1977. The polynomial-time hierarchy. Theor. Comput. Sci. 3, 1--22.
• 47: Weissman, V. and Lagoze, C. 2004. Towards a policy language for humans and computers. In Proceedings of the 8th European Conference on Digital Libraries (ECDL'04). 513--525.
• 48: Wright, G. H. v. 1951. An Essay in Modal Logic. North-Holland, Amsterdam.

INDEX TERMS

Primary Classification:
  H. Information Systems
  H.2 DATABASE MANAGEMENT
      H.2.7 Database Administration
          Subjects: Security, integrity, and protection

Additional Classification:
  K. Computing Milieux
  K.4 COMPUTERS AND SOCIETY
      K.4.4 Electronic Commerce
          Subjects: Security

General Terms:
Languages, Security

Keywords:
Digital rights management