# Threat Modelling and Beyond-Novel Approaches to Cyber Secure the Smart Energy System
## 2 Related Work
### Formal Verification in Smart Grids  
The application of formal methods for the prevention of cyber attacks in the SG domain is addressed from different perspectives. These include quantitative as well as qualitative properties. On the protocol level, two relevant publications exist for this matter. [PERSON] et al. [48] addresses the performance and efficiency of Smart Grids by checking a ZigBee-based routing protocol for the communication network. The focus of this work is the functionality of the protocol. This is confirmed by the conducted verification of collision avoidance and liveness properties. On the other hand, [PERSON] et al. [49] focuses on the secure authentication key agreement in the Canetti-Krawczyk adversary model. The authors emphasize the importance of several software components for the security and privacy in the SG domain. Therefore, the authors propose a provable secure authentication key agreement scheme.  
In [PERSON] et al. [50], PRISM is used for a reliability analysis and investigation of accuracy, stability and efficiency. The analysis was committed in cases where faults were detected in the transmission line system of a Smart Grid. In addition to that, the approach is applicable to calculate failure probabilities in network components. The reliability of a G3-Power Line Communication (PLC) networks is considered by [PERSON] et al. [51]. The work puts focus on the accuracy and reliability of the information flow. For this sake, it specially emphasizes the Fault Detection, Isolation and Supply Restoration behavior. [PERSON] et al. [52] uses the model checker SPIN in order to check the wide-area backup protection system (WABPS). This is specifically designed to offer a high degree of reliability in different failure scenarios. However, due to the advanced design, the calculation of the fault tolerance proves difficult. Therefore, the authors applied SPIN to check the limits of a failure. [PERSON] [53] applies the model checker UPPAAL for verification of the Agent Aided Distance Relaying Protection Scheme. This represents a hierarchically distributed and non-intrusive concept for decreasing blackout probability. In their work, this scenario occurred due to hidden failures of distance relays in the Advanced Metering Infrastructure.  
[PERSON] et al. [54] provides a security risk management solution for the protection of Smart Grids in case of cyber attacks. The authors use probabilistic model checking to model the attacker's behavior in form of a Markov Decision Process. For this sake, they rely on the model checker PRISM. Two types of attacker behaviors are considered, namely non-persistent and persistent behaviors, as well as their effect on critical components in an SG. On the other hand, [PERSON] and [PERSON] [55] studies the effects of distributed DoS attacks on the Advanced Metering infrastructure. The authors estimate best and worst case analyses in the context of a cloud-based openflow firewall. In the aftermath, they study DoS attacks with respect to different detection probabilities of the firewall.  
Similar to our proposed work, [PERSON] et al. [56] conduct a risk analysis for Smart Water Distribution use case. The corresponding authors focus on two main scenarios, namely water contamination and water tank overflow. Therefore, risk exposure scores are calculated for both scenarios. Additionally, these scores provide recommendations for system configurations to improve safety and security.