A SAT Based Verification Framework for Wireless LAN Security Policy Management Supported by STRBAC Model

The widespread proliferation of wireless networks (WLAN) demands formal evaluation and analysis of security policy management in enterprise networks. The enforcement of organizational security policies in wireless local area networks (WLA.Ns) requires protection over the network resources from unauthorized access. Hence it is required to ensure correct distribution of access control rules to the network access points conforming to the security policy. In WLAN security policy management, the role-based access control (RBAC) mechanisms can be deployed to strengthen the security perimeter over the network resources. Further, there is a need to model the time and location dependent access constraints. In this paper, we propose WLAN security management system supported by a spatio-temporal RBAC (STRBAC) model and a SAT based verification framework. The system stems from logical partitioning of the WLAN topology into various security policy zones. It includes a Global Policy Server (CPS) that formalizes the organizational access policies and determines the high level policy configurations; a Central Authentication & Role Server (CARS) which authenticates the users and the access points (AP) in various zones and also assigns appropriate roles to the users. Each policy zone consists of an Wireless Policy Zone Controller (WPZCon) that co-ordinates with a dedicated Local Role Server (LRS) to extract the low level access configurations corresponding to the zone access router. We also propose a formal spatio-temporal RBAC (STRBAC) model to represent the global security policies formally and a SAT based verification framework to verify the access configurations.