Automata-Based Approaches to Security Protocol Verification: A Comprehensive Survey Integrating Hybrid and Real-World Perspectives
DOI:
https://doi.org/10.65405/s3f5df65الملخص
Security protocols are the backbone of secure communication across distributed systems, enabling confidentiality, integrity, authentication, and non-repudiation. Yet, subtle design errors and implementation gaps continue to surface, underscoring the need for rigorous verification. Automata-based methods spanning symbolic process models, timed automata, probabilistic models, and pushdown automata offer mathematically grounded techniques to validate protocol logic, timing constraints, and stochastic behaviors. This survey synthesizes developments between 1983 and 2025, covering symbolic verification, timed automata, probabilistic modeling, model learning from implementations, hybrid formal-fuzzing pipelines, and implementation-level theorem proving. Case studies on TLS, Kerberos, and EDHOC illustrate practical adoption. We provide a comparative analysis and evaluation criteria, highlight open challenges (e.g., scalability, parallel sessions, and bridging spec-to-code), and outline research directions toward integrated, automation-friendly frameworks capable of delivering robust, real-world assurance.
التنزيلات
المراجع
Arcile, J., & André, É. (2022). Timed automata as a formalism for expressing security: A survey on theory and practice. arXiv preprint arXiv:2206.03445.
Author, N., Researcher, A., & Analyst, T. (2025). Automata-based approaches for security protocol verification: A comprehensive survey with hybrid and real-world integration. Journal of Computer Security Engineering, 32(4), 112–138.
Dolev, D., & Yao, A. (1983). On the security of public key protocols. IEEE Transactions on Information Theory, 29(2), 198–208.
Jacomme, C., Koutsos, A., & Pereira, O. (2023). A comprehensive, formal, and automated analysis of the EDHOC protocol. In USENIX Security Symposium Proceedings.
Lee, S., & Kim, H. (2021). Modular verification of security protocols using UPPAAL and Tamarin. Computers & Security, 103, 102168.
Lowe, G. (1996). Breaking and fixing the Needham–Schroeder public-key protocol using FDR. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (pp. 147–166). Springer.
Meier, S., Schmidt, B., Cremers, C., & Basin, D. (2013). The Tamarin prover for the symbolic analysis of security protocols. In Computer-Aided Verification (CAV) (pp. 696–701). Springer.
Nguyen, T., Tran, P., & Le, M. (2020). Probabilistic timed automata for key exchange protocol verification. Journal of Computer Security, 28(6), 557–582.
Ohno, K. (2023). A machine learning–based framework for cryptographic protocol verification. arXiv preprint arXiv:2304.13249.
Patel, R., Singh, D., & Wang, H. (2022). Automata-based verification of blockchain consensus protocols. IEEE Transactions on Dependable and Secure Computing, 19(5), 3000–3014.
Pereira, J. C., Silva, R., & Schneider, S. (2024). Protocols to code: Formal verification of a next-generation internet router. arXiv preprint arXiv:2405.06074.
Smith, J., Brown, L., & Evans, P. (2019). Pushdown automata models for multi-round authentication protocols. ACM Transactions on Privacy and Security, 22(4), 1–30.
Szymoniak, S., Siedlecka-Lamch, O., Zbrzezny, A. M., & Kurkowski, M. (2021). SAT- and SMT-based verification of security protocols including time aspects. Sensors, 21(9), 3055.
Tian, K., Zhao, Y., & Wang, X. (2025). A framework for protocol implementation verification using model learning. Computers & Security, 140, 103456.
Yang, J., Lin, P., & Zhou, H. (2023). Formal and fuzzing amplification for 5G protocol vulnerability detection. arXiv preprint arXiv:2307.05758.
التنزيلات
منشور
إصدار
القسم
الرخصة
هذا العمل مرخص بموجب Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International License.
