Towards formal security analysis of GTRBAC using timed automata

Samrat Mondal, Shamik Sural, Vijayalakshmi Atluri

Research output: Chapter in Book/Report/Conference proceedingConference contribution

18 Scopus citations

Abstract

An access control system is often viewed as a state transition system. Given a set of access control policies, a general safety requirement in such a system is to determine whether a desirable property is satisfied in all the reachable states. Such an analysis calls for formal verification. While formal analysis on traditional RBAC has been done to some extent, the extensions of RBAC lack such an analysis. In this paper, we propose a formal technique to perform security analysis on the Generalized Temporal RBAC (GTRBAC) model which can be used to express a wide range of temporal constraints on different RBAC components like role, user and permission. In the proposed approach, at first the GTRBAC system is mapped to a state transition system built using timed automata. Characteristics of each role, user and permission are captured with the help of timed automata. A single global clock is used to express the various temporal constraints supported in a GTRBAC model. Next, a set of safety and liveness properties is specified using computation tree logic (CTL). Model checking based formal verification is then done to verify the properties against the model to determine if the system is secure with respect to a given set of access control policies. Both time and space analysis has been done for studying the performance of the approach under different configurations.

Original languageEnglish (US)
Title of host publicationSACMAT'09 - Proceedings of the 14th ACM Symposium on Access Control Models and Technologies
Pages33-42
Number of pages10
DOIs
StatePublished - Nov 30 2009
Event14th ACM Symposium on Access Control Models and Technologies, SACMAT 2009 - Stresa, Italy
Duration: Jun 3 2009Jun 5 2009

Publication series

NameProceedings of ACM Symposium on Access Control Models and Technologies, SACMAT

Other

Other14th ACM Symposium on Access Control Models and Technologies, SACMAT 2009
CountryItaly
CityStresa
Period6/3/096/5/09

All Science Journal Classification (ASJC) codes

  • Software
  • Computer Networks and Communications
  • Safety, Risk, Reliability and Quality
  • Information Systems

Keywords

  • CTL
  • GTRBAC
  • Model checking
  • Security analysis
  • Timed automata

Fingerprint Dive into the research topics of 'Towards formal security analysis of GTRBAC using timed automata'. Together they form a unique fingerprint.

  • Cite this

    Mondal, S., Sural, S., & Atluri, V. (2009). Towards formal security analysis of GTRBAC using timed automata. In SACMAT'09 - Proceedings of the 14th ACM Symposium on Access Control Models and Technologies (pp. 33-42). (Proceedings of ACM Symposium on Access Control Models and Technologies, SACMAT). https://doi.org/10.1145/1542207.1542214