# 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
\begin{table}
\begin{tabular}{c c c c c c c} \hline \hline
**Case** & **IQSize\({}_{\textbf{AUTH}}\)** & **T\({}_{\textbf{auth}}\)-\({}^{\textbf{T}}\)x** & **CTL-Property-2** & **Case** & **IQSize\({}_{\textbf{AUTH}}\)** & **T\({}_{\textbf{auth}}\)-\({}^{\textbf{T}}\)tx** & **CTL-Property-2** \\ \hline
1 & 1 & = & Not Satisfied & 4 & 2 & = & Not Satisfied \\ \hline
2 & 1 & \(<\) & Not Satisfied & 5 & 2 & \(<\) & _Satisfied_ \\ \hline
3 & 1 & \(>\) & Not Satisfied & 6 & 2 & \(>\) & Not Satisfied \\ \hline \hline \end{tabular}
\end{table} 
Table 3: Setting of the model checking for Lemma 1 and model-checking results. CTL-Property-1 specifies that the system is put into no deadlock where no progress is made. CTL-Property-2 states that AttkMsgCnt is not larger than the maximum reception queue size of authenticator's CAN controller. To prove Lemma 1, we have six different configurations in Table 3, where the maximum reception queue size of the authenticator, the authentication time, and transmission time are varied. The maximum reception queue size is either of one or two. The transmission time and the authentication time are also varied in such a way that \(\text{T}_{\text{auth}}\text{-}\text{T}_{\text{tx}}\) where \(\text{-}=\{<,=,>\}\). In Table 3, \(\text{T}_{\text{auth}}\) and \(\text{T}_{\text{tx}}\) denote the authentication processing time and the transmission time, respectively. The results show that CAN authentication needs no more than two queues if the authentication time is less than the transmission time, so that no message is missed without verification. To validate our models, we simulate the model using statistical model checking technique and the following query:  
\[\text{Sim-Property-1: simulate [\leq\] 100;1] CANBus1.srvCNAID} \tag{3}\]  
This query states which CANID preempts CAN bus over time. Figure 7 shows a simulation of CAN authentication with different number of CAN controller. The \(x\)-axis represents the time and the \(y\)-axis represents the identifier of a CAN controller which makes it to transmit a message. Thus, Figure 7 shows which CAN controller makes it to transmit messages over time. The attacker's CANID is 2 and the authenticator's is 1. Figure 7(a) shows the case where the authenticator's CAN controller uses a single buffer of a reception queue so it cannot handle no more than one message. The first two messages are adversary messages sent by the attacker. The third and fourth messages are the AFR messages sent by the authenticator after addressing the first adversary message. Note that authenticator's CAN controller succeeds in sending the AFR messages for the first adversary message, but not the rest of the adversary messages. Meanwhile, the plot in Figure 7(b) shows different behavior of CAN authentication when authenticator's CAN controller 2 size of the reception queue. In Figure 7(b), the first two transmissions are made by the attacker. The second adversary message transmission  
Figure 7: Simulation of CAN authentication nodes. (**a**) This figure shows that the attack messages are overwhelming CAN bus by message flooding attack, and blocking all AFR messages from the authenticator. (**b**) This figure shows that two consecutive AFR messages for one attack message are transmitted on CAN bus without failure and the attack message cannot dominate CAN Bus. is possible while the authenticator is checking the first adversary message. However, the 4 transmissions following the first two adversary messages are made for AFR messages by the authenticator. That is consistent with Figure 4: Two attack messages can be consecutively transmitted over CAN bus, but AFR messages follow those attack messages. In following, all AFR messages are successfully sent following every attack message. No AFR message is delayed by adversary message, then no adversary message is adopted by ECUs due to AFR messages.