# Model Checking Resiliency and Sustainability of In-Vehicle Network for Real-Time Authenticity
## 1 Introduction
This minimizes the communication overload caused by a centralized authentication because the authentication fail report is transmitted only when a message cannot pass authentication. In addition, [PERSON] et al. addresses Bus-off Attacks (BoAs) by introducing their centralized message authentication to dual-CAN controllers. Under the adversary's BoA to the authenticator, the AFR message from the authenticator can also be destroyed by the adversary, resulting in consecutive transmission errors. If the transmission error count of the authenticator steps over a threshold, it is enforced to leave CAN bus for a while and reset to recover the connection to CAN bus. [PERSON] et al. adopts dual-CAN controllers for the authenticator to be more sustainable under BoA. [PERSON] et al. [21] also showed that (1) MAuth-CAN is robust against the masquerade attack and BoA, (2) it requires approximately 46% less CAN bandwidth than a comparable protocol [19], and (3) it does not need to modify the current CAN controller to apply the CAN protocol. However, they have not provided the proof of timing-related properties of MAuth-CAN that can be used for security proof and evidence for practical use of real applications. For instance, MAuth-CAN should prove that no adversary message is accepted by any node while authentication is in processing under DoS attack. It is related to a timeout for AFR, which delays message communication. Thus, it is necessary to check if such a timeout is bounded to check if the authentication delay meets the maximum acceptance communication delay. In this paper, we show that the authentication of MAuth-CAN is resilient enough to prevent a masquerade attack for the given timing constraints and is sustainable under a DoS attack. In addition, we prove that the timeout for authentication can be bounded with respect to the message transmission time. In this paper, we apply formal methods of model checking to prove the timing properties of MAuth-CAN. We build formal models of CAN and MAuth-CAN using timed automata and perform model-checking to verify the critical timing properties of MAuth-CAN using UPPAAL SMC and UPPAAL MC. We present two formal models of CAN and MAuth-CAN. The first model abstracts MAuth-CAN by a producer-consumer model in terms of authenticator and attacker, so that it is proved that the authenticator in terms of a consumer addresses all attack messages from the attacker in terms of a producer. The second model details CAN in the level of MAC frame of the data link layer, so that the model of MAuth-CAN is shown to be valid in the data-link layer of CAN networking. This paper presents sufficient conditions to ensure:  
* The centralized authentication of MAuth-CAN never fails to make AFR messages reach individual ECUs within a specific bounded time,
* The authentication of MAuth-CAN can never be a victim of BoA. The above conditions are relevant to (1) the size of reception queue of authenticator's CAN controller, (2) the relation between authentication time and CAN bus transmission time, and (3) the number of CAN controllers of the authenticator. This paper presents the following three contributions:  
* In terms of MAuth-CAN security, it shows that MAuth-CAN is resilient and sustainable against a message flooding attack and bus-off attack under the specific conditions this paper provides;
* It presents a usage of formal methods to obtain certificates of safety and security standards and regulations, such as ISO (International Organization for Standardization) 26262;
* It presents new formal models of CAN bus at the level of MAC (Media Access Control) of the data link layer that can be useful for verification of properties of other applications running on CAN bus. The rest of the paper is organized as follows: Section 2 discusses the related work. Section 3 presents the background theory of this work. Section 4 overviews MAuth-CAN, a centralized CAN authentication, two attack scenarios i.e., masquerade attack and BoA attack, and MAuth-CAN's countermeasure to those attacks.