Accurately extracting protocol-state machines (PSMs) from the long, densely written Request-for-Comments (RFC) standards that govern Internet‐scale communication remains a bottleneck for automated security analysis and protocol testing. In this paper, we introduce RFC2PSM, the first large-scale dataset that pairs 1,580 pages of cleaned RFC text with 108 manually validated states and 297 transitions covering 14 widely deployed protocols spanning the data-link, transport, session, and application layers. Built on this corpus, we propose PsmBench, a benchmark that (i) feeds chunked RFC to an LLM, (ii) prompts the model to emit a machine-readable PSM, and (iii) scores the output with structure-aware, semantic fuzzy-matching metrics that reward partially correct graphs.A comprehensive baseline study of nine state-of-the-art open and commercial LLMs reveals a persistent state–transition gap: models identify many individual states (up to $0.82$ F1) but struggle to assemble coherent transition graphs ($\leq 0.38$ F1), highlighting challenges in long-context reasoning, alias resolution, and action/event disambiguation. We release the dataset, evaluation code, and all model outputs as open-sourced, providing a fully reproducible starting point for future work on reasoning over technical prose and generating executable graph structures. RFC2PSM and PsmBench aim to catalyze cross-disciplinary progress toward LLMs that can interpret and verify the protocols that keep the Internet safe.

The IEEE 802.11 family of standards, better known as WiFi, is a widely used protocol utilized by billions of users. Previous works on WiFi formal verification have mostly focused on the four-way handshake and other security aspects. However, recent works have uncovered severe vulnerabilities in functional aspects of WiFi, which can cause information leakage for billions of devices. No formal analysis method exists able to reason on the functional aspects of the WiFi protocol. In this paper, we take the first steps in addressing this gap and present an extensive formal analysis of the functional aspects of the WiFi protocol, more specifically, the fragmentation and the power-save-mode process. To achieve this, we design a novel segment-based formal verification process and introduce a practical threat model (i.e., MAC spoofing) in Tamarin to reason about the various capabilities of the attacker. To this end, we verify 68 properties extracted from WiFi protocol specification, find 3 vulnerabilities from the verification, verify 3 known attacks, and discover 2 new issues. These vulnerabilities and issues affect 14 commercial devices out of 17 tested cases, showing the prevalence and impact of the issues. Apart from this, we show that the proposed countermeasures indeed are sufficient to address the issues. We hope our results and analysis will help vendors adopt the countermeasures and motivate further research into the verification of the functional aspects of the WiFi protocol.

LoRa, as a representative Low-Power Wide-Area Network (LPWAN) technology, can provide long-range communication for battery-powered IoT devices with a 10-year lifetime. LoRa links in practice, however, experience high dynamics in various environments. When the SNR falls below the threshold (e.g., in the building), a LoRa device disconnects from the network. We propose Falcon, which addresses the link dynamics by enabling data transmission for very low SNR or even disconnected LoRa links. At the heart of Falcon, we reveal that low SNR LoRa links that cannot deliver packets can still introduce interference to other LoRa transmissions. Therefore, Falcon transmits data bits on the low SNR link by selectively interfering with other LoRa transmissions. We address practical challenges in Falcon design. We propose a low-power channel activity detection method to detect other LoRa transmissions for selective interference. To interfere with the so-called interference-resilient LoRa, we accurately estimate the time and frequency offsets on LoRa packets and propose an adaptive frequency adjusting strategy to maximize the interference. We implement Falcon, all using commercial off-the-shelf LoRa devices, and extensively evaluate its performance. The results show that Falcon can provide reliable communication links for disconnected LoRa devices and achieves the SNR boundary upto 7.5 dB lower than that of standard LoRa.