## 5 Security Verification
### Informal Security Analysis  
In this section, we analyze important security characteristics of the proposed scheme. In the first four sections, we analyze the security characteristics of the proposed scheme. In the subsequent four sections, we analyze attacks that the proposed scheme can defend against. 1. Mutual Authentication and Key Establishment  
Figure 6: Results from the implementations of the unlinkable authentication scenario using ProVerif. Figure 7: Results from the implementations of the batch authentication scenario using ProVerif. In a SGIN, authentication passes through at least two interactions. In the first step, the UE sends a message to the LEO, and the UE is authenticated by the LEO. In the second step, the LEO returns the signature of the ECSDA to the UE, and the identity of the LEO is proven by the UE. This completes the process of mutual authentication between the UE and LEO. The keys of both the UE and LEO are issued by the trusted NCC during the initialization phase, and the authenticator holds the public keys of the target nodes, such as \(gpk\) and \(pk_{LEO}\). Therefore, the fake group members or LEOs cannot be authenticated by the legitimate node. Session Key Security  
In each phase of the proposed scheme, no matter in which scenario, the session key is calculated according to the Diffie-Hellman problem through two random numbers generated by the two entities (i.e., UE and LEO). Calculating the session key without knowing the two generators involves solving the discrete logarithm problem on an elliptic curve. At present, it is computationally infeasible to solve the discrete logarithm problem in polynomial time [36]. Forward/Backward Security  
New session keys \(SK=(g^{r_{1}})^{r_{2}}\) and \(SK=(g^{r_{2}})^{r_{1}}\) are negotiated in both authentication and roaming authentication phases of the proposed protocol. There is no computable correlation between the new session key and the session key of other sessions. No entity other than the UE and LEO can calculate the new session key. Privacy and Untraceability  
In SGIN unlinkable authentication scenario, it is difficult for an attacker to know the real identity of a UE through the signature. Unless the attacker can obtain the UE's private key and the UKL stored in the NCC, it cannot reveal the UE's identity. Or in another case, the attacker obtains \(gmsk\). But these are extremely difficult to do for the attacker. From another perspective, anonymity in the unlinkable authentication scenario is conditional. NCC has the right to recover the UE's private key \(A_{i}\) of the signature through \(gmsk\), so as to obtain the real identity of the UE. In addition, the anonymity is untraceable, and the UE can use different \(TID\) in different sessions, and the attacker cannot associate two different sessions of the same UE through signatures. In the batch authentication scenario, the UE is traceable due to the existence of \(RK\). However, it is difficult for the attacker to crack the real ID of the UE using the batch authentication key \(RAK\). In addition, the UE in the unlinkable authentication scenario does not send information correlating to batch authentication. Even if the UE is changed, the attacker cannot associate the UE in batch authentication scenario with the UE in the unlinkable authentication scenario. Resistance to Replay Attacks  
In each scenario, the entity sends a message \(M\) that contains a timestamp \(TS\). The integrity of the timestamp is protected by a signature, so it is difficult for an attacker to tamper with the timestamp. The other entity verifies the timestamp \(TS^{\prime}-TS<\Delta T\), where \(\Delta T\) is the interval that matches the current network condition. Therefore, the authentication party can confirm the freshness of the message and distinguish whether it is under replay attack.