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. © Springer-Verlag Berlin Heidelberg 2006.
CITATION STYLE
Yuan, C., He, Y., He, J., & Zhou, Y. (2006). A verifiable formal specification for RBAC model with constraints of separation of duty. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4318 LNCS, pp. 196–210). Springer Verlag. https://doi.org/10.1007/11937807_16
Mendeley helps you to discover research relevant for your work.