# SLMAS: A Secure and Light Weight Mutual Authentication Scheme for the Smart Wheelchair
## 4 Security Evaluation of the Proposed Methodology
### Automated Security Analysis Performed Formally with the AVISPA Tool  
AVISPA virtual environment program from [48] is used in this section to formally verify the suggested technique and test its resistance to RA and MITM attacks. The following are the AVISPA simulation phases: (1) The role framework for the role-oriented execution of the protocol processes in a high-level language is provided by the HLPSL (high-level protocol specification language), after which it is interpreted into intermediate format (IF) by its converter HLPSL2 IF. (2) The security check is subsequently carried out by the OF (output format) utilizing the translated IF.  
The role specifications for the sensor node (\(SN\)), server (\(S\)), trusted authority (\(TA\)), goal, environment, and session are depicted in Figure 3 and 4, accordingly. The AVISPA results, as depicted in Figure 5a,b, demonstrate the presented architecture's resilience against RA and MITM attacks. While the CL-AtSe back end analyzed 244 states in under 0.51 s, the OFMC back end evaluated 4816 nodes with a search time of 58.27 s and a heap depth of 9.  
\begin{table}
\begin{tabular}{l l} \hline \hline
**Sensor Node (SN)** & **Trusted Authority (\(TA\))** & **Server (S\({}_{\star}\))** \\ \hline Select \(RND\)s and \(T_{SN}\) & \(|TC-T_{SN}\leq\delta T|\) and check if \(PR_{I_{D_{R}}}\) exists in DB. \\  & IF TRUE: \\  & \(|SN_{I_{D_{R}}},X_{a}|=DEC_{\text{MSK}}|SN_{I_{D_{R}}},X_{a}|\) \\  & \(SEY_{TA_{R}}=H(K|_{\text{IM}}|MS|)\) \\  & \(V_{temp}=H(SEY_{TA_{R}}|S|SN_{I_{D_{R}}})\) \\  & \(RND_{S}=RND_{S}\oplus V_{temp}\) \\  & \(AUTH_{s}=H(RND_{S}||V_{temp}||T_{SN})\) \\  & IF TRUE: \\  & \(|S_{I_{D_{R}}},X_{\text{J}}|=DEC_{\text{MSK}}|X_{a}|\) \\  & \(SEY_{TA_{R}}=H(|MS|)\)\(|V_{temp}|=H(SEY_{TA_{R}}|S_{I_{R}})\) \\  & Pick \(RND_{A},RND_{S}\) and \(T_{A}\) \\  & \(AUTH_{TA}=H(RND_{A}||V_{temp}||T_{TA})\) \\  & \(RND_{I_{D}}=RND_{S}||V_{temp}\) \\  & \(Z_{TA_{R}}=H(KSEY_{TA_{R}}||RND_{S}||RND_{S}||Y_{TA_{R}}||MS\oplus V_{temp3}\) \\  & \(\frac{MSQ_{2}=(NR_{I_{D}},NRD_{S}||V_{temp}||MS)}{(TA-S_{k})}\) \\  & \(|TC-T_{TA}\leq\delta T|\) and \\  & \(F TRUE:\) \\  & \(V_{temp}=H(KSEY_{TA_{R}}||S_{I_{D_{R}}}||T_{TA})\) \\  & \(RDD_{A}=RND_{A}^{\prime}\oplus V_{temp4}\) \\  & \(AUTH_{TA}\triangleq H(RND_{A}||V_{temp}||T_{TA})\) \\  & IF TRUE: \\  & Pick \(RND_{G},RND_{S}\) and \(T_{a}\) \\  & \(SK_{\star\star}=H(RND_{G}||Z_{TA_{R}}\oplus V_{temp3}||T_{a})\) \\  & \(RND_{S}=RND_{S}\oplus V_{temp3}\) \\  & \(RND_{S}^{\prime}=RND_{S}\oplus V_{temp3}\) \\  & \(AUTH_{s}=H(RND_{S}||V_{temp}||T_{TA})\) \\  & \(\stackrel{{ MSQ_{2}=(SN_{I_{D}},RND_{S}||V_{temp}||T_{TA})}}{{ \leftarrow}}\) \\  & \(|TC-T_{SA}\leq\delta T|\) \\  & IF TRUE: \\  & Pick \(T_{TA}^{TA}\) \\  & \(RND_{S}=RND_{S}^{\prime}\oplus V_{temp3}\) \\  & \(RND_{S}=RND_{S}^{\prime}\oplus V_{temp3}\) \\  & \(AUTH_{s}\triangleq H(RND_{S}||V_{temp}||T_{s})\) \\  & \(Z_{TA_{R}}=Z_{TA_{R}}\oplus V_{temp}\) \\  & \(X_{TA_{R}}=H(RND_{S}||V_{temp}||T_{TA})\) \\  & \(KND_{S}^{\prime}=H(RND_{S}||Z_{TA_{R}}\oplus V_{temp3})\) \\  & \(\stackrel{{ MSQ_{2}=(SN_{I_{D}},RND_{S}^{\prime}\oplus V_{temp3})}}{{ \leftarrow}}\) \\  & \((TCA-T_{SA}\leq\delta T|\) \\  & IF TRUE: \\  & \(KND_{S}=RND_{S}^{\prime}\oplus V_{temp3}\) \\  & \(RND_{S}=RND_{S}^{\prime}\oplus V_{temp3}\) \\  & \(\stackrel{{ MSQ_{2}=(SN_{I_{D}},RND_{S}^{\prime}\oplus V_{temp3})}}{{ \leftarrow}}\) \\  & \(\stackrel{{ MSQ_{2}=(SN_{I_{D}},RND_{S}^{\prime}\oplus V_{temp3})}}{{ \leftarrow}}\) \\  & \((TCA-T_{SA}\leq\delta T|\) \\  & IF TRUE: \\  & \(AUITH_{TA}\triangleq\frac{1}{2}H(RND_{S}||V_{temp}||T_{TA}^{TA})\) \\  & \(RND_{S}=RND_{S}^{\prime}\oplus V_{temp3}\) \\  & \(Z_{TA_{R}}=Z_{TA_{R}}\oplus V_{temp}\) \\  & \(SK_{\star}=H(RND_{S}||Z_{TA_{R}}\oplus T_{s})\) \\ \hline \hline \end{tabular}
\end{table}
Table 5: Authentication and key-agreement process.