# Lightweight and Security-Enhanced Key Agreement Protocol Using PUF for IoD Environments
## 6 Proposed Protocol
### Drone Revocation Phase
#### 7.1.6 BAN Logic Proof  
Below is the BAN logic proof for the proposed protocol:  
**Step 1:**: \(GCS\) receives message \(M_{1}\).  
\[\begin{array}{ll}\mathit{S}_{1}:GCS\lhd(V_{M},r_{3})_{h(HID_{M}|K_{M})}\\ \mathit{\textbf{Step 2:}}&\text{Applying }\mathit{S}_{1}\text{ and }\mathit{A}_{11}\text{ to the MMR yields }\mathit{S}_{2}.\\ \mathit{S}_{2}:GCS|\equiv MD_{i}|\sim(V_{M},r_{3})\\ \mathit{\textbf{Step 3:}}&\text{Applying }\mathit{S}_{2}\text{ and }\mathit{A}_{1}\text{ to the FR yields }\mathit{S}_{3}.\\ \mathit{S}_{3}:GCS|\equiv\#(V_{M},r_{3})\\ \mathit{\textbf{Step 4:}}&\text{Applying }\mathit{S}_{2}\text{ and }\mathit{S}_{3}\text{ to the NVR yields }\mathit{S}_{4}.\\ \mathit{S}_{4}:GCS|\equiv MD_{i}|\equiv(V_{M},r_{3})\\ \mathit{\textbf{Step 5:}}& D_{j}\text{ receives message }M_{2}.\\ \end{array}\]\[S_{5}:D_{j}\trianglelefteq(V_{G},r_{3},r_{4},h(HID_{M}\parallel K_{M}))_{h(PID_{D }\parallel K_{D})}\]  
**Step 6:**: Applying \(S_{5}\) and \(A_{9}\) to the MMR yields \(S_{6}\).  
\[S_{6}:D_{j}|\equiv GCS|\sim(V_{G},r_{3},r_{4},h(HID_{M}\parallel K_{M}))\]
**Step 7:**: Applying \(S_{6}\) and \(A_{3}\) to the FR yields \(S_{7}\).  
\[S_{7}:D_{j}|\equiv\#(V_{G},r_{3},r_{4},h(HID_{M}\parallel K_{M}))\]
**Step 8:**: Applying \(S_{6}\) and \(S_{7}\) to the NVR yields \(S_{8}\).  
\[S_{8}:D_{j}|\equiv GCS|\equiv(V_{G},r_{3},r_{4},h(HID_{M}\parallel K_{M}))\]
**Step 9:**: \(GCS\) receives message \(M_{3}\).  
\[S_{9}:GCS\trianglelefteq(r_{5},R_{j},Auth_{D})_{h(HID_{M}\parallel K_{M}) \parallel h(PID_{D}\parallel K_{D})}\]
**Step 10:**: Applying \(S_{9}\) and \(A_{12}\) to the MMR yields \(S_{10}\).  
\[S_{10}:GCS|\equiv D_{j}|\sim(r_{5},R_{j},Auth_{D})\]
**Step 11:**: Applying \(S_{10}\) and \(A_{2}\) to the FR yields \(S_{11}\).  
\[S_{11}:GCS|\equiv\#(r_{5},R_{j},Auth_{D})\]
**Step 12:**: Applying \(S_{10}\) and \(S_{11}\) to the NVR yields \(S_{12}\).  
\[S_{12}:GCS|\equiv D_{j}|\equiv(r_{5},R_{j},Auth_{D})\]
**Step 13:**: \(MD_{i}\) receives message \(M_{4}\).  
\[S_{13}:MD_{i}\trianglelefteq(r_{4},r_{5},R_{j},h(PID_{D}\parallel K_{D}),Auth _{GCS})_{h(HID_{M}\parallel K_{M})}\]
**Step 14:**: Applying \(S_{13}\) and \(A_{7}\) to the MMR yields \(S_{14}\).  
\[S_{14}:MD_{i}|\equiv GCS|\sim(r_{4},r_{5},R_{j},h(PID_{D}\parallel K_{D}),Auth _{GCS})\]
**Step 15:**: Applying \(S_{14}\) and \(A_{4}\) to the FR, we can obtain \(S_{15}\).  
\[S_{15}:MD_{i}|\equiv\#(r_{4},r_{5},R_{j},h(PID_{D}\parallel K_{D}),Auth_{GCS})\]
**Step 16:**: Applying \(S_{14}\) and \(S_{15}\) to the NVR yields \(S_{16}\).  
\[S_{16}:MD_{i}|\equiv GCS|\equiv(r_{4},r_{5},R_{j},h(PID_{D}\parallel K_{D}),Auth _{GCS})\]
**Step 17:**: From \(S_{12}\), \(S_{16}\), \(S_{4}\), and \(S_{8}\), \(MD_{i}\) and \(D_{j}\) can compute the session key as \(SK=h(h(PID_{D}\parallel K_{D}\parallel R_{j})\parallel h(HID_{M}\parallel K_{ M})\parallel r_{3}\parallel r_{4}\parallel r_{5})\).  
\[S_{17}:MD_{i}|\equiv D_{j}|\equiv(MD_{i}\stackrel{{ SK}}{{ \longleftrightarrow}}D_{j})\] **(Goal 2)** \[S_{18}:D_{j}|\equiv MD_{i}|\equiv(MD_{i}\stackrel{{ SK}}{{ \longleftrightarrow}}D_{j})\] **(Goal 4)**
**Step 18:**: The jurisdiction rule can be applied to \(S_{17}\) and \(S_{18}\) using \(A_{5}\) and \(A_{6}\), respectively.  
\[S_{19}:MD_{i}|\equiv(MD_{i}\stackrel{{ SK}}{{ \longleftrightarrow}}D_{j})\] **(Goal 1)** \[S_{20}:D_{j}|\equiv(MD_{i}\stackrel{{ SK}}{{ \longleftrightarrow}}D_{j})\] **(Goal 3)**  
Thus, mutual authentication between \(MD_{i}\) and \(D_{j}\) is successfully achieved.