Reference
Abstract
Electronic, software-managed mechanisms using, for example, radio-frequency identification (RFID) cards, enable great flexibility in specifying access control policies to physical spaces. For example, access rights may vary based on time of day or could differ in normal versus emergency situations. With such fine-grained control, understanding and reasoning about what a policy permits becomes surprisingly difficult requiring knowledge of permission levels, spatial layout, and time. In this paper, we present a formal modeling framework, called Access Nets, suitable for describing a combination of access permissions, physical spaces, and temporal constraints. Furthermore, we provide evidence that model checking techniques are effective in reasoning about physical access control policies. We describe our results from a tool that uses reachability analysis to validate security policies.
BibTeX
@string{VMCAI = "International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)"}
@inproceedings{accessnets-vmcai11,
author = {Robert Frohardt and Bor-Yuh Evan Chang and Sriram Sankaranarayanan},
title = {Access Nets: Modeling Access to Physical Spaces},
booktitle = VMCAI,
year = {2011},
pages = {184-198},
}