# Model Checking Resiliency and Sustainability of In-Vehicle Network for Real-Time Authenticity
## 5 Formal Analysis of MAuth-CAN
### Model Checking Analysis of Theorem 1  
To avoid the complexity of formal analysis, we abstract interaction between CAN components, as shown in Figure 5.  
The model of CAN interaction comprises authenticator, attacker, and CAN bus. The attacker model has the same behavior as normal ECUs, but the authenticator in our model responds to the message from the attack by broadcasting AFR messages. We do not include the behavior of the CAN controller of CAN message receiver nodes in our model since the authenticator model has the same behavior as CAN message receiver and we focus on the resiliency of MAuth-CAN's authentication that handles every attack message. The authenticator model in Figure 5a waits for any message through CAN bus. When the authenticator reads a message (RxMsg) from CAN bus, the authenticator in Figure 5a transits into the location Authenticate for processing authentication. If the message passes the authentication, it returns to Idle state. Otherwise, it joins SendRep state. Then, it sends the AFR message for the unauthenticated message when CAN bus is available (CANBUS = FREE). The authenticator keeps any message in its reception queue (EnQ) when it is in authentication. If the queue is empty, the authenticator returns to the initial location Idle. Otherwise, it returns to Authenticate and performs authentication for another incoming message again. The CAN controller model of an attacker in Figure 5b is simpler than the authenticator. If the CAN controller has a message to send and CAN bus is available, it just sends it through CAN bus. Notice that it returns to the initial location when the transmission of the message is acknowledged by CAN bus through the event RxMsg. The CAN bus model in Figure 5c controls the permission for a CAN controller to access CAN bus. Initially, it allows any controller to use CAN bus by setting CANBUS:=FREE. If the CAN bus receives a message via TxMsg, it locks the key by setting CANBUS:=OCCUPIED, prohibits any node from using CAN bus, moves to Transmit location, and notifies the transmitting of a message. Finally, the CAN bus returns to the initial location Idle with unlocking the key with setting CANBUS:=FREE. Based on the CAN networking model in Figure 5, Figure 6 captures CAN behavior models in TA. It also comprises three models: Authenticator, ECU and CAN bus. Four TA processes are instantiated for simulation and verification: Two authenticator processes from the authenticator model, one CAN attacker process from the ECU model, and one CAN bus process from the CAN bus. Figure 5: CAN networking model. (**a**) This figure shows the state transitions of the authenticator in MAuth-CAN. (**b**) It shows the state transitions of an ECU in data transmission. (**c**) It shows the state transitions of the CAN bus for data transmission. As shown in Figure 5(a), two authenticator processes are instantiated from the authenticator model to capture message queuing behavior using the reception queue of size 2. It particularly highlights the concurrent behavior of the CAN controller's authentication, reception, and message transmission using the reception queue of size 2. When a new message arrives, authenticator's CAN controller checks the message and sends AFR messages for unauthenticated messages. While the authenticator is sending AFR, it can simultaneously receive another new message. It is because the reception queue and sending queue of a CAN controller are separate. However, only one of them can process authentication at the same time. The authenticator processes, ECUAuth_Q1 and ECUAuth_Q2, in Figure 5(a) have an invariant over Authenticate location, which limits the authentication time to a specific time bound AUTH_TIME. The authenticator process leaves Authenticate location after AUTH_TIME expires and transits to TxRep location so as to send one of AFR messages. In this interaction model, canstat represents the status of CAN bus. The authenticator process can send the AFR message through CAN bus when  
Figure 6: Simulation of CAN networking in TA.