Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Security and Trust Management

STM 2010: Security and Trust Management pp 210–225Cite as

Stateful Authorization Logic:

Proof Theory and a Case Study

  • Conference paper

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

Abstract

Authorization policies can be conveniently represented and reasoned about in logic. Proof theory is important for many such applications of logic. However, so far, there has been no systematic study of proof theory that incorporates system state, upon which access policies often rely. The present paper fills this gap by presenting the design and proof theory of an authorization logic BL that, among other features, includes direct support for external procedures to verify predicates on system state. We discuss design choices in the interaction between state and other features of the logic and validate the logic both foundationally, by proving relevant metatheoretic properties of the logic’s proof system, and empirically, through a case study of policies that control access to sensitive intelligence information in the U.S.

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

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   54.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   69.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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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 

  2. 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 

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

    Google Scholar 

  4. Bauer, L.: Access Control for the Web via Proof-Carrying Authorization. Ph.D. thesis, Princeton University (2003)

    Google Scholar 

  5. 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 

  6. Becker, M.Y.: Specification and analysis of dynamic authorisation policies. In: 22nd IEEE Computer Security Foundations Symposium (CSF), pp. 203–217 (2009)

    Google Scholar 

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

    Google Scholar 

  8. Becker, M.Y., Nanz, S.: A logic for state-modifying authorization policies. In: Biskup, J., López, J. (eds.) ESORICS 2007. LNCS, vol. 4734, pp. 203–218. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  9. Becker, M.Y., Sewell, P.: Cassandra: Flexible trust management applied to health records. In: 17th IEEE Computer Security Foundations Workshop (CSFW), pp. 139–154 (2004)

    Google Scholar 

  10. Borgstrm, J., Gordon, A.D., Pucella, R.: Roles, stacks, histories: A triple for Hoare. Tech. Rep. MSR-TR-2009-97, Microsoft Research (2009)

    Google Scholar 

  11. Broberg, N., Sands, D.: Paralocks: Role-based information flow control and beyond. SIGPLAN Notices 45(1), 431–444 (2010)

    Article  MATH  Google Scholar 

  12. DeYoung, H., Garg, D., Pfenning, F.: An authorization logic with explicit time. In: 21st IEEE Computer Security Foundations Symposium (CSF), pp. 133–145 (2009); extended version available as Carnegie Mellon University Technical Report CMU-CS-07-166

    Google Scholar 

  13. DeYoung, H., Pfenning, F.: Reasoning about the consequences of authorization policies in a linear epistemic logic, Workshop on Foundations of Computer Security, FCS (2009), http://www.cs.cmu.edu/~hdeyoung/papers/fcs09.pdf

  14. Garg, D.: Proof Theory for Authorization Logic and Its Application to a Practical File System. Ph.D. thesis, Carnegie Mellon University, Technical Report CMU-CS-09-168 (2009)

    Google Scholar 

  15. Garg, D., Pfenning, F.: Non-interference in constructive authorization logic. In: 19th Computer Security Foundations Workshop (CSFW), pp. 283–293 (2006)

    Google Scholar 

  16. Garg, D., Pfenning, F.: A proof-carrying file system. In: Proceedings of the 31st IEEE Symposium on Security and Privacy, Oakland, pp. 349–364 (2010)

    Google Scholar 

  17. Garg, D., Pfenning, F., Serenyi, D., Witten, B.: A logical representation of common rules for controlling access to classified information. Tech. Rep. CMU-CS-09-139, Carnegie Mellon University (2009)

    Google Scholar 

  18. Gentzen, G.: Untersuchungen über das logische Schließen. Mathematische Zeitschrift 39, 176–210, 405–431 (1935); English translation in Szabo, M.E. (ed.) The Collected Papers of Gerhard Gentzen, pp. 68–131. North-Holland, Amsterdam (1969)

    Google Scholar 

  19. Housley, R., Ford, W., Polk, W., Solo, D.: Internet X.509 public key infrastructure (1999), http://www.ietf.org/rfc/rfc2459.txt

  20. Jia, L.: Linear Logic and Imperative Programming. Ph.D. thesis, Department of Computer Science, Princeton University (2008)

    Google Scholar 

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

    Google Scholar 

  22. Martin-Löf, P.: On the meanings of the logical constants and the justifications of the logical laws. Nordic Journal of Philosophical Logic 1(1), 11–60 (1996)

    MathSciNet  MATH  Google Scholar 

  23. Office of the Director of Central Intelligence: DCID 1/19: Security policy for sensitive compartmented information and security policy manual (1995), http://www.fas.org/irp/offdocs/dcid1-19.html

  24. Office of the Director of Central Intelligence: DCID 1/7: Security controls on the dissemination of intelligence information (1998), http://www.fas.org/irp/offdocs/dcid1-7.html

  25. Office of the Press Secretary of the White House: Executive order 12958: Classified national security information (1995), http://www.fas.org/sgp/clinton/eo12958.html

  26. Office of the Press Secretary of the White House: Executive order 13292: Further amendment to executive order 12958, as amended, classified national security information (2003), http://nodis3.gsfc.nasa.gov/displayEO.cfm?id=EO_13292_

  27. Pfenning, F.: Structural cut elimination I. Intuitionistic and classical logic. Information and Computation 157(1/2), 84–141 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  28. Pfenning, F., Davies, R.: A judgmental reconstruction of modal logic. Mathematical Structures in Computer Science 11, 511–540 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  29. Saranli, U., Pfenning, F.: Using constrained intuitionistic linear logic for hybrid robotic planning problems. In: International Conference on Robotics and Automation (ICRA), pp. 3705–3710 (2007)

    Google Scholar 

  30. Schneider, F.B., Walsh, K., Sirer, E.G.: Nexus Authorization Logic (NAL): Design rationale and applications. Tech. rep. Cornell University (2009), http://ecommons.library.cornell.edu/handle/1813/13679

Download references

Author information

Authors and Affiliations

  1. Carnegie Mellon University, USA

    Deepak Garg & Frank Pfenning

Authors
  1. Deepak Garg
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Frank Pfenning
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Siemens AG - Corporate Technology, Otto-Hahn-Ring 6, 81730, München, Germany

    Jorge Cuellar

  2. Computer Science Department, E.T.S. Ingenieria Informatica, University of Malaga, Campus de Teatinos, 29170, Malaga, Spain

    Javier Lopez

  3. Facultad de Informatica (UPM), Fundación IMDEA Software, Campus Montegancedo, 28660 Boadilla del Monte, Madrid, Spain

    Gilles Barthe

  4. Certifiable Trustworthy IT Systems, Karlsruhe Institute of Technology (KIT), Am Fasanengarten 5, 76131, Karlsruhe, Germany

    Alexander Pretschner

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Garg, D., Pfenning, F. (2011). Stateful Authorization Logic:. In: Cuellar, J., Lopez, J., Barthe, G., Pretschner, A. (eds) Security and Trust Management. STM 2010. Lecture Notes in Computer Science, vol 6710. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-22444-7_14

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-22444-7_14

  • Publisher Name: Springer, Berlin, Heidelberg

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

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

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation