Abstract
We present a model of access control which provides fine-grained data-dependent control, can express permissions about permissions, can express delegation, and can describe systems which avoid the root-bottleneck problem. We present a language for describing goals of agents; these goals are typically to read or write the values of some resources. We describe a decision procedure which determines whether a given coalition of agents has the means (possibly indirectly) to achieve its goal. We argue that this question is decidable in the situation of the potential intruders acting in parallel with legitimate users and taking whatever temporary opportunities the actions of the legitimate users present. Our technique can also be used to synthesise finite access control systems, from an appropriately formulated logical theory describing a high-level policy.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
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)
Bacon, J.M., Moody, K., Yao, W.: Access control and trust in the use of widely distributed services. In: Guerraoui, R. (ed.) Middleware 2001. LNCS, vol. 2218, p. 295. Springer, Heidelberg (2001) ,Also: Software Practice and Experience 33, (2003)
Bandmann, O., Dam, M., Firozabadi, B.: Constrained delegations. In: Proc. IEEE Symposium on Security and Privacy, pp. 131–142 (2002)
Barka, E.S.: Framework for Role-Based Delagation Models. PhD thesis, George Mason University (2002)
De Capitani di Vimercati, S., Paraboschi, S., Samarati, P.: Access control: principles and solutions. Software Practice and Experience 33, 397–421 (2003)
Guelev, D.P.: Prolog code supporting Model-checking access control policies (November 2003), http://www.cs.bham.ac.uk/~dpg/mcacp/
Guelev, D.P., Ryan, M.D., Schobbens, P.Y.: Model-checking access control policies (April 2004), http://www.cs.bham.ac.uk/~dpg/fullaclpaper.ps/
Harrison, M., Ruzzo, W.: Monotonic protection systems. Academic Press, New York (1978)
Harrison, M.A., Ruzzo, W.L., Ullman, J.D.: On protection in operating systems. In: Proceedings of the fifth symposium on Operating systems principles, pp. 14–24. ACM Press, New York (1975)
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)
Lipton, R., Snyder, L.: On synchronization and security. Academic Press, New York (1978)
Riis Nielson, H., Nielson, F.: Semantics with Applications: A Formal Introduction. Wiley, Chichester (1992)
Sandhu, R.: The typed access matrix model. In: Proceedings of the IEEE Symposium on Research in Security and Privacy, pp. 122–136. IEEE Computer Society Press, Los Alamitos (1992)
Sandhu, R.S., Coyne, E.J., Feinstein, H.L., Youman, C.E.: Role-based access control models. IEEE Computer 29(2), 38–47 (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Guelev, D.P., Ryan, M., Schobbens, P.Y. (2004). Model-Checking Access Control Policies. In: Zhang, K., Zheng, Y. (eds) Information Security. ISC 2004. Lecture Notes in Computer Science, vol 3225. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30144-8_19
Download citation
DOI: https://doi.org/10.1007/978-3-540-30144-8_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23208-7
Online ISBN: 978-3-540-30144-8
eBook Packages: Springer Book Archive