Formal Security Evaluation And Improvement Of Two Types Of Typical In-vehicle Protocols

With the advent of the industry 4.0 era,modern vehicles have more and more electronic and software components to support various functions from vehicle comfort systems to advanced driver assistance systems or information and entertainment functions,resulting in a significant increase in system complexity.As a result,the automotive industry is moving towards virtualization of automotive hardware and software platforms that rely on Ethernet connections and TCP/IP communication protocols.With the hotness of the field of autonomous driving,the automotive Ethernet protocol has emerged as the times require.Compared with the traditional automotive bus protocol,it has great flexibility in network design and can meet the high-standard requirements of automobiles.For the automotive industry,the DDS protocol is an application of a new middleware protocol,which plays an indispensable supporting role in the vehicle electronic and electrical communication system.In recent years,there have been studies combining the FlexRay protocol with Ethernet technology to design gateways for vehicle-mounted networks,and there are also studies combining FlexRay and DDS for real-time communication analysis.However,there is still a lack of formal modeling analysis and security assessment for protocol security issues,and a lack of visual models for protocol interactions.Aiming at the above-mentioned status quo,based on the colored Petri net,combined with the Dolev-Yao attacker model,the DDS and FlexRay protocols suitable for vehicle network communication are modeled and security evaluated by formal analysis methods.The object of this thesis is to study the DDS protocol and FlexRay protocol suitable for vehicle communication.Firstly,the model is established based on the layered modeling idea guided by the theory of colored Petri nets.Secondly,the DolevYao attacker model is used to simulate the man-in-the-middle attack on the protocol network channel.Finally,a new protocol solution is proposed for the security loopholes in the protocol.The specific work of the thesis is as follows:1.The message flow diagram is established according to the protocol interaction process,and the model is established based on the colored Petri net theory through the protocol formalization tool CPN Tools.We divide the overall interaction process of the protocol into three layers,namely the top layer,the middle layer and the bottom layer.The top layer describes the protocol interaction process from a macro perspective,the middle layer refines the top layer,and the bottom layer describes specific messages.After the modeling is completed,a state space report is generated to judge whether the initial model is appropriate;2.An improved Dolev-Yao attacker model is introduced for the original model network channel,and replay,tampering and spoofing attacks are introduced in the original model.Using state space reports and ML functional programming language to discover the loopholes in the protocol.In addition,since the UDP layer of the DDS protocol depends on the security of the DTLS protocol,and experiments have shown that the TLS protocol is secure under the Dolev-Yao attacker model,this thesis uses the formal analysis tool Scyther after the CPN modeling is completed.Under the DolevYao attacker model and the strong security model,the simulation attack experiment is carried out,and the results show that the DTLS protocol is safe;3.Aiming at the vulnerabilities that have been discovered,a new protocol design scheme is targeted.Due to the inequality of shared key generation in the DDS protocol and the existence of replay attacks,the security of the protocol is strengthened by introducing timestamps and changing the way the shared key is generated.Aiming at replay and tampering attacks in the FlexRay protocol,the security of the protocol is reinforced by introducing security mechanisms such as timestamps,random numbers,and hash functions.Finally,a model is established based on the proposed new protocol scheme and an attacker model is introduced,and the security assessment is carried out through the state space report.The results show that the new DDS scheme effectively solves the replay attack,and the more secure shared key generation method improves the security of the protocol;the new FlexRay scheme effectively solves the replay and tampering attacks and improves the security of the protocol,thus proving that the design of the new scheme is effective.