FPFM : a formal specification and verification framework for security policies in multi-domain mobile networks

Abstract

We present a framework called Formal Policy Framework for Mobility (FPFM) for the specification and verification of domain and inter-domain security policies in a multi-domain mobile network environment. FPFM supports the specification of security policies with mobility and location constraints, role hierarchy mapping, interdomain services, inter-domain access rights and separation of duty. The specification of security policies in FPFM is based on a formal security policy model, called FPMRBAC (Formal Policy Model for Mobility with Role Based Access Control) and a XML based security policy specification language called XFPM-RBAC (XML Based Formal Policy Language for Mobility with Role Based Access Control). Formal verification of security policies ensure that the security policy is satisfied by the network elements in a given network configuration. FPFM supports extraction of formal specifications from defined network configurations, domain and inter-domain security policies. Another novel aspect of FPFM is the support for formal information flow analysis related to mobility within multiple security domains. Automated verification of formal specifications are carried out through model checking and theorem proving. A spatio-temporal model checking algorithm has been proposed and a model checking tool has been developed for spatio-temporal model checking of location and mobility constraints in security policy rules. Conflicts within security policy rules are resolved through theorem proving with the help of the Coq interactive theorem prover.