# Mdpj _sciences_
## 4 Formal Verification
### Formal Verification Using SVO Logic
The (H1) is defined as \(HN\mid\equiv\ \#(K_{S1})\), which cannot be considered an assumption because the \(HN\) is unable to assess the freshness of \(K_{S1}\) in typical scenarios. Consequently, the \(HN\) cannot fully trust the message received in (P1). (D10) \(UE\mid\equiv\ UE\xleftrightarrow{\{UE\xleftrightarrow{\textit{K}_{S2}}HN\ from\ HN\}}_{\textit{PK}_{U}}\), \(\langle UE\xleftrightarrow{\textit{K}_{S2}}HN,UE\xleftrightarrow{\textit{ R}_{S1}}SN\rangle_{K}\)  
by [PERSON] using (C2), (P2)  
(D11) \(UE\mid\equiv\ UE\xleftrightarrow{\{UE\xleftrightarrow{\textit{K}_{S2}}HN\ from\ HN\}}_{\textit{PK}_{U}}\)  
by (D10), RA, BA  
by (D11), (A3), RA, BA  
by (D12), (H2), NV, BA  
by (D13), (A4), JR, BA  
by (D  
(D17) \(UE\mid\equiv\ HN\mid\approx\ (UE\xleftrightarrow{\frac{K_{S2}}{\longleftrightarrow}}HN,UE \xleftrightarrow{\frac{R_{SN}}{\longleftrightarrow}}SN)\)  
by (D16), (H2), FR, NV, BA  
In the above derivation, (D12) and (D16) cannot be further evolved because the received \(c_{2}\) and MAC values cannot assure freshness to the \(UE\). This clearly demonstrates a security threat, as leakage of these values could result in severe attacks through their reuse. To address this, we incorporated (H2) and proceeded with the derivation. (D18) \(SN\mid\equiv\ SN\lhd\langle RES^{*}\ from\ UE,UE\xleftrightarrow{\frac{R_{SN}}{ \longleftrightarrow}}SN\rangle_{R_{SN}},\{K_{SEAF},SUPI\}_{K3}\)  
by [PERSON] using (C3), (P3)  
(D19) \(SN\mid\equiv\ UE\mid\sim\ (RES^{*},UE\xleftrightarrow{\frac{R_{SN}}{ \longleftrightarrow}}SN)\)  
by (D18), (A6), RA, BA  
by (D19), (A7), FR, NV, BA  
by (D20), SA, BA  
by (D21), (A8), BA  
by (D25), (D26), SA, BA  
by (D27), (A11), FR, NV  
by (D28), (A10), RA, BA  
by (D29), (A11), FR, NV  
by (D28), (A12), FR, NV  
by (D29), (A13), RA, BA  
by (D29), (A14), FR, NV, BA  
by (D29), (A15), RA, BA  
by (D29), (A16), RA, BA  
by (D29), (A17), RA, BA  
by (D29), (A18), BA, BA  
by (D29), (A19), FR, NV  
by (D29), (A10), SAFinally, based on belief (D28), the \(HN\) not only authenticates the UE through the \(K\), but it also ensures that the \(UE\) holds a belief in the \(K_{S2}\). Based on the SVO logic verification results presented above, the DMRN Protocol has revealed several critical security vulnerabilities, which can be explained via hypotheses (H1) and (H2) as follows:  
* The (H1) shows that the DMRN Protocol is vulnerable to security threats such as replay attacks due to the lack of timeliness in the \(SUIC1\) value. Consequently, it is desirable to provide timeliness to the \(K_{S1}\) so that the \(HN\) can verify the timeliness of \(C1\) and \(C2\). * In the case of (H2), the \(UE\) faces the following issues due to its inability to ensure the timeliness of the \(K_{S2}\). First, the \(UE\) is unable to authenticate the \(HN\) based on the MAC value within the AUTN sent by the \(HN\). Second, the \(UE\) cannot place sufficient trust in the master session key, anchor key, or any subsequent session keys derived from the two keys \(K\) and \(K_{S2}\). Although the DMRN Protocol attempts to address these security threats by encrypting the \(K_{S2}\) with the \(UE\)'s ephemeral public key \(p_{U}\), this is necessary to fundamentally resolve this issue.