TY - GEN
T1 - Automated Theorem Proving Algorithm for Verifying Security Protocols in Communication Networks
AU - Jasmin, M.
AU - Vij, Priya
AU - Anjaneyulu, Madugula
AU - Jasim, Laith Hussein
AU - Gopinath, S.
AU - Al Zahraa, Fatima Ayad Abd
AU - Alhayaly, Omar Usama
N1 - Publisher Copyright:
© 2025 IEEE.
PY - 2025
Y1 - 2025
N2 - Communication protocol security is becoming more important in today's interconnected society because of the increasing sophistication of hacking methods to compromise data privacy, authenticity, and integrity. Complex protocol systems are unsuitable for conventional verification methods due to their dependence on human judgment and scalability issues. Our paper presents PROTOSEC-ATP, a novel automated theorem-proving algorithm based on verifying communication network protocols. With symbolic model checking and first-order logic inference, PROTOSEC-ATP automates reasoning and extracts authentication and secrecy from protocol specifications. The method builds logical models of protocol operations and confirms that they meet security restrictions using resolution-based proving. PROTOSEC-ATP finds small logical mistakes in well-known, obscure protocols like Needham-Schroeder and Kerberos. Our approach verifies faster and more accurately than previous methods. Automation, scalability, and reliability underpin PROTOSEC-ATP's communication protocol security. Network protocol assurance is automated and reliable using this solution.
AB - Communication protocol security is becoming more important in today's interconnected society because of the increasing sophistication of hacking methods to compromise data privacy, authenticity, and integrity. Complex protocol systems are unsuitable for conventional verification methods due to their dependence on human judgment and scalability issues. Our paper presents PROTOSEC-ATP, a novel automated theorem-proving algorithm based on verifying communication network protocols. With symbolic model checking and first-order logic inference, PROTOSEC-ATP automates reasoning and extracts authentication and secrecy from protocol specifications. The method builds logical models of protocol operations and confirms that they meet security restrictions using resolution-based proving. PROTOSEC-ATP finds small logical mistakes in well-known, obscure protocols like Needham-Schroeder and Kerberos. Our approach verifies faster and more accurately than previous methods. Automation, scalability, and reliability underpin PROTOSEC-ATP's communication protocol security. Network protocol assurance is automated and reliable using this solution.
KW - Automated Theorem Proving(ATP)
KW - First-Order Logic
KW - Network Security
KW - Protocol Authentication
KW - Security Protocol Verification
UR - https://www.scopus.com/pages/publications/105031605256
U2 - 10.1109/ICCR67387.2025.11292282
DO - 10.1109/ICCR67387.2025.11292282
M3 - Conference contribution
AN - SCOPUS:105031605256
T3 - ICCR 2025 - 3rd International Conference on Cyber Resilience
BT - ICCR 2025 - 3rd International Conference on Cyber Resilience
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 3rd International Conference on Cyber Resilience, ICCR 2025
Y2 - 3 July 2025 through 4 July 2025
ER -