## 2 Materials and Methods
### Background and Related Work
#### 2.1.2 Threat Model  
This section describes the MFA_R threat-modeling process as the basis for creating the formally analyzed security requirements. Through a well-documented process, attack surfaces, threats, quantification through DREAD, classification with STRIDE, and prioritization with CVSS were considered. Accordingly, only after this further analysis was the security requirements for this project listed. The analysis of the MFA_R vulnerabilities (Figure 1) took place in three steps: (1) the definition of the attack surface, (2) threat modeling, and (3) countermeasures. This approach was chosen for better comprehensiveness in the analysis of threats, and with this adoption, it now encompasses classification, severity assessment, and risk assessment. As a result, the priority of approach and the priority of resource utilization can be chosen in threats with greater impact. In this case, the evaluation and proof of mitigation of such threats is demonstrated in our authentication mechanism. \begin{table}
\begin{tabular}{c c c c} \hline \hline \# & **Articles** & **Application** & **Year** \\ \hline \hline \multicolumn{4}{c}{LTL} \\ \hline p01 & [PERSON] et al. [36] & UAV & 2020 \\ p02 & [PERSON] [33] & IoT/11 measurements & 2020 \\ p03 & [PERSON] et al [34] & Weakening user obligation & 2020 \\ p04 & [PERSON] [35] & UML e SysML & 2020 \\ p05 & [PERSON] et al [32] & Edhan-Schoroeder & 2004 \\ \hline \multicolumn{4}{c}{CTL} \\ \hline p06 & [PERSON] et al. [42] & Multi Tenant FPGA/cloud & 2021 \\ p07 & [PERSON] et al. [43] & Z-Wave & 2021 \\ p08 & [PERSON] et al. [44] & On-the-fly checking & 2014 \\ p09 & [PERSON] et al. [41] & Zero-knowledge & 2012 \\ p10 & [PERSON] et al. [45] & Authentication/Fiat-Shamir & 2021 \\ \hline \multicolumn{4}{c}{TCTL} \\ \hline p11 & [PERSON] et al. [50] & Smart contracts & 2021 \\ p12 & [PERSON] [47] & Security policies & 2020 \\ p13 & [PERSON] et al. [49] & Autonomous agents & 2020 \\ p14 & [PERSON] et al. [51] & Robotic mission plan & 2020 \\ p15 & [PERSON] [52] & Microservices & 2020 \\ p16 & [PERSON] et al. [48] & ICCP & 2013 \\ \hline \multicolumn{4}{c}{MTL} \\ \hline p17 & [PERSON] et al [58] & Opacity & 2021 \\ p18 & [PERSON] et al. [53] & Apps IoT & 2021 \\ p19 & [PERSON] et al. [59] & Apps IoT & 2021 \\ p20 & [PERSON] [56] & IDS & 2013 \\ \hline \multicolumn{4}{c}{\(\rightarrow\)} & This work & MFA\_R (TM, components, \\ \multicolumn{4}{c}{TA, STM, and TCTL)} \\ \hline \hline \end{tabular}
\end{table} 
Table 1: Works that correlate security and temporal logic—the works are organized and presented by a temporal logic approach. The works are sorted in descending order according to the year of publication. However, it is observed that in our modeling, the category of external actors (device) was not addressed. This scoping is focused on analyzing MFA_R threats only. Consequently, the category of external actors will not participate in this modeling. As a result, a threat model (TM) was obtained that focused more on the mechanism design and on some threats mitigated by design-time solutions, for which formal verification was performed. This analysis starts with the definition of attack surface. The attack surface can be defined as potentially exploitable vulnerabilities in the solution's artifact set. Thus, the definition of the attack surface (1) of this project can be seen in Table 2, which presents the correlation between the vulnerabilities and the analyzed attack surface. Even though such vulnerabilities can involve both hardware and software, this work is limited to the software components existing in the modeling and its relationship with data transmission technologies. Additionally, in this attack surface modeling (Table 2) is grouped into three different categories: external actors, services, and data link. The category of external actors consists of the device that communicates with the MFA_R, which appears but is not detailed in the text. The category of services includes RegServ, AuthServ, and DataServ. Finally, the HTTPS and LPWAN protocols are in the link category.