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.