# Model Checking Resiliency and Sustainability of In-Vehicle Network for Real-Time Authenticity
## 1 Introduction  
Advanced digital control technology provides more convenience, safety, and predictability to automotive systems. Recently, many vehicles would not only make use of local sensors, but also cooperate with other vehicles and infrastructures, such as the Intelligent Transport System (ITS). For instance, Right-turn Collision Caution (RICC) cooperating with infrastructures can alert drivers in a risky situation hidden when they would make right turn. ITS monitors the situation about uncooning vehicles and pedestrians around intersections or a corner with poor visibility from drivers where a vehicle would make a right turn. It cooperates with the vehicle via road-to-vehicle communication so the information on potential approaching risk is conveyed by vehicle-to-vehicle communication with audio and visual alerts to warn the driver, and when necessary, the driver is alerted about the approach risk. The infrastructure uses a dedicated ITS frequency of 760 MHz for road-to-vehicle and vehicle-to-vehicle communication to gather information that cannot be obtained by vehicle sensors. In addition, various features, such as Communication Radar Cruise Control, Red Right Caution, and Emergency Vehicle Notification using networkcommunication also helps drivers be more predictive against approaching risky situations so that their driving is safe and predictable. However, the vehicle connecting to open networks can be vulnerable to security attacks. For instance, many studies such as [1; 2; 3; 4; 5; 6] have shown that the adversary is able to easily access an in-vehicle network from the outside and control vehicles. Once an adversary compromises an ECU, it disguises itself as a normal node, breaches to other ECUs, and controls and disrupts normal driving function. In addition, DoS (Denial of Service) is also one of the most common attacks that exhausts data processing and communication resources. To prevent the masquerade attack to a vehicle network, the most popular defense technologies are intrusion detection systems (IDS) and authentication systems. Most proposed IDS techniques are not, however, fast enough to protect the attack, i.e., the adversary can compromise the vehicle system before IDS detects the attack [7; 8; 9; 10; 11; 12; 13]. In order to address these issues, many authentication protocols have been studied, such as [14; 15; 16; 17; 18; 19; 20]. These works can be classified into two categories: authentication using group keys [14; 15; 16; 17] or authentication using pairwise keys [18; 19; 20]. In case that CAN uses a group key for message authentication, the group key could be exploited if any node using the group key is compromised. In case of authentication using pairwise keys, CAN bus can be overflowed by authentication tags (e.g., message authentication code) if CAN bus uses a basic pairwise key-based authentication method where every destination node requires a unique authentication tag for verification of a CAN message. Thus, the work [18; 19; 20] adopts a centralized node-based authentication to deal with the overflow issue. However, this centralized node-based authentication has two problems. First, the authentication by a centralized node can be delayed by DoS attack on the centralized node. Second, in case of the centralized authentication, the authenticator could miss a message if it is too slow to process every message. Thus, it should be guaranteed that the authentication is complete on time no matter how often the adversary sends an attack message. To address the above problems, [PERSON] et al. have proposed a new authentication protocol, named MAuth-CAN (Message Authentication-CAN), in [21]. MAuth-CAN uses an ECU node dedicated to authenticating each message over the CAN bus by using pairwise keys. For sharing the authentication result with other ECUs, the authenticator uses an authentication-fail error (AFR) message. The authentication fail report (i.e., AFR message) is transmitted and gives alerts to other nodes only when a message is authenticated.