Du Jinze, Tang Rui, Feng Tao
School of Computer and Communication, Lanzhou University of Technology, Lanzhou 730050, China.
Sensors (Basel). 2022 Sep 8;22(18):6792. doi: 10.3390/s22186792.
The combination of in-vehicle networks and smart car devices has gradually developed into Intelligent Connected Vehicles (ICVs). Through the vehicle security protocol, ICVs can quickly realize communication transmission. However, with the more frequent connections between smart in-vehicle devices and the network, the relationship between intelligent cars and external systems is becoming more and more complicated, and in-vehicle networks are gradually facing many security issues. Strengthening the security of in-vehicle protocols has become particularly important. This paper uses the model building method based on the Colored Petri Net (CPN) theory to model the Scalable service-Oriented MiddlewarE over IP (SOME/IP) protocol of the vehicle Ethernet. The security protocol is formally verified and analyzed by combining it with the Dolev-Yao adversary model detection method. After verification, the protocol is subject to three attack vulnerabilities: replay, tampering, and deception. We introduce timestamps and random numbers to strengthen the protocol security. After the final analysis and verification, the improved scheme in this paper can effectively improve the security performance of the protocol.
车载网络与智能汽车设备的结合逐渐发展成为智能网联汽车（ICV）。通过车辆安全协议，智能网联汽车能够快速实现通信传输。然而，随着智能车载设备与网络之间的连接愈发频繁，智能汽车与外部系统之间的关系变得越来越复杂，车载网络逐渐面临诸多安全问题。加强车载协议的安全性变得尤为重要。本文采用基于有色Petri网（CPN）理论的模型构建方法，对车载以太网的可扩展面向服务中间件（SOME/IP）协议进行建模。通过将其与Dolev-Yao敌手模型检测方法相结合，对安全协议进行形式化验证与分析。验证后，该协议存在重放、篡改和欺骗三种攻击漏洞。我们引入时间戳和随机数来增强协议安全性。经过最终的分析与验证，本文提出的改进方案能够有效提高协议的安全性能。
