## 2 Materials and Methods
### Authentication Mechanism Explained, Components View  
For a better understanding of formal verification and how it took place in MFA_R, this section provides an overview of the components involved in its processes. Since each component has its thread and memory separate from each other, it is very important to understand how these are organized and communicated. Although the multi-factor provides more security for authentication [85], it also involves greater complexity, and this can be seen in the various components that collaborate to enable its operation (Figure 3) in our platform. More specifically, the restricted device firmware communicates with three components on the server side: the registry service (**RegServ**), the authentication service (**AuthServ**), and the data publishing (**DataServ**). Server-side components collaborate with the authentication inspector (**AuthInspector**) and keep the data in the device data log artifact (**device_data**). **RegServ** is responsible for registering devices in the authentication mechanism. Registration needs to be performed only once, preferably before the equipment goes into the field, using a robust network (i.e., Wireless Fidelity--WiFi) and through a secure interface (such as HTTPS). This procedure reduces the number of data transferred by the link LPWAN (it is important to note that, if the device is configured in compatibility mode, its login and password are not generated but informed at the time of registration. The registration of legacy devices occurs through a different interface from the others), which is less secure and has a lower transmission speed. Thus, when registering, a device sends its data to the gateway, which registers it in the device's data artifact (**device_data**). After registration, the login and password for the device are generated by RegServ and sent to the device in the registration confirmation reply message. Also, the confirmation response sends the timestamp and the registration data. These will be used as data sources by the query API in device authentication later on. **AuthServ** is the component responsible for device authentication, queries, and enforcement. Initially, this component is responsible for authenticating the first factor and identifying the device type--in other words, if the device is incompatibility mode (a legacy device still in use) or if the device implements authentication with MFA_R. Thereafter, one of two paths can be taken: compatibility mode or normal authentication flow. If it is in **compatibility mode**, the data published by the device will be available for consumption. All devices in compatibility mode have their published data with a reputation of zero. This behavior is due to the mechanism identifying them with great potential for data falsification. However, the consumption of this data can occur if a system does not consider this fact as problematic, or even at a time of transition in the incorporation of this technology in new sensors. If the device is not in compatibility mode (**normal stream mode**), _AuthServ_ will generate a query using the query API and send it as a second factor. Thus, the requesting device, which has the mechanism's query API implemented, will resolve the sent query. When this happens, the device will authenticate itself with the second factor, going to the AUTH2 level. At this moment, **AuthServ** informs **AuthInspector** that the device is authenticated in AUTH2 and assigns it a score (reputation). The query works as a more robust challenge-response factor as it only passes a modified slice of the response. As a result, attacks are mitigated that statistically analyze the data sent over the network. Remaining under the responsibility of **AuthServ**, there is the enforcement process (Algorithm 8).