Skip to main content
SpringerLink
Log in

Logic in Access Control (Tutorial Notes)

  • Chapter
Foundations of Security Analysis and Design V (FOSAD 2009, FOSAD 2007, FOSAD 2008)

Part of the book series: Lecture Notes in Computer Science ((LNSC,volume 5705))

Abstract

Access control is central to security in computer systems. Over the years, there have been many efforts to explain and to improve access control, sometimes with logical ideas and tools. This paper is a partial survey and discussion of the role of logic in access control. It considers logical foundations for access control and their applications, in particular in languages for security policies. It focuses on some specific logics and their properties. It is intended as a written counterpart to a tutorial given at the 2009 International School on Foundations of Security Analysis and Design.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
eBook
USD 16.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 16.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abadi, M.: On SDSI’s linked local name spaces. Journal of Computer Security 6(1-2), 3–21 (1998)

    Article  Google Scholar 

  2. Abadi, M.: Logic in access control. In: Proceedings of the Eighteenth Annual IEEE Symposium on Logic in Computer Science, pp. 228–233 (2003)

    Google Scholar 

  3. Abadi, M.: Access control in a core calculus of dependency. Electronic Notes in Theoretical Computer Science 172, 5–31 (2007); Computation, Meaning, and Logic: Articles dedicated to Gordon Plotkin

    Article  MathSciNet  MATH  Google Scholar 

  4. Abadi, M.: Variations in access control logic. In: van der Meyden, R., van der Torre, L. (eds.) DEON 2008. LNCS, vol. 5076, pp. 96–109. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  5. Abadi, M., Banerjee, A., Heintze, N., Riecke, J.G.: A core calculus of dependency. In: Proceedings of the 26th ACM Symposium on Principles of Programming Languages, pp. 147–160 (1999)

    Google Scholar 

  6. Abadi, M., Burrows, M., Lampson, B., Plotkin, G.: A calculus for access control in distributed systems. ACM Transactions on Programming Languages and Systems 15(4), 706–734 (1993)

    Article  Google Scholar 

  7. Abadi, M., Wobber, T.: A logical account of NGSCB. In: de Frutos-Escrig, D., Núñez, M. (eds.) FORTE 2004. LNCS, vol. 3235, pp. 1–12. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  8. Appel, A.W., Felten, E.W.: Proof-carrying authentication. In: Proceedings of the 6th ACM Conference on Computer and Communications Security, pp. 52–62 (1999)

    Google Scholar 

  9. Bauer, L.: Access Control for the Web via Proof-Carrying Authorization. PhD thesis. Princeton University, Princeton (November 2003)

    Google Scholar 

  10. Bauer, L., Cranor, L., Reeder, R.W., Reiter, M.K., Vaniea, K.: A user study of policy creation in a flexible access-control system. In: CHI 2008: Conference on Human Factors in Computing Systems, pp. 543–552 (2008)

    Google Scholar 

  11. Bauer, L., Garriss, S., McCune, J.M., Reiter, M.K., Rouse, J., Rutenbar, P.: Device-enabled authorization in the grey system. In: Zhou, J., López, J., Deng, R.H., Bao, F. (eds.) ISC 2005. LNCS, vol. 3650, pp. 431–445. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  12. Bauer, L., Garriss, S., Reiter, M.K.: Distributed proving in access-control systems. In: Proceedings of the 2005 Symposium on Security and Privacy, pp. 81–95 (2005)

    Google Scholar 

  13. Becker, M.Y., Fournet, C., Gordon, A.D.: Design and semantics of a decentralized authorization language. In: Proceedings of the 20th IEEE Computer Security Foundations Symposium, pp. 3–15 (2007)

    Google Scholar 

  14. Benton, P.N., Bierman, G.M., de Paiva, V.C.V.: Computational types from a logical perspective. Journal of Functional Programming 8(2), 177–193 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  15. Bertino, E., Catania, B., Ferrari, E., Perlasca, P.: A logical framework for reasoning about access control models. ACM Transactions on Information and System Security 6(1), 71–127 (2003)

    Article  Google Scholar 

  16. Blaze, M., Feigenbaum, J., Ioannidis, J., Keromytis, A.D.: The KeyNote trust-management system, version 2. IETF RFC 2704 (September 1999)

    Google Scholar 

  17. Blaze, M., Feigenbaum, J., Lacy, J.: Decentralized trust management. In: Proceedings 1996 IEEE Symposium on Security and Privacy, pp. 164–173 (1996)

    Google Scholar 

  18. Cardelli, L.: Type systems. In: Tucker, A.B. (ed.) The Computer Science and Engineering Handbook, ch. 103, pp. 2208–2236. CRC Press, Boca Raton (1997)

    Google Scholar 

  19. Cederquist, J.G., Corin, R., Dekker, M.A.C., Etalle, S., den Hartog, J.I., Lenzini, G.: Audit-based compliance control. Int. J. Inf. Secur. 6(2), 133–151 (2007)

    Article  Google Scholar 

  20. Cirillo, A., Jagadeesan, R., Pitcher, C., Riely, J.: Do as I SaY! programmatic access control with explicit identities. In: Proceedings of the 20th IEEE Computer Security Foundations Symposium, pp. 16–30 (2007)

    Google Scholar 

  21. Crampton, J., Loizou, G., O’Shea, G.: A logic of access control. The Computer Journal 44(2), 137–149 (2001)

    Article  MATH  Google Scholar 

  22. DeTreville, J.: Binder, a logic-based security language. In: Proceedings of the 2002 IEEE Symposium on Security and Privacy, pp. 105–113 (2002)

    Google Scholar 

  23. Ellison, C., Frantz, B., Lampson, B., Rivest, R., Thomas, B., Ylönen, T.: SPKI certificate theory. IETF RFC 2693 (September 1999)

    Google Scholar 

  24. Fairtlough, M., Mendler, M.V.: Propositional lax logic. Information and Computation 137(1), 1–33 (1997)

    Article  MathSciNet  MATH  Google Scholar 

  25. Fournet, C., Gordon, A.D., Maffeis, S.: A type discipline for authorization in distributed systems. In: Proceedings of the 20th IEEE Computer Security Foundations Symposium, pp. 31–45 (2007)

    Google Scholar 

  26. Garg, D.: Principal-centric reasoning in constructive authorization logic. Technical Report CMU-CS-09-120, Computer Science Department, Carnegie Mellon University (April 2009)

    Google Scholar 

  27. Garg, D.: Proof search in an authorization logic. Technical Report CMU-CS-09-121, Computer Science Department, Carnegie Mellon University (April 2009)

    Google Scholar 

  28. Garg, D., Abadi, M.: A modal deconstruction of access control logics. In: Amadio, R.M. (ed.) FOSSACS 2008. LNCS, vol. 4962, pp. 216–230. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  29. Garg, D., Pfenning, F.: Non-interference in constructive authorization logic. In: Proceedings of the 19th IEEE Computer Security Foundations Workshop, pp. 283–296 (2006)

    Google Scholar 

  30. Gasser, M., Goldstein, A., Kaufman, C., Lampson, B.: The Digital Distributed System Security Architecture. In: Proceedings of the 1989 National Computer Security Conference, pp. 305–319 (1989)

    Google Scholar 

  31. Girard, J.-Y.: Interprétation Fonctionnelle et Elimination des Coupures de l’Arithmétique d’Ordre Supérieur. Thèse de doctorat d’état, Université Paris VII (June 1972)

    Google Scholar 

  32. Grove, A.J., Halpern, J.Y.: Naming and identity in epistemic logics, I: The propositional case. Journal of Logic and Computation 3(4), 345–378 (1993)

    Article  MathSciNet  MATH  Google Scholar 

  33. Gurevich, Y., Neeman, I.: DKAL: Distributed-knowledge authorization language. In: Proceedings of the 21st IEEE Computer Security Foundations Symposium, pp. 149–162 (2008)

    Google Scholar 

  34. Halpern, J.Y., van der Meyden, R.: A logic for SDSI’s linked local name spaces. Journal of Computer Security 9(1-2), 47–74 (2001)

    Article  Google Scholar 

  35. Halpern, J.Y., van der Meyden, R.: A logical reconstruction of SPKI. In: Proceedings of the 14th IEEE Computer Security Foundations Workshop, pp. 59–72 (2001)

    Google Scholar 

  36. Harrison, M.A., Ruzzo, W.L., Ullman, J.D.: Protection in operating systems. Communications of the ACM 19(8), 461–471 (1976)

    Article  MathSciNet  MATH  Google Scholar 

  37. Howell, J., Kotz, D.: A formal semantics for SPKI. In: Cuppens, F., Deswarte, Y., Gollmann, D., Waidner, M. (eds.) ESORICS 2000. LNCS, vol. 1895, pp. 140–158. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  38. Hughes, G.E., Cresswell, M.J.: An Introduction to Modal Logic. Methuen Inc., New York (1968)

    MATH  Google Scholar 

  39. Jajodia, S., Samarati, P., Subrahmanian, V.S.: A logical language for expressing authorizations. In: Proceedings of the 1997 IEEE Symposium on Security and Privacy, pp. 31–42 (1997)

    Google Scholar 

  40. Jajodia, S., Samarati, P., Subrahmanian, V.S., Bertino, E.: A unified framework for enforcing multiple access control policies. In: Proceedings of the ACM SIGMOD International Conference on Management of Data. SIGMOD Record, vol. 26(2), pp. 474–485 (1997)

    Google Scholar 

  41. Jia, L., Vaughan, J.A., Mazurak, K., Zhao, J., Zarko, L., Schorr, J., Zdancewic, S.: Aura: A programming language for authorization and audit. In: Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming, pp. 27–38 (2008)

    Google Scholar 

  42. Jim, T.: SD3: A trust management system with certified evaluation. In: Proceedings of the 2001 IEEE Symposium on Security and Privacy, pp. 106–115 (2001)

    Google Scholar 

  43. Lampson, B., Abadi, M., Burrows, M., Wobber, E.: Authentication in distributed systems: Theory and practice. ACM Transactions on Computer Systems 10(4), 265–310 (1992)

    Article  Google Scholar 

  44. Lampson, B.W.: Protection. In: Proceedings of the 5th Princeton Conference on Information Sciences and Systems, pp. 437–443 (1971)

    Google Scholar 

  45. Lampson, B.W.: Computer security in the real world. IEEE Computer 37(6), 37–46 (2004)

    Article  Google Scholar 

  46. Lesniewski-Laas, C., Ford, B., Strauss, J., Frans Kaashoek, M., Morris, R.: Alpaca: extensible authorization for distributed services. In: Proceedings of the 14th ACM Conference on Computer and Communications Security, pp. 432–444 (2007)

    Google Scholar 

  47. Li, N.: Local names in SPKI/SDSI. In: Proceedings of the 13th IEEE Computer Security Foundations Workshop, July 2000, pp. 2–15 (2000)

    Google Scholar 

  48. Li, N., Grosof, B.N., Feigenbaum: Delegation logic: A logic-based approach to distributed authorization. ACM Transactions on Information and System Security 6(1), 128–171 (2003)

    Article  Google Scholar 

  49. Li, N., Mitchell, J.C.: DATALOG with constraints: A foundation for trust management languages. In: Dahl, V., Wadler, P. (eds.) PADL 2003. LNCS, vol. 2562, pp. 58–73. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  50. Li, N., Mitchell, J.C., Winsborough, W.H.: Design of a role-based trust-management framework. In: Proceedings of the 2002 IEEE Symposium on Security and Privacy, pp. 114–130 (2002)

    Google Scholar 

  51. Li, N., Mitchell, J.C., Winsborough, W.H.: Beyond proof-of-compliance: security analysis in trust management. J. ACM 52(3), 474–514 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  52. Moggi, E.: Notions of computation and monads. Information and Control 93(1), 55–92 (1991)

    MathSciNet  MATH  Google Scholar 

  53. Necula, G.C.: Proof-carrying code. In: Proceedings of the 24th ACM Symposium on Principles of Programming Languages, pp. 106–119 (1997)

    Google Scholar 

  54. Pimlott, A., Kiselyov, O.: Soutei, a logic-based trust-management system. In: Hagiya, M., Wadler, P. (eds.) FLOPS 2006. LNCS, vol. 3945, pp. 130–145. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  55. Rivest, R.L., Lampson, B.: SDSI — A Simple Distributed Security Infrastructure (1996), http://theory.lcs.mit.edu/~cis/sdsi.html

  56. Rushby, J.: Design and verification of secure systems. In: Proceedings of the 8th ACM Symposium on Operating System Principles. ACM Operating Systems Review 15(5), 12–21 (1981)

    Google Scholar 

  57. Saltzer, J.H., Schroeder, M.D.: The protection of information in computer system. Proceedings of the IEEE 63(9), 1278–1308 (1975)

    Article  Google Scholar 

  58. Vaughan, J.A., Jia, L., Mazurak, K., Zdancewic, S.: Evidence-based audit. In: Proceedings of the 21st IEEE Computer Security Foundations Symposium, pp. 177–191 (2008)

    Google Scholar 

  59. Whitehead, N.: A certified distributed security logic for authorizing code. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol. 4502, pp. 253–268. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  60. Wobber, E., Abadi, M., Burrows, M., Lampson, B.: Authentication in the Taos operating system. ACM Transactions on Computer Systems 12(1), 3–32 (1994)

    Article  Google Scholar 

  61. eXtensible Access Control Markup Language (XACML) version 1.0. OASIS Standard (2003), http://www.oasis-open.org/committees/xacml/repository/

  62. eXtensible Rights Markup Language (XrML) version 2.0, http://www.xrml.org/

  63. Zhou, W., Mao, Y., Loo, B.T., Abadi, M.: Unified declarative platform for secure networked information systems. In: Proceedings of the 25th International Conference on Data Engineering, pp. 150–161 (2009)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Microsoft Research and University of California, Santa Cruz, USA

    Martín Abadi

Authors
  1. Martín Abadi
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Istituto di Scienze e Tecnologie dell’Informazione, Università degli Studi di Urbino “Carlo Bo”, Piazza della Repubblica 13, 61029, Urbino, Italy

    Alessandro Aldini

  2. IMDEA Software, UPM Facultad de Informatica, Campus Montegancedo, 28660, Boadilla del Monte, Madrid, Spain

    Gilles Barthe

  3. Dipartimento di Scienze dell’Informazione, Università degli Studi di Bologna, Mura Anteo Zamboni 7, 40127, Bologna, Italy

    Roberto Gorrieri

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Abadi, M. (2009). Logic in Access Control (Tutorial Notes). In: Aldini, A., Barthe, G., Gorrieri, R. (eds) Foundations of Security Analysis and Design V. FOSAD FOSAD FOSAD 2009 2007 2008. Lecture Notes in Computer Science, vol 5705. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-03829-7_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-03829-7_5

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-03828-0

  • Online ISBN: 978-3-642-03829-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation