Access control protect the resources of an organization by controlling who hasaccess to what objects.Role based access control has become the defacto authorizationmodels used by commercial applications widely because it can model various accesscontrol requirements and it simplifies access control management.Access control and its extensions have various constraints that may interact witheach other resulting in conflicts.Thus,it is important to ensure that access controlbreaches do not occur by verifying the access control model.Traditional access controlmodel validation methods focus on analyzing the access control model in isolationand are useful in describing potential conflicts that may occur between the differentfeatures of the model.Such analysis is independent of the application. However, thesecurity of the access control system is not only relerant with the access controlmodel,but also associated with the authorization rules.So it is important to analyze thesecurity of the authorization constraints of the access control system.Therefore,we propose a verification method of security authorization for RBACsystem.First,this approach specifies the RBAC system and their authorizationconstraints in a formal specification language.It specifies the entities that take part inthe access control model in the form of the class diagrams and used OCL statements tospecify the authorization constraints. Then it transforms these class diagrams andconstraint statements to a formal model. For the last step, it uses the formalverification to verify the security of the authorization constraints.Finally, we illustrate our approach using a real-world RBAC system.Experiments show that it can verify the security of the authorization constraints forRBAC system effectively. |