## 4 Developing SNEP Model in AVISPA
### Node to Node Key Agreement with Strong Freshness  
While developing the AVISPA model, we develop a combined model of two sub-protocols: node to node key agreement and data transmission with strong freshness. The protocol messages we have modeled are shown in Figure 6.  
In the following, we explain each message briefly:  
* We assume the scenario where node A sends a request Ra with a nonce Na to node B, but they do not have any shared key. However, A and B share master secrets \(\chi_{AS}\) and \(\chi_{BS}\) with the trusted third party S, from which symmetric keys Kas and Kbs are derived.
* [PERSON] requests [PERSON] to establish a symmetric key between A and B. While sending this request, [PERSON] sends a fresh nonce, Nb with Na. Note that the keyed hash of the first part, _i.e._, h(Kbs.Na.Nb.A.B), is included for message authentication.
* Next, S generates a new symmetric key, SKab, and sends this to A and B through two separate messages. While sending A (B), this key is encrypted with Kas (Kbs). Moreover, the keyed hash is calculated using Kas (Kbs), which also includes the nonce Na (Nb).
* Now, B sends Rb encrypted by SKab to A in response to the request it received in the first message. The keyed hash sent with this message is calculated using SKab, which includes Na.  
In the AVISPA model we develop, there are three agent roles: server for the trusted third party (S), alice for node A and bob for the other node (B). Figure 7 shows the partial HLPSL specification that we develop to model these three roles. The security goals of the node to node key agreement protocol and the data transmission protocol with strong freshness were mentioned earlier. However, AVISPA is not able to validate all of those properties. The following security properties can be validated using AVISPA:  
1. Secrecy of the symmetric key SKab, which is validated using the HLPSL goal secrecy_of and the corresponding secret fact secret(SKab, skab, {A, S, B}). Here, the label skab identifies the goal, and {A, S, B} is the set of agents that are allowed to learn the value SKab.
2. Upon receiving the third message, [PERSON] authenticates [PERSON] through the nonce [PERSON]. We use the label alice_server_na to identify the goal. To validate this security goal, we add witness(S, A, alice_server_na, Na') and request(A, S, alice_server_na, Na) statements inside the roles of S and A, respectively.  
Figure 6: Messages for node to node key agreement with strong freshness.  
3. Upon receiving the fourth message, [PERSON] authenticates [PERSON] through the nonce Nb. We use the label bob_server_nb to identify the goal. To validate this security goal, we add witness(S, B, bob_server_nb, Nb') and request(B, S, bob_server_nb, Nb) statements inside the roles of S and B, respectively.
4. Upon receiving the fifth message, [PERSON] authenticates [PERSON] through the nonce [PERSON]. We use the label alice_bob_na to identify the goal. To validate this security goal, we add witness(B, A, alice_bob_na, Na) and request(A, B, alice_bob_na, Na) statements inside the roles of B and A, respectively.
5. The secrecy of the response of B to A (_i.e._, Rb) is validated using the fact secret(Rb, rb, {A, B, S}). Here, the label rb identifies the goal, and {A, B, S} is the set of agents that are allowed to learn the value Rb.  
Figure 7: Agent roles modeled in the node to node key agreement with strong freshness.