The Research Of Formal RBAC Model

As a kind of method based on symbolic logic, Formal method has gained more and more attention because of its preciseness. It has been applied broadly in systems in which the security and reliability are the key issues. For example, protocol security analysis, operating system security model, software development. In the research of operating system security model, it is very essential to take the formal method to ensure the security of the model.RBAC model has much advantage compared with the tradition access and control model. However, there is a common defect that all of RBAC models now are not described by formal language, and don't study the mechanism how the roles of RBAC run in the operating system. And therefore, they haven't proved the security strictly.In the paper, we study these problems memtioned above by symbolic logic, and propose a formal model of RBAC. In the model, we describe the mechanism how roles run in the operating system in details, and prove the security strictly.Firstly, we propose an axiom system by a language of two rank and some axioms. At the same time, we give an explanation (which is called a secure operation system based on RBAC), and all theorems of the axiom system are true by this explain. Then we actually establish a model in the symbolic logic.Secondly, we analyze the essence of the security in the access control. The security of access control is characterized by usability, domination and traceability. RBAC is one kind of access control. So our model needs to satisfy the three characteristics.Finally, we propose the Domain Theorem and Traceability Theorem which is proved by the axioms and rules. Then we can ensure domination and traceability. And usability is obvious in our model. After all, we ensure the security of our model.With our efforts, hypothesis and process of RBAC has become precise which could be atheoretic foundation in the research of RBAC.