## 6 Security Evaluation with ProVerif
### User Authentication  
When the user tries to access the controller \(c\), the user's sign key \(sk_{u}\) is needed. We modeled a set of cryptographic primitives \(F_{c}\) and \(F_{d}\) that are used in our key protection system, and are defined in Listing 4. The user's sign key \(sk_{u}\) is encrypted with the key derived from the user's password and random salt value, and the encrypted key is then stored in \(d\). The user only knows their ID and password, but not the salt value. Therefore, \(d\) should request the salt value for the salt server \(s\) if the device is connected to the Internet or mobile device \(m\). After receiving the salt value from \(s\) or \(m\), \(d\) computes the decryption key by performing the key-derivation function (\(KDF\)) for the user's password \(pass_{u}\) and salt and decrypts the ciphertext of \(sk_{u}\) with the decryption key. To obtain the access permission to the controller \(c\), \(d\) receives the nonce \(n\) from \(c\), signs the user's ID and \(n\) with the decrypted user's sign key \(sk_{u}\), and then sends the signed value to \(c\). If the received signature is verified successfully, \(c\) responds \(d\) with the symmetric key which will be used to secure subsequent communication between them. A brief representation in ProVerif is shown in Listing 5. ```
Functions: F_c={GetPKey, ENC, SIGN, GenCert, KDF, HASH} HASH(data) = hashed value. KDF(data, salt, HASH, iteration) = hashed value. ENC(Encryption key, data) = ciphertext. GetPKey(Private key) = Public key. GenCert(Public key, Private key) = Certificate. SIGN(Private key, data) = signed value. F_d={DEC, CheckSIGN, ExtractPKey} DEC(Key, ciphertext) = data. CheckSIGN(Signed value, Public key) = True or False. ExtractPKey(Certificate) = Public key. ```  
Listing 4: List of functions required for the user authentication process. ```
Storedinformation: ENC(\(k^{1}\), \(sk_{u}\)) ENC(\(k^{2}\), \(sk_{u}\)) Certificate\(cert_{u}\) Process: Device\(\hat{=}\) out(\(c_{priv}\), (\(id_{u}\), \(pass_{u}\))). in(\(c_{priv}\), \(\hat{salt^{1}}\) or \(\hat{salt^{2}}\)). let\(\hat{k}\) = KDF(\(pass_{u}\), salt, HASH, 10000) in let\(dec\_sk_{u}\) = DEC(\(\hat{k}\), ENC(\(k^{1}\) or \(k^{2}\), \(sk_{u}\))) in out(\(c\), \(Certificate\)). in(\(c\), \(n\)). out(\(c\), SIGN(\(dec\_sk_{u}\), (\(id_{u}\), \(n\)))). in(\(c\), \(encrypted\ value)). let\(key\) = DEC(\(dec\_sk_{u}\), \(encrypted\ value)\) in out(\(c\), ENC(\(key\), m)). ```  
Listing 5: Procedure performed on device \(d\) for the user authentication. In the salt server \(s\) or mobile device \(m\), the user credential information and salt value were registered in the key enrollment procedure. These are ready to receive the user ID \(id_{u}\) and password \(pass_{u}\) from \(d\). If \(s\) or \(m\) find a match with the received information from \(d\), they respond to \(d\) with the stored salt value \(salt^{1}\) (or \(salt^{2}\)). The ProVerif expression is shown in Listing 6. ```
Storedinformation:(id_{u}, HASH(\(pass_{u}\)), salt\(l^{1}\) or \(salt^{2}\)) Process: Salt\(\hat{=}\) in(\(c_{priv}\), (\(\hat{id}_{u}\), \(pa\)\(s_{u}\))). if\(\hat{id}_{u}\) = \(id_{u}\) then if HASH(\(pa\)\(s_{u}\)) = HASH(\(pass_{u}\)) then out(\(c_{priv}\), salt\(l^{1}\) or \(salt^{2}\)). ```  
Listing 6: Procedure performed on the salt server \(s\) or mobile device \(m\) for the user authentication. In the user authentication process, \(c\) receives a certificate from \(d\) and checks the validity of the certificate. If the received certificate is valid, \(c\) sends a random nonce \(n\) to \(d\) as a challenge and waits for a response from \(d\). Once receiving the signature of \(n\) from \(d\), \(c\) verifies the signature with the user's public key. If the signature is valid, \(c\) sends the symmetric key to \(d\) for securing subsequent communication. The brief ProVerif expression is provided in Listing 7.