## 8 Conclusions  
We present a formally verified certificate-based user authentication method using a secondary network device to protect a user's sign key. In the proposed method, the user's sign key is encrypted and can only be decrypted with the assistance of a secondary device. To show the feasibility of the proposed method, we implemented a prototype with popularly used cryptographic algorithms (AES-256, RSA-3072, and ECDSA-256). Through the security evaluation using ProVerif and the performance evaluation of the prototype implementation, we confirmed that the proposed method can bring significant benefits with respect to security with only a slight sacrifice in performance (0.073 s increase with respect to the execution time for the user authentication procedure).  
As part of future work, we plan to conduct real-world experiments through the deployment of the proposed method with a company that is developing industrial controller solutions, and analyze its usability issues (e.g., user satisfaction and network stability) in real-world settings.  
The source code of our implementation and the data files of the evaluation results are available at a GitHub repository ([[https://github.com/rymuff/keyprotection](https://github.com/rymuff/keyprotection)]([https://github.com/rymuff/keyprotection](https://github.com/rymuff/keyprotection))). The GitHub repository contains the URL links to the source codes of the client application, the salt server, the mobile application, and the controller. The repository also contains the URL links to the following data files of the evaluation results: the data files of the analysis results of the authentication using a conventional system and the proposed system and the data files of the execution time and power consumption measurements of the backdoor application.  
Methodology, J.C. ([PERSON]) and S.H.; Software, J.C. ([PERSON]); Formal Analysis, J.C. ([PERSON]); Data Curation, J.C. ([PERSON]); Writing--Original Draft Preparation, J.Choi and H.K.; Writing--Review & Editing, S.H.; Supervision, H.K. All authors have read and agreed to the published version of the manuscript.  
This research was supported by the MIST (Ministry of Science and ICT), Korea, under the ICT Consilience Creative program (IITP-2019-2015-0-00742) supervised by the IITP (Institute for Information & communications Technology Planning & Evaluation) and by the National Research Foundation of Korea (NRF) grant funded by the Korea government (MSIT) (No. 2019R1C1C1007118).  
The authors declare no conflict of interest.  
The following abbreviations are used in this manuscript:  
AESAdvanced Encryption Standard  
IIoTIndustrial Internet of Things  
PBKDF2 Password-Based Key Derivation Function 2  
SSLSecure Socket Layer  
TLSTransport Layer Security  
LTE/4 GLong-Term Evolution  
ECDSAElliptic Curve Digital Signature Algorithm  
NISTNational Institute of Standards and Technology  
GCMGalois/Counter Mode  
HMACHash-based Message Authentication Code  
CSPRNGCryptographically Secure Pseudorandom Number Generator  
SHA3 Secure Hash Algorithm  
RESTRepresentational State Transfer  
SPPSerial Port Profile  
ICSIndustrial Control System  
QRcodeQuick Response code  
\(sk_{u}\)Sign key of user