Spatiotemporal model checking of location and mobility related security policy specifications

For the formal verification of security in mobile networks, a requirement is that security policies associated with mobility and location constraints are formally specified and verified. For the formal specification and verification of security policies, formal methods ensure that a given network configuration that includes certain network elements satisfies a given security policy. A process calculus based approach is presented, where ambient calculus is used for formal specification of security policies and ambient logic is used for formal representation of mobility and location constraints. A spatiotemporal model checking algorithm is presented for the model checking of formal specifications in ambient calculus with respect to formulas in ambient logic. The presented algorithm allows spatiotemporal model checking of security policy rules and consists of spatial and temporal model checking algorithms. The spatial model checking algorithm is implemented in the Java language and the temporal model checking algorithm is implemented using the NuSMV model checker.

Anahtar Kelimeler:

Key words: Security policy, model checking, ambient calculus, spatiotemporal

Spatiotemporal model checking of location and mobility related security policy specifications

Keywords:

Key words: Security policy, model checking, ambient calculus, spatiotemporal,

PDF

___

D. ¨ Unal, O. Akar, M. Ufuk C ¸ a˘ glayan, “Model checking of location and mobility related security policy specifications in ambient calculus”, Lecture Notes in Computer Science, Vol. 6258, pp. 155–168, 2010.
M. Becker, C. Fournet, A. Gordon, “Design and semantics of a decentralized authorization language”, Proceedings of the 20th IEEE Computer Security Foundations Symposium, pp. 3–15, 2007.
S. Jajodia, P. Samarati, M.L. Sapino, V.S. Subrahmanian, “Flexible support for multiple access control policies”, ACM Transactions on Database Systems, Vol. 26, pp. 214–260, 2001.
S. Jajodia, P. Samarati, V.S. Subrahmanian, “A logical language for expressing authorizations”, Proceedings of the IEEE Symposium on Security and Privacy, pp. 31–42, 1997.
E. Bertino, F. Buccafurri, E. Ferrari, P. Rullo, “A logical framework for reasoning on data access control policies”, Proceedings of the 12th IEEE Computer Security Foundations Workshop, pp. 175–189, 1999.
N. Damianou, N. Dulay, E. Lupu, M. Sloman, “The Ponder policy specification language”, Proceedings of the International Workshop on Policies for Distributed Systems and Networks, pp. 18–38, 2001.
T.Y.C. Woo, S.S. Lam, “Authorizations in distributed systems: A new approach”, Journal of Computer Security, Vol. 2, pp. 107–136, 1993.
F. Cuppens, C. Saurel, “Specifying a security policy: a case study”, Proceedings of the 9th IEEE Computer Security Foundations Workshop, pp. 123–134, 1996.
T. Ryutov, C. Neuman, “Representation and evaluation of security policies for distributed system services”, Proceedings of DARPA Information Survivability Conference and Exposition, pp. 172–183, 2000.
A.A. Yavuz, F. Alagoz, E. Anarim, “A new multi-tier adaptive military MANET security protocol using hybrid cryptography and signcryption”, Turkish Journal of Electrical Engineering & Computer Sciences, Vol. 18, pp. 1–22, 20 N. Zhang, M. Ryan, D.P. Guelev, “Synthesising verified access control systems through model checking”, Journal of Computer Security, Vol. 16, pp. 1–61, 2008.
D. ¨ Unal, M.U. C ¸ a˘ glayan, “Theorem proving for modeling and conflict checking of authorization policies”, Proceedings of the International Symposium on Computer Networks, 2006.
M. Drouineaud, M. Bortin, P. Torrini, K. Sohr, “A first step towards formal verification of security policy properties for RBAC”, Proceedings of the Fourth International Conference on Quality Software, pp. 60–69, 2004.
K. Sohr, M. Drouineaud, G. Ahn, M. Gogolla, “Analyzing and managing role based access control policies”, IEEE Transactions on Knowledge and Data Engineering, Vol. 20, pp. 924–939, 2008.
L. Cardelli, A.D. Gordon, “Mobile ambients”, Theoretical Computer Science, Vol. 240, pp. 177–213, 2000.
D. Scott, Abstracting application-level security policy for ubiquitous computing, PhD thesis, University of Cambridge, 2005.
A. Compagnoni, P. Bidinger, “Role based access control for boxed ambients”, Theoretical Computer Science, Vol. 398, pp. 203–216, 2008.
L. Cardelli, A.D. Gordon, “Anytime, anywhere: modal logics for mobile ambients”, Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 365–377, 2000.
L. Cardelli, A.D. Gordon, “Ambient logic”, Mathematical Structures in Computer Science, 2006.
W. Charatonik, A. Gordon, J. Talbot, “Finite-control mobile ambients”, Proceedings of the 11th European Symposium on Programming Languages and Systems, pp. 295–313, 2002.
W. Charatonik, S.D. Zilio, A.D. Gordon, S. Mukhopadhyay, J. Talbot, “Model checking mobile ambients”, Theoretical Computer Science, Vol. 308, pp. 277–331, 2003.
R. Mardare, C. Priami, P. Quaglia, A. Vagin, “Model checking biological systems described using ambient calculus”, Proceedings of the 2004 International Conference on Computational Methods in Systems Biology, pp. 85–103, 2005. D. Hirschkoff, E. Lozes, D. Sangiorgi, “Separability, expressiveness, and decidability in the ambient logic”, Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, pp. 423–432, 2002.
D. Hirschkoff, E. Lozes, D. Sangiorgi, “On the expressiveness of the ambient logic”, Logical Methods in Computer Science, Vol. 2, pp. 1–35, 2006.
D.F. Ferraiolo, R. Sandhu, S. Gavrila, D.R. Kuhn, R. Chandramouli, “Proposed NIST standard for role based access control”, ACM Transactions on Information and System Security, Vol. 4, pp. 224–274, 2001.
D. ¨ Unal, M.U. C ¸ a˘ glayan, “XFPM-RBAC: XML based specification language for security policies in multi-domain mobile networks”, Security and Communication Networks, 2012. In press.
C.C. Giunchiglia, A. Cimatti, E. Clarke, F. Giunchiglia, M. Roveri, “NUSMV: a new symbolic model checker”, International Journal on Software Tools for Technology Transfer, Vol. 2, pp. 410–425, 2000.