# A Secure and Lightweight Group Mobility Authentication Scheme for 6 LoWPAN Networks
## 4 System Models
### Formal Verification Based on Scyther Tool  
The Scyther tool [32] was used to verify the proposed group handover authentication protocol. Verified schemes are primarily characterized by secrecy and authentication. Several security protocol elements can be expressed using Scyther's Security Protocol Description Language (SPDL), including protocol definitions, role definitions, and data types. Scyther supports several robust security models, including DY and eCK, and several claims, such as Weakagree, Secret, Alive, Nisynch, and Niagree. These claims possess strong security properties. Among these are the ability to protect message confidentiality, detect MITM and replay attacks, guarantee the PFS of SL_GAS, and detect key leaks. Black-box verification is incorporated into Scyther. It is up to each role to determine whether it can achieve the security attribute or security goal. The attack output graph will indicate failure if the declared security attribute is not met. Otherwise, it will indicate OK. Using SPDL, 6L\({}_{\text{MNGL}}\) aggregates all authentication information of group members from 6L\({}_{\text{MN}i}\). In the **initial authentication phase**, secure communications are established in five primary roles--6L\({}_{\text{MAG}}\), 6L\({}_{\text{MNGL}}\), 6L\({}_{\text{MN}i}\), LMA, and AAA. The protocol was modeled for this verification with two group members (6L\({}_{\text{MN}i}\)) and their associated interactions. Scyther's flexibility allows scaling the number of group members, though it may prolong the analysis time. As shown in the verification results (Figure 6), the Scyther tool verified all critical security claims for each role:  
* 6L\({}_{\text{MN}i}\): Verified the secrecy of its alias identity (\(AID_{i}\)), tag (\(Tag_{i}\)), and its synchronization properties (Nisynch). * 6L\({}_{\text{MNGL}}\): Verified the secrecy of the group leader's temporary identity (\(Tag_{\text{GL}}\)), aggregated authentication information (\(AID_{\text{GL}}\), \(T_{\text{GL}}\), and \(R3\)), and synchronization with other entities. * 6L\({}_{\text{MAG}}\): Verified the secrecy and integrity of the aggregated tag (\(Tag_{\text{G}}\)) and synchronization. * AAA: Verified the secrecy of critical parameters, such as the temporary credentials (\(T_{\text{C}}\)) and nonce (\(N_{3}\)), and their liveness properties. * LMA: Verified the secrecy of the shared group session key (\(E_{\text{KG}}\)\(\leftrightarrow\)\({}_{L}\)) and the temporary nonce (\(N_{2}\)). The results demonstrate that the initial authentication phase is resilient to parameter changes and robust against various security threats, such as unauthorized access, impersonation, and replay attacks. The verified claims ensure that the protocol's design adheres to high-security standards, providing a solid foundation for secure group communication in the 6 LoWPAN network. Therefore, it considers _GID_ to be the group's identity. After _GID_ has been verified in Scyther, the whole group is safe if there are no vulnerabilities. At the SL_GAS' **handover phase**, five basic roles are played: 6L\({}_{\text{MAG}}\), 6L\({}_{\text{MNGL}}\), 6L\({}_{\text{MNi}}\), LMA, and AAA server. In this protocol, two members of the group are assumed. The number of group members in Scyther can be easily increased, although this may result in a prolonged analysis period. SPDL is used to code and analyze the proposed handover phase. SPDL is analyzed using Scyther. _TID\({}_{6G}\)_ represents the temporary identity of the group, while the remaining roles correspond to the protocol entities. As illustrated in Figure 7a-c, SL_GAS has been demonstrated to be resilient to parameter setting changes when tested with the Scyther tool. The three available parameters are the graph output, verification, and advanced parameters. The authors in [33] describe these parameters in detail. The following verification parameters were set up in the first setting: 50 runs, typed matching, 100 patterns for each claim, and 32 for the graph output.