(untitled) (Comprehensive Journal of Science, 2025)
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.