Security analysis of GTRBAC and its variants using model checking

Samrat Mondal, Shamik Sural, Vijayalakshmi Atluri

Research output: Contribution to journalArticlepeer-review

9 Scopus citations


Security analysis is a formal verification technique to ascertain certain desirable guarantees on the access control policy specification. 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 the use of formal verification techniques. While formal analysis on traditional Role Based Access Control (RBAC) has been done to some extent, recent extensions to RBAC lack such an analysis. In this paper, we consider the temporal RBAC extensions and propose a formal technique using timed automata to perform security analysis by analyzing both safety and liveness properties. Using safety properties one ensures that something bad never happens while liveness properties show that some good state is also achieved. GTRBAC is a well accepted generalized temporal RBAC model which can handle a wide range of temporal constraints while specifying different access control policies. Analysis of such a model involves a process of mapping a GTRBAC based system into a state transition system. Different reduction rules are proposed to simplify the modeling process depending upon the constraints supported by the system. The effect of different constraints on the modeling process is also studied.

Original languageEnglish (US)
Pages (from-to)128-147
Number of pages20
JournalComputers and Security
Issue number2-3
StatePublished - Mar 2011

All Science Journal Classification (ASJC) codes

  • Computer Science(all)
  • Law


  • Computation tree logic
  • Liveness property
  • Safety property
  • Timed automata
  • Verification

Fingerprint Dive into the research topics of 'Security analysis of GTRBAC and its variants using model checking'. Together they form a unique fingerprint.

Cite this