Text size
  • Small
  • Medium
  • Large
  • Standard
  • Blue text on blue
  • High contrast (Yellow text on black)
  • Blue text on beige

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

    Fourth International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS 2010)

    Paris, France, 1 - 2 July 2010


    Laïd Kadloul, Karim Djouani and Walid Tfaili


    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.


    PDF filePDF Version of this Paper (381kb)