Abstract
In this paper a Timed Automata (TA) based verification framework is proposed for Temporal RBAC. Roles, users, permissions - three basic components of RBAC are modeled using TA. These components interact with each other through channel synchronization. A parallel composition of TA is used to construct the complete system. Temporal constraints on roles, user-role assignments and role-permission assignments are conveniently expressed in this representation. Furthermore, both role hierarchy and separation of duty (SoD) have been incorporated in the proposed framework. Security properties are specified using Computation Tree Logic (CTL) and verified by model checking.
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
Sandhu, R., Coyne, E., Feinstein, H., Youman, C.: Role based access control models. IEEE Computer 29(2), 38–47 (1996)
Bertino, E., Bonatti, P.A.: TRBAC: A temporal role based access control model. ACM Transactions on Information and System Security 4(3), 191–223 (2001)
Joshi, J.B.D., Bertino, E., Latif, U., Ghafoor, A.: A generalized temporal role-based access control model. IEEE Transactions on Knowledge and Data Engineering 17(1), 4–23 (2005)
Ahmed, T., Tripathi, A.R.: Static verification of security requirements in role based CSCW systems. In: 8th ACM Symposium on Access Control Models and Technologies, Italy, pp. 196–203 (June 2003)
Li, N., Tripunitara, M.V.: Security analysis in role based access control. ACM Transactions on Information System Security 9(4), 391–420 (2006)
Jha, S., Li, N., Tripunitara, M., Wang, Q., Winsborough, W.: Towards formal verification of role based access control policies. IEEE Transactions on Dependable and Secure Computing (to appear, 2008)
Shafiq, B., Masood, A., Joshi, J., Ghafoor, A.: A role based access control policy verification framework for real time systems. In: 10th IEEE International Workshop on Object Oriented Real Time Dependable Systems, USA, pp. 13–20 (2005)
Alur, R., Courcoubetis, C., Dill, D.L.: Model checking for real time systems. In: 5th Symposium on Logic in Computer Science, USA, pp. 414–425 (1990)
Furfaro, A., Nigro, L.: Temporal verification of communicating real time state machines using Uppaal. In: IEEE International Conference on Industrial Technology, Slovenia, pp. 399–404 (2003)
Mondal, S., Sural, S.: Security analysis of Temporal-RBAC using timed automata. In: 4th International Conference on Information Assurance and Security, Italy, pp. 37–40 (2008)
Alur, R., Dill, D.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)
Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: 4th International School on Formal Methods for the Design of Computer, Communication and Software Systems: Real Time, Italy, pp. 200–236 (2004)
Joshi, J.B.D., Bertino, E., Ghafoor, A.: Hybrid role hierarchy for generalized temporal role based access control model. In: 26th Annual International Computer Software and Application Conference, England, pp. 951–956 (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mondal, S., Sural, S. (2008). A Verification Framework for Temporal RBAC with Role Hierarchy (Short Paper). In: Sekar, R., Pujari, A.K. (eds) Information Systems Security. ICISS 2008. Lecture Notes in Computer Science, vol 5352. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-89862-7_11
Download citation
DOI: https://doi.org/10.1007/978-3-540-89862-7_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-89861-0
Online ISBN: 978-3-540-89862-7
eBook Packages: Computer ScienceComputer Science (R0)