New Modalities for Access Control Logics: Permission, Control and Ratification

  • Valerio Genovese
  • Deepak Garg
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7170)


We present a new modal access control logic, ACL + , to specify, reason about and enforce access control policies. The logic includes new modalities for permission, control, and ratification to overcome some limits of current access control logics. We present a Hilbert-style proof system for ACL +  and a sound and complete Kripke semantics for it. We exploit the Kripke semantics to define Seq-ACL + : a sound, complete and cut-free sequent calculus for ACL + , implying that ACL +  is at least semi-decidable. We point at a Prolog implementation of Seq-ACL +  and discuss possible extensions of ACL +  with axioms for subordination between principals.


Access Control Modal Logic Sequent Calculus Kripke Semantic Proof Search 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abadi, M.: Logic in access control. In: Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science (LICS), pp. 228–233 (2003)Google Scholar
  2. 2.
    Abadi, M.: Variations in Access Control Logic. In: van der Meyden, R., van der Torre, L. (eds.) DEON 2008. LNCS (LNAI), vol. 5076, pp. 96–109. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  3. 3.
    Abadi, M.: Logic in access control (tutorial notes). In: Proceedings of the 9th International School on Foundations of Security Analysis and Design (FOSAD), pp. 145–165 (2009)Google Scholar
  4. 4.
    Basin, D., D’Agostino, M., Gabbay, D.M., Matthews, S., Viganó, L.: Labelled Deduction. Springer, Heidelberg (2000)zbMATHCrossRefGoogle Scholar
  5. 5.
    Bauer, L.: Access Control for the Web via Proof-Carrying Authorization. Ph.D. thesis, Princeton University (2003)Google Scholar
  6. 6.
    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)CrossRefGoogle Scholar
  7. 7.
    Becker, M.Y., Fournet, C., Gordon, A.D.: SecPAL: Design and semantics of a decentralized authorization language. Journal of Computer Security 18(4), 619–665 (2010)Google Scholar
  8. 8.
    Boella, G., Gabbay, D.M., Genovese, V., van der Torre, L.: Fibred security language. Studia Logica 92(3), 395–436 (2009)MathSciNetzbMATHCrossRefGoogle Scholar
  9. 9.
    Dinesh, N., Joshi, A.K., Lee, I., Sokolsky, O.: Permission to speak: A logic for access control and conformance. Journal of Logic and Algebraic Programming 80(1), 50–74 (2011)MathSciNetzbMATHCrossRefGoogle Scholar
  10. 10.
    Garg, D.: Principal centric reasoning in constructive authorization logic. In: Informal Proceedings of Intuitionistic Modal Logic and Application (IMLA) (2008), Full version available as Carnegie Mellon Technical Report CMU-CS-09-120Google Scholar
  11. 11.
    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)CrossRefGoogle Scholar
  12. 12.
    Garg, D., Pfenning, F.: Non-interference in constructive authorization logic. In: Proceedings of the 19th IEEE Computer Security Foundations Workshop (CSFW), pp. 283–293 (2006)Google Scholar
  13. 13.
    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
  14. 14.
    Genovese, V., Giordano, L., Gliozzi, V., Pozzato, G.L.: A constructive conditional logic for access control: A preliminary report. In: Proceedings of the 19th European Conference on Artificial Intelligence (ECAI), pp. 1073–1074 (2010)Google Scholar
  15. 15.
    Genovese, V., Giordano, L., Gliozzi, V., Pozzato, G.L.: Logics for access control: A conditional approach. In: Informal Proceedings of the 1st Workshop on Logic in Security (LIS), pp. 78–92 (2010)Google Scholar
  16. 16.
    Genovese, V., Giordano, L., Gliozzi, V., Pozzato, G.L.: A Conditional Constructive Logic for Access Control and its Sequent Calculus. In: Brünnler, K., Metcalfe, G. (eds.) TABLEAUX 2011. LNCS, vol. 6793, pp. 164–179. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  17. 17.
    Gurevich, Y., Neeman, I.: Logic of infons: The propositional case. ACM Transactions on Computational Logic 12(2), 1–28 (2011)MathSciNetCrossRefGoogle Scholar
  18. 18.
    Lampson, B.W., Abadi, M., Burrows, M., Wobber, E.: Authentication in distributed systems: Theory and practice. ACM Transactions on Computer Systems 10(4), 265–310 (1992)CrossRefGoogle Scholar
  19. 19.
    Negri, S.: Proof analysis in modal logic. Journal of Philosophical Logic 34, 507–544 (2005)MathSciNetzbMATHCrossRefGoogle Scholar
  20. 20.
    Negri, S., von Plato, J.: Proof Analysis. Cambridge University Press (2011)Google Scholar
  21. 21.
    Schneider, F.B., Walsh, K., Sirer, E.G.: Nexus Authorization Logic (NAL): Design rationale and applications. ACM Transcations on Information and System Security 14(1), 1–28 (2011)CrossRefGoogle Scholar
  22. 22.
    Wobber, E., Abadi, M., Burrows, M.: Authentication in the taos operating system. ACM Transactions on Computer Systems 12(1), 3–32 (1994)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2012

Authors and Affiliations

  • Valerio Genovese
    • 1
    • 2
  • Deepak Garg
    • 3
  1. 1.University of LuxembourgLuxembourg
  2. 2.University of TorinoItaly
  3. 3.Max Planck Institute for Software SystemsGermany

Personalised recommendations