Hybrid Access Control Model for IoT Environments: Formalization and Verification Using Timed Automata

The Internet of Things (IoT) represents a technological revolution by enabling the interconnection of multiple devices and systems. With this expansion of connected objects, security issues, particularly in access control, become paramount. Due to their complexity and diversity, IoT environments require sophisticated, dynamic, and flexible access control models capable of addressing their specific constraints. This article formalizes and extends the E-UACML model (Emergency Unified Access Control Modelling Language) for IoT environments. Using formal verification techniques, we translate E-UACML into timed automata to validate its properties with the UPPAAL tool. Timed automata enable the integration of timing and synchronization, which are essential for verifying spatio-temporal constraints in IoT systems. Verification, carried out through Computation Tree Logic (CTL), ensures that access control policies meet rigorous security requirements, including spatio-temporal constraints. The results demonstrate the effectiveness of this approach in ensuring flexible and secure access control in IoT environments.