## 6 Evaluation and Discussion
### Protocol Validation  
In this section, we evaluated our proposal using AVISPA. AVISPA uses a formal language named High-level Protocol Specification Language (HLPSL) to verify the correctness and security of communication protocols [43]. To ensure the security of our proposed protocol, we identified four roles, namely role_PV, role_MS, role_VRE, and role_SCA, which represent the \(PV\), \(MS\), \(VRE\), and \(SCA\), respectively. We then established sessions between these entities to simulate the exchange of protocol-based messages. In accordance with the diagram presented in Figure 7, these sessions are as follows: (1) the PV and MS establish two sessions, one for the join message and another one for the sign message; (2) the \(MS\) and \(VRE\) establish a session to verify the information of the join message received from the \(PV\); (3) the \(MS\) establishes a session with the \(SCA\) to send a certificate request message. The validation process aims to ensure the secrecy of the information sent within two messages:  
* \(PV\hookrightarrow MS:si/(NDN-BDA/MS/join/CID/VID)K_{MS})\). * \(PV\hookrightarrow MS:si/(NDN-BDA/MS/sign/VID/<key>/K_{MS})\). Additionally, it aims to authenticate several messages:  
* \(PV\hookrightarrow MS:si/(NDN-BDA/MS/join/CID/VID)K_{MS})\). * \(MS\hookrightarrow VRE:si/(NDN-BDA/MS/join/CID/VID)\). * \(VRE\hookrightarrow MS:d/(NDN-BDA/MS/join/CID/VID)\). * \(MS\hookrightarrow PV:d/(NDN-BDA/MS/join/CID/VID)K_{MS})\). * \(PV\hookrightarrow MS:si/(NDN-BDA/MS/sign/VID/<key>/K_{MS}\). * \(MS\hookrightarrow SCA:si/(NDN-BDA/SCA/sign/CID/VID/<key>)\). * \(SCA\hookrightarrow MS:d/(NDN-BDA/SCA/sign/CID/VID)\). * \(MS\hookrightarrow PV:d/(NDN-BDA/MS/sign/VID/<key>/K_{MS}\). The HLPSL role specification of the system nodes, namely the \(VP\), \(MS\), \(VRE\), and \(SCA\), is presented in Figure 8. The definition code of the \(MS\) node is represented from _Line 3_ to _Line 36_. The \(MS\) interacts with all the other entities in the system. Therefore, we need to add all the system nodes as agents within the definition code of \(MS\), as shown in _Line 3_. The role specification of the \(MS\) utilizes the public keys belonging to the \(MS\), \(VP\), \(VRE\), and \(SCA\), denoted as Kms, Kpv, Kvre, and Ksca, respectively. It also employs two communication channels, SND, used to send messages, and RCV, to receive messages. It also uses local variables to store/create incoming/outgoing messages (_Line 7_). The \(MS\) role specification includes a set of transitions, which outline all the actions that the \(MS\) performs during communication sessions (_Lines 11-35_). The HLPSL specification defines a set of actions. Along with SND and RCV, an action may also be secret, which verifiesmessage encryption, witness to enable message authentication, and wrequest to verify the message's authenticity. For example, in _Line 16_, the \(MS\) requests the message that it sends to the \(VRE\) to be authenticated. Similarly, in _Line 13_, the \(MS\) verifies the authenticity of the message that it received from \(PV\). The \(PV\) role specification starts from _Line 39_ and ends in _Line 59_. \(PV\) employs only two agents: the VP and MS, as the \(PV\) communicates only with the \(MS\) (_Line 39_). The role_PV definition also defines the actions performed by the \(PV\), which includes sending secret messages (_Lines 48 and 53_). Similarly, the \(VRE\) specification ranges from _Line 62_ to _Line 77_. It also defines two agents: the VRE and MS, with whom it communicates. The \(VRE\) performs two actions. It verifies the received message from the \(MS\) (_Lines 70-72_) and sends a data packet to \(MS\) (_Lines 75-77_). The \(SCA\) also defines two agents, and it performs two actions: receiving a message from the \(MS\) (_Line 89-90_) and sending the data to the \(MS\) (_Lines 92-94_). Figure 8: HLPSL specification code used for the definition of the NDN-BDA roles.