Automatically verifying STRAC policy

In the IoT (Internet of Things), inconsistent ACP (Access Control Policies) would cause disastrous consequences, for example, fire disasters and failures of cardiac pacemakers, as a result, ACP should be verified before they are applied. Tediousness and error-proneness of manual verifications make automatic and formal verification necessary. In this paper, timed automata is presented to formally model the STRAC (Spatio-Temporal Access Control based on Reputation, one policy for the IoT) policies and CTL (Computation Tree Logic) is adopted to describe the properties that should be satisfied by these policies. Then model checker UPPAAL is proposed to automatically verify whether STRAC policies conform to security properties. Experiment results show that our approach is effective.