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.

Content

Author and article information

Contributors

Laïd Kahloul

Karim Djouani

Walid Tfaili

Conference

Publication date: July 2010

Publication date (Print): July 2010

Pages: 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

DOI: 10.14236/ewic/VECOS2010.8

SO-VID: 43b980fa-4340-49c2-a4ad-6ee4fc95d1f2

Copyright statement: © 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

License:

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/

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

Conference acronym: VECOS

Conference number: 4

Conference location: Paris, France

Conference date: 1-2 July 2010

Conference sponsor: Electronic Workshops in Computing (eWiC)

Conference theme: Verification and Evaluation of Computer and Communication Systems (VECoS 2010)

Product

Product Information: 1477-9358BCS Learning & Development

Self URI (article page): https://www.scienceopen.com/hosted-document?doi=10.14236/ewic/VECOS2010.8

Self URI (journal page): https://ewic.bcs.org/

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

Abstract