Research on verification method of Gatekeeper model of Internet of Vehicles protocol for time constraints

Data transmission time is crucial in real-time broadcast communication authentication protocols for vehicular networks. Prolonged transmission times can lead to communication delays, adversely impacting vehicle performance and protocol security. Utilizing computer simulations and tests proves challenging in imposing practical constraints on data transmission times and conducting security analyses for vehicular broadcast communication authentication protocols. Therefore, this paper proposes a real-time modeling and verification approach for vehicular broadcast communication source authentication. This method employs a model of the vehicular broadcast source authentication protocol to impose practical time constraints and management on data, addressing the issue of time verification in data transmission and enhancing the security of the vehicular Ethernet broadcast source authentication protocol. The modeling approach focuses on the real-time vehicular broadcast source authentication protocol, Gatekeeper, applying practical time constraints to different types of transmitted data. The analysis considers the necessary time security attributes within the protocol, establishing a timed automaton model based on the protocol's source authentication process. Finally, the real-time, confidentiality, and robustness of the vehicular broadcast source authentication protocol, Gatekeeper, were validated using the model-checking tool UPPAAL.

I. Introduction

With the continuous evolution of automotive bus networks, traditional on-board network buses cannot meet low latency and high real-time data transmission demands. Consequently, the emergence of in-vehicle Ethernet has become essential [1]. In the real-time communication of in-vehicle Ethernet, factors influencing security performance predominantly include network bandwidth resources, data real-time characteristics, and the security of communication protocols. Among these, security protocols' real-time data communication capability has the most significant impact.