## 2 Materials and Methods
### Theory of Threat Modeling
#### 2.4.7 Formal Verification  
Formal proofs increase the trustworthiness of verified systems. The state-of-the-art shows various attempts to formally verify security properties. [PERSON] in [34] provides the formal security proofs of three standards that are formally verified using the proof assistant EasyCrypt. [PERSON] et al. [35] presented a method for verifying the security properties of source code embedded on smart cards, through combining functional verification at the source code level and the verification of high-level properties on a formal model built from the program and its specification. Model checking is used in [36] to develop techniques that support the development of tools to solve analysis problem instances in trust management policy. In hardware, formal verification is also needed. The work presented in [37] proposes a method to formally verify the correctness and the security properties of a network on chip (NOC) router in order to provide the proper communication functionality and to avoid NOC attacks. Detailed surveys on the use of formal verification for enhancing the security in different levels across the system stack exist in [38; 39; 40]. It is shown in the literature that formal methods and verification provide improved results in resilience against adversaries. In this work, we chose the B-method as a formal verification method to prove that the security properties of the optimized system still hold after optimization, and accordingly, that the proposed algorithm is not deteriorating the system security. Incorporating formal models into the design process results in more robust systems. In order to increase trust in the system's functionality, researchers study a wide range of modeling and verification technologies. The fundamental goal of the verification process is to investigate a model for the accuracy of functional requirements stated as formal properties. The role of formal verification is to ensure the system being designed will satisfy certain properties. Formal verification ensures the correctness of the system in early design stages and consequently improves its reliability. Verification, validation, and hazard analysis procedures on critical systems are usually carried out in separate stages of system development and by different teams of engineers. However, formal verification can be integrated with design tools to verify certain properties are satisfied at different stages and also at run-time. Theorem proving and model checking are the two most prevalent methods for automatic formal verification. The formal description can be used to guide further development activities; moreover, it can be used to verify that the requirements for the system being developed have been entirely and precisely specified. A variety of formal methods and notations available are available, such as Z notation, VDM, and B-method. Three categories can be used to classify the formal verification methods--equivalence checking, model checking, and theorem proving [41]. Equivalence checking verifies that two designs have the same apparent behaviors (e.g., an optimized design has the same observable behavior as its earlier version). Two distinct types of equivalence checking for digital systems are available according to the type of circuits either combinational or sequential. For combinational systems, the two outputs are passed into canonical representations, and if the representations are identical, the two systems are equivalent. In model checking, an automatic process is used to check if a system satisfies a known property. The model checking process starts by describing the system being verified and its required behavior formally. A formal model of the system is build as a collection of finite state machines, and the behavior is modeled as a set of properties (usually defined in terms of temporal logic formulas). Then, the properties' satisfaction levels are checked automatically by exhaustively exploring the state space of the system.