Finite automata models for secure protocol verification
Rohit Agarwalrohit.agrwal@gla.ac.inDepartment of Computer Engineering & ApplicationsGLA UniversityMathura, Uttar Pradesh, 281406, IndiaView full profile → , *Rajesh Kumar TripathiCorresponding authorrajesh.tripathi@gla.ac.inDepartment of Computer Engineering & ApplicationsGLA UniversityMathura, Uttar Pradesh, 281406, IndiaView full profile → , Arjit Tomararjit.tomar@niu.edu.inDepartment of Computer Science & EngineeringSchool of Engineering & TechnologyNoida International UniversityGreater Noida, Uttar Pradesh, 203201, IndiaView full profile → , Prashant Vijay Thokalthokalprashantelect@sanjivani.org.inDepartment of Electrical EngineeringSanjivani College of EngineeringSavitribai Phule Pune UniversityKopargaon, Ahilyanagar, Maharashtra, 423603, IndiaView full profile → , Shwetambari Pandurang Katakeshwetambari.katake@vit.eduDepartment of Computer EngineeringVishwakarma Institute of TechnologyPune, Maharashtra, 411037, IndiaView full profile → , Chhavi Patlechhavi.patle@rungta.orgDepartment of Computer Science and EngineeringRungta College of Engineering and TechnologyRungta International Skills UniversityBhilai, Chhattisgarh, 490024, IndiaView full profile →
* Corresponding author · click or hover a name for details
- Received:
- 01 Apr 2026
- Published Online:
- 31 Oct 2026
- Article type:
- Research Article
- Language:
- EN
- Article no.:
- JDMSC-3070
- Pages:
- 4521–4534
Abstract
Modern digital infrastructures (such as cloud computing, IoT systems and distributed applications) heavily rely on secure communication protocols in which confidentiality, integrity, and authentication are essential. Nevertheless, the growing complexity of such systems and the development of advanced cyber-attacks reveal serious weaknesses of current methods of verification, especially their scalability and computation costs, as well as the possibility to simulate adversarial behavior. In this paper, the author discusses these issues with a proposal of a finite automata-based system of verifying a secure protocol. This work is mainly aimed at creating a highly mathematical and computationally efficient model of modeling and verifying communication protocols in adversarial conditions. In the proposed methodology, the protocols are represented as finite automata in which states are the configuration of the system, and transitions are the exchange of messages between the states. Adversary model is composed with automata and security requirements like confidentiality, integrity and authentication are formalized as constraints. To verify that the violations occur, the analysis of reachability and language-theoretic methods are used to identify the violations by exploring unsafe states. The findings indicate that the proposed framework is highly scalable and highly accurate with moderate computational cost which is better than conventional approaches to model checking, Petri nets and logic-based approaches. The measures of evaluation are the complexity of the state, verification time, overhead of transition, and memory usage, which demonstrate a better efficiency and effective attack detection possibilities.
Keywords
Subject Classifications
References
[1] G. Barthe, U. D. Lago, G. Malavolta, and I. Rakotonirina, “Tidy: Symbolic verification of timed cryptographic protocols,” in Proc. ACM SIGSAC Conf. Comput. Commun. Secur. (CCS), Los Angeles, CA, USA (Nov. 2022).
[2] Z. Chen, A. Yakaryılmaz, and J. Wu, “Verification power of rational-valued affine automata,” arXiv preprint arXiv:2509.07857 (2025).
[3] Z. Chen and A. Yakaryılmaz, “Two-way affine automata can verify every language,” arXiv preprint arXiv:2502.12879 (2025).
[4] W. Deng, D. Qiu, and J. Yang, “Opacity of extended finite automata with event parameters,” IEEE Trans. Autom. Control, early access (2025).
[5] J. Jiang, G. Dai, and Y. Wang, “Design and Security Verification of Secure Elections Voting Protocol Using APTC,” 2025 5th International Conference on Information Communication and Software Engineering (ICICSE), Chongqing, China, pp. 159-163 (2025), doi: 10.1109/ICICSE66971.2025.11430115.
[6] C. Middelburg, “Dormancy-aware timed branching bisimilarity with an application to communication protocol analysis,” Theor. Comput. Sci., vol. 912, p. 114681 (2024).
[7] Y. Mu, L. Juan, G. Shen, and W. Zihao, “Runtime verification of self-adaptive multi-agent system using probabilistic timed automata,” J. Intell. Fuzzy Syst., vol. 45, pp. 10305–10322 (2023).
[8] M. Namdev, K. Showkat, S. Vishnoi, and P. Dadheech, “Explainable machine learning frameworks for cryptography protocol design using discrete structures,” Journal of Discrete Mathematical Sciences and Cryptography, vol. 28, no. 5-B, pp. 2059–2069 (2025), doi: 10.47974/JDMSC-2423.
[9] O. Sankur, “Timed automata verification and synthesis via finite automata learning,” in Proc. 29th Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), ETAPS 2023, Paris, France, pp. 335–349 (Apr. 2023).
[10] R. S. Lois and D. G. Cole, “Designing Secure and Resilient Cyber-Physical Systems Using Formal Models,” 2022 Resilience Week (RWS), National Harbor, MD, USA, pp. 1-6 (2022), doi: 10.1109/RWS55399.2022.9984044.
[11] K. K. Thota and R. J. R. Raj, “Minimal DFA with optimization of pattern matching (MDFAOPM) for network traffic analysis and attacks,” International Journal of Information Security and Privacy, vol. 19, no. 1, pp. 1–24 (2025), doi: 10.4018/IJISP.384918.
[12] A. Ahmed, A. Shoufan, and K. Belwafi, “Light-Weight Security Protocol and Data Model for Chip-to-Chip Zero-Trust,” in IEEE Access, vol. 11, pp. 60335-60348 (2023), doi: 10.1109/ACCESS.2023.3285630.
