# Threat Modelling and Beyond-Novel Approaches to Cyber Secure the Smart Energy System
## 7 Risk Analysis Using Formal Methods
### UC2: Smart Home and Smart Meter Hijacking  
#### 7.3.1 Probabilistic Model Generation  
The UC2 configuration is presented in Figure 9. Similarly to the previous use case, the system is modeled in the PRISM model checker as an MDP process.  
\begin{table}
\begin{tabular}{l c c c c} \hline \hline
**Attack** & \(cost=1\) & \(cost=2\) & \(cost=3\) & \(cost=4\) & \(cost=5\) \\ \hline
1.1 Hijack heating & 0.0000 & 0.3481 & 0.4908 & 0.5473 & 0.5473 \\
1.2 Hijack HVAC & 0.0000 & 0.0000 & 0.2054 & 0.3709 & 0.4365 \\ \hline \hline \end{tabular}
\end{table}
Table 10: Smart home and HVAC hijack use case risk exposure scores.  
\begin{table}
\begin{tabular}{l c c} \hline \hline
**Vulnerability** & **Associated Threat** & **Threat Id** & **Expl. Prob.** \\ \hline ST–G1 link & Link jammed: denied transmission & 1028 & 0.65 \\ HVAC (actuation A1/A2) & Tailored context/incorrect actuation & 1013 & 0.59 \\ G (gain control) & Tailored context/incorrect reading & 1111 & 0.59 \\ HEMS (actuation A1/A2) & Tailored context/incorrect actuation & 1005 & 0.57 \\ \hline \hline \end{tabular}
\end{table}
Table 8: Vulnerabilities, exploitation probabilities and associated threats for UC1.  
\begin{table}
\begin{tabular}{l c c} \hline \hline
**Attack** & **Impact** & **Attack Properties** \\ \hline Attack scenario 1.1: & High & Attack takes control over heating, high or optimal temperature is \\ Hijack heating & & detected, heating is switched on, resulting in damage \\ Attack scenario 1.2: & High & Attack takes control over HVAC, optimal temperature is detected, \\ Hijack HVAC & & both cooling and heating are switched on, resulting in damage and high power consumption \\ \hline \hline \end{tabular}
\end{table}
Table 9: Modeled attacks, their impact and properties for UC1.  
The following service policies, reflecting the system response, permeate through the system model:  
* _SM1/2 policy:_ Smart meters SM1 and SM2 measure the power consumption and notify IHD in near real time, and MDMS periodically (every 15 min);
* _MDMS policy:_ The MDMS is periodically updated, and checks the consistency of the consumption/billing in the neighborhood;
* _Service Cloud policy:_ The MDMS is periodically polled with the credentials provided by customer;
* _User policy:_ The service cloud periodically notifies the user about the power consumption;
* _Maintenance policy:_ The service cloud notifies responsible actors in case of a consumption inconsistency.  
Similarly to the first use case, it is assumed that an attacker actively attacks the system, and that he has skills and means to perform a certain attack by exploiting existing vulnerabilities.  
Figure 8: Smart home and HVAC hijack use case results.  
Figure 9: Smart home and smart meter hijacking use-case architecture.  
The minimum set of vulnerabilities that can be exploited in order to perform a described attack, identified by the threat modeling and attack modeling processes, is presented in Table 11. The system is modeled with the assumptions similar to UC1 - the attacker identified vulnerabilities, and the exploitation of one or more vulnerabilities is necessary in order to successfully carry out an attack. Exploitation probabilities are defined for all listed vulnerabilities, and presented in Table 11.