Paper Info
Title
Security Analysis of Temporal-RBAC Using Timed Automata
Abstract
Role Based Access Control (RBAC) is arguably the most common access control mechanism today due to its applicability at various levels of authorization in a system. Time varying nature of access control in RBAC administered systems is often implemented through Temporal-RBAC - an extension of RBAC in the temporal domain. In this paper, we propose an initial approach towards verification of security properties of a Temporal-RBAC system. Each role is mapped to a timed automaton. A controller automaton is used to activate and deactivate various roles. Security properties are specified using Computation Tree Logic (CTL) and are verified with the help of a model checking tool named Uppaal. We have specifically considered reachability, safety and liveness properties to show the usefulness of our approach.
Year
DOI
Venue
2008
10.1109/IAS.2008.10
Naples
Keywords
Field
DocType
controller automaton,security analysis,deactivate various role,computation tree logic,initial approach,various level,security property,temporal-rbac system,liveness property,access control,timed automata,common access control mechanism,temporal logic,computational modeling,security,ctl,timed automaton,model checking,authorisation,formal verification,role based access control,automata theory,automata
Computation tree logic,Model checking,Computer security,Computer science,Role-based access control,Theoretical computer science,Timed automaton,Access control,Temporal logic,Liveness,Formal verification
Conference
ISBN
Citations 
PageRank 
978-0-7695-3324-7
13
0.64
References 
Authors
9
2
Name
Order
Citations
PageRank
Samrat Mondal110018.02
Shamik Sural2100896.36