Abstract
Formal method provides a way to achieve an exact and consistent definition of security for a given scenario. This paper presents a formal state-based verifiable RBAC model described with Z language, in which the state-transition functions are specified formally. Based on the separation of duty policy, the constraint rules and security theorems are constructed. Using a case study, we show how to specify and verify the consistency of formal RBAC system with theorem proving. By specifying RBAC model formally, it provides a precise description for the system security requirements. The internal consistency of this model can be validated by verification of the model.
Supported by National High-Tech Research and Development Program of China (863) under Grant No. 2002AA141080; National Natural Science Foundation of China under Grant No.60073022 and 60373054;Graduate Student Innovation Grant of Chinese Academy of Sciences.
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
Barroca, L.M., McDrmid, J.A.: Formal Methods: Use and Relevance for the Development of Safety Critical Systems. The Computer Journal 35(6), 579–599 (1992)
Clarke, E., Wing, J.: Formal Methods: State of the Art and Future Directions. ACM Computing Surveys 28(4), 626–643 (1996)
Sandhu, R., Coyne, E.J., Feinstein, H.L.: Role-based Access Control Model. IEEE Computer 29(2), 38–47 (1996)
ANSI INCITS 359-2004. Role Based Access Control. American National Standard for Information Technology (2004)
Shafiq, B., Masood, A., Ghafoor, A., et al.: A Role-Based Access Control Policy Verification Framework for Real-Time Systems. In: IEEE Workshop on Object-oriented Real-time Databases, Sedona, Arizona, pp. 13–20 (2005)
Zao, J., Hochtech, W., Chu J., et al.: RBAC Schema Verification Using Lightweight Formal Model and Constraint Analysis. MIT (December 2002) (accessed, June 2006), http://alloy.mit.edu/contributions/RBAC.pdf
Khayat, E.J., Abdallah, A.E.: A Formal Model for Flat Role-based Access Control. In: ACS/IEEE International Conference on Computer Systems and Applications (AICCSA 2003), July 2003, Tunis, Tunisia (2003)
Drouineaud, M., Bortin, M., Torrini, P., et al.: A First Step Towards Formal Verification of Security Policy Properties for RBAC. In: Proceedings of the Quality Software, Fourth International Conference on (QSIC 2004), pp. 60–67 (September 2004)
Koch, M., Mancini, L.V., Presicce, F.P.: A Graph-Based Formalism for RBAC. ACM Transactions on Information and System Security 5(3), 332–365 (2002)
Zhao, C., Heilili, N., Liu, S.P., et al.: Representation and Reasoning on RBAC: A Description Logic Approach. In: Van Hung, D., Wirsing, M. (eds.) ICTAC 2005. LNCS, vol. 3722, pp. 394–406. Springer, Heidelberg (2005)
Zhou, Z.Y., Liang, B., Jiang, L.: A Formal Description of SECIMOS Operating System. In: Gorodetsky, V., Kotenko, I., Skormin, V.A. (eds.) MMM-ACNS 2005. LNCS, vol. 3685, pp. 286–297. Springer, Heidelberg (2005)
Sprivey, J.M.: The Z Notation: A Reference Manual, 2nd edn. Prentice-Hall, Englewood Cliffs (1992)
ORA Canada Z/EVES (accessed, June 2006), http://www.ora.on.ca/z-eves/
Saaltink, M.: Z/EVES 2.0 User’s Guide. TR-99-5493-06a, ORA Canada (October 1999)
Kuhn, D.R.: Mutual Exclusion of Roles as a Means of Implementing Separation of Duty in Role-Based Access Control Systems. In: Proc. of the 2nd ACM Workshop on Role-Based Access Control, Fairfax, VA, pp. 23–30 (1997)
Good, D.I., Akers, R.L., Smith, L.M.: Report on Gypsy 2.05. Tech. Rept. ICSCA-CMP-48, the University of Texas at Austin (1986)
Young, W.D.: Comparing Specification Paradigms: Gypsy and Z. In: Proceedings of the 12th National Computer Security Conference, Baltimore, MA, pp. 83–97 (1989)
Brucker, A.D., Rittinger, F., Wolff, B.: HOL-Z 2.0: A Proof Environment for Z-Specifications. J. UCS 9(2), 152–172 (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Yuan, C., He, Y., He, J., Zhou, Z. (2006). A Verifiable Formal Specification for RBAC Model with Constraints of Separation of Duty. In: Lipmaa, H., Yung, M., Lin, D. (eds) Information Security and Cryptology. Inscrypt 2006. Lecture Notes in Computer Science, vol 4318. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11937807_16
Download citation
DOI: https://doi.org/10.1007/11937807_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-49608-3
Online ISBN: 978-3-540-49610-6
eBook Packages: Computer ScienceComputer Science (R0)