## 2 Materials and Methods
### Background and Related Work
#### 2.1.1 Temporal Logic
The operators \(\bigvee\varphi_{[t,1,t2]}\) (eventually) and \(\square_{[t,1,t2]}\) (always) have the same interpretation, while the operators \(\boldsymbol{\Phi}\varphi_{[t,1,t2]}\) (eventually in the past) and \(\blacksquare_{[t,1,t2]}\) (always in the past) are used to represent the past. As per the mentioned operators, [t,t2] represents the time interval specified in the expression. It is still worth mentioning that MTL uses the quantifiers \(\bigvee\) and \(\exists\) to describe its formulas. Some important works regarding the security areas that use MTL are presented here, beginning with [PERSON] et al. [58] (which uses MTL to prove opacity linked to a defined \(\Delta\) time while also providing proof of the complexity of the theme and a useful case in the context of cloud computing) and continuing with [PERSON] et al. [53], which presents a service called IoTSEER (which models the behavior of IoT apps from their source code). The presented model is unified and allows for evaluating undesired states caused by physical interactions. The authors use MTL to express the policies evaluated in the Simulink (a modeling, simulation, and analysis tool--[[https://www.mathworks.com/products/simulink.html](https://www.mathworks.com/products/simulink.html)]([https://www.mathworks.com/products/simulink.html](https://www.mathworks.com/products/simulink.html)), accessed on 1 July 2023) from Matlab (_Software analysis numeric_--[[https://www.mathworks.com/products/matlab.html](https://www.mathworks.com/products/matlab.html)]([https://www.mathworks.com/products/matlab.html](https://www.mathworks.com/products/matlab.html)), accessed on 1 July 2023), which govern the physical iterations between apps helping in the deployment of the devices. Another relevant work is that of [PERSON] [56], which presents an intrusion detection system (IDS) solution based on temporal logic. His solution uses many-sorted first-order metric temporal logic (MSFOMTL) to represent attacks and temporal patterns concisely. Finally, [PERSON] et al. [59] present PatrIoT, a tool evaluating the actions of programmable IoT apps according to policies described in their language. Such language can be translated into MTL and is the basis for describing policies that deny executing actions that violate them. This type of logic highlights [PERSON]'s work, which uses MSFOMTL for a security solution with IDS. Among the tools utilized in the cited works, Uppaal is the one that stands out the most. Its utilization in works that adopt the TCTL is practically unanimous, characterizing it as the best choice for this type of logic. Other tools adopted in works that used the CTL, such as NuSMV, BSP, and ASMETA, should be mentioned. Simulink also appears in the adoption of MTL, and this simulation tool is commercially widespread in engineering projects. Concerning the application, in Table 1 studies that have varying purposes within the security area were selected. The largest number of works is applied to the IoT area; however, areas range from network protocols, authentication, and security policies, to the security of standalone (software or hardware) agents. However, one can consider the emphasis on the formal verification of zero-knowledge authentication, which is in the same security sub-area of this work. Although many works in the literature cover a range of verification and formal modeling aspects for security, such works focus on something other than authentication's verification and modeling aspects in distributed IoT systems. Due to these limitations, our work is necessary and current to meet such aspects of this modeling. Generally, the importance of formal security verification in different application areas can be noted. Additionally, it was found that the pair TCTL and Uppaal is an suitable choice for the formal verification of security in systems and hardware, according to several works listed above.