Formalizing Sphinx in Lean

A Lean formalization of the Sphinx packet format, generic over its cryptographic primitives, and what it does and doesn’t prove.
By David Stainton |
Tags:
Engraving of the Great Sphinx of Giza, half buried in sand

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 processing of a KEM Sphinx message ((α, β, γ), δ) into ((α′, β′, γ′), δ′) at mix n.

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.

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

Some of my contributions to Sphinx:

Last modified October 31, 2026: Blog: drop duplicate links, fold considerations section (0a599c69)