State-inferer: LLM-Driven State Machine Extraction and Formal Verification for Secure Protocol Implementations

Abstract The security of a network protocol implementation depends on the finite-state machine that its code realizes. Implementations often deviate from their RFC specifications, and these deviations lead to state-machine vulnerabilities such as authentication bypass. Static extraction of state machines from source code suffers from path explosion, dynamic inference is limited by the inputs it observes, and analyses based on large language models (LLMs) cannot fit a protocol codebase into the context window and miss transitions that depend on internal variables. This paper presents State-inferer, a white-box framework that combines program slicing, LLMs, and model checking to extract and verify protocol state machines. Instead of retrieving code by textual similarity, State-inferer slices the system dependence graph under depth bounds and gives the LLM one code fragment per state transition. From these fragments it builds a state transition system whose transitions carry guards over internal variables, and it specializes RFC security properties into linear temporal logic formulas over this system for checking with nuXmv. We evaluate State-inferer on seven open-source implementations of TLS, IKEv2, and SSH. State-inferer achieves a macro-average strict transition-level F-score of 95.2, compared with 78.9 for the strongest baseline, and uncovers four previously unknown vulnerabilities, all of which have been assigned CVE or CNVD identifiers.