## 6 Security Evaluation with ProVerif
### ProVerif Results  
To verify the security and correctness of our proposed protocols, we ran ProVerif on the codes described in Sections 6.1 and 6.2. We set the attacker as an active Dolev-Yao adversary [25]. In addition, to verify that our protocols are safe under the threat model described in Section 4, we assumed four cases: standard, information leakage from \(d\), information leakage from \(m\), and information leakage from both \(d\) and \(m\).  
**Standard case.** As we mentioned at the beginning of Section 6, we used the private channel when communicating between the mobile and user devices, and used the public channel when communicating between the user's device and controller. As a result, ProVerif showed that the attacker cannot obtain the user's sign key \(\mathit{sk}_{u}\).  
**Information leakage from the user's device \(d\) alone.** In this case, we assumed that an attacker could access the data stored in \(d\) such as \(\mathit{id}_{u}\), encrypted user's sign key \(\textsc{ENC}(k\),\(\mathit{sk}_{u})\), and \(\mathit{cert}_{u}\). To mimic this data leakage, we sent the data over the public channel. According to ProVerif results, the attacker cannot still obtain the user's sign key \(\mathit{sk}_{u}\).  
**Information leakage from the mobile device, \(m\), alone.** In this case, we assumed that an attacker could access the data stored in \(m\) such as \(\mathit{id}_{u}\), \(\textsc{HASH}(\mathit{pass}_{u})\), and \(\mathit{salt}^{1}\) or \(\mathit{salt}^{2}\). To mimic this data leakage, we sent the data over the public channel. The ProVerif results show that the attacker still cannot obtain the user's sign key \(\mathit{sk}_{u}\).  
**Information leakage from both \(d\) and \(m\).** In this case, we assumed that an attacker can access the data stored in both \(d\) and \(m\), including \(\mathit{id}_{u}\), \(\textsc{ENC}(k\),\(\mathit{sk}_{u})\), \(\textsc{HASH}(\mathit{pass}_{u})\), \(\mathit{salt}^{1}\) or \(\mathit{salt}^{2}\), and \(\mathit{cert}_{u}\). To mimic this case of data leakage, we sent the data over the public channel. The results of ProVerif show that the attacker can successfully obtain the user's sign key \(\mathit{sk}_{u}\). The detailed process for obtaining \(\mathit{sk}_{u}\) is shown in Listing 8.  
```
\(d\rightarrow\textsc{ATTACKER}:\textsc{ENC}(k\),\(\mathit{sk}_{u})\)\(m\rightarrow\textsc{ATTACKER}:\textsc{HASH}(\mathit{pass}_{u})\),saltBydictionaryattack,ATTACKERget\(\mathit{pass}_{u}\)fromHASH(\(\mathit{pass}_{u}\))ATTACKER:generate\(k\)usingKDFfunctionwith\(\mathit{pass}_{u}\)and\(\mathit{salt}\)ATTACKER:With\(k\),get\(\mathit{sk}_{u}\)fromENC(\(k\),\(\mathit{sk}_{u}\))usingDECfunction
```  
**Listing 8** Attack trace for information leakage from both the user and mobile devices, \(d\) and \(m\), respectively.  
Even without active intervention, the attacker can obtain the user's sign key \(sk_{u}\), but only if the attacker can access the data stored in both \(d\) and \(m\) to obtain ENC(\(k\), \(sk_{u}\)), HASH(\(pass_{u}\)), and \(salt\) together. The attacker can use the dictionary attack to successfully guess \(pass_{u}\) from HASH(\(pass_{u}\)). Using \(pass_{u}\) and \(salt\), the attacker can then make the encrypted key \(k\) using the key-derivation function KDF(\(pass_{u}\), \(salt\), HASH, 10,000). Using \(sk_{u}\), the attacker can mimic the user with the user's digital certificate and freely access the controller \(c\).