# 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  
Recall the scenario that BoA enforces the CAN controller of the authenticator to leave CAN bus for a while. When the authenticator tries to transmit AFR messages, the attacker causes transmission error. The attacker with the same priority of CAN bus begins the attack message transmission at the same time when the authenticator begins message transmission. Then, two messages conflicts, resulting in transmission error. The repeated transmission errors accumulate up to a specific count, then CAN system gets rid of the attacker and the authenticator from CAN bus for a while. The CAN authentication should be designed to sustainable against this BoA. In order to capture such a complicated situation, we present more concrete and detailed model of the CAN controller and bus in TA. Our CAN controller model in TA captures a detailed behavior of the CAN controller based on the CAN protocol in Figure 8. We capture CAN controller's behavior in a bit-wise level as if a simple protocol is captured by a TA as shown in Figure 9. In Figure 9, a frame consists of a specific number of bits and TA captures the behavior of such a frame with the same series of time units. Here, we do not consider the semantics of bits and focus on a bit-wise timing behavior of the protocol. If a protocol evolves from one frame to another frame, TA captures the frames transits from one location and to another location. Basically, a frame is captured by a location in our TA model, where our TA model stays for the same time units as the number of bits of a frame. For example, the Start frame using 1 bit in Figure 9 is captured by the Start location where TA stays for the same number of time units as 1 bit. A specific event occurring on a frame can be captured by an event causing a transition leaving off the location representing the frame. For example, if a Data frame in Figure 9 encounters an error and needs re-transmission, then TA captures it by a transition returning from Data location to Start location. Figures 10 and 11 shows TA models of CAN bus and controller in the MAC level of the data link layer. The CAN controller has three modes: Receiving mode, transmission mode, and error handling mode. The receiving mode consists of receiving (Rxring) and error handing locations (RxErrRep, RxErrSuffing, RxErrDelimite). The transmission mode is composed of multiple transmissions of different frames, as shown in Figure 11. When a CAN controller needs data transmission, the CAN controller model at the location Rxing in Figure 10 checks if CAN bus is available by checking the condition variable canstat. The SOF frame of Figure 8 is modeled by the invariant x \(\leq\) SOF over the location StartTrans and the guard x==SOF on the transition leaving StartTrans in Figure 11. Note that the Arbitration Field frame needs an interaction of CAN controller with the CAN bus for CAN bus arbitration and such a scheduling responsibility is placed upon the CAN bus, so the Arbitration Field frame is modeled on the location CANArbitration in CAN bus model of Figure 10. The last 1 bit of Arbitration frame field and the first 2 bits of Control field are abstracted together by the location DestControl. When more than one CAN controller attempt to make any frame transmissions simultaneously, it may lead to a transmission error status of CAN controller and bus. The transmission error is captured by the transition leaving the location Txing of Figure 11 having no guard. The transition may be taken non-deterministically to leave the location Txing, and that implies that our CAN controller model of TA can go to a transmission error (handling) status at any time. When a transmission error occurs, the CAN controller is put into one of Active Error model, Passive Error mode, or Reset. When a transmission error happens, the CAN controller goes to at Active Error mode and an Active Error frame will be transmitted on the bus if TEC (Transmission Error Counter) is lesser than 128.