Blog

• Introduction to Pigeonhole Protocol
• Formalizing Sphinx in Lean
• Katzenpost threat model document
• Mixnet Literature Overview
• hpqc - hybrid post quantum cryptography library
• Katzenpost at 37C3
• Audio Engineering Considerations for a Modern Mixnet
• Website Relaunch and migration to Hugo
• Monthly News Update (May 2019)
• Monthly News Update (April 2019)
• Rustification
• Monthly News Update (Nov 2018)
• Monthly News Update (Feb 2018)

Introduction to Pigeonhole Protocol

Pigeonhole is a protocol for asynchronous, unlinkable communication. Without a read capability, no one can tell which messages belong together, and sender and reader need not be online at the same time. That second property is the only reason Pigeonhole stores anything. Our paper, Echomix: a Strong Anonymity System with Messaging, and Understanding Pigeonhole have the details. This post treats Pigeonhole as an abstraction that does not depend on the network beneath it: what it is, what it guarantees, what we build with it, and the two networks it now runs on.

What Pigeonhole is

A Pigeonhole channel is a sequence of boxes: fixed-size ciphertexts, each signed and named by a Box ID. Two capabilities govern it. The write capability writes boxes and derives the read capability; the read capability finds, verifies and decrypts them. A channel has one writer and any number of readers, and two one-way channels make a two-way one.

Boxes are immutable, with one exception: tombstones. The holder of the write capability can replace a box with a tombstone, an empty ciphertext with a valid signature over it, which deletes the box. That is a feature.

Box indexes come from a KDF ratchet, which moves forward but not backward. A read capability that starts at index n reaches box n and every box after it, never one before. You can therefore share a channel from now on without sharing its history.

Storage replicas verify, store and forward boxes; they cannot read them. They keep the current and the previous replica epoch, a week each, so a box lives one to two weeks before it is garbage-collected. Anything that must last, such as a ticket tracker, a calendar or revision control, belongs elsewhere.

What it guarantees, and against whom

• Confidential: only holders of the read capability can decrypt a box.
• Authentic: a box that verifies was written by the holder of the write capability. That is a key, not a person: whoever holds the write capability is the author.
• Unlinkable: without the read capability, no one, the replicas included, can tell which boxes belong to one channel.

Who learns which node wrote or read a box depends on the network. On the mixnet, no one does: not the replica, not the courier that relays the query, not a global observer of the network. On an open mesh, the replica a node talks to sees which boxes it writes and fetches, and when; anyone may run a replica, and a network observer sees which node talks to which replica.

BACAP, the scheme beneath the boxes, keeps contents and linkage safe even from a quantum adversary, but its signatures are Ed25519, so such an adversary could forge a write into a box whose ID it has seen. A channel has no post-compromise security of its own: a leaked capability works until the participants move to a fresh channel.

What we build with it

Chat. For one-on-one chat, Alice and Bob each write a channel and give the other its read capability. In group chat every member writes their own channel and reads everyone else’s; messages are ordered per author, with no global order. Our group chat protocol is katzenqt1, in pigeonhole_protocols, and these clients speak it, so they all share groups:

• katzenqt: Qt desktop client
• hushphone: Rust and Slint, push-to-talk voice messages, Linux and Android, over the mixnet or a Reticulum mesh
• jam: Lean terminal client
• frank_chat: Lean 4 client with security oriented dependent types
• katzenrns: Python client for a Reticulum mesh
• pigeonhole_reticulous: group chat on the LilyGO T-Deck Plus, over a Reticulum mesh

Replicated state machines. Any application that is a fold over append-only events fits: each participant publishes events on their own channel, and every client computes state = fold(events). Voting, ephemeral shared documents, sensor aggregation and incident logs all qualify, provided events are small, order matters only per author, and the data may expire. A single-writer channel gives each event exactly one author, which is the actor uniqueness that Conflict-free Replicated Data Types (CRDTs) assume, so CRDT state converges whatever the order of arrival. A late joiner who cannot replay expired events takes a snapshot of an existing member’s state over a one-shot channel and merges it; CRDT merges are idempotent, so overlap is harmless. Tallying votes looks like this (illustrative only: the Rust prototype on the crdts crate has been removed from thin_client):

let mut tally: Map<SlotId, MVReg<Vote, Actor>, Actor> = Map::new();
for event in group.receive_from_all_timeout(poll_deadline).await? {
    tally.apply(event.op); // same result in any order
}

Where it runs

Pigeonhole meets the network at the box: write a box, read a box, by Box ID. The Katzenpost mixnet and Reticulum are two bindings of that one interface. Everything above it, BACAP and katzenqt1 included, is shared, so every Pigeonhole application runs on either. On the mesh, the replica is replica_rns, and the specification has the details.

* Full replication came with pigeonhole_rns PR #6, now merged; sharding is kept for the future closed mesh of the replica specification.

We timed bare box operations, with no chat client in the way: write three boxes to a fresh channel one after another, read them back at once (the first read), then read them again. Figures are cumulative seconds, the median of five runs on 5 November 2026, with the range in brackets.

The mixnet client was the Python thin client on its own kpclientd, with the default ARQ: each operation is two round trips over five-hop Sphinx routes (the Pigeonhole ARQ), and a read retries until the box is there. The mesh client was pigeonhole_rns, over TCP to a replica on the same machine and to the namenlos bridge replica, 145 ms away. The mesh figures exclude the 5 to 6 seconds Reticulum took to set up the Link, and are rounded up to the client’s 50 ms polling interval.

A replica can also be a bridge to a Katzenpost storage replica, so mesh users and mixnet users share groups. We have tested exactly that: katzenrns users on a mesh chatting with hushphone users on namenlos through the namenlos bridge. Since a box is the same object on every network, a mesh with bridges to several mixnets joins those mixnets together; the bridge rules for that are landing now.

What comes next

• Prometheus: uploading metrics to a Prometheus aggregator anonymously over the mixnet.
• NNCP: sending and receiving files anonymously through existing NNCP infrastructure.
• Tally: transparent voting on the broadcast API. Members publish ballots visible to the group and may change them; since each channel has one writer, no one else can. A CRDT register keeps concurrent ballots side by side rather than dropping one, and katzenqt1 already reserves message types for it. A meeting scheduler follows: the options are time slots, the ballots availability.

Conclusion

The abstraction is the point. Pigeonhole is defined at the box, so networks plug in underneath it, and every application above, from chat to Tally, works on each of them.

That makes the Katzenpost mixnet more powerful with Reticulum than without it. The mixnet keeps what only it gives: metadata privacy against a global observer and hybrid post-quantum links. Bridged to meshes, it gains reach, to places with radio and no internet, and speed, a fifth of a second per box instead of twenty-five seconds, for the members who can accept a mesh’s weaker metadata privacy. And a mesh can join several mixnets together, so that the users of each share groups.

Formalizing Sphinx in Lean

Lean Weekly News scooped this post. Their verification section already reports that cryptlib’s Sphinx packets are binary compatible with the Katzenpost Go implementation, hybrid X25519 and ML-KEM-768 KEM Sphinx included, and links to katzenpost/cryptlib, cryptlib.io and the Reservoir package page. What follows is the longer story.

In Lean, a field of a structure type can be a proposition. That one feature changes how a cryptography library can be written.

In a language like Rust a trait is an empty husk that only declares function signatures. It’s still a useful contract: all instances must define the trait’s methods. In Lean we describe a primitive generically with a structure whose fields hold functions and data types, which is how Rust or Go would do it too. Dependent types let us go a step further: a field can also be a proposition about the other fields. Here is cryptlib’s NIKE (non-interactive key exchange) type, abridged:

structure NIKE where
  PrivateKey   : Type
  PublicKey    : Type
  SharedSecret : Type
  -- ...
  Safe : PublicKey → Prop
  derivePublicKey : PrivateKey → PublicKey
  groupAction : PrivateKey → {pk : PublicKey // Safe pk} → SharedSecret
  -- ...
  derive_safe : ∀ sk, Safe (derivePublicKey sk)
  -- ...
  commutes : ∀ sk₁ sk₂,
    groupAction sk₁ ⟨derivePublicKey sk₂, derive_safe sk₂⟩
      = groupAction sk₂ ⟨derivePublicKey sk₁, derive_safe sk₁⟩

Every NIKE instance must supply a proof of commutes, so a NIKE whose group operation is not commutative cannot be constructed. The KEM (key encapsulation mechanism) type likewise carries its round trip correctness as a field. And these proofs compose: when the hashed ElGamal NIKE-to-KEM adapter builds a KEM from a NIKE, it cannot construct the KEM without filling in that correctness field, which it does using the NIKE’s commutes. The theorem “a lawful NIKE gives a lawful KEM” never has to be stated separately, and nobody can forget to apply it.

This post is about taking that idea up a level, from primitives to a protocol. I recently used Claude Code to formalize the Sphinx packet format in Lean, generic over its NIKE or KEM, stream cipher, KDF, MAC and wide-block cipher. Correctness is proved once over any choice of those primitives, and a padding leak that later researchers found in Sphinx becomes impossible to express in the type. The security proofs are the harder part, and I’ll be honest below about what is and isn’t proved yet. Links for background on Sphinx are collected at the end.

Background: Katzenpost’s Sphinx and HPQC

The Katzenpost mixnet uses a Go implementation of Sphinx that is generic over a NIKE, plus a KEM Sphinx variant that is generic over a KEM. Both can be hybrid post quantum. The NIKE and KEM interfaces come from HPQC, our hybrid post quantum cryptography library, which also provides a NIKE combiner, a KEM combiner, and a NIKE to KEM adapter (hashed ElGamal construction), so that for example X25519 can be combined with ML-KEM into a hybrid KEM. cryptlib started as a Lean model of HPQC.

Why a structure and not a type class

Lean programmers may wonder why NIKE is a structure and not a type class, since that is what Mathlib would do. The two are closer than they look. As Functional Programming in Lean puts it, “every type class defines a structure that has a field for each overloaded operation”, and the difference is that a structure’s accessors take the structure value as an explicit parameter while a type class method takes it as an instance implicit, which Lean finds by searching on the type. That search works for Mathlib because each type has one canonical algebraic structure: there is one Group ℤ. Our primitives all operate on ByteArray, so there is no canonical “the NIKE for ByteArray” to find, and which NIKE or KEM is in play is a runtime value chosen by name, not a type. So cryptlib passes the structure explicitly, and its proposition fields travel with the value. The book’s chapter on structures is a good starting point if structures with function and proof fields are new to you.

How cryptlib got here

A couple of years ago I started the Lean theorem prover meetup at the Noisebridge hacker space in San Francisco, a weekly study group with some very smart attendees. On the Lean Zulip I ended up chatting with Mario Carneiro about program verification and modeling cryptography in Lean, and at some point he posted a minimal KEM type whose struct contains a proposition field with the KEM completeness theorem: everything the KEM encapsulates can be decapsulated.

At the time I didn’t want yet another symbolic modeler for cryptography. I was already using Proverif, which works great and automates finding security flaws, and a Lean model would have none of that automation. I didn’t yet understand that what Mario was showing me is much more than a symbolic model.

So I wrote Lean implementations of a few HPQC constructions: the NIKE to KEM adapter, the NIKE combiner, the KEM combiner. About two years later, at the Utrecht University Summer Lean Theorem Prover class, I came back to them and wrote theorems the conventional way, as separate statements:

• A NIKE is lawful if its group operation is commutative.
• A KEM is lawful if it can decapsulate everything it encapsulates.
• Given a lawful NIKE, the NIKE to KEM adapter produces a lawful KEM.

Then I realized that the first two belong inside the types, as the commutes and completeness fields shown in the introduction, and that the third then disappears: the adapter cannot construct its KEM without proving completeness from the NIKE’s commutes. Those proposition fields are proof obligations for every instance, which is the point. Only valid instances can be expressed at all.

From primitives to Sphinx

I asked Claude Code to write a Sphinx implementation in Lean, verified against test vectors shared with the Katzenpost Sphinx implementation. The formalization went through roughly four phases:

1. Implement Sphinx as a static construction with specific primitives.
2. Try to prove the Sphinx paper’s security properties, and fail: the proofs drown in the complexity of the individual primitives.
3. Rewrite Sphinx over generic dependent types for each primitive in the construction: NIKE/KEM, stream cipher, KDF, MAC, wide-block cipher.
4. Try again: correctness is now proved outright, over any NIKE or KEM and any choice of the other primitives. The other three properties are formalized, with the steps that aren’t proved yet isolated as explicit hypotheses.

The composition benefit from the introduction showed up at protocol scale as a reduction in proof obligations. Proving anything about the static construction with, say, the AEZ wide-block cipher meant also reasoning about AEZ. With a generic wide-block cipher type whose struct carries an encryption/decryption completeness proposition, the Sphinx proofs only need that one proposition and never look inside AEZ.

Sphinx Security Properties

Section 4 of the Sphinx paper frames Sphinx’s security in terms of four properties. The first three come from Camenisch and Lysyanskaya’s formal treatment of onion routing, and in section 4.4 the paper proves their fourth property, “security”, together with Sphinx’s own requirement that forward and reply messages be indistinguishable:

1. correctness
2. integrity
3. wrap-resistance
4. security, and indistinguishability of forward and reply messages

First, correctness. A correctness theorem for Sphinx is very similar to the KEM correctness theorem we discussed above. It says that we can fully unwrap Sphinx packets that we create such that the final payload is equal to the original encapsulated payload.

Second, integrity. The Sphinx paper says that even an adversary who knows every mix node’s private key can’t forge a header that a whole chain of honest nodes will accept, except with negligible probability. In practice each hop checks its own MAC over the header, and the claim is that nobody can build a public key, encrypted header and MAC that pass the check at every one of the hops unless the packet was built honestly.

Third, wrap resistance. This means the adversary cannot be given a specific target Sphinx packet and produce a new Sphinx packet which unwraps to the target Sphinx packet, even if the adversary gets to choose the mix node’s private key.

Fourth, security and indistinguishability. An adversary who controls every mix node except one, and chooses the messages, destinations and paths, cannot tell which of two packets entered the honest node, and in particular cannot tell whether a packet is a forward message or a reply.

It turns out this four property framework is not the end of the story. Breaking and (Partially) Fixing Provably Secure Onion Routing showed that these properties don’t actually imply ideal onion routing, so even complete proofs of all four wouldn’t show that Sphinx is secure. The later papers replace them with layer unlinkability and tail indistinguishability properties, which do imply it. Integrity and wrap-resistance no longer appear as separate properties, and forward/reply indistinguishability is built into the new unlinkability games.

Sphinx type

Here is the KEM Sphinx unwrap operation at one mix. A packet is a header (α, β, γ) and a payload δ: α is the KEM ciphertext, β the encrypted routing info, γ the MAC, δ the payload.

The four circles are exactly the primitive fields of the Sphinx type below. Decapsulate KEM is kem, KDF is kdf, Verify MAC is mac, SPRP Decrypt is the wide-block cipher, and the cipher stream that is XORed over the routing info comes from stream. NIKE Sphinx replaces the decapsulation with a Diffie-Hellman operation plus the blinding step that derives α′, and is otherwise the same circuit.

Below is our Sphinx type, abridged to its primitives and the two functions the discussion needs. The full definition is in Interface.lean.

structure Sphinx where
  State : Type
  PrivateKey : Type
  Command : Type
  -- ...
  geometry : Geometry.Geometry

  /-- Wide-block cipher for the payload, MAC for header integrity, KDF for per-hop keys, stream
  cipher for routing-info encryption. -/
  cipher : Cryptlib.Primitives.WideBlockCipher.WideBlockCipher
  mac    : Cryptlib.Primitives.MAC.MAC
  kdf    : Cryptlib.Primitives.KDF.KDF
  stream : Cryptlib.Primitives.StreamCipher.StreamCipher

  /-- Unused routing-info slots are filled with random bytes drawn from `State`. -/
  wrap : List Types.PathHop → Vector UInt8 geometry.forwardPayloadLength →
    EStateM String State (Vector UInt8 geometry.packetLength)

  unwrap : PrivateKey → (pkt : ByteArray) →
    Except String (Option ByteArray × Vector UInt8 32 × List Command × Option (Vector UInt8 pkt.size))
  -- ...

  /-- Completeness: `unwrap` undoes `wrap` on the forward payload, given no hop's `commands`
  contains `null` or `nextNodeHop` and the last hop carries no `surbReply`. -/
  unwrap_complete : ∀ (path : List Types.PathHop) (privKeys : List PrivateKey)
      (payload : Vector UInt8 geometry.forwardPayloadLength) (st : State)
      (pkt : Vector UInt8 geometry.packetLength) (st' : State),
    -- ... well-formedness hypotheses ...
    wrap path payload st = .ok pkt st' →
    unwrapChainAux unwrap privKeys (ofVector pkt) = .ok (some (ofVector payload))

  -- `indistinguishable` and `integrity`: the paper's §4.4 and §4.2 arguments, discussed below.

Notice that wrap takes no filler argument (nor does newSURB, elided above). Earlier versions took the filler for unused hops from the caller, and nothing in the type stopped a caller from passing zeros. That is exactly the path length leak found in the “Breaking and (Partially) Fixing” paper: a recognizable padding pattern tells the last mix how long the path was. The Katzenpost Go implementation already fills these bytes with randomness. The Lean wrap draws the filler from its own random State instead, so a zero filler can no longer be expressed. That’s the dependent type thesis again: fix it in the type, and every instance gets the fix.

Now an honest caveat about the security fields. unwrap_complete really is a proof obligation on each instance: it talks about that instance’s own wrap and unwrap, so an instance with a broken wrap cannot be constructed. integrity and indistinguishable are different. They have default values, proved once, about an abstract model of the paper’s games (Integrity.Sys, Indistinguishability.Sys) that never mentions this instance’s wrap or unwrap. So today they record the paper’s arguments inside the type, but they don’t yet constrain the instance the way unwrap_complete does. They also still rest on explicit hypotheses:

• Integrity assumes the step the paper itself only calls “a careful, but straightforward, calculation”, and assumes the hardness of the paper’s “Problem P”.
• Indistinguishability reduces the first hybrid step to DDH, but takes the other two steps as hypotheses, and its game doesn’t let the adversary query the honest node. The Gap Diffie-Hellman proof shows that once the adversary can query it, DDH isn’t enough and the Gap Diffie-Hellman assumption is needed.

We wanted every security property to live in a struct proposition field, and wrap-resistance and envelope independence only hold for NIKE Sphinx. So the Sphinx type has two sub-types, and only NIKESphinxScheme carries them:

structure NIKESphinxScheme extends Cryptlib.Protocols.Sphinx.Interface.Sphinx where
  nike : NIKE
  Envelope : Type
  [envelopeDecEq : DecidableEq Envelope]
  /-- The header's group element. -/
  parseEnvelope : Vector UInt8 geometry.packetLength → Envelope
  /-- The blinding factor space. -/
  Factor : Type
  [factorFintype : Fintype Factor]
  [factorSampleable : SampleableType Factor]
  blind : Factor → Envelope → Envelope
  /-- Wrap-resistance (§4.3): if blinding `e` is a bijection, a uniform factor hits `target` with
  probability `1/|Factor|`. -/
  wrap_resistant : ∀ (e target : Envelope), Function.Bijective (blind · e) →
      Pr{let x ← ($ᵗ Factor) >>= fun b => pure (decide (blind b e = target))}[x = true] =
        (Fintype.card Factor : ℝ≥0∞)⁻¹ :=
    fun _ target hbij => uniformHit_eq hbij target
  /-- The envelope depends only on the starting `State`, not on the path or payload. -/
  envelope_indep : ∀ (hop0 hop1 : Types.PathHop) (rest0 rest1 : List Types.PathHop)
      (payload0 payload1 : Vector UInt8 geometry.forwardPayloadLength) (st : State)
      (pkt0 pkt1 : Vector UInt8 geometry.packetLength) (st0' st1' : State),
    wrap (hop0 :: rest0) payload0 st = .ok pkt0 st0' →
    wrap (hop1 :: rest1) payload1 st = .ok pkt1 st1' →
    parseEnvelope pkt0 = parseEnvelope pkt1

and

structure KEMSphinxScheme extends Cryptlib.Protocols.Sphinx.Interface.Sphinx where
  kem : KEM

KEM Sphinx has no blinding step, so it is not wrap-resistant: a holder of the node’s private key can decapsulate any ciphertext, compute the header keystream, and craft routing info that unwraps to any target. That is a theorem in the repository (unwrapKEM_routingInfoBlock_not_wrap_resistant), not a field: a proposition field is a guarantee every instance must prove, and “an attack exists” guarantees nothing.

The caveat about integrity and indistinguishable also applies to wrap_resistant: it holds for any blind whenever blinding is a bijection, which is assumed rather than proved, and nothing yet ties blind to what this instance’s unwrap actually does.

I can’t think of a reason why wrap-resistance would matter in Katzenpost’s deployment of Sphinx, and the newer security frameworks seem to agree, since they no longer state it as a separate property at all. So KEM Sphinx losing it is fine. The real cost of KEM Sphinx is bandwidth: one KEM ciphertext per hop.

What’s next for formalizing Sphinx

This work is not finished, and some of it may be wrong. Correctness is proved, but the security fields still rest on the hypotheses listed above, and a formalization of a model is only as good as the model. If the games in Integrity.Sys or Indistinguishability.Sys misstate the paper, Lean will happily check a proof about the wrong thing. Review is welcome.

The plan is to move cryptlib’s security fields from the 2009 four property framework to the properties the followup papers showed actually imply secure onion routing, and to tie them to each instance’s own wrap and unwrap the way unwrap_complete already is:

• For NIKE Sphinx, the layer unlinkability and tail indistinguishability properties from the Gap Diffie-Hellman proof. That proof is about a cyclic group, so it covers the X25519 half of our hybrid NIKE and nothing more. A post quantum result for the CTIDH half needs the group action analogues of the Diffie-Hellman assumptions from the CSIDH and CTIDH papers, the Sphinx proof redone in the group action setting, and the NIKE combiner argument that the hybrid is secure if either component is. None of that exists yet.
• For KEM Sphinx, the EROR style properties, whose proofs only need an IND-CCA secure KEM, a MAC and a PRF. That fits cryptlib’s generic KEM type well, and it’s a path to a post quantum security proof, which the Diffie-Hellman based proofs can’t give.

What’s next for cryptlib

Sphinx is one protocol. We will model and formalize more of them as it benefits the Katzenpost mix network project to do so. So far cryptlib also partially formalizes BACAP, the blinded cryptographic capability system from our paper, under Cryptlib/Protocols/BACAP. It also models a few other HPQC constructions that Katzenpost uses: our KEM combiner, and MKEM, our multi-recipient KEM-like scheme built on a NIKE.

cryptlib has already paid off outside its own repository. uproar is our Noise and PQ Noise framework written in Lean, built on cryptlib’s primitive types. That is yet another protocol the Katzenpost mix network runs that we can now model in Lean.

Each protocol adds to a vocabulary of cryptographic primitive types and protocol components, and once that vocabulary is large enough, modeling our core mixnet protocols becomes much easier: they are assembled from parts whose proof obligations are already discharged.

Conclusion: dependent types for the win

Three things, in increasing order of how under-appreciated they are.

Interactive theorem provers for the win. An LLM wrote most of the proofs in this formalization, and it is good at that. It is not yet good at deciding what is worth proving. Every hypothesis in the security fields above is a claim about what the Sphinx paper’s games actually say, and a human has to check that those are the right statements before a proof of them means anything.

High assurance software for the win. Being able to run the same Lean code that the proofs are about, against test vectors shared with the Go implementation, and then prove properties of that very code, is very powerful indeed.

And dependent types for the win. This is the least known and least recognized of the three, and it seems badly under-rated. Correctness proofs compose for free, and design flaws like the zero padding leak can be ruled out by the type itself. My advice to every Lean programmer is to reach for dependent types whenever you can. You may reap rewards you did not expect, and your code will be more beautiful and expressive for it.

Sphinx Links

• The original Sphinx paper: Sphinx: A Compact and Provably Secure Mix Format

Followup work by other researchers to improve Sphinx and specify stronger security properties:

• Breaking and (Partially) Fixing Provably Secure Onion Routing: shows that the security properties the Sphinx proof relies on don’t actually imply ideal onion routing, and finds a path length leak in Sphinx’s zero padding.

• Provable Security for the Onion Routing and Mix Network Packet Format Sphinx: the first security proof for Sphinx that holds, for a slightly adapted Sphinx, under the Gap Diffie-Hellman assumption rather than DDH.

• EROR: Efficient Repliable Onion Routing with Strong Provable Privacy: a packet format that also prevents the payload tagging attack Sphinx allows, at the cost of doubling the payload.

• Onion Routing with Replies: the formal model for onion routing with replies that EROR builds on.

• Outfox: a Postquantum Packet Format for Layered Mixnets: a post quantum Sphinx variant for fixed length routes. It cites my Post Quantum Sphinx paper as lacking formal security guarantees, which is part of what this work is trying to address.

• OmniSphinx: Active Mix Networks: packets carry code that determines how mixes process them, so one network can emulate many mix formats.

• Improving the Sphinx Mix Network: proposes replacing Sphinx’s separate MAC and payload cipher with one authenticated encryption call per hop.

Some of my contributions to Sphinx:

• The Katzenpost Specification of the Sphinx packet format: https://katzenpost.network/docs/specs/sphinx/

• The Katzenpost Specification of the KEM Sphinx variant: https://katzenpost.network/docs/specs/kemsphinx/

• The Katzenpost Proverif model of KEM Sphinx: https://github.com/katzenpost/formal_specifications/blob/main/sphinx/kem_sphinx.passive.pv

• The Katzenpost implementation of the Sphinx, originally written by Yawning Angel: https://github.com/katzenpost/katzenpost/tree/main/core/sphinx I later added the KEM Sphinx variant and test vectors which are shared with the Lean implementation.

Katzenpost threat model document

Here we present a draft of the Katzenpost mixnet threat model document. We regard the threat model document as a living document which is frequently edited and in need of ongoing maintenance as we continue to develop newer mixnet protocols. Currently it is being organized by mixnet attack category and we have arranged attacks in a table with corresponding attacker capabilities. Later sections of the document present a deep dive into the core cryptographic protocols that comprise Katzenpost, namely these three:

1. Katzenpost Directory Authority PKI protocol
2. PQ Noise based wire protocol (on top of TCP or QUIC)
3. Sphinx nested encrypted packet routing protocol

Those are the basics necessary for point to point communications through the mix network. However mixnet protocols will then add their own cryptographic protocols which simply make use of the above three protocols in service to their goals of message transportation.

We thank Wau Holland Stiftung for funding this work.

Threat Model Doc

Mixnet Literature Overview

We are presenting our overview of existing Mixnet literature. It takes some liberties with what is included or not. It proposes new ways to talk about some issues, and provides a critical analysis of some of the existing papers. It also endeavors to introduce the reader to the language of anonymity systems, while maintaining mathematical rigor.

This doc, in particular, does not talk about the Katzenpost design. It does introduce the reader to some of the reasons why we’ve been making certain design decisions, and a keen eye might be led to some of the similar conclusions. But here we focus on already published research. We also stick to theory and don’t focus on any practical systems being built today.

The specific networking decisions implemented in Katzenpost so far, and the threats they mitigate and don’t, will be addressed in an upcoming, detailed threat model document.

We thank Wau Holland Stiftung for funding this work.

Lit Review Doc

Note form Eva: I understand that the tone of some of this analysis may come across as harsh. I personally take full responsibility for this tone and critique in particular.

At the same time, the point of this doc is not to present original research. Some exploitable mistakes in existing research were withheld from this version, and original contributions are included if I, personally, feel like they are merely reinventing the wheel in bridging some of the gaps between Mixnets and Mathematics. Some of the other original research is mentioned, but will be expanded on elsewhere.

hpqc - hybrid post quantum cryptography library

The Katzenpost developement team has recently released a new golang cryptography library known as hpqc. The theme of the library is hybrid post quantum cryptographic constructions, namely:

• hybrid KEMs (key encapsulation mechanism)
• hybrid NIKEs (non-interactive key exchange)
• hybrid signature schemes

In each of the three main subdirectories, “kem”, “nike” and “sign” there exists interface definitions for Scheme, PrivateKey and PublicKey. For signature schemes and KEMs we’re borrowing the interface sets from cloudflare’s circl library.

And each of these subdirectories has a schemes package where all the imeplementations are registered and can be referenced by unique string name, take for examples the KEM schemes documentation. However the implementations that are registered don’t show up in the API docs but we can see them in the source code.

hpqc gives you the power to compose an arbitrary number of KEMs and NIKEs, for example the above source file defines many KEMs in composition like this one:

	combiner.New(
		"X25519-mlkem768-ctidh512",
		[]kem.Scheme{
			adapter.FromNIKE(x25519.Scheme(rand.Reader)),
			mlkem768.Scheme(),
			adapter.FromNIKE(ctidh512.Scheme()),
		},
	),

This library makes seven unique contributions in golang:

1. a set of generic NIKE interfaces for NIKE scheme, public key and private key types

NIKE interfaces documentation source code

These are useful for making your cryptographic protocol not rely on a specific NIKE such as an elliptic curve diffiehellman function like x25519 or x448.

2. generic hybrid NIKE, combines any two NIKEs into one

NIKE hybrid scheme documentation source code

Many cryptographic protocols can use a hybrid post quantum NIKE in place of a NIKE. Here the NIKE interfaces are satisfied by this hybrid scheme type.

3. security preserving KEM combiner

security preserving KEM combiner documentation source code

Our security preserving KEM combiner can combine an arbitrary number of KEMs althought it’s usually useful enough to combine just two KEMs. We get our design from the KEM Combiners paper which makes the observation that if a KEM combiner is not security preserving then the resulting hybrid KEM will not have IND-CCA2 security if one of the composing KEMs does not have IND-CCA2 security. Likewise the paper points out that when using a security preserving KEM combiner, if only one of the composing KEMs has IND-CCA2 security then the resulting hybrid KEM will have IND-CCA2 security.

Our KEM combiner uses the split PRF design for an arbitrary number of KEMs, here shown with only three, in pseudo code:

func SplitPRF(ss1, ss2, ss3, cct1, cct2, cct3 []byte) []byte {
    cct := cct1 || cct2 || cct3
    return PRF(ss1 || cct) XOR PRF(ss2 || cct) XOR PRF(ss3 || cct)
}

4. a “NIKE to KEM adapter” which uses an ad hoc hashed elgamal construction

NIKE to KEM adapter documentation source code

It is very common in modern hybrid post quantum cryptographic protocol constructions to see a NIKE adapted into a KEM and then combined with a post quantum KEM.

Our ad hoc hashed elgamal construction for adapting any NIKE to a KEM is, in pseudo code:

func ENCAPSULATE(their_pubkey publickey) ([]byte, []byte) {
    my_privkey, my_pubkey = GEN_KEYPAIR(RNG)
    ss = DH(my_privkey, their_pubkey)
    ss2 = PRF(ss || their_pubkey || my_pubkey)
    return my_pubkey, ss2
}

func DECAPSULATE(my_privkey, their_pubkey) []byte {
    s = DH(my_privkey, their_pubkey)
    shared_key = PRF(ss || my_pubkey || their_pubkey)
    return shared_key
}

5. cgo bindings for the Sphincs+ C reference source

Our Sphincs+ wrapper conforms to the signature scheme interfaces:

Sphincs+ signature scheme documentation source code

We maintain our Sphincs+ C reference fork and golang bindings in this git repo: https://github.com/katzenpost/sphincsplus/

Here’s the cgo bindings source code: https://github.com/katzenpost/sphincsplus/blob/main/ref/binding.go

6. cgo bindings for the CTIDH C source

Our CTIDH golang bindings have been much improved through collaboration and are now maintained by the Vula project in this git repo:

https://codeberg.org/vula/highctidh

hpqc currently has a wrapper type for each CTIDH key size, as documented here:

https://pkg.go.dev/github.com/katzenpost/hpqc@v0.0.17/nike/ctidh/ctidh511 https://pkg.go.dev/github.com/katzenpost/hpqc@v0.0.17/nike/ctidh/ctidh512 https://pkg.go.dev/github.com/katzenpost/hpqc@v0.0.17/nike/ctidh/ctidh1024 https://pkg.go.dev/github.com/katzenpost/hpqc@v0.0.17/nike/ctidh/ctidh2048

7. generic hybrid signature scheme, combines any two signature schemes into one

It is useful to combine a classical signature scheme such as ed25519 with a post quantum signature scheme such as Sphincs+.

hybrid signature scheme documentation source code

Katzenpost at 37C3

Dr. Eva Infeld and surveillance expert and developer Leif Ryge held a session at the Chaos Communication Congress about the current state of the project, some of the things we’re working on, and some of the pitfalls many anonymity systems fall into. Building an anonymity system fit for our dystopian age is a hard problem, but we’re doing it.

Audio Engineering Considerations for a Modern Mixnet

Modern Mixnets have a unique set of requirements when it comes to processing audio. The bandwidth is scarce, but we expect to use modern devices and have ample processing power. We aim to secure the communication against even sophisticated attacks that come from capturing the metadata, and prioritize tools that are free, open source and written with security in mind. In this unique setting, we present a set of recommendations for implementing codecs, DSPs, and sophisticated noise reduction tools, to deliver either impressive quality at low bandwidth or good quality at impressively low bandwidth.

Read Research Paper

Website Relaunch and migration to Hugo

To match all the code development in Katzenpost in the last year, it was time for a website relaunch. Our site was a migration from Sphinx, which is primarily for documentation, to Hugo which is wildly configurable for all sorts of websites. Given the technical nature and need for nice documentation interface, we used the well crafted and maintained Docsy theme.

Website Dependencies

• Hugo static site generator
• Docsy theme for Hugo
• Bootstrap 5 is bundled in Docsy
• Decap CMS for a user-friendly GUI

Monthly News Update (May 2019)

Greetings,

The last few weeks have been very busy. I now have the basic working prototype implementation of a new Katzenpost messaging system. This new system has mutual location hiding properties for communication partners because recipients retreive their messages from a remote spool using a Sphinx SURB based protocol. SPHINX SPHINXSPEC

Naming things is tricky. I had to call it something:

• https://github.com/katzenpost/katzenpost/tree/main/catshadow

This messaging system is inspired by agl’s pond, obviously. See agl’s pond.

I forked agl’s Double Ratchet from pond:

• doubleratchet

Also forked agl’s PANDA:

• panda

Communication partners use a remote spool service which is now, memspool but later it will be a replicating CRDT:

• memspool

In order to exchange double ratchet keys and spool identities to form a bidirectional cryptographic channel, clients make use of the PANDA service. That is to say, PANDA (Phrase Automated Nym Discovery Authentication) is just another mixnet service like the memspool service mentioned above.

The user interface I wrote is a CLI terminal interface and it really kind of sucks. I’m feeling rather inspired by Special’s golang Ricochet. The UI and the backend are two separate processes and communicate by unix domain socket. Cool. Maybe I should do a similar construction that way someone else can later write a crazy C++ Gtk UI for this thing. Although I suspect this strategy doesn’t work well with Android. Unclear. At any rate, catshadow is crash fault tolerant, I hope. It is also internally way more simple than mailproxy and doesn’t use database transactions or anything like that. State is persisted to disk in an encrypted statefile… passphrase, argon2, nacl secretbox of course.

Anyway describing this whole thing is basically a paper worth of words which I shall attempt to articulate later. The overall strategy for Katzenpost should be for this client to merely serve as a demonstration. Whereas it would be far better to help another software project integrate with Katzenpost. Projects such as Briar and Wire come to mind. That having been said, I’d like to soon start a volunteer operated Katzenpost mix network so that we have some real infrastructure that allows us to start using catshadow to send each other encrypted messages. The amount of metadata we leak onto the network will depend on how many people use the system, number of mixes and of course how it is tuned. Since tuning is currently an unsolved problem, it’s all just a fun game anyway.

OK folks that’s all for now. I am not sure exactly what the next steps should be and I’m planning on deliberating while I discuss it with my colleagues and advisors. Either I will start a demo mixnet all on one machine that we can use to try out catshadow or I will attempt to instigate a volunteer operated mixnet. Things will get very cool once we have multiple applications that can use the mixnet. :)

Cheers,

David

Monthly News Update (April 2019)

Greetings,

The Panoramix grant project funded by the European Commission has officially ended but the Katzenpost free software project lives on. Masala and I continue to work on Katzenpost for grant money given to us by Samsung.

We recently learned a few things about mixnet design in a series of design meetings. The conclusions from our learnings is too much information and detail for this here post. However I will summarize some of our conclusions below. Our discussions usually revolved around mixnet CRDT applications, client reliability, message spool server design, client decoy traffic and, preventing attacks: statistical disclosure and active confirmation attacks.

Although far from complete, we added some design considerations to the following draft specification documents:

https://github.com/katzenpost/docs/blob/master/drafts/client.rst https://github.com/katzenpost/docs/blob/master/drafts/deaddrop.rst https://github.com/katzenpost/docs/blob/master/drafts/decoy_traffic.rst

The new Katzenpost mixnet design will work as follows:

• Clients will NOT send each other messages directly to each other’s Provider. A client’s Provider and spool ID is kept secret while clients share remote spool identities and remote spool Providers with each other instead. This allows a threat model of mutual distrust between clients. This design can help prevent clients from leaking more metadata such as geographical location.

• Messages are encrypted as follows: Firstly, the higher layer communications channel mechanism will use a modern cryptographic ratchet for forward secrecy and post compromise security properties. However, this ciphertext will be encapsulated by the Noise X oneway handshake. The nonce used by Noise X ensures that even if the client transmits the ratchet ciphertext, the Noise X ciphertext will always look different. This accomplishes our goal of not leaking retransmissions to spool Providers.

• Spool servers are now kept outside of the Katzenpost mix server source repository. That is to say, we make use of a plugin system for our mix server so that Providers can add arbitrary services to the mix network. We intend to use an iterative approach to designing and implementing remote message spools. The basic messaging use case as described above can be improved in the future by implementing the message spools as CRDT’s. This will allow spools to be replicated and this eliminates single points of failure in the network. In contrast the original Loopix design, each client has a single message spool on their Provider. If this Provider has an outage then that client will be unable to access their message spool.

• Clients and mixnet plugin services will together optionally make use of a publish subscribe protocol.

• Clients will send normal and decoy traffic in accordance with the timing provided by the original Loopix tuning parameters: λP, λL, λD, λM.

Our mission is to enable other communications software projects to use mix networks to reduce their metadata leakage. To that end we have been working on mixnet client libraries that can be used by anyone. Although in the future we are planning to write a generic client daemon which you can interact with using a Unix domain socket. We hope that this will be an effective combination for enabling other projects to use a Katzenpost mix network.

Although we are still in an unstable and rapid development phase we made some recent improvements to the Katzenpost mix server:

• Made it support running in networked environments with NAT devices.

• Added a new plugin system which is hopefully less annoying to use than our existing gRPC based plugin system. The new plugin system uses CBOR over HTTP over Unix domain sockets. Katzenpost mix server plugins allow you to add arbitrary query/response services to your mix network. That is, you send a SURB and a query payload to a service and it can send one reponse using that SURB.

I’ve provided some “echo” service plugins as examples of how to write plugins for Katzenpost in our server_plugins repo:

https://github.com/katzenpost/server_plugins

HOWEVER, we have for over a year supported BTC and Zcash cryptocurrency submitions via the “currency” plugin, here:

https://github.com/katzenpost/server_plugins/tree/master/grpc_plugins/currency

Other areas of improvement include fixing some bugs in the Voting Authority server and changing our PKI document to include all the Loopix tuning parameters: λP, λL, λD, λM. Thanks to Masala and Moritz we made recent progress in implementing a continuous integration system that runs kimchi based integration tests.

Yes, Katzenpost is a general purpose transport for message oriented applications. All client applications using the mix network look the same. My “elite dark mixnet wallet” for Zcash will have a traffic profile of λP, λL, λD just like mixnet chat client. Just as soon as we stabilize our client library we will actively seek collaborations with application developers.

I’ve made a few screencasts to explain about mix networks and Katzenpost:

• Katzenpost Introduction draft https://www.youtube.com/watch?v=vDJihqksd6w

• A Brief Introduction to mix networks https://www.youtube.com/watch?v=1VMUb47QhfE

• Mix Network Topology https://www.youtube.com/watch?v=bxk4H_X_OsM

• Introduction to Statistical Disclosure Attacks and Defenses for Mix Networks https://www.youtube.com/watch?v=pHLbe1JKrAQ

Cheers,

David Stainton

Rustification

Hi,

I wrote some notes about making mixnet components in Rust that are binary compatible with existing Katzenpost components

Rustification

The goal should be binary compatibility with the golang implementation of Katzenpost such that the existing golang components can interoperate with the new Rust components. Perhaps the biggest advantage of using Rust would be for writing mixnet clients as opposed to mix servers. A Rust mixnet client could easily present a FFI that could be used by user interfaces written in Java for Android and Swift for iOS.

I wrote several relavant rust crates:

• https://crates.io/crates/aez
• https://crates.io/crates/ecdh_wrapper
• https://crates.io/crates/mix_link
• https://crates.io/crates/rust-lioness
• https://crates.io/crates/epoch
• https://crates.io/crates/sphinx_replay_cache
• https://crates.io/crates/sphinxcrypto

Sphinx binary compatibility

• https://crates.io/crates/sphinxcrypto

The rust Sphinx uses the exact same cryptographic primitives as the golang implementation. Therefore it should be fairly easy to make them binary compatible. They should share test vectors.

Mix link layer binary compatibility

• https://crates.io/crates/mix_link

Currently this mix link layer crate uses Noise_XX_25519_ChaChaPoly_BLAKE2b however if the Katzenpost link layer were to upgrade to Kyber then the task of making this crate binary compatibility would be greatly simplified.

Here’s an implementation of Kyber:

• https://crates.io/crates/kyber

This mix_link crate uses the snow Noise protocol library implementation:

• https://crates.io/crates/snow

However we SHOULD patch snow with Kyber PQ KEM hybrid forward secrecy. Here’s the snow github ticket for this task:

• https://github.com/mcginty/snow/issues/39

Mix server

Current work in progress rust mix server:

• https://github.com/david415/mix_server

Development progress has halted due to not being able to interoperate with the existing Katzenpost Directory Authority system.

Monthly News Update (Nov 2018)

Greetings!

This is our second edition of katzenpost news. There’s been a lot of progress since the last report I posted many months ago.

Firstly I’d like to mention our future development plans:

• mix and directory authority key agility
• generative testing for the voting Directory Authority system
• generative testing for all of the things where appropriate
• load and performance testing the mix server
• design and development of an application agnostic mixnet client message oriented protocol library
• design and development of one or more applications that use our new mixnet protocol client library
• potentially assist in integration with other software projects that want to use a mixnet transport protocol

Our recent accomplishments include:

• Eradication of our usage of JOSE/JWS and usage of the golang Jose library. We no longer use JOSE/JWS for signing mix descriptors and directory authority documents. Instead we use the “cert” library I wrote which gives us certificate format agility AND cryptographic algorithmic agility.

specification: https://github.com/katzenpost/docs/blob/master/specs/certificate.rst

golang implementation: https://github.com/katzenpost/core/tree/master/crypto/cert

• Our mix server now has a language agnostic plugin system for adding mixnet services. We have a modular API that allows you to write new services in golang and staticly compile them into the binary, however this new plugin system allows you to add services using external programs as plugins. These external plugins use gRPC over Unix domain socket to talk to the mix server (Provider). Using these plugins we can make new mixnet protocols that are either one way or strict call and response protocols that use SURBs to send the replies.

Here’s the mix server documentation for this new feature: https://github.com/katzenpost/docs/blob/master/handbook/mix_server.rst#external-kaetzchen-plugin-configuration

Here’s the Kaetzchen specification document which explains a bit how this plugin system works although it doesn’t discuss implementation details: https://github.com/katzenpost/docs/blob/master/specs/kaetzchen.rst

This repository contains an “echo service” written in Rust, Golang and Python. Also it contains a plugin to perform crypto currency submissions, the idea being that mixnets can be used to transport a transaction blob to a Provider service which then submits the transaction to the database, the blockchain or whatever:

https://github.com/katzenpost/server_plugins

• we now have a set of incomplete Katzenpost Handbook documents:

https://github.com/katzenpost/docs/blob/master/handbook/index.rst

Mailproxy Client Daemon https://github.com/katzenpost/docs/blob/master/handbook/mailproxy.rst

Katzenpost Mix Server Infrastructure https://github.com/katzenpost/docs/blob/master/handbook/mix_server.rst

Katzenpost Mix Network Public Key Infrastructure https://github.com/katzenpost/docs/blob/master/handbook/nonvoting_pki.rst

Torification of Katzenpost https://github.com/katzenpost/docs/blob/master/handbook/tor.rst

Katzenpost Voting Directory Authority https://github.com/katzenpost/docs/blob/master/handbook/voting_pki.rst

• we now have a HACKING guide for new Katzenpost developers:

https://github.com/katzenpost/docs/blob/master/HACKING/index.rst

• we now have a release process and some binary releases:

https://github.com/katzenpost/docs/blob/master/release_checklist.rst https://github.com/katzenpost/docs/blob/master/releases.rst https://github.com/katzenpost/daemons/releases

• We have released the voting Directory Authority (mixnet PKI) implementation since it is known to work properly as far as we were able to test thus far. This was more work and more difficult than we originally anticipated for both design and programming the implementation.

The design of this PKI was not fully supported by the Panoramix grant project because our academic collaborators were not under official obligation to work on this given that our three month period of design work officially ended. Thus, we were fortunate to receive their advice anyway.

Our specification document is rather still rather incomplete unfortunately:

https://github.com/katzenpost/docs/blob/master/specs/pki.rst

Masala has done most of the development work and together we fixed some bugs in the implementation. The design of our PKI is a synthesis of design ideas that come from some brilliant minds and we’d like to thank Yawning Angel, Claudia Diaz, Ania Piotrowska and Nick Mathewson.

Our PKI uses a Shared Random Value to seed the randomization of our topology. We’d like to thank George Kandianakis for answering our questions about Tor’s hash based commit and reveal shared random value protocol.

What does randomizing our topology mean? Loopix and Katzenpost use the stratified topology which means that the client’s path selection must select a mix from each layer. This topology is enforced by our mix link layer protocol. The PKI generates and publishes a network consensus document\ and this specifies which mixes belong in which topology layer.

When one or more mix network layers change such that they only contain mixes operated by a single operators or contain only one mix that is what we mean by imbalanced. “Too few security domains” gives too much control over path selection to one or more mix operators.

The voting Directory Authority servers detect these mix outages by the absense of a newly uploaded mix descriptors for the voting round. Upon detecting this threshold event the shared random value is used to seed topology randomization. Claudia and Ania rightly pointed out that we MUST try to avoid rerandomization, it is detrimental to the anonymity properties of the mix network because it splits each mix’s anonymity set into two. That is, incoming messages for each mix are either from layer X or from layer Y, this topology distinction in message source means that those two categories of messages will not be mixed together and this is what is meant by splitting the anonymity set into two.

• Masala and I fixed a plethora of race conditions in client and server code for both the Directory authority and mix servers.

• I added a prototype mixnet client and server for supporting Adam Langely’s PANDA protocol:

https://github.com/katzenpost/panda

PANDA was used in Pond, and Pond has sadly been abandoned by it’s creator. I would like there to be many useful mixnet clients, including a kind of “Pond replacement” that can perform key exchanges using PANDA.

During the last section of my mixnet talk at Bornhack 2018 I demonstrated the mixnet PANDA client and server working:

https://www.youtube.com/watch?v=DhBWKWQztdA

Sincerely, David Stainton

Monthly News Update (Feb 2018)

katzenpost monthly news

Greetings!

This is our first edition of katzenpost monthly news. I’ll be summarizing recent events from our first hackfest in Athens in early December 2017 to the present.

What we did in Athens:

• setup a test mix network
• remote collaboration with Yawning Angel to fix bugs and add features to the server side
• wrote some basic installation documentation
• Moritz created and deployed the katzenpost website with glossary and FAQ
• explored technical issues related to python and java language bindings to golang libraries
• discussed at length the possibilies for various kinds of mixnet clients
• Vincent wrote a prototype android instant messenger client
• met with the GrNet people and told them how to install a katzenpost mix network and answered their questions
• meskio and kaliy added an external user db interface for Provider authentication
• meskio wrote prototype python clients for testing purposes
• we had many group discussion about mix network design
• special guest visitor: George Kadianakis from Tor Project

Since that time we have been working on our PKI specification. Nick Mathewson sent us a six page review of our spec and Yawning sent a two page reply; both of these e-mails contain lots of design details and have been useful in our editing of the spec thus far:

https://github.com/katzenpost/docs/blob/master/specs/pki.txt

Additionally since the Athens hackfest I, masala and Yawning have made changes so that interaction with the nonvoting PKI to NOT use HTTP but instead uses our Noise based wire protocol (which incidentally uses a Post Quantum hybrid key exchange). The PKI spec has been updated with these new changes. If you are curious about our wire protocol you can read about it here:

https://github.com/katzenpost/docs/blob/master/specs/wire-protocol.txt

During the Brussels hackfest we:

• worked on our Google Summer of Code project submission AND additional work on our website: https://katzenpost.mixnetworks.org/contribute.html https://github.com/katzenpost/mixnet_uprising/wiki/Project-Ideas

• kwadronaut and I used a server on our test mixnet to test out Yawning’s new Provider postgres database interface for spool and user authentication databases; Postgres is optional but it is much high performance than boltdb which has no granular transactional locks.

• Vincent improved upon the java and python bindings to client library, currently this client library is known as “mailproxy”

• Vincent wrote an android k9mail katzenpost prototype for demonstrations

• held lengthy discussions about autoresponder based keyserver for the purpose of distributing client encryption keys

• we collectively wrote rough draft specifications for autoresponder services known as kaetzchen and a keyserver:

  • autoresponder protocol known as kaetzchen https://github.com/katzenpost/docs/blob/master/drafts/kaetzchen.txt

  • keyserver specification (rough draft) https://github.com/katzenpost/docs/blob/master/drafts/keyserver.txt

• masala wrote a golang CLI client: https://github.com/katzenpost/demotools/tree/master/cliclient

• masala worked on making bandwidth overhead estimations of the PKI protocol: https://github.com/mixmasala/docs/blob/mix_bandwidth_estimation/drafts/pki-bandwidth-estimate.txt https://github.com/mixmasala/docs/blob/mix_bandwidth_estimation/tuning/bw.py

  Note: Bandwidth and scaling estimations is something that Nick Mathewson has requested in his review of our PKI specification document.

• had conversations with several guests at our hackfest including:

  • Claudia Diaz
  • video conference with Yawning Angel
  • the developers of sequoia-pgp https://sequoia-pgp.org/
  • Harry Halpin
  • an associate of Harry who is involved in the crypto currency financial industry

• Tg created NixOS packages for the katzenpost components https://github.com/katzenpost/nixpkgs

  and NixOS katzenpost configuration for automatic deployment to linux containers: https://github.com/katzenpost/nixops

• meskio and kaliy: worked on a number of things, including

  • LEAP based account registration for katzenpost Providers

  • setup Prometheus to monitor our test mixnet

  • performed stress tests to determine how network load would be affected by various client concurrency levels and bandwidth usage: https://github.com/katzenpost/katzsim

Since the Brussels hackfest, Masala and I visited Claudia Diaz and Tariq Elahi at KU Leuven to discuss mix network designs. In particular we asked various questions about the AQMs used in the Katzenpost server side and later got clarification from Yawning. We also discussed mix network tuning and learned that the preferred method of tuning mixnets is to run lots of simulations and use different kinds of analysis to determine an appropriate set of tuning parameters.

During this discussion Tariq mentioned that their simulations are likely not using the exact same AQMs as Katzenpost server side. We decided that these simulations could be executed using our “mixnet emulator” which is called kimchi. It runs an entire katzenpost mix network and nonvoting authority in a single golang process.

We patiently await for a response to our query: “What features should the mixnet emulator/simulator have?”

Yawning recently implemented the keyserver:

https://github.com/katzenpost/server/blob/master/internal/provider/kaetzchen/keyserver.go

and the mailproxy client side for interacting with the keyserver:

https://github.com/katzenpost/mailproxy/blob/master/api_kaetzchen.go

Since then Yawning’s focus has been to improve server side stability and performance. You can see his task list here: https://github.com/orgs/katzenpost/projects/2

Masala and I have been working on writing a voting directory authority server.

Currently our test mixnet works because Yawning has not only written most of the code but he also wrote a nonvoting Directory Authority PKI. However, the nonvoting PKI is not suitable for production use where a decentralized design should be used to achieve the desired security properties.

Beyond our officially sanctioned work on this project, and in my free time, I’ve been exploring other use-cases for mixnets. I’ve been thinking about “strong location hiding properties”. What I came up with is a kind of kaetzchen dead drop service where you can retreive messages from a remote Provider. The client would never directly interact with the remote Provider but instead only uses the mixnet to retrieve messages.

https://github.com/katzenpost/docs/blob/master/drafts/deaddrop.txt

Cheers!

David