I founded and lead Katzenpost, a free software mix network: an anonymous communication network built to resist traffic analysis by global passive adversaries. I designed its protocols and I am by far its largest committer. The design is written up in Echomix: a Strong Anonymity System with Messaging (Infeld, Stainton, Ryge, Hacker, 2025).

• 🕸️ Pigeonhole on Reticulum. Pigeonhole storage replicas on Reticulum meshes (pigeonhole_rns) and a bridge replica that joins the mesh to the mixnet, so one group chat has members on a Reticulum mesh and members on the mixnet, talking through the bridge without knowing it (katzenrns).
• 📟 Mixnet group chat on a handheld. pigeonhole_reticulous: group chat firmware for the LilyGO T-Deck Plus (ESP32-S3) that does its own BACAP encryption and CTIDH-1024 contact vouchers on the device. The CTIDH field arithmetic is hand-written Xtensa MAC16 assembly: 11,422 instructions per field multiply against fiat-crypto's 81,661, about 7× fewer, bit-exact with fiat.
• 📞 hushphone. Group chat with push-to-talk voice for Linux and Android, in Rust and Slint, over the Katzenpost mixnet or a Reticulum mesh (Reticulum-rs, or the Python RNS embedded with PyO3).
• 🐦 Pigeonhole protocols. pigeonhole_protocols: group chat and mixnet services over Pigeonhole storage, as sans-IO state machines in Go, Rust and Python sharing one set of test vectors.
• 🔐 Post-quantum crypto. hpqc: hybrid post-quantum KEMs, NIKEs and signatures for Go and Python: a security-preserving KEM combiner, a NIKE-to-KEM adapter, a hybrid signer, CTIDH, ML-KEM, FrodoKEM, Classic McEliece, NTRU Prime, HQC, and BACAP, our blinding-and-capability scheme. Plus highctidh-rs, Rust bindings to CTIDH-1024.
• 📜 Cryptlib: a Lean cryptography library. It started as a Lean model of hpqc and now does two jobs: real, runnable high-assurance software and protocol simulators, and proofs of security properties of primitives and protocols. Primitives are Lean structures whose fields carry their laws (a NIKE must commute, a KEM must round-trip), so an instance that breaks them cannot be constructed. cryptlib.io · GitHub
• 🧅 Formalizing Sphinx in Lean. The Sphinx packet format in cryptlib, generic over its NIKE or KEM, stream cipher, KDF, MAC and wide-block cipher. Correctness is proved once for any choice of those primitives, and the padding leak later found in Sphinx can no longer be expressed: wrap takes no filler argument. Integrity, wrap-resistance and indistinguishability are formalized, with the steps not yet proved stated as explicit hypotheses.
• 🧮 High assurance in Lean 4. Protocols written in a proof assistant, with security properties in the types: cryptlib (with the Sphinx formalization and part of BACAP), uproar (Noise and PQ Noise), lean_tls, lean_quic, huh (a remote shell on PQ Noise), frank_chat and jam (mixnet group chat clients), paw (an Elm-style GUI library with security laws in its types), tessera (terminal UIs) and cborg (CBOR).

• 🌐 Katzenpost: katzenpost.network · github.com/katzenpost
• 📄 Paper: Echomix: a Strong Anonymity System with Messaging
• 🧪 Cryptlib: cryptlib.io · Formalizing Sphinx in Lean
• ✍️ Blog: sphinx.rs