Modeling and verifying NDN‐based IoV using CSP. Issue 10 (21st July 2021)

• Record Type: Journal Article
• Authors: Chen, Ningning; Zhu, Huibiao; Yin, Jiaqi; Fei, Yuan; Xiao, Lili; Zhu, Minghua
• Other Names: Braione Pietro guestEditor.; Briola Daniela guestEditor.; De Angelis Guglielmo guestEditor.; Gallo Francesco guestEditor.; Poggi Francesco guestEditor.; Quattrocchi Giovanni guestEditor.
• Is Part Of: Journal of software. Volume 34:Issue 10(2022)
• Page Start: n/a
• Page End: n/a
• Publication Date: 2021-07-21
• Subjects: Named Data Networking (NDN) -- Internet of Vehicles (IoV) -- process algebra CSP -- blockchain -- modeling and verification; Software engineering -- Periodicals; Computer software -- Development -- Periodicals; Software maintenance -- Periodicals; 005.1
• DOI: 10.1002/smr.2371
• Languages: English
• ISSNs: 2047-7473

Abstract

Abstract: 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, namely, deadlock freedom, data reliability, 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 construct a blockchain‐based mechanism by creating a blockchain‐based distribution trusted platform on top of NDN‐based IoV. Through the analysis of the improved model, the blockchain‐based mechanism can truly guarantee the security of NDN‐based IoV. Abstract :