Ứng dụng Proverif kiểm tra sự an toàn của giao thức xác thực và thỏa thuận khóa dựa vào blockchain cho mạng 5G
Email:
trannguyetnga512@gmail.com
Từ khóa:
Giao thức xác thực và thỏa thuận khóa 5G-AKA, Blockchain, Proverif, Giao thức xác thực và thỏa thuận khóa 5G-AKA, Blockchain, Proverif
Tóm tắt
Giao thức xác thực và thỏa thuận khóa AKA có vai trò quan trọng trong việc đảm bảo an toàn trong hệ thống của mạng di động 5G. Tuy nhiên, giao thức 5G-AKA vẫn gặp phải nhiều vấn đề liên quan đến việc đảm bảo tính bí mật, xác thực và toàn vẹn giữa người dùng, mạng dịch vụ và mạng thường trú. Nhiều nghiên cứu đã đưa ra để khắc phục những yếu điểm còn tồn tại trong giao thức 5G-AKA. Công nghệ blockchain với tính chất phi tập trung và khả năng chống giả mạo, đã được ứng dụng để thiết kế các giao thức xác thực an toàn hơn. Bài báo này với mục đích kiểm tra an toàn giao thức xác thực và thỏa thuận khóa 5G-AKA dựa vào blockchain, bằng việc sử dụng công cụ proverif để phân tích các thuộc tính bí mật, xác thực và các thuộc tính tương đương. Kết quả phân tích cho thấy giao thức đáp ứng các yêu cầu bảo mật như đảm bảo bí mật khóa phiên, xác thực thực thể hai chiều và khả năng chống lại nhiều loại tấn công phổ biến như tấn công xen giữa và tấn công phát lại. Nghiên cứu cho thấy tiềm năng của blockchain trong việc nâng cao an ninh cho mạng 5G, đồng thời khẳng định vai trò thiết yếu của các công cụ phân tích hình thức như ProVerif trong việc phát triển các hệ thống an toànTài liệu tham khảo
[1]. A. Peltonen, Formal Verification and Standardization of Security Protocols: Proverif and Extensions, 8th Internetnational Conference ICAIS on Artificial Intelligence and Security, Qinghai, China, July 15-20, 2022. https://doi.org/10.1007/978-3-031-06788-4_42
[2]. B.Blanchet, Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif, Foundations and Trends® in Privacy and Security, 1 (2016) 1–135. http://dx.doi.org/10.1561/3300000004.
[3].A.Armando, D.Basin, Y.Boichut, Y.Chevalier, L.Compagna, J.Cuellar, P.H.Drielsma, P.C.Heám, O.Kouchnarenko, J.Mantovani, S.Modersheim, D.V.Oheimb, M.Rusinowitch, J.Santiago, M.Turuani, L.Vigano, L.Vigneron, The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications, International Conference on Computer Aided Verification, Berlin, Heidelberg, Springer, 3576 (2005) 281–285. https://doi.org/ 10.1007/11513988_27
[4]. G. Lowe, Breaking and fixing the Needham-Schroeder Public-Key Protocol using FDR, International Workshop on Tools and Algorithms for the Construction and Analysis of Systems TACAS, Berlin, Heidelberg, Springer, 1055 (1996) 147–166. https://doi.org/ 10.1007/3-540-61042-1_43
[5].C.Cremers, Unbounded verification, falsification, and characterization of security protocols by pattern refinement, Proceedings of the ACM Conference on Computer and Communications Security, (2008) 119–128. https://doi.org/10.1145/1455770.1455787
[6].B. Schmidt, S. Meier, C. Cremers, D. Basin, Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties, in IEEE 25th Computer Security Foundations Symposium, (2012) 78–94. https://doi.org/10.1109/CSF.2012.25
[7].B. Blanchet, B. Smyth, V. Cheval, M. Sylvestre, Proverif 2.05: Automatic Cryptographic Protocol Verifier, User Manual and Tutorial, (2023) https://bblanche.gitlabpages.inria.fr/proverif/manual.pdf
[8]. B.Blanchet, The Security Protocol Verifier ProVerif and its Horn Clause Resolution Algorithm, In Proceedings HCVS/VPT, 373 (2022) 14–22. https://doi.org/10.48550/arXiv.2211.12227
[9]. B.Blanchet, Using Horn Clauses for Analyzing Security Protocols, Cryptology and Information Security Series, 5 (2011) 86-111. https://doi.org/10.3233/978-1-60750-714-7-86
[10]. K.Prakash, Balachandra, Authentication and Key Agreement in 3GPP Networks, Computer Science & Information Technology (CS & IT), (2015) 143-154. https://airccj.org/10.5121/csit.2015.51313
[11]. A.Braeken, M.Liyanage, J. M. P.Kumar, Novel 5G Authentication Protocol to Improve the Resistance Against Active Attacks and Malicious Serving Networks, in IEEE Access, 7 (2019) 64040-64052. https://doi.org/10.1109/ACCESS.2019.2914941
[12]. H.Yang, H.Zheng, J.Zhang, Y.Wu, Y.Lee, Y.Ji, Blockchain-based trusted authentication in cloud radio over fiber network for 5G, 16th International Conference on Optical Communications and Networks (ICOCN), Wuzhen, China, (2017) 1-3. https://doi.org/10.1109/ICOCN.2017.8121598
[13]. J. Xu, K. Xue, H. Tian, J. Hong, D. S. L. Wei, P. Hong, An Identity Management and Authentication Scheme Based on Redactable Blockchain for Mobile Networks, IEEE Transactions on Vehicular Technology, 69 (2020) 6688–6698. https://doi.org/10.1109/TVT.2020.2986041
[14]. M. Hojjati, A. Shafieinejad, H. Yanikomeroglu, A Blockchain-Based Authentication and Key Agreement (AKA) Protocol for 5G Networks, IEEE Access, 8 (2020) 216461–216476. https://doi.org/10.1109/ACCESS.2020.3041710
[2]. B.Blanchet, Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif, Foundations and Trends® in Privacy and Security, 1 (2016) 1–135. http://dx.doi.org/10.1561/3300000004.
[3].A.Armando, D.Basin, Y.Boichut, Y.Chevalier, L.Compagna, J.Cuellar, P.H.Drielsma, P.C.Heám, O.Kouchnarenko, J.Mantovani, S.Modersheim, D.V.Oheimb, M.Rusinowitch, J.Santiago, M.Turuani, L.Vigano, L.Vigneron, The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications, International Conference on Computer Aided Verification, Berlin, Heidelberg, Springer, 3576 (2005) 281–285. https://doi.org/ 10.1007/11513988_27
[4]. G. Lowe, Breaking and fixing the Needham-Schroeder Public-Key Protocol using FDR, International Workshop on Tools and Algorithms for the Construction and Analysis of Systems TACAS, Berlin, Heidelberg, Springer, 1055 (1996) 147–166. https://doi.org/ 10.1007/3-540-61042-1_43
[5].C.Cremers, Unbounded verification, falsification, and characterization of security protocols by pattern refinement, Proceedings of the ACM Conference on Computer and Communications Security, (2008) 119–128. https://doi.org/10.1145/1455770.1455787
[6].B. Schmidt, S. Meier, C. Cremers, D. Basin, Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties, in IEEE 25th Computer Security Foundations Symposium, (2012) 78–94. https://doi.org/10.1109/CSF.2012.25
[7].B. Blanchet, B. Smyth, V. Cheval, M. Sylvestre, Proverif 2.05: Automatic Cryptographic Protocol Verifier, User Manual and Tutorial, (2023) https://bblanche.gitlabpages.inria.fr/proverif/manual.pdf
[8]. B.Blanchet, The Security Protocol Verifier ProVerif and its Horn Clause Resolution Algorithm, In Proceedings HCVS/VPT, 373 (2022) 14–22. https://doi.org/10.48550/arXiv.2211.12227
[9]. B.Blanchet, Using Horn Clauses for Analyzing Security Protocols, Cryptology and Information Security Series, 5 (2011) 86-111. https://doi.org/10.3233/978-1-60750-714-7-86
[10]. K.Prakash, Balachandra, Authentication and Key Agreement in 3GPP Networks, Computer Science & Information Technology (CS & IT), (2015) 143-154. https://airccj.org/10.5121/csit.2015.51313
[11]. A.Braeken, M.Liyanage, J. M. P.Kumar, Novel 5G Authentication Protocol to Improve the Resistance Against Active Attacks and Malicious Serving Networks, in IEEE Access, 7 (2019) 64040-64052. https://doi.org/10.1109/ACCESS.2019.2914941
[12]. H.Yang, H.Zheng, J.Zhang, Y.Wu, Y.Lee, Y.Ji, Blockchain-based trusted authentication in cloud radio over fiber network for 5G, 16th International Conference on Optical Communications and Networks (ICOCN), Wuzhen, China, (2017) 1-3. https://doi.org/10.1109/ICOCN.2017.8121598
[13]. J. Xu, K. Xue, H. Tian, J. Hong, D. S. L. Wei, P. Hong, An Identity Management and Authentication Scheme Based on Redactable Blockchain for Mobile Networks, IEEE Transactions on Vehicular Technology, 69 (2020) 6688–6698. https://doi.org/10.1109/TVT.2020.2986041
[14]. M. Hojjati, A. Shafieinejad, H. Yanikomeroglu, A Blockchain-Based Authentication and Key Agreement (AKA) Protocol for 5G Networks, IEEE Access, 8 (2020) 216461–216476. https://doi.org/10.1109/ACCESS.2020.3041710
Tải xuống
Chưa có dữ liệu thống kê
Nhận bài
03/03/2025
Nhận bài sửa
21/04/2025
Chấp nhận đăng
10/06/2025
Xuất bản
15/06/2025
Chuyên mục
Công trình khoa học
Kiểu trích dẫn
Trần Thị, N., Nguyễn Đức, C., & Mai Đức, T. (1749920400). Ứng dụng Proverif kiểm tra sự an toàn của giao thức xác thực và thỏa thuận khóa dựa vào blockchain cho mạng 5G. Tạp Chí Khoa Học Giao Thông Vận Tải, 76(5), 673-687. https://doi.org/10.47869/tcsj.76.5.3
Số lần xem tóm tắt
38
Số lần xem bài báo
10
