TY - GEN
T1 - Formalization and verification of VANET
AU - Li, Ran
AU - Zhu, Huibiao
AU - Xiao, Lili
AU - Yin, Jiaqi
AU - Fei, Yuan
AU - Lu, Gang
N1 - Publisher Copyright:
© 2020 Knowledge Systems Institute Graduate School. All rights reserved.
PY - 2020
Y1 - 2020
N2 - Vehicular Ad Hoc Network (VANET) is a subclass of Mobile Ad Hoc Network (MANET) types. As a key part of the Intelligent Transportation Systems (ITSs) framework, it can be used not only to provide value added services, but also to guarantee the security of ITS. Since VANET is extensively applied, its security is of great significance. In this paper, we model the architecture of VANET using process algebra Communicating Sequential Processes (CSP). By utilizing model checker Process Analysis Toolkit (PAT), we verify five properties (deadlock freedom, divergence freedom, data leakage, vehicle faking and RSU faking) of the model and find that the proposed architecture may cause data leakage. Hence, we improve the model by encrypting the messages with receiver's public key to cope with this problem. The new verification results show that our study can guarantee the security of VANET.
AB - Vehicular Ad Hoc Network (VANET) is a subclass of Mobile Ad Hoc Network (MANET) types. As a key part of the Intelligent Transportation Systems (ITSs) framework, it can be used not only to provide value added services, but also to guarantee the security of ITS. Since VANET is extensively applied, its security is of great significance. In this paper, we model the architecture of VANET using process algebra Communicating Sequential Processes (CSP). By utilizing model checker Process Analysis Toolkit (PAT), we verify five properties (deadlock freedom, divergence freedom, data leakage, vehicle faking and RSU faking) of the model and find that the proposed architecture may cause data leakage. Hence, we improve the model by encrypting the messages with receiver's public key to cope with this problem. The new verification results show that our study can guarantee the security of VANET.
KW - CSP
KW - Modeling
KW - Security
KW - VANET
KW - Verification
UR - https://www.scopus.com/pages/publications/85090508082
U2 - 10.18293/SEKE2020-011
DO - 10.18293/SEKE2020-011
M3 - 会议稿件
AN - SCOPUS:85090508082
T3 - Proceedings of the International Conference on Software Engineering and Knowledge Engineering, SEKE
SP - 1
EP - 6
BT - SEKE 2020 - Proceedings of the 32nd International Conference on Software Engineering and Knowledge Engineering
PB - Knowledge Systems Institute Graduate School
T2 - 32nd International Conference on Software Engineering and Knowledge Engineering, SEKE 2020
Y2 - 9 July 2020 through 19 July 2020
ER -