Fourth International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS 2010) (VECOS)
Verification and Evaluation of Computer and Communication Systems (VECoS 2010)
1-2 July 2010
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.