274
views
0
recommends
+1 Recommend
1 collections
    0
    shares
       
      • Record: found
      • Abstract: found
      • Conference Proceedings: found
      Is Open Access

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

      proceedings-article

      , ,

      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

      Security Policies, RBAC model, TRBAC, Timed Colored Petri Nets, Formal Modelling, Formal Verification

      Bookmark

            Abstract

            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.

            Content

            Author and article information

            Contributors
            Conference
            July 2010
            July 2010
            : 1-12
            Affiliations
            [0001]LISSI Laboratory,

            Paris Est University,

            Paris, France.

            Computer Science Departement,

            Biskra University, Algeria,
            [0002]LISSI Laboratory,

            Paris Est University

            Paris, France.

            F’SATI at TUT,

            Pretoria South Africa.
            [0003]LISSI Laboratory,

            Paris Est University

            Paris, France.
            Article
            10.14236/ewic/VECOS2010.8
            43b980fa-4340-49c2-a4ad-6ee4fc95d1f2
            © Laïd Kahloul et al. Published by BCS Learning and Development Ltd. Fourth International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS 2010), Paris, France

            This work is licensed under a Creative Commons Attribution 4.0 Unported License. To view a copy of this license, visit http://creativecommons.org/licenses/by/4.0/

            Fourth International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS 2010)
            VECOS
            4
            Paris, France
            1-2 July 2010
            Electronic Workshops in Computing (eWiC)
            Verification and Evaluation of Computer and Communication Systems (VECoS 2010)
            Product
            Product Information: 1477-9358BCS Learning & Development
            Self URI (journal page): https://ewic.bcs.org/
            Categories
            Electronic Workshops in Computing

            Comments

            Comment on this article