Protocol state machines skip retrieval: State-inferer slices code per transition for an LLM and reaches a strict F-score of 95.2

The state machine a protocol implementation actually executes can now be recovered transition by transition from source code, with each transition carrying guards over internal variables rather than only the message received. Earlier routes either hit path explosion in static analysis of large programs, saw only behavior reached by test inputs in dynamic learning, or were limited by the LLM context window and missed transitions that depend on internal variables. On seven open-source TLS, IKEv2 and SSH implementations, State-inferer reaches a macro-average strict transition-level F-score of 95.2, against 78.9 for Codex, 77.1 for Claude Code and 46.2 for ProtocolGPT; the skeleton F-scores that ignore guards are 99.2, 88.6, 88.3 and 67.5 respectively.

The code context for each state transition comes from program slicing rather than from chunks retrieved by textual similarity. Similarity retrieval returns code blocks that mention the target state variable but not the cross-function, cross-file call chain, so transition preconditions are dropped and reachability is misjudged. Starting from state-variable assignment nodes, a forward search on the system dependence graph bounded at data-flow depth 8 and control-flow depth 5, followed by a symmetric backward search from each endpoint, yields one fragment per transition from the intersection plus the two endpoints; in the WolfSSL TLS 1.3 handshake, logic spanning 4 functions and about 400 lines is reduced to a 42-line fragment, an 89.5% reduction.

RFC security properties are rewritten automatically into linear temporal logic formulas over concrete implementation variables and checked by exhaustive state-space exploration in nuXmv. RFCs state requirements at the protocol-semantics level without naming any implementation variable, and implementations differ widely in variable naming and state structure, so one property template cannot be reused as is. Across 39 meta-property/implementation pairs and 117 generated formulas over three runs, 109 are equivalent to the expert reference formula, an accuracy of 93.2%; the rest are 4 semantic errors, 2 syntax errors and 2 mapping errors, and syntax and mapping errors are caught mechanically before model checking.

The evaluation covers seven open-source implementations of TLS, IKEv2 and SSH, each limited to the server-side state machine of a fixed release; slicing and nuXmv checking run locally, and analyzing one implementation takes about 18 minutes. The authors propose extending the analysis to deep call chains, complex macros and asynchronous control flow, and automating parts of reference-model construction and property alignment.

Reference models are built by hand and, although two experts annotated independently and reconciled differences, some ambiguity remains; baselines were evaluated only with GLM-5.1, and the default slicing depths were chosen from a sensitivity analysis on the same subjects, though the authors report F is flat around the defaults and larger bounds do not change results. Transition-level matching measures edge-by-edge agreement with the reference model and does not establish trace equivalence or long-run behavioral equivalence.