# Mdpj _sciences_
### Contributions  
This paper presents a comprehensive and multi-faceted security analysis of the DMRN Protocol, which has been engineered to achieve both perfect forward secrecy and support for PQC in 6G Authentication and Key Agreement. Our primary contributions are outlined below:  
* We conducted a comprehensive survey of nine existing protocols, including the DMRN Protocol, performing a comparative analysis based on six key criteria: mutual authentication, secure key exchange, SUPI protection, and other relevant factors. * A rigorous security analysis of the DMRN Protocol was performed using two distinct formal verification tools: SVO logic and ProVerif. This multi-tool approach provides a more comprehensive and robust evaluation of the protocol's security properties. \begin{table}
\begin{tabular}{c c c c c c} \hline \hline
**Protocol** & **MA** & **KE** & **SUPI** & **PFS** & **DmS** & **QS** \\ \hline
5G-AKA’ & \(\bigcirc\) & \(\bigcirc\) & \(\bigcirc\) & \(\times\) & \(\times\) & \(\times\) \\ SUCI-AKA & \(\bigcirc\) & \(\bigcirc\) & \(\bigcirc\) & \(\times\) & \(\bigcirc\) & \(\times\) \\
5G-IPAKA & \(\bigcirc\) & \(\bigcirc\) & \(\bigcirc\) & \(\times\) & \(\times\) & \(\times\) \\
5G-AKA-LCCO & \(\bigcirc\) & \(\bigcirc\) & \(\times\) & \(\bigcirc\) & \(\times\) \\
5G-AKA-FS & \(\bigcirc\) & \(\bigcirc\) & \(\bigcirc\) & \(\bigcirc\) & \(\times\) \\ WirelessPQCSim & * & * & \(\bigcirc\) & * & * & \(\bigcirc\) \\ DMRN & \(\times\) & \(\times\) & \(\bigcirc\) & \(\bigcirc\) & \(\times\) & \(\bigcirc\) \\ EAP-AKA’-FS & \(\bigcirc\) & \(\bigcirc\) & \(\bigcirc\) & \(\bigcirc\) & \(\bigcirc\) & \(\bigcirc\) \\ EAP-AKA’-PQC & \(\bigcirc\) & \(\bigcirc\) & \(\bigcirc\) & \(\bigcirc\) & \(\bigcirc\) & \(\bigcirc\) \\ \hline \hline \end{tabular}  
* MA: Mutual Authentication; KE: Key Exchange; SUPI: SUPI Concealment; PFS: Perfect Forward Secrecy; DmS: Defense against malicious SNs; QS: Quantum-Safe; \(\bigcirc\): Satisfied; \(\times\): Not satisfied; -: Unable to check.  
\end{table} 
Table 1: Comparison in terms of security requirements with related works. * In the ProVerif verification, we defined four scenarios, each of which was thoroughly and precisely explored to assess potential attack vectors. * For the DMRN Protocol, we compared and analyzed the results from both SVO logic and ProVerif under four scenarios, using six criteria. Our findings revealed that, contrary to the authors' claims, the DMRN Protocol is vulnerable to attacks by compromised or malicious SNs. Additionally, the protocol was found to be susceptible to HN masquerade attacks. Lastly, it was demonstrated that the DMRN Protocol does not completely support mutual authentication and secure key exchange. Our multi-faceted approach to formal verification allows for a more comprehensive assessment of the DMRN Protocol's security properties. By employing two representative tools in the areas of modal logic and model checking, each with its unique strengths and capabilities, we can examine the protocol from various perspectives, thereby increasing the likelihood of detecting subtle vulnerabilities that might be overlooked in a single-tool analysis. The vulnerabilities we have identified through this process have significant implications for the security of future 6G networks. They highlight potential weaknesses in key management, authentication processes, and resistance to specific attack vectors. These findings are crucial for researchers and standardization bodies working on the development of robust security protocols for next-generation mobile networks. Furthermore, our work emphasizes the importance of thorough and diverse verification methodologies in the development of security protocols. The multi-tool approach we have employed proves to be highly effective in providing a more complete picture of a protocol's security landscape. This methodology can serve as a model for future security analyses of complex protocols, especially those intended for critical infrastructure such as 6G networks.