KEM-Sphinx scheme type

Constructions and proofs are in kem_sphinx_theorems.lean.

structure Cryptlib.Protocols.Sphinx.KEMSphinx.KEMSphinxSchemeextends 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
• 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
• kem : Primitives.KEM.KEM.KEM
• not_wrap_resistant (key iv target : ByteArray) : ∃ (raw : ByteArray), Common.xorBytes raw (self.stream.keystream key iv target.size) = target

  Not wrap-resistant: any target routing-info block is reachable by some ciphertext.