## 6 Security Analysis
### Formal Proof Under BAN Logic
#### 6.2.5 BAN Logic Proof  
The BAN logic proof of our scheme is conducted below:  
**Step 1:**: \(S_{1}\) can be derived from \(M_{1}\):  
\[S_{1}:CS\lhd\{SID_{j},n_{i1}\}_{UI_{i}}\]  
**Step 2:**: By employing the MMR with \(S_{1}\) and \(A_{6}\), \(S_{2}\) can be derived:  
\[S_{2}:CS\mid\equiv U_{t_{i}}\mid\sim(SID_{j},n_{i1})\]
**Step 3:**: By employing the FR with \(S_{2}\) and \(A_{1}\), \(S_{3}\) can be derived:  
\[S_{3}:CS\mid\equiv\#(SID_{j},n_{i1})\]
**Step 4:**: By employing the NVR with \(S_{2}\) and \(S_{3}\), \(S_{4}\) can be derived:  
\[S_{4}:CS\mid\equiv U_{t_{i}}\mid\equiv(SID_{j},n_{i1})\]
**Step 5:**: \(S_{5}\) can be obtained from \(M_{2}\):  
\[S_{5}:IoT_{SL_{j}}\lhd\{n_{i1},n_{i2}\}_{S_{1j}}\]
**Step 6:**: \(S_{6}\) can be derived by applying the MMR to \(S_{5}\) and \(A_{7}\):  
\[S_{6}:IoT_{SL_{j}}\mid\equiv CS\mid\sim(n_{i1},n_{i2})\]
**Step 7:**: By employing the FR with \(S_{6}\) and \(A_{2}\), \(S_{7}\) can be derived:  
\[S_{7}:IoT_{SL_{j}}\mid\equiv\#(n_{i1},n_{i2})\]
**Step 8:**: By employing the NVR with \(S_{6}\) and \(S_{7}\), \(S_{8}\) can be derived:  
\[S_{8}:IoT_{SL_{j}}\mid\equiv CS\mid\equiv(n_{i1},n_{i2})\]
**Step 9:**: \(S_{9}\) can be obtained from \(M_{3}\):  
\[S_{9}:CS\lhd\{n_{i3}\}_{S_{1j}}\]
**Step 10:**: By employing the MMR with \(S_{9}\) and \(A_{8}\), \(S_{10}\) can be derived:  
\[S_{10}:CS\mid\equiv IoT_{SL_{j}}\mid\sim(n_{i3})\]
**Step 11:**: By employing the FR with \(S_{10}\) and \(A_{3}\), \(S_{11}\) can be derived:  
\[S_{11}:CS\mid\equiv\#(n_{i3})\]
**Step 12:**: By employing the NVR with \(S_{10}\) and \(S_{11}\), \(S_{12}\) can be derived:  
\[S_{12}:CS\mid\equiv IoT_{SL_{j}}\mid\equiv(n_{i3})\]
**Step 13:**: \(S_{13}\) and \(S_{14}\) can be derived from \(S_{8}\) and \(S_{12}\). \(IoT_{SL_{j}}\) and \(CS\) can calculate a session key \(SK=h(UID_{i}||SI_{j})\oplus h(n_{i1}||n_{i2}||n_{i3})\):  
\[S_{13}:CS\mid\equiv IoT_{SL_{j}}\mid\equiv(IoT_{SL_{j}}\lhd^{SK}CS) \qquad(\text{Goal 8})\] \[S_{14}:IoT_{SL_{j}}\mid\equiv CS\mid\equiv(IoT_{SL_{j}}\lhd^{SK}CS) \qquad(\text{Goal 6})\]  
**Step 14:**: \(S_{15}\) and \(S_{16}\) can be derived by employing the JR with \(S_{13}\) and \(A_{12}\), and \(S_{14}\) and \(A_{11}\), respectively:  
\[S_{15}:CS \equiv(IoT_{S_{Lj}}\xleftrightarrow{SK}CS)\] (Goal 7) \[S_{16}:IoT_{S_{Lj}} \equiv(IoT_{S_{Lj}}\xleftrightarrow{SK}CS)\] (Goal 5)
**Step 15:**: \(S_{17}\) can be derived from \(M_{4}\):  
\[S_{17}:U_{r_{i}}\lhd\{n_{i2},n_{i3},UID_{i}^{new},h(UID_{i}||S_{lj})\}_{UI_{i}}\]
**Step 16:**: By employing the MMR with \(S_{17}\) and \(A_{5}\), \(S_{18}\) can be derived:  
\[S_{18}:U_{r_{i}}\mid\equiv CS\mid\sim(n_{i2},n_{i3},UID_{i}^{new},h(UID_{i}|| S_{lj}))\]
**Step 17:**: By employing the FR with \(S_{18}\) and \(A_{4}\), \(S_{19}\) can be derived:  
\[S_{19}:U_{r_{i}}\mid\equiv\#(n_{i2},n_{i3},UID_{i}^{new},h(UID_{i}||S_{lj}))\]
**Step 18:**: By employing the NVR with \(S_{18}\) and \(S_{19}\), \(S_{20}\) can be derived:  
\[S_{20}:U_{r_{i}}\mid\equiv CS\mid\equiv(n_{i2},n_{i3},UID_{i}^{new},h(UID_{i}|| S_{lj}))\]
**Step 19:**: \(S_{21}\) and \(S_{22}\) can be derived from \(S_{4}\) and \(S_{18}\). \(U_{r_{i}}\) and \(CS\) can calculate the session key \(SK=h(UID_{i}||S_{lj})\oplus h(n_{i1}||n_{i2}||n_{i3})\):  
\[S_{21}:U_{r_{i}}\mid\equiv CS\mid\equiv(U_{r_{i}}\xleftrightarrow{SK}CS)\] (Goal 2) \[S_{22}:CS\mid\equiv U_{r_{i}}\mid\equiv(U_{r_{i}}\xleftrightarrow{SK}CS)\] (Goal 4)
**Step 20:**: \(S_{23}\) and \(S_{24}\) can be derived by employing the JR with \(S_{21}\) and \(A_{9}\), and \(S_{22}\) and \(A_{10}\), respectively:  
\[S_{23}:U_{r_{i}}\mid\equiv(U_{r_{i}}\xleftrightarrow{SK}CS)\] (Goal 1) \[S_{24}:CS\mid\equiv(U_{r_{i}}\xleftrightarrow{SK}CS)\] (Goal 3)