## 4 Discussion
Regarding aspects of advantages, disadvantages, and limitations, the works presented here exhibit a relevant view of the area of formal verification and security, in particular those focused on the area of authentication and IoT. However, even though they put forward a great contribution, none presents an intelligible and easily replicated view of the construction process of the artifacts involved in the modeling necessary for the formal verification of the security properties of the proposed solutions. Our work also contributes through this replicable process, which ranges from the selection of security aspects through threat modeling to their conversion and verification through temporal logic using timed automata. As for the **TM** presented, it contributed to identifying threats that should be evaluated. A more detailed view can be obtained by analyzing the artifacts published on our project website ([[https://github.com/wesleybez/mfar_formalverification](https://github.com/wesleybez/mfar_formalverification)]([https://github.com/wesleybez/mfar_formalverification](https://github.com/wesleybez/mfar_formalverification)), accessed on 1 July 2023) and in another publication by the authors that describes the threat-modeling process in greater detail. Furthermore, its process took place in three stages: the definition of the attack surface; the identification, categorization, prioritization, and risk assessment of threats; and the description of countermeasures through the security requirements shown in Table 6. As a result, threat modeling proved to be a thorough assessment that produced important artifacts for formal verification. Quantitatively, the data on threat modeling can be seen in Figure 13(a)-c. Figure 13(a) shows the number of threats by STRIDE category, highlighting the tampering (T) category that had the highest number of threats and the repudiation (R) category with zero threats. In Figure 13(b), which shows threats by attack surface, the negative highlight goes to s05  
Figure 13: Related works—quantitative data. (LPWAN), which is the AT most susceptible to causing more damage, according to DREAD. Finally, the DREAD methodology presents v7 (tampering data) and v11 (unauthorized access) as the threats that create the greatest risk to the mechanism. The **components** came with an overview of the parts of the authentication mechanism and how they communicate (with each other and with the devices). Additionally, they explained how MFA_R works through descriptions and algorithms, explaining its operation and clarifying some of its details. As for the **STMs**, it can be noted that the diagram was generated from the authentication STM (Figure 5) but has significant changes, such as the removal of compatibility support, the possibility of sensor reset, and the abstraction of query generation. However, it is important to point out that the modeling did not happen linearly. After verifying the needs of new states in the TAs, it was necessary to go back to the STMs and correct them. Accordingly, the proposed process helped refine the MFA_R modeling, allowing one to correct problems at design time. As for **automata modeling**, it is important to highlight three points: (i) **compatibility mode**, (ii) **sensor reset**, and (iii) **query abstraction**. Therefore, the diagram does not cover support for **compatibility mode** (i) as it is understood that the decision to operate a device in compatibility mode is prior to authentication itself. By incorporating the compatibility state into the model, the automaton would be in a livelock, which can denote starvation or infinite execution of a state cycle [96]--it never reaches a final state, an infinite movement between states [97], or deadlock, which are associated with threads that are waiting for events to continue executing [96], usually associated with the use of shared resources; this would produce problems for validating other properties--if simulated and evaluated in the project.