xDomain: cross-border proofs of access

ABSTRACT

A number of research systems have demonstrated the benefits of accompanying each request with a machine-checkable proof that the request complies with access-control policy - a technique called proof-carrying authorization. Numerous authorization logics have been proposed as vehicles by which these proofs can be expressed and checked. A challenge in building such systems is how to allow delegation between institutions that use different authorization logics. Instead of trying to develop the authorization logic that all institutions should use, we propose a framework for interfacing different, mutually incompatible authorization logics. Our framework provides a very small set of primitives that defines an interface for communication between different logics without imposing any fundamental constraints on their design or nature. We illustrate by example that a variety of different logics can communicate over this interface, and show formally that supporting the interface does not impinge on the integrity of each individual logic. We also describe an architecture for constructing authorization proofs that contain components from different logics and report on the performance of a prototype proof checker.

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: Edward Wobber , Martín Abadi , Michael Burrows , Butler Lampson, Authentication in the Taos operating system, Proceedings of the fourteenth ACM symposium on Operating systems principles, p.256-269, December 05-08, 1993, Asheville, North Carolina, United States
• 3: 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]
• 4: Dirk Balfanz , Drew Dean , Mike Spreitzer, A Security Infrastructure for Distributed Java Applications, Proceedings of the 2000 IEEE Symposium on Security and Privacy, p.15, May 14-17, 2000
• 5: Ljudevit Bauer , Andrew W. Appel, Access control for the web via proof-carrying authorization, Princeton University, Princeton, NJ, 2003
• 6: L. Bauer, S. Garriss, J. M. McCune, M. K. Reiter, J. Rouse, and P. Rutenbar. Device-enabled authorization in the Grey system. In Information Security: 8th International Conference, ISC 2005, volume 3650 of Lecture Notes in Computer Science, pages 431--445, Sept. 2005.
• 7: Lujo Bauer , Scott Garriss , Michael K. Reiter, Distributed Proving in Access-Control Systems, Proceedings of the 2005 IEEE Symposium on Security and Privacy, p.81-95, May 08-11, 2005 [doi>10.1109/SP.2005.9]
• 8: L. Bauer, S. Garriss, and M. K. Reiter. Efficient proving for practical distributed access-control systems. In Computer Security-ESORICS 2007: 12th European Symposium on Research in Computer Security, volume 4734 of Lecture Notes in Computer Science, pages 19--37, Sept. 2007.
• 9: L. Bauer, L. Jia, M. K. Reiter, and D. Swasey. xDomain: Cross-border proofs of access. Technical Report CMU-CyLab-09-005, CyLab, Carnegie Mellon University, Mar. 2009.
• 10: M. Blaze , J. Feigenbaum , J. Ioannidis , A. Keromytis, The KeyNote Trust-Management System Version 2, RFC Editor, 1999
• 11: K. D. Bowers, L. Bauer, D. Garg, F. Pfenning, and M. K. Reiter. Consumable credentials in logic-based access-control systems. In Proceedings of the 2007 Network and Distributed System Security Symposium, pages 143--157, Feb. 2007.
• 12: John DeTreville, Binder, a Logic-Based Security Language, Proceedings of the 2002 IEEE Symposium on Security and Privacy, p.105, May 12-15, 2002
• 13: Henry DeYoung , Deepak Garg , Frank Pfenning, An Authorization Logic With Explicit Time, Proceedings of the 2008 21st IEEE Computer Security Foundations Symposium, p.133-145, June 23-25, 2008 [doi>10.1109/CSF.2008.15]
• 14: D. Garg, L. Bauer, K. D. Bowers, F. Pfenning, and M. K. Reiter. A linear logic of authorization and knowledge. In Computer Security-ESORICS 2006: 11th European Symposium on Research in Computer Security, volume 4189 of Lecture Notes in Computer Science, pages 297--312, Sept. 2006.
• 15: Deepak Garg , Frank Pfenn, Non-Interference in Constructive Authorization Logic, Proceedings of the 19th IEEE workshop on Computer Security Foundations, p.283-296, July 05-07, 2006 [doi>10.1109/CSFW.2006.18]
• 16: M. J. C. Gordon , T. F. Melham, Introduction to HOL: a theorem proving environment for higher order logic, Cambridge University Press, New York, NY, 1993
• 17: Joseph Y. Halpern , Ron van der Meyden, A logic for SDSI's linked local name spaces, Journal of Computer Security, v.9 n.1-2, p.105-142, Jan. 1,2001
• 18: J. Y. Halpern and V. Weissman. Using first-order logic to reason about policies. In Proceedings of the 16th IEEE Computer Security Foundations Workshop, pages 187--201, June 2003.
• 19: Robert Harper , Furio Honsell , Gordon Plotkin, A framework for defining logics, Journal of the ACM (JACM), v.40 n.1, p.143-184, Jan. 1993 [doi>10.1145/138027.138060]
• 20: Jonathan R. Howell , David Kotz, Naming and sharing resources across administrative boundaries, Dartmouth College, Hanover, NH, 2000
• 21: Jon Howell , David Kotz, A Formal Semantics for SPKI, Proceedings of the 6th European Symposium on Research in Computer Security, p.140-158, October 04-06, 2000
• 22: 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]
• 23: C. Lesniewski-Laas, B. Ford, J. Strauss, R. Morris, and M. F. Kaashoek. Alpaca, a proof-carrying authentication framework for cryptographic primitives and protocols. In Proceedings of the 14th ACM Conference on Computer and Communications Security, 2007.
• 24: 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]
• 25: 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
• 26: Kazuhiro Minami , David Kotz, Secure context-sensitive authorization, Pervasive and Mobile Computing, v.1 n.1, p.123-156, March 2005 [doi>10.1016/j.pmcj.2005.01.004]
• 27: George C. Necula, Proof-carrying code, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.106-119, January 15-17, 1997, Paris, France [doi>10.1145/263699.263712]
• 28: George Ciprian Necula , Peter Lee, Compiling with proofs, Carnegie Mellon University, Pittsburgh, PA, 1998
• 29: Frank Pfenning, Structural cut elimination, Information and Computation, v.157 n.1-2, p.84-141, Feb. 25/March 15, 2000 [doi>10.1006/inco.1999.2832]
• 30: Frank Pfenning , Carsten Schürmann, System Description: Twelf - A Meta-Logical Framework for Deductive Systems, Proceedings of the 16th International Conference on Automated Deduction: Automated Deduction, p.202-206, July 07-10, 1999
• 31: The Coq Development Team. The Coq Proof Assistant Reference Manual. LogiCal Project, 2006.

INDEX TERMS

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

Additional Classification:
  H. Information Systems
  H.2 DATABASE MANAGEMENT
      H.2.0 General
          Subjects: Security, integrity, and protection**

  K. Computing Milieux
  K.6 MANAGEMENT OF COMPUTING AND INFORMATION SYSTEMS
      K.6.5 Security and Protection (D.4.6, K.4.2)
          Subjects: Authentication

General Terms:
Security, Verification

Keywords:
distributed authorization, logic-based access control, trust management