# Model Checking Resiliency and Sustainability of In-Vehicle Network for Real-Time Authenticity
## 2 Related Work  
In 2010, [PERSON] et al. were the first to demonstrate attacks on in-vehicle network using a real vehicle [1]. They introduced the CARSHARK tool, which makes it easy for an adversary to analyze and inject attack packets on in-vehicle network, i.e., CAN bus. After the first vehicle attack, many studies included new attack surfaces on an in-vehicle network [2; 3; 4; 5]. To deal with these cyber-attacks on in-vehicle network, intrusion detection systems [7; 8; 9; 10; 11; 12; 13] and message authentication protocols [14; 15; 16; 17; 18; 19; 20; 21] were studied. In the work of [7; 8; 9; 10], the transmission frequencies or sequences of CAN packets were used to detect the CAN traffic abnormality caused by in-vehicle network attacks. Recently, deep neural network (DNN) model-based intrusion detection systems that take transmission frequencies or sequences of CAN packets as input values have been proposed in [11; 12]. However, these studies [7; 8; 9; 10; 11; 12] cannot detect masquerade attacks by a compromised ECU because the compromised node can mimic the transmission frequencies or sequences of CAN packets to bypass intrusion detection algorithms. To handle the masquerade attacks, [PERSON] et al. proposed an ECU's clock-based intrusion detection system [13]. In this study, a clock skew for each ECU is profiled as a hardware fingerprint, which is unique for every ECU, and this inimitable value is used to identify a masquerading ECU. However, this study cannot be used to deal with masquerade attacks using aperiodic CANmessages generated from aperiodic vehicle operations, such as auto-parking, lane keeping aid (LKA), and adaptive cruise control (ACC) functions. Furthermore, this clock-based intrusion detection can be defeated by the clock emulation attack proposed in [22]. To address the limitations of existing intrusion detection systems, message authentication protocols for in-vehicle network have been designed. In general, message authentication protocols can be divided into two categories: a group key-based authentication [14; 15; 16; 17] and a central node-based authentication [18; 19; 20; 21]. In the group key-based authentication studies [14; 15; 16; 17], one group key shared by all ECUs is used to generate authentication tags such as message authentication code. However, these studies cannot also handle masquerade attacks because one group key could be accessed by a compromised node. In light of this, centralized node-based authentication studies have been presented in [18; 19; 20; 21] for handling masquerade attacks by compromised ECUs. Since the centralized node-based authentication does not share one group key with all ECUs, a compromised ECU cannot access the authentication keys stored in other ECUs. However, the methods [18; 19] cannot be applied into legacy vehicles because the CAN-controller must be modified to include new functions that do not follow the CAN-standard or incurs network overhead that exceeds the maximum capacity of the CAN bus. Furthermore, the protocol [20] also has limitation that several bytes of a CAN message is not included in the authentication value generation process. To handle these issues of authentication protocols, [PERSON] et al. presented an authentication report-based message authentication [21]. This protocol does not incur network overhead nor require CAN controller modification, but there is a message authentication delay caused by an authentication report message. Even though the work of [21] evaluated the authentication delay by using CAN development boards, there is no formal analysis about the delay which could affect real-time operations of vehicles. Thus, this paper puts the authentication delay of [21] into formal analysis using UPPAAL SMC and UPPAAL MC.