# Prognosis: Closed-Box Analysis of Network Protocol Implementations

arXiv: https://arxiv.org/abs/2201.02577 · HTML: https://mlsanity.com/paper/2201.02577/

## Key facts

- Cited by 7 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 14 Nov 2021.

## Built on by (most cited first, 7 of 7)

- [Large Language Models for Validating Network Protocol Parsers](https://mlsanity.com/paper/2504.13515/) (2025)
- [Tree-Based Adaptive Model Learning](https://mlsanity.com/paper/2209.00122/) (2022)
- [ALARM: Active LeArning of Rowhammer Mitigations](https://mlsanity.com/paper/2211.16942/) (2022)
- [Conflict-Aware Active Automata Learning (Extended Version)](https://mlsanity.com/paper/2308.14781/) (2023)
- [Conflict-Aware Active Automata Learning](https://mlsanity.com/paper/2310.01003/) (2023)
- [RFSeek and Ye Shall Find](https://mlsanity.com/paper/2509.10216/) (2025)
- [SMT-Based Active Learning of Weighted Automata](https://mlsanity.com/paper/2605.07758/) (2026)

## Abstract (arXiv)

We present Prognosis, a framework offering automated closed-box learning and analysis of models of network protocol implementations. Prognosis can learn models that vary in abstraction level from simple deterministic automata to models containing data operations, such as register updates, and can be used to unlock a variety of analysis techniques -- model checking temporal properties, computing differences between models of two implementations of the same protocol, or improving testing via model-based test generation. Prognosis is modular and easily adaptable to different protocols (e.g., TCP and QUIC) and their implementations. We use Prognosis to learn models of (parts of) three QUIC implementations -- Quiche (Cloudflare), Google QUIC, and Facebook mvfst -- and use these models to analyze the differences between the various implementations. Our analysis provides insights into different design choices and uncovers potential bugs. Concretely, we have found critical bugs in multiple QUIC implementations, which have been acknowledged by the developers.