## 5 Conclusions and Future Works  
The work successfully and formally verified, through ATs and TCTL, the correctness of the proposed mechanism. It was verified that the mechanism is free of dead-locks (c00), as well as the condition of being authenticated to send data (c01 and c02), and, finally, that failures in authentication, sending data, and impersonation attempts lead to a final state of failure (c03-c06). Such correctness translates into the successful verification of properties created from security requirements. With a workflow that covered everything from components to modeling in timed automata, it was possible to create a framework of artifacts that supported it. Thus, through formal methods, the properties of models were successfully demonstrated, which expressed the safety requirements. In addition, a set of reusable resources was created for the extension or creation of a mechanism similar to the one proposed (project site ([[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)). Accordingly, a survey of the state-of-the-art and related works was carried out; threat modeling was also designed that supported the selection of security requirements (aspects) that would be transformed into TCTL properties, following the modeling of components and a short description of its operation; and the modeling of state machines, and their conversion to timed automata was carried out, ending with the creation of properties in TCTL and their verification. The entire process was self-explanatory so that it could be easily verified and reused in future works. As such, any work of similar scope will be able to follow the workflow proposed here and one can use the artifacts published on our GitHub as a basis for producing one's own. Overall, formal verification was used to demonstrate the properties of our computational multi-factor authentication mechanism for restricted devices and LPWAN. Thus, it was possible to express the evolution of the component states during the mechanism operation  
Figure 15: Quantitative overview of state diagrams and modeling in timed automata. and model them so that there were no interlocks between the parts. The security aspects that the mechanism meets were also successfully verified. In future work, some of the other security aspects to be complemented in the model will be analyzed. Verification will also be performed using tools that use the Dolev-Yao [98] model of an adversary to validate security protocols (i.e., ProVerify and Tamarin Prover). This additional validation aims to better understand the aspects involved in the communication and evaluate the communication protocol used in the data exchange between the devices. Since timed automata are not capable of fully analyzing some aspects of the cryptographic protocols involved in LPWAN communication, the use of such verifiers becomes very important. Additionally, reinforcement in the present study will be carried out through a more in-depth analysis of the threat model applicable to the proposed mechanism and the mitigation of threats found. This becomes essential when the network technology to be used at the time of analysis is brought to light. LPWAN protocols, to a large extent, add a layer of security to the system as it already has some security features implemented in its protocols. Finally, a more practical study of the MFA_R application is also necessary through scalability issues, deployment options, and simulation using real sensors--going beyond the computational simulation carried out in the previously mentioned articles [14; 28; 29]. Writing--original draft preparation, W.R.B. ; writing--review and editing, J.E.M. ; and supervision, C.B.W. All authors have read and agreed to the published version of the manuscript  
This research received no external funding. Not applicable. The authors declare no conflict of interest.