Hội thảo nghiên cứu ứng dụng Mật mã và An toàn thông tin

Bài viết

Paradigms in Security Protocol Verification: A Multi-Tool Analysis

  • Lê Vĩnh Thịnh · Ho Chi Minh City University of Technology and Education (HCMUTE) (VN)
DOI: 10.54654/isj.v3i23.1059
Từ khóaGiao thức xác minhgiao thức làm giảgiao thức phân tíchbảo mậtmật mã học

Tóm tắt

Trong lĩnh vực bảo mật Internet, đảm bảo tính vững chắc và toàn vẹn của các giao thức truyền thông là điều tối quan trọng. Bài báo này cung cấp một phân tích toàn diện về bốn công cụ hàng đầu để xác minh giao thức bảo mật: Scyther, ProVerif, CryptoVerif và Tamarin. Mỗi công cụ được đánh giá về những điểm mạnh và ứng dụng độc đáo của nó, đặc biệt trong bối cảnh điện toán đám mây và IoT. Nghiên cứu bắt đầu với Scyther, nhấn mạnh khả năng làm giả tự động và xác minh đa giao thức của nó. Tiếp theo, ProVerif được xem xét về khả năng lập luận biểu tượng và hiệu quả trong việc xử lý các giao thức bảo mật phức tạp. Bài báo sau đó khám phá cách tiếp cận tính toán của CryptoVerif đối với việc xác minh giao thức, tập trung vào cách nó mô hình hóa và xác minh các giao thức dưới nhiều giả định mật mã khác nhau. Cuối cùng, các tính năng nâng cao của Tamarin trong phân tích biểu tượng và khả năng quản lý các thuộc tính bảo mật phức tạp được thảo luận, nhấn mạnh độ sâu của nó trong xác minh giao thức chính thức. Phân tích so sánh này không chỉ nhấn mạnh những đóng góp riêng biệt của mỗi công cụ mà còn cung cấp một góc nhìn rộng hơn về hiệu quả của chúng trong việc giải quyết cả những thách thức bảo mật hiện tại và mới nổi. Bằng cách phân tích các phương pháp và hạn chế của các công cụ này, bài báo nhằm cung cấp những hiểu biết có giá trị về bối cảnh đang phát triển của việc xác minh giao thức bảo mật và các hướng đi tiềm năng trong tương lai trong lĩnh vực nghiên cứu an ninh mạng quan trọng này.

Lượt tải theo tháng

0173312/2402/2503/2504/2505/2506/2507/2508/2509/2510/2511/2512/2501/2602/2603/2604/2605/26

Di chuột vào cột để xem số lượt tải.

Cách trích dẫn

Lê Vĩnh Thịnh (2024). Paradigms in Security Protocol Verification: A Multi-Tool Analysis . Tạp chí Khoa học và Công nghệ trong lĩnh vực An toàn thông tin, 3(23), 62-81. https://doi.org/10.54654/isj.v3i23.1059

Tài liệu tham khảo

  1. 1.M. A. Fikri, K. Ramli, and D. Sudiana, “Formal Verification of the Authentication and Voice Communication Protocol Security on Device X Using Scyther Tool,” IOP Conf. Ser. Mater. Sci. Eng., vol. 1077, no. 1, p. 012057, Feb. 2021. doi: 10.1088/1757-899X/1077/1/012057.
  2. 2.N. Dalal, J. Shah, K. Hisaria, and D. Jinwala, “A Comparative Analysis of Tools for Verification of Security Protocols,” Int. J. Commun. Netw. Syst. Sci., vol. 03, no. 10, pp. 779–787, 2010. doi: 10.4236/ijcns.2010.310104.
  3. 3.H. A. Elbaz, M. H. Abd-elaziz, and T. M. Nazmy, “Analysis and Verification of a Key Agreement Protocol over Cloud Computing Using Scyther Tool,” vol. 2, no. 2, 2014.
  4. 4.L. Chen and C. Kudla, “Identity based authenticated key agreement protocols from pairings,” in 16th IEEE Computer Security Foundations Workshop, 2003. Proceedings., Pacific Grove, CA, USA: IEEE Comput. Soc, 2003, pp. 219–233. doi: 10.1109/CSFW.2003.1212715.
  5. 5.Y. Yang, H. Yuan, L. Yan, and Y. Ruan, “Post‐quantum identity‐based authenticated multiple key agreement protocol,” ETRI J., vol. 45, no. 6, pp. 1090–1102, Dec. 2023, doi: 10.4218/etrij.2022-0320.
  6. 6.C. J. Cremers, “The Scyther Tool: Verification, falsification, and analysis of security protocols,” in International Conference on Computer Aided Verification, Springer, 2008, pp. 414–418. Accessed: Nov. 04, 2016. Available: http://link.springer.com/chapter/10.1007/978-3-540-70545-1_38.
  7. 7.C. J. F. Cremers, “Unbounded verification, falsification, and characterization of security protocols by pattern refinement,” in Proceedings of the 15th ACM conference on Computer and communications security, Alexandria Virginia USA: ACM, Oct. 2008, pp. 119–128. doi: 10.1145/1455770.1455787.
  8. 8.C. Xi and L. Siqi, “Research on semantics and algorithm of formal analysis tool Scyther,” in 2022 IEEE 4th International Conference on Civil Aviation Safety and Information Technology (ICCASIT), Dali, China: IEEE, Oct. 2022, pp. 1058–1074.doi: 10.1109/ICCASIT55263.2022.9987170.
  9. 9.X. Zhang, Y. Zhu, C. Gu, and X. Miao, “A Formal Verification Method for Security Protocol Implementations Based on Model Learning and Tamarin,” J. Phys. Conf. Ser., vol. 1871, no. 1, pp. 012102, Apr. 2021, doi: 10.1088/1742-6596/1871/1/012102.
  10. 10.S. Meier, B. Schmidt, C. Cremers, and D. Basin, “The TAMARIN Prover for the Symbolic Analysis of Security Protocols,” in Computer Aided Verification, vol. 8044, N. Sharygina and H. Veith, Eds., in Lecture Notes in Computer Science, vol. 8044, Berlin, Heidelberg: Springer Berlin Heidelberg, 2013, pp. 696–701. doi: 10.1007/978-3-642-39799-8_48.
  11. 11.Y. Xiong, C. Su, W. Huang, F. Miao, W. Wang, and H. Ouyang, “Verifying Security Protocols using Dynamic Strategies,” Aug. 25, 2019, arXiv: arXiv:1807.00669. A Jan. 18, 2024. Available: http://arxiv.org/abs/1807.00669.
  12. 12.D. Basin, C. Cremers, J. Dreier, and R. Sasse, “Tamarin: Verification of Large-Scale, Real-World, Cryptographic Protocols,” IEEE Secur. Priv., vol. 20, no. 3, pp. 24–32, May 2022, doi: 10.1109/MSEC.2022.3154689.
  13. 13.P.V. Hau and D. T. T. Hien, “Enhancing Web Application Security: A Deep Learning and NLP-based Approach for Accurate Attack Detection” in Journal of Science and Technology on Information Security, vol. 3, no. 20, pp. 77-87, December 2023. doi: https://doi.org/10.54654/isj.v3i20.1008.
  14. 14.B. Blanchet, “The Security Protocol Verifier ProVerif and its Horn Clause Resolution Algorithm,” Electron. Proc. Theor. Comput. Sci., vol. 373, pp. 14–22, Nov. 2022, doi: 10.4204/EPTCS.373.2.
  15. 15.J. Yao, C. Xu, D. Li, S. Lin, and X. Cao, “Formal Verification of Security Protocols: ProVerif and Extensions,” in Artificial Intelligence and Security, vol. 13339, X. Sun, X. Zhang, Z. Xia, and E. Bertino, Eds., in Lecture Notes in Computer Science, vol. 13339, pp. 500–512, Cham: Springer International Publishing, 2022. doi: 10.1007/978-3-031-06788-4_42.
  16. 16.E.-Y. Yap, J.-J. Chin, and A. Goh, “Verifying MQV-Based Protocols Using ProVerif,” in IT Convergence and Security, vol. 782, H. Kim and K. J. Kim, Eds., in Lecture Notes in Electrical Engineering, vol. 782, pp. 55–63, Singapore: Springer Singapore, 2021. doi: 10.1007/978-981-16-4118-3_6.
  17. 17.M. Abadi, B. Blanchet, and C. Fournet, “The Applied Pi Calculus: Mobile Values, New Names, and Secure Communication,” 2016, arXiv. doi: 10.48550/ARXIV.1609.03003.
  18. 18.B. Blanchet and B. Smyth, “Automated Reasoning for Equivalences in the Applied Pi Calculus with Barriers,” in 2016 IEEE 29th Computer Security Foundations Symposium (CSF), Lisbon: IEEE, pp. 310–324, Jun. 2016. doi: 10.1109/CSF.2016.29.
  19. 19.B. Blanchet, “CryptoVerif: a Computationally-Sound Security Protocol Verifier (Initial Version with Communications on Channels),” 2023, arXiv. doi: 10.48550/ARXIV.2310.14658.
  20. 20.K. Cohn-Gordon, C. Cremers, B. Dowling, L. Garratt, and D. Stebila, “A Formal Security Analysis of the Signal Messaging Protocol,” J. Cryptol., vol. 33, no. 4, pp. 1914–1983, Oct. 2020. doi: 10.1007/s00145-020-09360-1.
  21. 21.K. Bhargavan, B. Blanchet, and N. Kobeissi, “Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate,” in 2017 IEEE Symposium on Security and Privacy (SP), San Jose, CA, USA: IEEE, pp. 483–502, May 2017, doi: 10.1109/SP.2017.26.
  22. 22.B. Blanchet, "Dealing with Dynamic Key Compromise in Crypto Verif," in 2024 IEEE 37th Computer Security Foundations Symposium (CSF), Enschede, Netherlands, pp. 495-510 2024. doi:10.1109/CSF61375.2024.00015.
  23. 23.B. Lipp, B. Blanchet, and K. Bhargavan, “A Mechanised Cryptographic Proof of the WireGuard Virtual Private Network Protocol,” in 2019 IEEE European Symposium on Security and Privacy (EuroS&P), Stockholm, Sweden: IEEE, Jun. 2019, pp. 231–246. doi: 10.1109/EuroSP.2019.00026.
  24. 24.B. Blanchet, P. Boutry, C. Doczkal, B. Grégoire and P. -Y. Strub, "CV2EC: Getting the Best of Both Worlds," 2024 IEEE 37th Computer Security Foundations Symposium (CSF), Enschede, Netherlands, pp. 279-294, 2024, doi: 10.1109/CSF61375.2024.00019.
  25. 25.T. M. C. Le, X. T. Pham, and V. T. Le, “Advancing Security Protocol Verification: A Comparative Study of Scyther, Tamarin” in Journal of Technical Education Science, vol. 19, no. 1, pp. 43–53, Feb. 2024. doi: 10.54644/jte.2024.1523.
  26. 26.T. L. Vinh, H. Cagnon, S. Bouzefrane, and S. Banerjee, “Property-based token attestation in mobile computing: Property-based token attestation in mobile computing,” in Concurr. Comput. Pract. Exp., pp. e4350, Oct. 2017. doi: 10.1002/cpe.4350.

Bài viết liên quan