eTheses Repository

# Verification of temporal-epistemic properties of access control systems

Koleini, Masoud (2012)
Ph.D. thesis, University of Birmingham.

 PDF (1477Kb)

## Abstract

Verification of access control systems against vulnerabilities has always been a challenging problem in the world of computer security. The complication of security policies in large- scale multi-agent systems increases the possible existence of vulnerabilities as a result of mistakes in policy definition. This thesis explores automated methods in order to verify temporal and epistemic properties of access control systems. While temporal property verification can reveal a considerable number of security holes, verification of epistemic properties in multi-agent systems enable us to infer about agents' knowledge in the system and hence, to detect unauthorized information flow. This thesis first presents a framework for knowledge-based verification of dynamic access control policies. This framework models a coalition-based system, which evaluates if a property or a goal can be achieved by a coalition of agents restricted by a set of permissions defined in the policy. Knowledge is restricted to the information that agents can acquire by reading system information in order to increase time and memory efficiency. The framework has its own model-checking method and is implemented in Java and released as an open source tool named $$\char{cmmi10}{0x50}$$$$\char{cmmi10}{0x6f}$$$$\char{cmmi10}{0x6c}$$$$\char{cmmi10}{0x69}$$$$\char{cmmi10}{0x56}$$$$\char{cmmi10}{0x65}$$$$\char{cmmi10}{0x72}$$. In order to detect information leakage as a result of reasoning, the second part of this thesis presents a complimentary technique that evaluates access control policies over temporal-epistemic properties where the knowledge is gained by reasoning. We will demonstrate several case studies for a subset of properties that deal with reasoning about knowledge. To increase the efficiency, we develop an automated abstraction refinement technique for evaluating temporal-epistemic properties. For the last part of the thesis, we develop a sound and complete algorithm in order to identify information leakage in Datalog-based trust management systems.

Type of Work: Ph.D. thesis. Ryan, Mark and Becker, Moritz Colleges (2008 onwards) > College of Engineering & Physical Sciences School of Computer Science QA75 Electronic computers. Computer scienceQA76 Computer softwareT Technology (General) University of Birmingham 3706
This unpublished thesis/dissertation is copyright of the author and/or third parties. The intellectual property rights of the author or third parties in respect of this work are as defined by The Copyright Designs and Patents Act 1988 or as modified by any successor legislation. Any use made of information contained in this thesis/dissertation must be in accordance with that legislation and must be properly acknowledged. Further distribution or reproduction in any format is prohibited without the permission of the copyright holder.

Repository Staff Only: item control page