Using Timed Colored Petri Nets and CPN-tool to Model and Verify TRBAC Security Policies

Role Based Access Control (RBAC) is one of the most used models in designing and implementation of security policies in large networking systems. The classical model doesn’t consider temporal aspects which are so important in such policies. Temporal RBAC (TRBAC) is proposed to deal with these aspects. Although the elegance of these models, design a security policy remains a challenge. One is obliged to prove the consistency and the correctness of the policy. Using formal verification allows proving that the designed policy is consistent. In this paper1, we present a formal modelling/analysis approach for TRBAC policies. We use Timed Colored Petri Nets to model the TRBAC policy, and then CPN-tool is used to analyze the generated models. The analysis allows proving many important properties about the TRBAC security policy.