Abstract
Cyber Physical Systems (CPS) are complex systems that operate in a dynamic environment where security characteristics of contexts are unique, and uniform access to secure resources anywhere anytime to mobile entities poses daunting challenges. To capture context parameters such as location and time in an access control policy for CPS, we propose a Generalized Spatio- Temporal RBAC (GST-RBAC) model. In this model spatial and temporal constraints are defined for role enabling, user-role assignment, role-permission assignment, role activation, separation of duty and role hierarchy. The inclusion of multiple types of constraints exposes the need of composing a policy which is verifiable for consistency. The second contribution in this paper is GST-RBAC policy specification and verification framework using light weight formal modeling language, Alloy. The analysis assists in consistency verification leading to conflict free composition of the actual policy for implementation for CPS.
