# Energy Efficient Dynamic Symmetric Key Based Protocol for Secure Traffic Exchanges in Smart Homes
## 4 Security Analysis
### Formal Security Analysis
Based on \(\text{IME}_{1}\), the seeing rule (SR) in \(\text{BLN}_{4}\) is deployed to yield BAN Logic 1 (\(\text{BLP}_{1}\)):  
\(\text{BLP}_{1}\): TA\(\bullet\)P\({}_{U}\), \(\mathbb{Q}_{U}\): \(<ID_{U}\), \(\text{ID}_{M}\), \(\mathbb{N}_{1}\)\(>\)\(\uppsi\), \(\mathbb{R}_{U}\)\(<\)\(\mathbb{N}_{4}\)\(>\)\(\text{ID}_{M}\), \(\mathbb{T}_{1}\)  
Hinged on \(\text{ITA}1\), MMR and is applied to \(\text{BLP}_{1}\) to yield \(\text{BLP}_{2}\):  
\(\text{BLP}_{2}\): TA\(|\equiv\text{SHO}|\sim\)\(\mathbb{N}_{4}\)  
The application of FPR in \(\text{BLP}_{2}\) results in \(\text{BLP}_{3}\):  
\(\text{BLP}_{3}\): TA\(|\equiv\text{SHO}|\equiv\)\(\mathbb{N}_{4}\)  
Based on \(\text{BLP}_{3}\), JR is applied to obtain \(\text{BLP}_{4}\):  
\(\text{BLP}_{4}\): TA\(|\equiv\)\(\mathbb{N}_{4}\)  
From \(\text{ITA}_{2}\) and \(\text{ITA}_{5}\), JR is applied on \(\text{BLP}_{4}\) yields \(\text{BLP}_{5}\):  
\(\text{BLP}_{5}\): TA\(|\equiv\text{SHO}\overset{\mathbb{Q}_{U}}{\leftrightarrow}\text{TA}\)  
On the other hand, using NVR on \(\text{BLP}_{5}\), \(\text{BLP}_{6}\) is obtained:  
\(\text{BLP}_{6}\): TA\(|\equiv\text{SHO}|\equiv\text{SHO}\overset{\mathbb{Q}_{U}}{\leftrightarrow}\text{TA}\)  
Based on \(\text{IME}_{2}\) and \(\text{ITA}_{4}\), SR is applied to yield \(\text{BLP}_{7}\):  
\(\text{BLP}_{7}\): SHD\(\triangle\)P\({}_{5}\),T\({}_{3}\)  
The application of MMR on \(\text{BLP}_{7}\) results in\(\text{BLP}_{8}\):  
\(\text{BLP}_{8}\): SHD\(|\equiv\) TA\(|\sim\)\(\mathbb{Q}_{U}\)  
Based on \(\text{BLP}_{8}\), the FPR is deployed to yield \(\text{BLP}_{9}\):  
\(\text{BLP}_{9}\): SHD\(|\equiv\) TA\(|\equiv\)\(\mathbb{Q}_{U}\)  
Next, using JR on \(\text{BLP}_{9}\) results in \(\text{BLP}_{10}\):  
\(\text{BLP}_{10}\): SHD\(|\equiv\)\(\mathbb{Q}_{U}\)  
Applying JR on \(\text{BLP}_{10}\), \(\text{BLP}_{11}\) is obtained:  
\(\text{BLP}_{11}\): SHD\(|\equiv\) TA\(\overset{\mathbb{ZS}}{\leftrightarrow}\)SHD  
However, the application NVR on \(\text{BLP}_{11}\) results in \(\text{BLP}_{12}\):  
\(\text{BLP}_{12}\): SHD\(|\equiv\) TA\(|\equiv\) TA\(\overset{\mathbb{ZS}}{\leftrightarrow}\)SHD  
Conversely, based on \(\text{IME}_{3}\), SR is deployed to yield \(\text{BLP}_{13}\):  
\(\text{BLP}_{13}\): TA\(\triangle\)P\({}_{\text{T}}\),T\({}_{5}\)  
Afterwards based on \(\text{ITA}_{3}\), MMR is deployed in \(\text{BLP}_{13}\) to obtain \(\text{BLP}_{14}\):  
\(\text{BLP}_{14}\): TA\(|\equiv\) SHD\(|\sim\)P\({}_{\text{T}}\)  
According to \(\text{BLP}_{14}\) and \(\text{ITA}_{6}\), FPR is applied to produce \(\text{BLP}_{15}\):  
\(\text{BLP}_{15}\): TA\(|\equiv\) SHD\(|\equiv\)P\({}_{\text{T}}\)  
Using JR on \(\text{BLP}_{15}\), \(\text{BLP}_{16}\) is obtained:  
\(\text{BLP}_{16}\): TA\(|\equiv\)P\({}_{\text{T}}\)  
On the other hand, applying JR on \(\text{BLP}_{16}\) yields \(\text{BLP}_{17}\):  
\(\text{BLP}_{17}\): TA\(|\equiv\) SHD\(\overset{\mathbb{ZS}}{\leftrightarrow}\)TA  
The application of NVR on \(\text{BLP}_{17}\) yields \(\text{BLP}_{18}\):  
\(\text{BLP}_{18}\): TA\(|\equiv\) SHD\(|\equiv\) SHD\(\overset{\mathbb{ZS}}{\leftrightarrow}\)TA  
Based on \(\text{IME}_{4}\), the SR is applied to obtain \(\text{BLP}_{19}\):  
\(\text{BLP}_{19}\): SHO\(\triangle B\):\(<\)\(\mathbb{Q}_{U}\)New\(>\)\(\text{ID}_{M}\), \(\mathbb{P}_{\text{TA}}\),T\({}_{6}\)Using MMR on \(\mathrm{BLP}_{19}\) results in \(\mathrm{BLP}_{20}\):  
\(\mathrm{BLP}_{20}\): SHO\(|\equiv\) TA\(|\sim\)Q\({}_{\mathrm{U}}\)  
According to \(\mathrm{BLP}_{20}\), FPR is applied to get \(\mathrm{BLP}_{21}\):  
\(\mathrm{BLP}_{21}\): SHO\(|\equiv\) TA\(|\equiv\)Q\({}_{\mathrm{U}}\)  
However, the deployment of JR on \(\mathrm{BLP}_{21}\) yields \(\mathrm{BLP}_{22}\):  
\(\mathrm{BLP}_{22}\): SHO\(|\equiv\)Q\({}_{\mathrm{U}}\)  
Based on \(\mathrm{BLP}_{22}\) and \(\mathrm{ITA}_{7}\), JR is applied to obtain \(\mathrm{BLP}_{23}\):  
\(\mathrm{BLP}_{23}\): SHO\(|\equiv\) TA\(|\)SHO  
On the other hand, the application of NVR on \(\mathrm{BLP}_{23}\) yields \(\mathrm{BLP}_{24}\):  
\(\mathrm{BLP}_{24}\): SHO\(|\equiv\) TA\(|\equiv\) TA\(|\)SHO  
It has been shown through \(\mathrm{BLP}_{1}\) to \(\mathrm{BLP}_{24}\) that SHO, TA, and SHD execute mutual authentication amongst themselves and negotiate the common session key.