## 2 Materials and Methods
### Background and Related Work
#### 2.1.1 Temporal Logic  
To begin with, temporal logic is one of the ways of specifying modal logic that can be presented as linear time or branching time [30]. First, the linear time approach can be seen as computing a word formed from a formula to be evaluated; its processing can happen in the form of events or run-time. The second approach, branching time, creates branches that are not represented as a word but instead as a branching tree, consequently increasing resource consumption during the verification process. All the approaches discussed below are from these two branches of temporal logic spring. Furthermore, the emergence of temporal logic occurred when the unified verification of concurrent and sequential programs was a great challenge [31] and the inadequacy of the current methods for verifying the real-time system was highlighted. Thus, different solutions for temporal logic were introduced over time, such as linear temporal logic (LTL), computational tree logic (CTL), timed computational tree logic (TCTL), and metric temporal logic (MTL), which will be presented together with some related works. As a result, for each logic approach, there is an introduction, a discussion of language aspects, and relevant related works; a table summarizing the works presented is at the end. **Linear temporal logic (TLL)** is a type of logic that processes paths or words and was proposed by [PERSON] [31] in 1977 in his prominent article \"the temporal logic of programs\". As for its syntax, its connectives are \(X\) (next), which is unary, and \(U\) (until), which is binary. From these, one can derive \(F\varphi\) (eventually) and \(G\varphi\) (henceforth). \(X\) (next) checks if the next event/symbol of the word matches the one noted in the expression; \(U\) (until) checks if the event/symbol is maintained until a second symbol occurs; \(F\varphi\) (eventually) checks if there is a future where the event/symbol is attainable; and \(G\varphi\) (henceforth) checks if after reaching an event/symbol it is kept. Through these connectors, it is possible to describe properties and evaluate the dynamic aspects of the system. Some works using LTL for security are noteworthy, such as the work by [PERSON] et al. [32], which presents an approach using Monte Carlo analysis through LTL formulas to identify attacks in the Needham-Schroeder authentication protocol. It is also worth mentioning [PERSON] and [PERSON] [33], who propose an approach using model learning and model checking to assess security through LTL in IoT systems. They evaluate three different systems against eleven security measures. Also, for [PERSON] et al. [34] the use of LTL comes to express the desired behavior of the system, even at design time. In their study, the authors evaluate two systems for the weakening user obligations concept proposed in the work. There is a study by [PERSON] and [PERSON] [35] on state-of-the-art analysis in the verification, quantification, and specification of software models in UML and SysML. The authors conclude that LTL is the most used approach for this purpose. Rounding out the LTL work, we have [PERSON] et al. [36] who presents a verification in runtime using LTL to detect false injection attacks in unmanned aerial vehicles (UAV). In these five studies, different ways of using LTL in security are presented, especially [PERSON] et al. [32], who, like this work, focus on authentication. Following approaches in temporal logic, **computational tree logic (CTL)** is used to describe properties in branching time and was proposed by [PERSON] and [PERSON] [37] in 1981 and subsequently complemented in another work [38] by the same authors. Its notation was inspired by the unified branching-time (UB) [39] language. In this type of approach, each node of the tree presents a number of possible futures [40] that can have their properties expressed through the operators \(E\) (existential) and \(A\) (universal).