A Verifiable Formal Specification for RBAC Model with Constraints of Separation of Duty

  • Chunyang Yuan
  • Yeping He
  • Jianbo He
  • Zhouyi Zhou
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4318)


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.


Formal Specification Verification RBAC Separation of Duty 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    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)CrossRefGoogle Scholar
  2. 2.
    Clarke, E., Wing, J.: Formal Methods: State of the Art and Future Directions. ACM Computing Surveys 28(4), 626–643 (1996)CrossRefGoogle Scholar
  3. 3.
    Sandhu, R., Coyne, E.J., Feinstein, H.L.: Role-based Access Control Model. IEEE Computer 29(2), 38–47 (1996)Google Scholar
  4. 4.
    ANSI INCITS 359-2004. Role Based Access Control. American National Standard for Information Technology (2004)Google Scholar
  5. 5.
    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)Google Scholar
  6. 6.
    Zao, J., Hochtech, W., Chu J., et al.: RBAC Schema Verification Using Lightweight Formal Model and Constraint Analysis. MIT (December 2002) (accessed, June 2006),
  7. 7.
    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)Google Scholar
  8. 8.
    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)Google Scholar
  9. 9.
    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)CrossRefGoogle Scholar
  10. 10.
    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)CrossRefGoogle Scholar
  11. 11.
    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)CrossRefGoogle Scholar
  12. 12.
    Sprivey, J.M.: The Z Notation: A Reference Manual, 2nd edn. Prentice-Hall, Englewood Cliffs (1992)Google Scholar
  13. 13.
    ORA Canada Z/EVES (accessed, June 2006),
  14. 14.
    Saaltink, M.: Z/EVES 2.0 User’s Guide. TR-99-5493-06a, ORA Canada (October 1999)Google Scholar
  15. 15.
    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)Google Scholar
  16. 16.
    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)Google Scholar
  17. 17.
    Young, W.D.: Comparing Specification Paradigms: Gypsy and Z. In: Proceedings of the 12th National Computer Security Conference, Baltimore, MA, pp. 83–97 (1989)Google Scholar
  18. 18.
    Brucker, A.D., Rittinger, F., Wolff, B.: HOL-Z 2.0: A Proof Environment for Z-Specifications. J. UCS 9(2), 152–172 (2003)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2006

Authors and Affiliations

  • Chunyang Yuan
    • 1
    • 2
  • Yeping He
    • 1
  • Jianbo He
    • 1
    • 2
  • Zhouyi Zhou
    • 1
    • 2
  1. 1.Institute of SoftwareChinese Academy of SciencesBeijingPRC
  2. 2.Graduate School of the Chinese Academy of SciencesBeijingPRC

Personalised recommendations