## 3 Results--Formal Verification of Security Properties Evaluation  
This section presents the simulation (Figure 12) of the MFA_R mechanism and its formal verification through the TCTL queries performed in the selected tool. Such tasks were conducted through Uppaal's simulator tab, a built-in tool that allows for the visualization of available transactions, lists the steps taken during execution, and enumerates the variables list. Furthermore, through these tools, it is possible to visualize the instantiated templates and a diagram showing the exchange of messages during the simulation (this can happen step-by-step or automatically since, in the automated case, the presentation speed of the transitions can be configured). Additionally, evaluation through a trace log (simulation trace) of the paths that lead to unwanted states (i.e., deadlocks) is permitted. This feature allows us to correct them at design time, preventing future crashes. This simulation was developed using an Intel Core i7-4510U processor and 16 GB of RAM with the system Ubuntu 18.04.03 LTS operating. As for the verification of properties, the security aspects (Table 6) were converted to the TCTL query language, according to Table 8. Thus, the conversion did not take place directly (one-to-one). Some aspects were converted into more than one query to provide a complete verification of the aspects. First, it was analyzed if the model is free of deadlocks (Table 8--c00), and for that, a query was executed that evaluates each possible execution path (\(A\)[]). The result was that there are no deadlocks in the project, and this result was made possible through some refinements performed during the development of the study. One of the consequences of this verification proposed here was the correction of the initially proposed behavioral model. As a result, there were modifications to the STMs and ATs, which made the MFA_R deadlock-free. Figure 11: TA of the evolution of authentication levels within the proposed mechanism. It contains seven states and 13 transitions, two of which are final states and all-event query transitions. It serves as a panel for better understanding and priority queries of the other templates. As for the **a01** aspect, two queries were created: **c01** and **c02**. The first one (**c01**) checks if there is a possible way to reach the data reception state (_authentication.q5_) without going through the positive result of the second-factor authentication (_authentication.q3_). The second query (**c02**) can be translated as evaluating whether there is a path that allows the sensor to send data (_sensor.q7_) without the authentication mechanism being ready to receive (_authentication.q5_). The first validation was presented as TRUE, and the second was FALSE. Consequently, the combination of the two leads to the conclusion that sending data without going through the second authentication factor is impossible. Following the **a02** aspect, it was verified whether the discovery (spoofing) of _auth_code_ leads to removal from the system. This aspect was translated into the query (**c03**), which checks if an _auth_code_ error is identified at any time; the mechanism will eventually end up with a critical failure (_authentication.q8_). This query is TRUE and used the error code generated by the authentication template. As a result, it was impossible to spoof/discover _auth_code_ without being discovered and removed from the system.