The abstract Sphinx interface

Reference: George Danezis and Ian Goldberg, Sphinx: A Compact and Provably Secure Mix Format, IEEE S&P 2009, https://eprint.iacr.org/2008/475. A bare §n.m in this directory refers to that paper's sections.

A packet scheme with completeness (unwrap_complete), integrity (§4.2) and indistinguishability (§4.4). Wrap-resistance (§4.3) is stated on NIKESphinxScheme only, since it needs a re-blindable group element.

@[reducible, inline]

abbrev Cryptlib.Protocols.Sphinx.Interface.SeedStream : Type

Counter plus an infinite stream of 32-byte seeds.

Equations

• Cryptlib.Protocols.Sphinx.Interface.SeedStream = (ℕ × (ℕ → Vector UInt8 32))

def Cryptlib.Protocols.Sphinx.Interface.nextSeed : EStateM String SeedStream (Vector UInt8 32)

Equations

• Cryptlib.Protocols.Sphinx.Interface.nextSeed (i, str) = EStateM.Result.ok (str i) (i + 1, str)

def Cryptlib.Protocols.Sphinx.Interface.initWith (str : ℕ → Vector UInt8 32) : SeedStream

Initial state: counter zero over a seed stream, which must be unpredictable.

Equations

• Cryptlib.Protocols.Sphinx.Interface.initWith str = (0, str)

def Cryptlib.Protocols.Sphinx.Interface.seedBytes (str : ℕ → Vector UInt8 32) (i n : ℕ) : ByteArray

n bytes from the seed stream starting at seed i: byte k is byte k % 32 of seed i + k / 32.

Equations

• Cryptlib.Protocols.Sphinx.Interface.seedBytes str i n = { data := Array.ofFn fun (k : Fin n) => (str (i + ↑k / 32))[↑k % 32] }

theorem Cryptlib.Protocols.Sphinx.Interface.seedBytes_size (str : ℕ → Vector UInt8 32) (i n : ℕ) : (seedBytes str i n).size = n

def Cryptlib.Protocols.Sphinx.Interface.drawBytes (n : ℕ) : EStateM String SeedStream ByteArray

Draw n bytes from the seed stream, consuming ⌈n/32⌉ seeds.

Equations

• Cryptlib.Protocols.Sphinx.Interface.drawBytes n (i, str) = EStateM.Result.ok (Cryptlib.Protocols.Sphinx.Interface.seedBytes str i n) (i + (n + 31) / 32, str)

def Cryptlib.Protocols.Sphinx.Interface.fillerLength (geom : Geometry.Geometry) (nrHops : ℕ) : ℕ

Routing-info bytes a nrHops-hop path leaves unused. These are filled with random bytes, not zeros, which would reveal the path length (Kuhn et al., S&P 2020).

Equations

• Cryptlib.Protocols.Sphinx.Interface.fillerLength geom nrHops = (geom.nrHops - nrHops) * geom.perHopRoutingInfoLength

def Cryptlib.Protocols.Sphinx.Interface.unwrapChainAux {PrivateKey Command : Type} (unwrap : PrivateKey → (pkt : ByteArray) → Except String (Option ByteArray × Vector UInt8 32 × List Command × Option (Vector UInt8 pkt.size))) : List PrivateKey → ByteArray → Except String (Option ByteArray)

Repeatedly unwrap, one key per hop, stopping at the first hop with no forward packet.

Equations

• One or more equations did not get rendered due to their size.
• Cryptlib.Protocols.Sphinx.Interface.unwrapChainAux unwrap [] x✝ = pure none

structure Cryptlib.Protocols.Sphinx.Interface.Sphinx : Type 1

• State : Type
• PrivateKey : Type
• Command : Type
• stateI : Inhabited self.State
• privI : Inhabited self.PrivateKey
• geometry : Geometry.Geometry
• cipher : Primitives.WideBlockCipher.WideBlockCipher

  Wide-block cipher for the payload, MAC for header integrity, KDF for per-hop keys, stream cipher for routing-info encryption.

• mac : Primitives.MAC.MAC
• kdf : Primitives.KDF.KDF
• stream : Primitives.StreamCipher.StreamCipher
• derivePublicKey : self.PrivateKey → ByteArray

  Raw public key bytes.

• wrap : List Types.PathHop → Vector UInt8 self.geometry.forwardPayloadLength → EStateM String self.State (Vector UInt8 self.geometry.packetLength)

  Unused routing-info slots are filled with random bytes drawn from State.

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

  (payload, replayTag, cmds, forwardPkt).

• newSURB : List Types.PathHop → EStateM String self.State (Vector UInt8 self.geometry.surbLength × ByteArray)
• newPacketFromSURB : Vector UInt8 self.geometry.surbLength → ByteArray → Except String (ByteArray × Vector UInt8 32)
• unwrapReliable : self.State → Prop

  Starting states from which the backing scheme never hits a decryption failure. True for perfectly correct schemes.

• unwrap_complete (path : List Types.PathHop) (privKeys : List self.PrivateKey) (payload : Vector UInt8 self.geometry.forwardPayloadLength) (st : self.State) (pkt : Vector UInt8 self.geometry.packetLength) (st' : self.State) : path ≠ [] → self.unwrapReliable st → List.map (fun (x : Types.PathHop) => x.publicKey) path = List.map self.derivePublicKey privKeys → (∀ hop ∈ path, ∀ c ∈ hop.commands, c ≠ Commands.RoutingCommand.null ∧ ∀ (id m : Vector UInt8 32), c ≠ Commands.RoutingCommand.nextNodeHop id m) → (∀ c ∈ path[path.length - 1]!.commands, ∀ (id : Vector UInt8 16), c ≠ Commands.RoutingCommand.surbReply id) → self.wrap path payload st = EStateM.Result.ok pkt st' → unwrapChainAux self.unwrap privKeys (Util.Bytes.ofVector pkt) = Except.ok (some (Util.Bytes.ofVector payload))

  Completeness: unwrap undoes wrap on the forward payload, given no hop's commands contains null or nextNodeHop and the last hop carries no surbReply.

• indistinguishable {F G Seed KeyMu KeyPi Beta Gamma Delta : Type} [Field F] [AddCommGroup G] [Module F G] [AddCommGroup Beta] [SampleableType F] [SampleableType Seed] [SampleableType KeyMu] [SampleableType KeyPi] [SampleableType Beta] [SampleableType Gamma] [SampleableType Delta] [SampleableType (Seed × KeyMu × KeyPi)] [Finite F] (S : Indistinguishability.Sys F G Seed KeyMu KeyPi Beta Gamma Delta) : Indistinguishability.AdvantageLeType S

  Indistinguishability (§4.4). See Indistinguishability.advantage_le.

• integrity {F G Seed Idx Yy Kappa : Type} [Field F] [AddCommGroup G] [Module F G] [Nonempty Yy] (S : Integrity.Sys F G) (hρ : G → Seed) (ρhat0 : Seed → Kappa) (ρ0 : Seed → Idx) (f : Idx → Yy → Kappa) : Integrity.IntegrityBoundType S hρ ρhat0 ρ0 f

  Integrity (§4.2). See Integrity.integrity_bound.

@[instance_reducible]

instance Cryptlib.Protocols.Sphinx.Interface.instInhabitedSphinx : Inhabited Sphinx

Equations

• One or more equations did not get rendered due to their size.