Abstract
We describe a sound, complete, and terminating procedure for goal-directed proof search in \(\text{BL}_{\text{sf}}^{\textsf{G}}\), an expressive fragment of a recently presented access control logic, BLsf. \(\text{BL}_{\text{sf}}^{\textsf{G}}\) is more expressive than many other Datalog-based access control logics that also have very efficient decision procedures, and our search procedure finds proofs of authorization quickly in practice. We also extend our search procedure to find missing credentials when a requested authorization does not hold and discuss an implementation of our techniques in an extension of the Unix file synchronization program rsync.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abadi, M.: Logic in access control. In: Proceedings of the IEEE Symposium on Logic in Computer Science (LICS), pp. 228–233 (2003)
Abadi, M., Burrows, M., Lampson, B., Plotkin, G.: A calculus for access control in distributed systems. ACM Transactions on Programming Languages and Systems (TOPLAS) 15(4), 706–734 (1993)
Avijit, K., Datta, A., Harper, R.: Distributed programming with distributed authorization. In: Proceedings of the ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI), pp. 27–38 (2010)
Bauer, L.: Access Control for the Web via Proof-Carrying Authorization. Ph.D. thesis, Princeton University (2003)
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)
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)
Becker, M.Y., Russo, A., Sultana, N.: Foundation of logic-based trust management. In: Proceedings of the IEEE Symposium on Security and Privacy, pp. 161–175 (2012)
DeTreville, J.: Binder, a logic-based security language. In: Proceedings of the IEEE Symposium on Security and Privacy, pp. 105–113 (2002)
Garg, D.: Proof Theory for Authorization Logic and Its Application to a Practical File System. Ph.D. thesis, Carnegie Mellon University (2009)
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)
Garg, D., Pfenning, F.: A proof-carrying file system. In: Proceedings of the IEEE Symposium on Security and Privacy, pp. 349–364 (2010)
Genovese, V., Rispoli, D., Gabbay, D.M., van der Torre, L.: Modal access control logic: Axiomatization, semantics and FOL theorem proving. In: Proceedings of the Fifth Starting AI Researchers’ Symposium (STAIRS), pp. 114–126 (2010)
Genovese, V., Garg, D., Rispoli, D.: Labeled goal-directed search in access control logic (2012), Technical Report. Online at http://www.mpi-sws.org/~dg/
Genovese, V., Garg, D., Rispoli, D.: Labeled sequent calculi for access control logics: Countermodels, saturation and abduction. In: Proceedings of the 25th IEEE Symposium on Computer Security Foundations (CSF), pp. 139–153 (2012)
Gurevich, Y., Neeman, I.: Logic of infons: The propositional case. ACM Transactions on Programming Languages and Systems (TOPLAS) 12(2) (2011)
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 (ICFP), pp. 27–38 (2008)
Miller, D., Nadathur, G., Pfenning, F., Scedrov, A.: Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic 51, 125–157 (1991)
Negri, S.: Proof analysis in modal logic. Journal of Philosophical Logic 34, 507–544 (2005)
Pimlott, A., Kiselyov, O.: Soutei, a logic-based trust-management system. In: Hagiya, M. (ed.) FLOPS 2006. LNCS, vol. 3945, pp. 130–145. Springer, Heidelberg (2006)
Schneider, F.B., Walsh, K., Sirer, E.G.: Nexus Authorization Logic (NAL): Design rationale and applications. ACM Transactions on Information and System Security (TISSEC) 14(1), 1–28 (2011)
Swamy, N., Chen, J., Fournet, C., Strub, P.Y., Bhargavan, K., Yang, J.: Secure distributed programming with value-dependent types. In: Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming (ICFP), pp. 266–278 (2011)
Viganò, L.: A framework for non-classical logics. Ph.D. thesis, Universität des Saarlandes (1997), also available as the book Labelled non-classical logics. Springer (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Genovese, V., Garg, D., Rispoli, D. (2013). Labeled Goal-Directed Search in Access Control Logic. In: Jøsang, A., Samarati, P., Petrocchi, M. (eds) Security and Trust Management. STM 2012. Lecture Notes in Computer Science, vol 7783. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38004-4_5
Download citation
DOI: https://doi.org/10.1007/978-3-642-38004-4_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-38003-7
Online ISBN: 978-3-642-38004-4
eBook Packages: Computer ScienceComputer Science (R0)