cid 25cc1912cb3b3d03f0191db11b97f4e2f184c9197ee08f6dae4901cc85d983e2 · original · via openalex
Title: IKEv2-FV: A BIP-Based Formal Verification Framework for the IKEv2 Protocol Authors: Chuan Li; Yong Zhang; Xia Yang; Rui Yao; Wensheng Guo; Haiyong Sun Venue: International Symposium on AI and Cybersecurity (ISAICS) Year: 2025 Canonical: doi:10.1109/isaics66888.2025.11350064 URL: https://doi.org/10.1109/isaics66888.2025.11350064 Collector: openalex OA: false ABSTRACT IPSec (Internet Protocol Security), as an open standard for network-layer security protocols, aims to provide security services for IP network communications. However, even protocols that have been extensively studied and deployed for extended periods continue to demonstrate vulnerabilities. As the core protocol of IPSec, IKEv2 is designed to ensure mutual authentication between two peers and generate shared keys that serve as the security foundation for IPSec communications. Applying formal methods to verify the IKEv2 protocol constitutes a critical step in ensuring its security and reliability. Existing formal verification frameworks for IKEv2 often employ excessive abstraction of protocol design and attacker behavior, resulting in superficial verification that fails to uncover subtle vulnerabilities within the protocol. This paper proposes the IKEv2-FV framework, which applies the three-layer BIP (Behavior, Interaction, Priority) architecture to formal modeling and security verification of the IKEv2 protocol. By precisely characterizing protocol design details and attacker behavior, it achieves in-depth formal modeling of the protocol. Experiments demonstrate that IKEv2FV achieves higher accuracy and localization precision than traditional verification frameworks in detecting known IKEv2 vulnerabilities.