Modeling and verifying NDN-based IoV using CSP

As a crucial component of intelligent transportation system, Internet of Vehicles (IoV) plays an important role in the smart and intelligent cities. However, current Internet architectures cannot guarantee efficient data delivery and adequate data security for IoV. Therefore, Named Data Networking (NDN), a leading architecture of Information-Centric Networking (ICN), is introduced into IoV. Although problems about data distribution can be resolved effectively, the combination of NDN and IoV causes some new security issues. In this paper, we apply Communicating Sequential Processes (CSP) to formalize NDN-based IoV. We mainly focus on its data access mechanism and model this mechanism in detail. By feeding the formalized model into the model checker Process Analysis Toolkit (PAT), we verify four vital properties including deadlock freedom, data availability, PIT deletion faking and CS caching pollution. According to verification results, the model cannot ensure the security of data with the appearance of intruders. To solve these problems, we adopt a method derived from Blockchain in our improvement. Through the analysis of the improved model, we can truly guarantee the security of NDN-based IoV.