# Model Checking Resiliency and Sustainability of In-Vehicle Network for Real-Time Authenticity
## 5 Formal Analysis of MAuth-CAN
### Model Checking Analysis of Theorem 2
If TEC is greater than 127 and lesser than  
Figure 8: CAN-Frame in base format in bit levels [30]. Figure 9: Modeling a dummy protocol into TA. (**a**) This figure gives an example of a simple protocol in packet frames. (**b**) This figure captures the simple protocol into a TA model in a bit-wise level. 255, then the CAN controller is led to Passive Error mode and a Passive Error frame will be transmitted on the bus. The CAN controller in Passive Error mode is given a penalty in such a way that it is more delayed to make transmission than the CAN controller in Active Error or Normal modes. The situation is captured by our CAN controller model of TA where the CAN controller in Passive Error mode should stay over SuspTrans location for 8 time-units. When TEC of a CAN controller is greater than 255, then the controller enters Bus Off state, where no frames cannot be transmitted by the controller [30]. We capture the BO situation with Reset location in Figure 11, where the CAN controller stays for a while without being able to send any message. Now, we present the formal verification results of model checking for MAuth-CAN under BoA. In order to prove Theorem 1 that the CAN controller in charge of the authentication is sustainable to BoA, we need to verify if our dual-CAN controllers can never be put into Passive Error mode when the attacker crafts continually to cause transmission errors. We introduce to Lemma 3 as follows:  
Figure 11: A CAN controller model in TA. Figure 10: CAN bus model in TA. **Lemma 3**. : _Dual-CAN controllers of MAuth-CAN authentication is never put into Passive Error mode together at the same time when the attacker is in Passive Error mode._  
We prove Lemma 3 by model checking as follows: In order to reduce the state space of our models, the TA authenticator model and the TA at-tacker model in Figures 12 and 13 are mutated from the CAN controller model of Figure 11 so that they terminate analysis when one of them goes into Passive Error mode. That is, when either of the authenticator controller or the attack controller goes to Passive Error mode first, then the analysis is over. We verify that both dual-CAN controllers for authentication never go to Passive Error mode at the same time. In this way, our model checking using the mutated CAN controller models can be less suffering state-explosion issue. We use the following queries to prove Lemma 3:  
\[\textbf{CTL-Property-5: A[] not deadlock} \tag{6}\]  
**CTL-Property-6: A[] CANContAttk3.errMod==ERR_PAS imply**  
**(CANContAuth1.errMod!= ERR_PAS or CANContAuth2.errMod!= ERR_PAS)**  
**CTL-Property-7: A[] (CANContAuth1.errMod! = ERR_PAS or CANContAuth2.errMod! = ERR_PAS)**  
CTL-Property-5 specifies that the system model should never be in deadlock status in which every process stops running. We use it to check if our TA model is valid to check using model checking. CTL-Property-6 specifies that the error mode (errMod) of both authenticators (CANContAuth1 and CANContAuth2) would never be in Passive Error mode (ERR_PAS) together at the same time when the error mode (errMod) of the attacker (CANContAtt3) happens to be in Passive Error mode (ERR_PAS). Similarly, CTL-Property-7 is used to check if they can fall into Passive Error mode. Figure 9.0 An ECU controller model of the authenticator in TA. Figure 14 shows that the properties above are met by our model, implying that Lemma 3 is proved by the model checking of the CTL properties. By proving Lemma 3, we conclude that Theorem 1 is proved and that our authentication using dual-CAN controllers is resilient to BoA even when the attacker can exploit the highest priority of CAN controller. Our model checking environment is as follows:  
* Processor: Intel Core i7 CPU, 1.80 GHz, 2.30 GHz
* RAM: 16.0 GB
* OS: Windows 10-64 Bits