## 2 Materials and Methods
### MFA_R Timed Automata Modeling  
This section presents the formal modeling of MFA_R using timed automata. The automata provides an option for a formal approach that can be used to model dynamic aspects and their variability, going beyond the expression potential of the UML [87]. As a result, this is a formal approach that guarantees formal verification by confirming the (safety) properties of the system. To ensure such properties, the tool used in the modeling was Uppaal. This tool is the de facto standard for modeling timed automata [88], through which it was possible to express the temporal evolution and synchronize events through channels, use variables to control the flow, and perform the simulation of the designed models. In addition to the functionalities mentioned earlier, the programming of functions is a possibility that the tool brings and that allows us to extend its potential. Additionally, with Uppaal, it was possible to model several timed automata to evolve in parallel [89]. This design was possible because a project in this tool can describe different templates, and each template represents the modeling of an automaton. Consequently, in order to be simulated, a template must be instantiated in the system declaration section of the project, and every template can be instantiated as many times as necessary. For example, to model the behavior of five identical components, create a template and instantiate it five times. Figure 7: The evolution of the authentication levels’ state machine diagram for the proposed mechanism. It features seven states and 12 transitions. It is responsible for modeling the behavior, evolution, and constraints of MFA_R authentication levels. It is still possible to communicate the templates via channels (channels-chan) and chain events between the templates. However, as mentioned earlier, the tool also provides an interface for queries using temporal logic with reduced TCTL. As a result, it was noted that Uppal was the most suitable choice for developing automata models. Thus, in the present study, four models (templates) were created to represent the components and processes of the mechanism. Such a creation was based on the previously presented state machine diagrams. Comparatively, due to the greater representativeness of the ATs, it was possible to express in the latter the dependence between the events that happen in different components (synchronization), unlike the pure STMs. Consequently, this dependency allowed us to chain events and to model and verify the system's evolution and componentsall concurrently and in sync. The first model is the **sensor registration** process (Figure 8), which contains three states and four transitions. The states represent the unregistered device (\(n\)), the device awaiting registration (\(r0\)), and the registered device (\(r1\)). It is concluded that the diagram is very similar to the STM that gave rise to it (Figure 4), asserting the transparent diagram conversion process and lifecycle monitoring through TAs as well. It is important to remember that this phase of the authentication process takes place over a network with higher data throughput than the LPWAN and a secure channel (i.e., HTTPS). Although this phase is safe from the network's point of view, its modeling is necessary for the feasibility of other properties. The second diagram (Figure 9) models the sensor's **authentication process**. Namely, it models the behavior of the authentication mechanism as a whole. In general, this model is the core of the proposed authentication mechanism. More specifically, it expresses the three authentication factors, the reputation system, and access invalidation. This model is responsible for triggering most of the transitions that will allow the other templates (models) to evolve. Its design phase was the most difficult phase of this work and took several cycles, which resulted in the refactoring of the related STMs. Figure 8: TA of the sensor registration process.