Specification of SA-RBAC Policy Based on Colored Petri Net

Specification and verification of access control (AC) policies is a significant and challenging problem. Colored Petri net (CPN) is a powerful modeling and analyzing tool having the advantages of intuitive visual framework with the rigor and precision of a semantics founded on category theory. In this paper, a concrete specification of SA-RBAC policy on CPN is described in detail for our improved RBAC model SA-RBAC (self-authentication RBAC). And all the states in the CPN model describing SA-RBAC policy can be proved to be consistent.