Abstract
Verification of security for mobile networks requires specification and verification of security policies in multiple-domain environments. Mobile users present challenges for specification and verification of security policies in such environments. Formal methods are expected to ensure that the construction of a system adheres to its specification. Formal methods for specification and verification of security policies ensure that the security policy is consistent and satisfied by the network elements in a given network configuration. We present a method and a model checking tool for formal specification and verification of location and mobility related security policies for mobile networks. The formal languages used for specification are Predicate Logic and Ambient Calculus. The presented tool is capable of spatial model checking of Ambient Calculus specifications for security policy rules and uses the NuSMV model checker for temporal model checking.
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
Becker, M., Fournet, C., Gordon, A.: Design and semantics of a decentralized authorization language. In: 20th IEEE Computer Security Foundations Symposium, pp. 3–15. IEEE Computer Society Press, Los Alamitos (2007)
Bertino, E., Ferrari, E., Buccafurri, F.: A logical framework for reasoning on data access control policies. In: 12th IEEE Computer Security Foundations Workshop, pp. 175–189. IEEE Computer Society Press, Los Alamitos (1999)
Cardelli, L., Gordon, A.D.: Anytime, anywhere: modal logics for mobile ambients. In: 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - POPL 2000, pp. 365–377 (2000)
Cardelli, L., Gordon, A.D.: Mobile ambients. Theoretical Computer Science 240(1), 177–213 (2000)
Charatonik, W., Gordon, A., Talbot, J.: Finite-control mobile ambients. In: Le Métayer, D. (ed.) ESOP 2002. LNCS, vol. 2305, pp. 295–313. Springer, Heidelberg (2002)
Charatonik, W., Zilio, S.D., Gordon, A.D., Mukhopadhyay, S., Talbot, J.: Model checking mobile ambients. Theoretical Computer Science 308(1-3), 277–331 (2003)
Compagnoni, A., Bidinger, P.: Role-based access control for boxed ambients. Theoretical Computer Science 398(1-3), 203–216 (2008)
Cuppens, F., Saurel, C.: Specifying a security policy: a case study. In: 9th IEEE Computer Security Foundations Workshop, pp. 123–134. IEEE Computer Society Press, Los Alamitos (1996)
Damianou, N., Dulay, N., Lupu, E., Sloman, M.: The Ponder policy specification language. In: Sloman, M., Lobo, J., Lupu, E.C. (eds.) POLICY 2001. LNCS, vol. 1995, pp. 18–38. Springer, Heidelberg (2001)
Drouineaud, M., Bortin, M., Torrini, P., Sohr, K.: A first step towards formal verification of security policy properties for RBAC. In: Proc. QSIC (2004)
Ferraiolo, D.F., Sandhu, R., Gavrila, S., Kuhn, D.R., Chandramouli, R.: Proposed NIST standard for role-based access control. ACM Trans. Inf. Syst. Secur. 4(3), 224–274 (2001)
Giunchiglia, C.C., Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: Nusmv: a new symbolic model checker. International Journal on Software Tools for Technology Transfer 4, 410–425 (2000)
Jajodia, S., Samarati, P., Subrahmanian, V.S.: A logical language for expressing authorizations. In: IEEE Symposium on Security and Privacy, pp. 31–42 (1997)
Jajodia, S., Samarati, P., Sapino, M.L., Subrahmanian, V.S.: Flexible support for multiple access control policies. ACM Trans. Database Syst. 26(2), 214–260 (2001)
Mardare, R., Priami, C., Quaglia, P., Vagin, O.: Model checking biological systems described using ambient calculus. Computational Methods in Systems Biology, 85–103 (2005)
Ryutov, T., Neuman, C.: Representation and evaluation of security policies for distributed system services. In: DARPA Information Survivability Conference and Exposition, pp. 172–183 (2000)
Scott, D.: Abstracting application-level security policy for ubiquitous computing. Ph.D. thesis, University of Cambridge (2005)
Sohr, K., Drouineaud, M., Ahn, G., Gogolla, M.: Analyzing and managing Role-Based access control policies. IEEE Transactions on Knowledge and Data Engineering 20(7), 924–939 (2008)
Unal, D., Caglayan, M.U.: Theorem proving for modeling and conflict checking of authorization policies. In: Proc. ISCN (2006)
Woo, T.Y.C., Lam, S.S.: Authorizations in distributed systems: A new approach. Journal of Computer Security 2, 107–136 (1993)
Zhang, N., Guelev, D., Ryan, M.: Synthesising verified access control systems through model checking. Journal of Computer Security 16(1), 1–61 (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Unal, D., Akar, O., Ufuk Caglayan, M. (2010). Model Checking of Location and Mobility Related Security Policy Specifications in Ambient Calculus. In: Kotenko, I., Skormin, V. (eds) Computer Network Security. MMM-ACNS 2010. Lecture Notes in Computer Science, vol 6258. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14706-7_12
Download citation
DOI: https://doi.org/10.1007/978-3-642-14706-7_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-14705-0
Online ISBN: 978-3-642-14706-7
eBook Packages: Computer ScienceComputer Science (R0)