loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
2008 The Fourth International Conference on Information Assurance and Security
Security Analysis of Temporal-RBAC Using Timed Automata
September 08-September 10
ISBN: 978-0-7695-3324-7
ASCII Text
x 
 
Samrat Mondal, Shamik Sural, "Security Analysis of Temporal-RBAC Using Timed Automata," Information Assurance and Security, International Symposium on, pp. 37-40, 2008 The Fourth International Conference on Information Assurance and Security, 2008.
 
 
BibTex
x
 
@article{ 10.1109/IAS.2008.10,
author = {Samrat Mondal and Shamik Sural},
title = {Security Analysis of Temporal-RBAC Using Timed Automata},
journal ={Information Assurance and Security, International Symposium on},
volume = {0},
year = {2008},
isbn = {978-0-7695-3324-7},
pages = {37-40},
doi = {http://doi.ieeecomputersociety.org/10.1109/IAS.2008.10},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Information Assurance and Security, International Symposium on
TI - Security Analysis of Temporal-RBAC Using Timed Automata
SN - 978-0-7695-3324-7
SP37
EP40
A1 - Samrat Mondal,
A1 - Shamik Sural,
PY - 2008
KW - Temporal-RBAC
KW - Timed Automata
KW - Security Analysis
KW - Model Checking
KW - CTL
VL - 0
JA - Information Assurance and Security, International Symposium on
ER -
 
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.
Index Terms:
Temporal-RBAC, Timed Automata, Security Analysis, Model Checking, CTL
Citation:
Samrat Mondal, Shamik Sural, "Security Analysis of Temporal-RBAC Using Timed Automata," ias, pp.37-40, 2008 The Fourth International Conference on Information Assurance and Security, 2008
Usage of this product signifies your acceptance of the Terms of Use.