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 AccessNets, 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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2) (1994)
Barrett, C., Deters, M., Oliveras, A., Stump, A.: Design and results of the third annual satisfiability modulo theories competition (SMT-Comp 2007). International Journal on Artificial Intelligence Tools 17(4) (2008)
Bauer, L., Garriss, S., Reiter, M.K.: Efficient proving for practical distributed access-control systems. In: Biskup, J., López, J. (eds.) ESORICS 2007. LNCS, vol. 4734, pp. 19–37. Springer, Heidelberg (2007)
Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, p. 193. Springer, Heidelberg (1999)
Clarke, E., Grumberg, O., Peled, D.: Model Checking (1999)
Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. 16(5) (1994)
de Moura, L., Bjørner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)
Dutertre, B., de Moura, L.: The YICES SMT solver, http://yices.csl.sri.com/tool-paper.pdf
Ferraiolo, D.F., Kuhn, D.R., Chandramouli, R.: Role-based Access Control (2003)
Frohardt, R., Chang, B.-Y.E., Sankaranarayanan, S.: Access Nets: Modeling access to physical spaces (extended version). Technical Report CU-CS-1076-10, Department of Computer Science, University of Colorado, Boulder (2010)
Genrich, H.J., Lautenbach, K.: System modelling with high-level Petri nets. Theor. Comput. Sci. 13(1) (1981)
Guelev, D.P., Ryan, M.D., Schobbens, P.-Y.: Model-checking access control policies. In: Zhang, K., Zheng, Y. (eds.) ISC 2004. LNCS, vol. 3225, pp. 219–230. Springer, Heidelberg (2004)
Helbing, D., Farkas, I., Vicsek, T.: Simulating dynamical features of escape panic. Nature 407(6803) (2000)
Henderson, L.: The statistics of crowd fluids. Nature 229 (1971)
Holzmann, G.: The SPIN Model Checker (2003)
Jensen, K.: Coloured Petri nets and the invariant-method. Theor. Comput. Sci. 14(3) (1981)
Jha, S., Li, N., Tripunitara, M.V., Wang, Q., Winsborough, W.H.: Towards formal verification of role-based access control policies. IEEE Transactions on Dependable and Secure Computing (TDSC)Â 5(4) (2008)
Lovas, G.: Modeling and simulation of pedestrian traffic flow. Transportation Research BÂ 28(6) (1994)
Murata, T.: Petri nets: Properties, analysis and applications. Proc. IEEEÂ 77(4) (1989)
Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: From an abstract DPLL procedure to DPLL(T). J. ACM 53(6) (2006)
Pelechano, N., Malkawi, A.: Evacuation simulation models: Challenges in modeling high rise building evacuation with cellular automata approaches. Automation in Construction 17(4) (2008)
Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst. 24(3) (2002)
Sampemane, G., Naldurg, P., Campbell, R.H.: Access control for active spaces. In: Computer Security Applications, ACSAC (2002)
Shen, T.: ESM: A building evacuation simulation model. Building and Environment 40(5) (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Frohardt, R., Chang, BY.E., Sankaranarayanan, S. (2011). Access Nets: Modeling Access to Physical Spaces. In: Jhala, R., Schmidt, D. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2011. Lecture Notes in Computer Science, vol 6538. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-18275-4_14
Download citation
DOI: https://doi.org/10.1007/978-3-642-18275-4_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-18274-7
Online ISBN: 978-3-642-18275-4
eBook Packages: Computer ScienceComputer Science (R0)