# 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
(**a**) This figure shows two UPPAAL processes of message authenticator that individually process authentication of incoming message. (**b**) This figure shows an UPPAAL process of an ECU that continuously sends messages, simulating message flooding attack. (**c**) This figure shows an UPPAAL process of a CAN bus that simulates the message transmission in the synchronization with the sender ECU and the receiver ECU. no node occupies CAN bus, then castat value of CANBus1 is set to true (1). When TA authenticator enters RepeatAFRMsg location, it broadcasts two consecutive packets for one AFR message. The ECU process in ECUTx1_Q1 of Figure 6b may send any attack message (txMsg[cantid][attkid]) at any time if CAN bus is available. If the reception of the attack message is acknowledged by the authenticator i.e., rxMsg[cantid][attkid] is received, it may send another message. The CAN bus in CANBus1 of Figure 6c manages the permission for use of CAN bus using canstat. If the CAN bus process receives a message from an ECU and the authenticator, it sets canstat to false (0). Then, any CAN controller cannot occupy CAN bus. The transmission of messages is captured with the clock x and the invariant TRX_TIME over Transmit location. The CAN bus process stays over Transmit location for TRX_TIME time units, and then it leaves Transmit location with synchronizing the channel rxMsg and setting canstat to true (1). Particularly, The CAN bus model is designed to count the number of attack messages using the function checkAttk(). The number is denoted by AttMsgCnt. AttMsgCnt keeps increasing, meaning that the authenticator fails to check the attack message. If AttMsgCnt keeps below a specific number, particularly the reception queue size of the authenticator, it means that the authenticator succeeds in authenticating every attack message. MAuth-CAN authenticator must not miss any message without verification, meaning that no ECU should not read unauthenticated message. All CAN controllers on ECUs temporarily store any incoming message in the reception queue during authentication. They postpone reading it until a predefined authentication time ends. However, when the AFR message arrives within the predefined authentication time, the CAN controller regards that the message in the reception queue fails the authentication and discards it. For the reasons, it is crucial to characterize the AFR waiting time TB i.e., the duration that an ECU waits for AFR message. Also, the CAN authenticator is capable of verifying consecutive adversary messages and transmit AFR messages within a predefined authentication time so as to protect every ECU from adversary messages. In terms of the authenticator, we prove the following lemma in order to characterize the CAN controller of the authenticator that can protect adversary messages in any forms:  
**Lemma 1**. : _If the CAN controller of the authenticator is given the reception queue of size 2 and the transmission time is less than the authentication time, it can always verify every new message and every ECU does not miss AFR._  
In order to prove Lemma 1, we model-check the CAN controller model of the authenticator and checks the number of delayed AFR messages in the transmission queue. If the variable AttkMsgCnt is not larger than the size of the reception queue, we can say that the authenticator has no remaining AFR to send. The following two CTL properties are checked by UPPAAL MC and the verification results are also shown in Table 3:  
\[\textbf{CTL-Property-1: A[] not deadlock} \tag{1}\]  
\[\textbf{CTL-Property-2: A[] AttkMsgCnt}\leq\textbf{IQSizeAUTH} \tag{2}\]