## 7 Weak Authentication
Its method of establishing whether a property holds is to test for the refinement of a transition system capturing the property by the candidate machine. It also has the ability to check the determinism of a state machine, and this is used primarily for checking security properties [34]. Since using FDR2 modeling language is very time consuming and error prone [32], Casper [35] has been used, which is a compiler for analyzing security protocols. This combination is also known as the Casper/FDR2 approach and has been used in many works [32,34,36,37]. A Casper input file consists of eight headers that are described in Table 6. Using this input file, Casper will be able to generate a CSP compatible syntax, which will be then checked by FDR2. #### 8.1.2 Security Proof

ECDH and HMAC are added into the design, and the rest of the security in Seluge++ depends on the hash dependency pattern of Seluge. Therefore, our claim of an authentic protocol depends on the security proof of new features. Consequently, to make sure that the generated key is only shared between the base station and the node, the key generation of Seluge++ is implemented in Casper with the help of the given examples in Casper's installation, as shown in Algorithm 4. \begin{table}
\begin{tabular}{l l} \hline \hline
**Header** & **Description** \\ \hline \#Free Variables & Defines the agents, custom types and variables. \\ \hline \#Processes & Is actually the list of agents. \\ \hline \#Protocol Description & Shows the messages that has to be exchanged between agents. This is actually the implementation of the protocol. \\ \hline \#Specification & Security properties that have to be checked (e.g., the secrecy of a session key). \\ \hline \#Actual Variables & Real variables. These will help to specify which of the free variables have to be renewed per each run of the protocol for each agent. \\ \hline \#Function & User-custom functions can be defined here. \\ \hline \#System & Instantiates agents with real variables. \\ \hline \#Intruder Information & The attacker capabilities must be specified here. \\ \hline \hline \end{tabular}
\end{table} 
Table 6: Header description of Casper’s input file. Figure 8: The FDR2 (Failures-Divergence Refinement) results of Seluge++ key generation in Casper. ```
1:#Free variables
2:datatype F = G \(|\) Exp(F,Num) unwinding 2
3:BS, ND: Agent
4:Ds, Dn: Num
5:N1: Nonce
6:Pub: Agent \(->\) PublicKey
7:Pri: Agent \(->\) SecretKey
8:H: HashFunction
9:pwd: Agent x Agent \(->\) Password
10:InverseKeys = (sk,sk), (Exp, Exp), (Pub, Pri),(pwd, pwd)
11:sk, Yn,Ys: F
12:#Processes
13:BASE(BS, Ds, SK) knows Pub, Pri(BS), pwd(BS,ND)
14:MOTE(ND,Dn, N1, SK) knows Pub, pwd(BS,ND)
15:#Protocol description
16:0. \(->\) BS : ND
17:[BS! = ND]
18:1. BS \(->\) ND : {Exp(G, Ds)%Qs} {Pri(BS)}
19:[BS! = ND and isExp(Qs)]
20: \(<\) sk := Exp(Qs, Dn) \(>\)
21:2. ND \(->\) BS : Exp(G, Dn)%Qn, {Exp(G, Dn)%Qn}{pwd(BS, ND)}
22:[ND! = BS and isExp(Qn)]
23: \(<\) sk := Exp(Qn, Ds) \(>\)
24:3. BS \(->\) ND : BS
25:4. ND \(->\) : sk
```
**Algorithm 4** Seluge++ key generation implemented in Casper. ```
1:#Free variables
2:datatype F = G \(|\) Exp(F,Num) unwinding 2
3:BS, ND: Agent
4:Ds, Dn: Num
5:N1: Nonce
6:Pub: Agent \(->\) PublicKey
7:Pri: Agent \(->\) SecretKey
8:H: HashFunction
9:pwd: Agent x Agent \(->\) Password
10:InverseKeys = (sk,sk), (Exp, Exp), (Pub, Pri),(pwd, pwd)
11:sk, Yn,Ys: F
12:#Processes
13:BASE(BS, Ds, SK) knows Pub, Pri(BS), pwd(BS,ND)
14:MOTE(ND,Dn, N1, SK) knows Pub, pwd(BS,ND)
15:#Protocol description
16:0. \(->\) BS : ND
17:[BS! = ND]
18:1. BS \(->\) ND : {Exp(G, Ds)%Qs} {Pri(BS)}
19:[BS! = ND and isExp(Qs)]
20: \(<\) sk := Exp(Qs, Dn) \(>\)
21:2. ND \(->\) BS : Exp(G, Dn)%Qn, {Exp(G, Dn)%Qn}{pwd(BS, ND)}
22:[ND! = BS and isExp(Qn)]
23: \(<\) sk := Exp(Qn, Ds) \(>\)
24:3. BS \(->\) ND : BS
25:4. ND \(->\) : sk
```
**Algorithm 5** Seluge++ key generation implemented in Casper. ```
36:#Functions
37:inline isExp(y) = member(y, F_(1)) and y!