TY - JOUR TI - Formal security analysis of access control models and their spatiotemporal extensions DO - https://doi.org/doi:10.7282/T3T43W35 PY - 2015 AB - Providing restrictive and secure access to resources is a challenging and socially important problem. Today, there exists a variety of formal security models to meet the wide needs of requirements in specifying access control policies. These include Discretionary Access Control (DAC) and Role Based Access Control (RBAC). For every model, it is necessary to analyze and prove that the system is secure, or in other words, access rights of sensitive data are not leaked to potentially untrusted users (rights leakage), as well as the data itself (data leakage). Analysis is essential to understand the implications of security policies and helps organizations gain confidence on the control they have on resources while providing access, and devise and maintain policies. There is a dire need for such analysis tools that help security administrators as they make administrative changes to reflect changes in policy. In this dissertation we tackle two major problems: Rights leakage problem and data leakage problem. For the rights leakage problem, we focus on RBAC and its temporal and spatiotemporal extensions, since RBAC has been successfully incorporated in a variety of commercial systems, and has become the norm in many of today’s organizations for enforcing security. Towards this end, we first propose suitable administrative models that govern changes to policies. Then we develop efficient security analysis techniques and tools, in which we explore a decomposition strategy, that splits the temporal or spatio temporal security analysis problems into smaller and more manageable sub-problems which in fact, are RBAC security analysis problems on which the existing RBAC security analysis tools can be employed. We then evaluate them from a theoretical perspective by analyzing their complexity, as well as from a practical perspective by evaluating their performance using real world and simulated data sets. For the data leakage problem, we consider two types of data leakages: confidentiality violating and integrity violating. In confidentiality violating data leakage, sensitive data in an object can be leaked to potentially untrusted users via another object that is readable by those users. In integrity violating data leakage, on the other hand, data can be leaked to an object where the user is not allowed to write to explicitly. We propose techniques to eliminate these possible leakages by using three different strategies: Conservative, Proactive and Retrospective. We then computationally evaluate them to show the running times and restrictiveness of our proposed methodologies in terms of identifying the possible data leakages and eliminating them. KW - Management KW - Access control KW - Computer security LA - eng ER -