Formal modeling and verification of ICN-IoT middleware architecture

As a key technology of the Internet of Things (IoT), middleware plays an important role in managing virtualized resources and services. However, traditional Internet architectures cannot ensure adequate data security and efficient data delivery for IoT middlewares. Therefore, Information-Centric Networking (ICN), a paradigm of the future network, is introduced into IoT middlewares. Since ICN-IoT middleware is attracting more and more attentions, its security is worth discussing. In this paper, we adopt Communicating Sequential Processes (CSP) to model the ICN-IoT middleware architecture. Five properties (deadlock freedom, data availability, action keys leakage, device faking and user faking) of the model are verified by utilizing the model checker Process Analysis Toolkit (PAT). According to the verification results, the model cannot guarantee the security of data. To solve the problems, we encrypt messages with the receiver's public key, and improve the model by introducing a method similar to the digital signature. The new verification results demonstrate that our study can assure the security of the ICN-IoT middleware architecture.