NIKE-Sphinx scheme type

Constructions and proofs are in nike_sphinx_theorems.lean.

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

A Sphinx scheme whose header carries a re-blindable group element Envelope.

• State : Type
• PrivateKey : Type
• Command : Type
• stateI : Inhabited self.State
• privI : Inhabited self.PrivateKey
• geometry : Geometry.Geometry
• cipher : Primitives.WideBlockCipher.WideBlockCipher
• mac : Primitives.MAC.MAC
• kdf : Primitives.KDF.KDF
• stream : Primitives.StreamCipher.StreamCipher
• derivePublicKey : self.PrivateKey → ByteArray
• wrap : List Types.PathHop → Vector UInt8 self.geometry.forwardPayloadLength → EStateM String self.State (Vector UInt8 self.geometry.packetLength)
• unwrap : self.PrivateKey → (pkt : ByteArray) → Except String (Option ByteArray × Vector UInt8 32 × List self.Command × Option (Vector UInt8 pkt.size))
• 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
• 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))
• 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
• 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
• nike : Primitives.NIKE.NIKE.NIKE
• Envelope : Type
• envelopeDecEq : DecidableEq self.Envelope
• parseEnvelope : Vector UInt8 self.geometry.packetLength → self.Envelope

  The header's group element.

• Factor : Type

  The blinding factor space.

• factorFintype : Fintype self.Factor
• factorSampleable : SampleableType self.Factor
• blind : self.Factor → self.Envelope → self.Envelope
• wrap_resistant (e target : self.Envelope) : (Function.Bijective fun (x : self.Factor) => self.blind x e) → Pr[= true | do let b ← $ᵗ self.Factor pure (decide (self.blind b e = target))] = (↑(Fintype.card self.Factor))⁻¹

  Wrap-resistance (§4.3): if blinding e is a bijection, a uniform factor hits target with probability 1/|Factor|.

• envelope_indep (hop0 hop1 : Types.PathHop) (rest0 rest1 : List Types.PathHop) (payload0 payload1 : Vector UInt8 self.geometry.forwardPayloadLength) (st : self.State) (pkt0 pkt1 : Vector UInt8 self.geometry.packetLength) (st0' st1' : self.State) : self.wrap (hop0 :: rest0) payload0 st = EStateM.Result.ok pkt0 st0' → self.wrap (hop1 :: rest1) payload1 st = EStateM.Result.ok pkt1 st1' → self.parseEnvelope pkt0 = self.parseEnvelope pkt1

  The envelope depends only on the starting State, not on the path or payload.