pith. sign in

arxiv: 2605.01721 · v1 · submitted 2026-05-03 · 💻 cs.CR · cs.LO

Automated Channel Fault Analysis with Tofu

Jacob Ginesin , Max von Hippel , Cristina Nita-Rotaru This is my paper

Pith reviewed 2026-05-10 15:26 UTC · model grok-4.3

classification 💻 cs.CR cs.LO
keywords channel fault analysisLTL protocol specificationsattack trace synthesisdistributed protocol verificationexhaustive state-space searchTCP security analysis
0
0 comments X

The pith

Tofu automates detection or refutation of channel fault attacks on any protocol specified in linear temporal logic.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

Distributed protocols run over channels that may be faulty or attacker-controlled, allowing arbitrary insertion, dropping, replay, or reordering of messages. Prior verification efforts usually build custom proofs for each protocol under its own fault model. This work instead supplies a general automated method that accepts an arbitrary linear temporal logic description of a protocol and exhaustively searches the combined state space of the protocol and all possible channel faults. The resulting tool either produces a concrete attack trace or proves that no such attack exists. The method is applied to the TCP protocol as a demonstration.

Core claim

Tofu performs sound and complete analysis by exhaustively enumerating the state space formed by an LTL protocol specification together with a channel model that permits message insertion, dropping, replay, and reordering, thereby either synthesizing fault-based attack traces or establishing their absence.

What carries the argument

Exhaustive state-space search over the product of the protocol's LTL states and the channel fault behaviors.

If this is right

  • Security claims against channel faults can be established automatically rather than by hand for any LTL-encoded protocol.
  • Attack traces become available as explicit counterexamples when faults succeed.
  • Absence of attacks can be certified for protocols whose state space is tractable, as shown for TCP.
  • The same exhaustive-search approach applies uniformly across different protocols without redefining the fault model each time.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • If encoding overhead stays low, the technique could be applied to many existing protocol descriptions that are already close to temporal logic.
  • Similar exhaustive product constructions might be reused for fault models other than channels.
  • For very large protocols the method would require state-space reduction techniques to remain practical.

Load-bearing premise

Any protocol of interest can be faithfully written as a linear temporal logic formula whose combined state space with channel faults remains small enough to explore completely.

What would settle it

A concrete protocol and channel fault attack that Tofu reports as absent when the attack is known to exist, or a practical protocol whose state space causes Tofu to fail to terminate.

Figures

Figures reproduced from arXiv: 2605.01721 by Cristina Nita-Rotaru, Jacob Ginesin, Max von Hippel.

Figure 1
Figure 1. Figure 1: A high-level overview of the Tofu workflow We now describe how the formal gadgets of Section 3 are realized within Promela. Channel parsing. Tofu begins by parsing the user-provided Promela model to extract all channel declarations, including their names, buffer sizes, and message types. Tofu supports both standard channels (e.g., chan c = [8] of {int, int, int}) and indexed multi-channels (e.g., chan c[N]… view at source ↗
read the original abstract

Distributed protocols are the linchpin of the modern internet, underpinning every internet service. This has in turn motivated a massive body of research ensuring the security, reliability, and performance of distributed protocols. In these works, a wide-ranging assumption is that distributed protocols operate over faulty or attacker-controlled channels, where messages can be arbitrarily inserted, dropped, replayed, or reordered. Formal verification work targeting distributed protocols typically defines its own notion of faulty or malicious channels, then constructively proves their protocol is correct with respect to it. In this work we take a fundamentally different approach: we develop a rigorous methodology for automatically conducting channel fault analysis on distributed protocols, and we introduce Tofu, a generalizable tool that implements our methodology. Tofu provides sound, complete analysis, synthesizing channel fault-based attack traces on arbitrary linear temporal logic (LTL) protocol specifications or proving the absence of such through an exhaustive state-space search. We demonstrate the applicability of Tofu by employing it to study TCP.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 1 minor

Summary. The paper introduces Tofu, a tool implementing a methodology for automated channel fault analysis on distributed protocols. Protocols are encoded as LTL specifications; Tofu then performs exhaustive state-space search over the combined protocol-plus-channel model to either synthesize attack traces arising from channel faults (insertions, drops, replays, reorders) or prove their absence. The central claim is that the analysis is sound and complete for arbitrary LTL specifications. Applicability is demonstrated via a TCP case study.

Significance. If the soundness and completeness claims hold with a rigorously justified finite state space, the work would provide a useful automated complement to existing manual or ad-hoc channel-fault models in protocol verification. The reliance on standard LTL model checking is a strength that could enable reuse of existing checkers, but the practical scope is limited by the need for finite bounds on channels and data domains.

major comments (2)
  1. [Abstract] Abstract: the claim that Tofu 'provides sound, complete analysis ... through an exhaustive state-space search' for 'arbitrary' LTL protocol specifications is load-bearing for the entire contribution, yet the abstract (and, on the basis of the supplied text, the manuscript) supplies no derivation, proof sketch, or description of how the channel model is encoded in LTL or how the combined state space is rendered finite. Without explicit bounds on channel contents, message values, or queue lengths, the search cannot be exhaustive for typical distributed protocols.
  2. [TCP Case Study] TCP case study: the manuscript must demonstrate that any bounds imposed on the channel model are sufficient to capture all relevant fault behaviors for TCP; otherwise the absence proofs are only relative to the chosen bound and the completeness claim does not hold.
minor comments (1)
  1. [Abstract] The abstract would benefit from a single sentence stating the model checker or encoding library employed, so readers can immediately assess the practical implementation.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful review and for highlighting the need to strengthen the justification of our soundness and completeness claims. We address each major comment below and will revise the manuscript to incorporate the requested clarifications and justifications.

read point-by-point responses

  1. Referee: [Abstract] Abstract: the claim that Tofu 'provides sound, complete analysis ... through an exhaustive state-space search' for 'arbitrary' LTL protocol specifications is load-bearing for the entire contribution, yet the abstract (and, on the basis of the supplied text, the manuscript) supplies no derivation, proof sketch, or description of how the channel model is encoded in LTL or how the combined state space is rendered finite. Without explicit bounds on channel contents, message values, or queue lengths, the search cannot be exhaustive for typical distributed protocols.

    Authors: We agree that the abstract and current manuscript text do not supply a derivation or proof sketch for the finiteness argument. The methodology relies on a finite-state encoding in which the channel is modeled as a bounded queue (maximum length K) whose contents are drawn from a finite message domain; the combined system is then explored exhaustively by an off-the-shelf LTL model checker. Soundness holds because every trace in the bounded model is a valid execution under the fault semantics; completeness holds relative to the chosen bounds. We will revise the abstract to qualify the claim as applying to bounded channel models, add an explicit description of the LTL channel encoding and the bounding parameters in Section 3, and include a short proof sketch showing that the state space is finite and that the search is exhaustive within those bounds. revision: yes

  2. Referee: [TCP Case Study] TCP case study: the manuscript must demonstrate that any bounds imposed on the channel model are sufficient to capture all relevant fault behaviors for TCP; otherwise the absence proofs are only relative to the chosen bound and the completeness claim does not hold.

    Authors: We accept that the current case-study presentation does not contain an explicit argument that the chosen bounds are sufficient. In the revised manuscript we will add a dedicated subsection to the TCP evaluation that (1) states the concrete bounds used (queue length 4, sequence-number domain reduced to 8 values while preserving modulo-2^32 wrap-around behavior via abstraction), (2) provides a short argument that any fault sequence requiring a longer queue or larger domain is observationally equivalent to one within the bound because of TCP's retransmission and cumulative-ACK rules, and (3) reports a small sensitivity experiment confirming that increasing the bounds does not produce additional attack traces. This will make the absence results hold for all relevant TCP fault behaviors. revision: yes

Circularity Check

0 steps flagged

No circularity; Tofu implements standard LTL model checking without self-referential reductions

full rationale

The paper describes Tofu as a tool that encodes protocols in LTL and performs exhaustive state-space search to synthesize attack traces or prove their absence. No equations, fitted parameters, or load-bearing self-citations appear in the abstract or described methodology that would reduce the soundness/completeness claim to an input by construction. The approach relies on established model-checking techniques rather than any of the enumerated circular patterns such as self-definitional quantities, renamed predictions, or ansatzes smuggled via prior self-work. Practical bounds on state spaces are an implementation detail of the encoding, not a derivation that equates outputs to inputs.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The abstract relies on the standard assumption that LTL can express the relevant safety and liveness properties of distributed protocols and that model-checking techniques can be extended to enumerate channel faults. No free parameters or invented physical entities are mentioned.

axioms (2)
  • domain assumption Linear temporal logic is an adequate specification language for the safety and liveness properties of the distributed protocols under study.
    Invoked when the paper states that Tofu operates on arbitrary LTL protocol specifications.
  • domain assumption Exhaustive state-space search over the product of protocol and channel behaviors is feasible and terminates.
    Required for the claim of completeness via exhaustive search.

pith-pipeline@v0.9.0 · 5468 in / 1346 out tokens · 30164 ms · 2026-05-10T15:26:57.396638+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

27 extracted references · 27 canonical work pages

  1. [1]

    Automatic synthesis of distributed protocols

    Rajeev Alur and Stavros Tripakis. Automatic synthesis of distributed protocols. SIGACT News, 48(1):55–90, March 2017

    work page 2017

  2. [2]

    Scapy: Explore the net with new eyes

    Philippe Biondi. Scapy: Explore the net with new eyes. Talk at T2’05 Security Conference, 2005.https://scapy.net/

    work page 2005

  3. [3]

    An efficient cryptographic protocol verifier based on Prolog rules

    Bruno Blanchet. An efficient cryptographic protocol verifier based on Prolog rules. In14th IEEE Computer Security Foundations Workshop (CSFW-14), pages 82–96. IEEE, 2001

    work page 2001

  4. [4]

    Formal Protocol Verification Ap- plied

    Bruno Blanchet. CryptoVerif: A computationally sound mechanized prover for cryptographic protocols. InDagstuhl Seminar “Formal Protocol Verification Ap- plied”, October 2007

    work page 2007

  5. [5]

    packetdrill: Scriptable network stack testing, from sockets to packets

    Neal Cardwell, Yuchung Cheng, Lawrence Brakmo, Matt Mathis, Barath Ragha- van, Nandita Dukkipati, Hsiao keng Jerry Chu, Andreas Terzis, and Tom Herbert. packetdrill: Scriptable network stack testing, from sockets to packets. In2013 USENIX Annual Technical Conference (USENIX ATC 13), pages 213–218, San Jose, CA, June 2013. USENIX Association

    work page 2013

  6. [6]

    Layered formal verification of a tcp stack

    Guillaume Cluzel, Kyriakos Georgiou, Yannick Moy, and Clément Zeller. Layered formal verification of a tcp stack. In2021 IEEE Secure Development Conference (SecDev), pages 86–93, 2021

    work page 2021

  7. [7]

    Wesley M. Eddy. Transmission control protocol (TCP). RFC 9293, August 2022

    work page 2022

  8. [8]

    A formal analysis of SCTP: Attack synthesis and patch verification

    Jacob Ginesin, Max von Hippel, Evan Defloor, Cristina Nita-Rotaru, and Michael Tüxen. A formal analysis of SCTP: Attack synthesis and patch verification. In33rd USENIX Security Symposium (USENIX Security 24), pages 3099–3116, Philadel- phia, PA, August 2024. USENIX Association

    work page 2024

  9. [9]

    Lorch, Bryan Parno, Michael L

    Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R. Lorch, Bryan Parno, Michael L. Roberts, Srinath Setty, and Brian Zill. Ironfleet: proving practical distributed systems correct. InProceedings of the 25th Symposium on Operating Systems Principles, SOSP ’15, page 1–17, New York, NY, USA, 2015. Association for Computing Machinery. 16 J. Ginesin et al

    work page 2015

  10. [10]

    Network emulation with NetEm.Proceedings of Linux Con- ference Australia (linux.conf.au), April 2005

    Stephen Hemminger. Network emulation with NetEm.Proceedings of Linux Con- ference Australia (linux.conf.au), April 2005

    work page 2005

  11. [11]

    Holzmann

    Gerard J. Holzmann. The model checker SPIN.IEEE Transactions on Software Engineering, 23(5):279–295, May 1997

    work page 1997

  12. [12]

    Springer International Publishing, Cham, 2019

    Chiao Hsieh and Sayan Mitra.Dione: A Protocol Verification System Built with Dafny for I/O Automata, volume 11918 ofLecture Notes in Computer Science, page 227–245. Springer International Publishing, Cham, 2019

    work page 2019

  13. [13]

    Addison-Wesley, 2002

    Leslie Lamport.Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, 2002

    work page 2002

  14. [14]

    Lynch.Distributed Algorithms

    Nancy A. Lynch.Distributed Algorithms. Morgan Kaufmann, 1996

    work page 1996

  15. [15]

    The TAMARIN prover for the symbolic analysis of security protocols

    Simon Meier, Benedikt Schmidt, Cas Cremers, and David Basin. The TAMARIN prover for the symbolic analysis of security protocols. InComputer Aided Veri- fication (CAV 2013), volume 8044 ofLecture Notes in Computer Science, pages 696–701. Springer, 2013

    work page 2013

  16. [16]

    Adversarial Robustness Verifica- tion and Attack Synthesis in Stochastic Systems

    Lisa Oakley, Alina Oprea, and Stavros Tripakis. Adversarial Robustness Verifica- tion and Attack Synthesis in Stochastic Systems . In2022 2022 IEEE 35th Com- puter Security Foundations Symposium (CSF) (CSF), pages 380–395, Los Alami- tos, CA, USA, August 2022. IEEE Computer Society

    work page 2022

  17. [17]

    Automated attack synthesis by extracting finite state ma- chines from protocol specification documents

    Maria Leonor Pacheco, Max von Hippel, Ben Weintraub, Dan Goldwasser, and Cristina Nita-Rotaru. Automated attack synthesis by extracting finite state ma- chines from protocol specification documents. In2022 IEEE Symposium on Secu- rity and Privacy (SP), pages 51–68, 2022

    work page 2022

  18. [18]

    The temporal logic of programs

    Amir Pnueli. The temporal logic of programs. In18th Annual Symposium on Foundations of Computer Science (FOCS), pages 46–57. IEEE, 1977

    work page 1977

  19. [19]

    Transmission control protocol

    Jon Postel. Transmission control protocol. RFC 793, September 1981

    work page 1981

  20. [20]

    Prasad Sistla, Moshe Y

    A. Prasad Sistla, Moshe Y. Vardi, and Pierre Wolper. The complementation prob- lem for Büchi automata with applications to temporal logic.Theoretical Computer Science, 49(2–3):217–237, 1987

    work page 1987

  21. [21]

    Vardi and Pierre Wolper

    Moshe Y. Vardi and Pierre Wolper. An automata-theoretic approach to automatic program verification. InProceedings of the 1st Symposium on Logic in Computer Science (LICS), pages 332–344. IEEE, 1986

    work page 1986

  22. [22]

    Auto- mated attacker synthesis for distributed protocols

    Max von Hippel, Cole Vick, Stavros Tripakis, and Cristina Nita-Rotaru. Auto- mated attacker synthesis for distributed protocols. In Antonio Casimiro, Frank Ortmeier, Friedemann Bitsch, and Pedro Ferreira, editors,Computer Safety, Reli- ability, and Security (SAFECOMP 2020), volume 12234 ofLecture Notes in Com- puter Science, Cham, 2020. Springer

    work page 2020

  23. [23]

    Modeling message queues in TLA+

    Hillel Wayne. Modeling message queues in TLA+. Blog post, October 2018. Accessed: 2026-03-12

    work page 2018

  24. [24]

    ϕholds at positioniinσ

    James R. Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock, Xi Wang, Michael D. Ernst, and Thomas Anderson. Verdi: a framework for implementing and formally verifying distributed systems. InProceedings of the 36th ACM SIG- PLAN Conference on Programming Language Design and Implementation, PLDI ’15, page 357–368, New York, NY, USA, 2015. Association for ...

    work page 2015

  25. [25]

    Becausen≤ℓand|b| ≤ℓare bounded, infinite mutation without eventually reachingn= 0or|b|= 0is impossible

    State-mutatingtransitionsstrictlyandmonotonicallydecreasefiniteresources: the consume counternis decremented upon observing/dropping, and the buffer size|b|is decremented upon replaying. Becausen≤ℓand|b| ≤ℓare bounded, infinite mutation without eventually reachingn= 0or|b|= 0is impossible

    work page

  26. [26]

    An infinite sequence ofPasstransitions remains in a non-Endstate forever, thus never satisfying thedonelabel

    The non-mutating transitions (Passskip(c)self-loops) maintain the current state. An infinite sequence ofPasstransitions remains in a non-Endstate forever, thus never satisfying thedonelabel

    work page

  27. [27]

    Once a gadget transitions toEnd, the only available transition is theEnd τ − → Endself-loop

    TheTerminateorEmptytransitions lead strictly toEnd. Once a gadget transitions toEnd, the only available transition is theEnd τ − → Endself-loop. Therefore, to satisfydoneinfinitely often, the gadget must reach theEndstate, effectively exhausting its fault injection capabilities. No cyclic livelock satisfying the property exists. Theorem 7 (Composability)....

    work page