NIKE-Sphinx

Sphinx packet creation and unwrapping over any NIKE, with sizes read from the NIKE's own fields. createHeader takes its randomness as arguments, so it is pure.

@[instance_reducible]

instance Cryptlib.Protocols.Sphinx.NIKESphinx.instDecidableEqPublicKey (nike : Primitives.NIKE.NIKE.NIKE) : DecidableEq nike.PublicKey

Equations

• Cryptlib.Protocols.Sphinx.NIKESphinx.instDecidableEqPublicKey nike a b = decidable_of_iff (nike.encodePublicKey a = nike.encodePublicKey b) ⋯

@[instance_reducible]

noncomputable instance Cryptlib.Protocols.Sphinx.NIKESphinx.instFintypePrivateKey (nike : Primitives.NIKE.NIKE.NIKE) : Fintype nike.PrivateKey

Equations

• Cryptlib.Protocols.Sphinx.NIKESphinx.instFintypePrivateKey nike = Fintype.ofInjective nike.encodePrivateKey ⋯

@[instance_reducible]

instance Cryptlib.Protocols.Sphinx.NIKESphinx.instDecidableEqPrivateKey (nike : Primitives.NIKE.NIKE.NIKE) : DecidableEq nike.PrivateKey

Equations

• Cryptlib.Protocols.Sphinx.NIKESphinx.instDecidableEqPrivateKey nike a b = decidable_of_iff (nike.encodePrivateKey a = nike.encodePrivateKey b) ⋯

@[instance_reducible]

instance Cryptlib.Protocols.Sphinx.NIKESphinx.instInhabitedPrivateKey (nike : Primitives.NIKE.NIKE.NIKE) : Inhabited nike.PrivateKey

Equations

• Cryptlib.Protocols.Sphinx.NIKESphinx.instInhabitedPrivateKey nike = { default := nike.privateKeyFromSeed (Vector.replicate 32 0) }

@[instance_reducible]

instance Cryptlib.Protocols.Sphinx.NIKESphinx.instInhabitedPublicKey (nike : Primitives.NIKE.NIKE.NIKE) : Inhabited nike.PublicKey

Equations

• Cryptlib.Protocols.Sphinx.NIKESphinx.instInhabitedPublicKey nike = { default := nike.derivePublicKey default }

@[instance_reducible]

noncomputable instance Cryptlib.Protocols.Sphinx.NIKESphinx.instSampleableTypePrivateKey (nike : Primitives.NIKE.NIKE.NIKE) : SampleableType nike.PrivateKey

Equations

• Cryptlib.Protocols.Sphinx.NIKESphinx.instSampleableTypePrivateKey nike = SampleableType.ofFintype nike.PrivateKey

@[simp]

theorem Cryptlib.Protocols.Sphinx.NIKESphinx.size_nikeBlind (nike : Primitives.NIKE.NIKE.NIKE) (pk factor : ByteArray) : (Cryptlib.Protocols.Sphinx.NIKESphinx.nikeBlind✝ nike pk factor).size = pk.size

theorem Cryptlib.Protocols.Sphinx.NIKESphinx.nikeDH_bridge (nike : Primitives.NIKE.NIKE.NIKE) (sk : nike.PrivateKey) (pk : nike.PublicKey) (h : nike.Safe pk) : Cryptlib.Protocols.Sphinx.NIKESphinx.nikeDH✝ nike sk (Util.Bytes.ofVector (nike.encodePublicKey pk)) = Except.ok (Util.Bytes.ofVector (nike.encodeSharedSecret (nike.groupAction sk ⟨pk, h⟩)))

On an encoded Safe public key, nikeDH computes the encoded groupAction.

theorem Cryptlib.Protocols.Sphinx.NIKESphinx.nikeBlind_bridge (nike : Primitives.NIKE.NIKE.NIKE) (pk : nike.PublicKey) (sk : nike.PrivateKey) (h : nike.Safe pk) (factor : ByteArray) (hfactor : nike.decodePrivateKey (Common.toVecN nike.privateKeySize factor) = some sk) : Cryptlib.Protocols.Sphinx.NIKESphinx.nikeBlind✝ nike (Util.Bytes.ofVector (nike.encodePublicKey pk)) factor = Util.Bytes.ofVector (nike.encodePublicKey (nike.reinterpret (nike.groupAction sk ⟨pk, h⟩)))

On an encoded Safe public key and factor bytes decoding to sk, nikeBlind computes the encoded reinterpret (groupAction sk pk h).

structure Cryptlib.Protocols.Sphinx.NIKESphinx.HopKeys : Type

Per-hop keys. blindingFactor is raw bytes so HopKeys does not depend on the NIKE.

• headerMAC : Vector UInt8 32
• headerEncryption : Vector UInt8 32
• headerEncryptionIV : Vector UInt8 16
• payloadEncryption : Vector UInt8 48
• blindingFactor : ByteArray

@[instance_reducible]

instance Cryptlib.Protocols.Sphinx.NIKESphinx.instInhabitedHopKeys : Inhabited HopKeys

Equations

• Cryptlib.Protocols.Sphinx.NIKESphinx.instInhabitedHopKeys = { default := Cryptlib.Protocols.Sphinx.NIKESphinx.instInhabitedHopKeys.default }

def Cryptlib.Protocols.Sphinx.NIKESphinx.deriveHopKeys (kdfS : Primitives.KDF.KDF) (sharedSecret : ByteArray) : HopKeys

Derive one hop's keys from its shared secret.

Equations

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

def Cryptlib.Protocols.Sphinx.NIKESphinx.createHeader (nike : Primitives.NIKE.NIKE.NIKE) (macS : Primitives.MAC.MAC) (kdfS : Primitives.KDF.KDF) (streamS : Primitives.StreamCipher.StreamCipher) (geom : Geometry.Geometry) (clientPrivateKey filler : ByteArray) (path : Array Types.PathHop) : Except String (ByteArray × Array Types.SPRPKey)

filler must be (geom.nrHops - path.size) * geom.perHopRoutingInfoLength bytes; it hides the hop count of a short path.

Equations

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

theorem Cryptlib.Protocols.Sphinx.NIKESphinx.createHeader_hdr_size (nike : Primitives.NIKE.NIKE.NIKE) (macS : Primitives.MAC.MAC) (kdfS : Primitives.KDF.KDF) (streamS : Primitives.StreamCipher.StreamCipher) (geom : Geometry.Geometry) (clientPrivateKey filler : ByteArray) (path : Array Types.PathHop) (hdr : ByteArray) (sprpKeys : Array Types.SPRPKey) (hvalid : geom.ValidForNIKE nike) (hmactag : macS.tagSize = Constants.macLength) (h : createHeader nike macS kdfS streamS geom clientPrivateKey filler path = Except.ok (hdr, sprpKeys)) : hdr.size = geom.headerLength

createHeader's header size is 2 + nike.publicKeySize + geom.routingInfoLength + macLength, which is geom.headerLength when geom is valid for nike.

def Cryptlib.Protocols.Sphinx.NIKESphinx.newNIKEPacket (nike : Primitives.NIKE.NIKE.NIKE) (cipher : Primitives.WideBlockCipher.WideBlockCipher) (macS : Primitives.MAC.MAC) (kdfS : Primitives.KDF.KDF) (streamS : Primitives.StreamCipher.StreamCipher) (geom : Geometry.Geometry) (clientPrivateKey filler : ByteArray) (path : Array Types.PathHop) (payload : ByteArray) : Except String ByteArray

Build a forward packet.

Equations

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

theorem Cryptlib.Protocols.Sphinx.NIKESphinx.newNIKEPacket_size (nike : Primitives.NIKE.NIKE.NIKE) (cipher : Primitives.WideBlockCipher.WideBlockCipher) (macS : Primitives.MAC.MAC) (kdfS : Primitives.KDF.KDF) (streamS : Primitives.StreamCipher.StreamCipher) (geom : Geometry.Geometry) (clientPrivateKey filler : ByteArray) (path : Array Types.PathHop) (payload pkt : ByteArray) (hvalid : geom.ValidForNIKE nike) (hmactag : macS.tagSize = Constants.macLength) (h : newNIKEPacket nike cipher macS kdfS streamS geom clientPrivateKey filler path payload = Except.ok pkt) (hpay : payload.size = geom.forwardPayloadLength) : pkt.size = geom.packetLength

newNIKEPacket on a geom.forwardPayloadLength payload yields geom.packetLength bytes.

def Cryptlib.Protocols.Sphinx.NIKESphinx.wrapNIKE (nike : Primitives.NIKE.NIKE.NIKE) (cipher : Primitives.WideBlockCipher.WideBlockCipher) (macS : Primitives.MAC.MAC) (kdfS : Primitives.KDF.KDF) (streamS : Primitives.StreamCipher.StreamCipher) (geom : Geometry.Geometry) (path : List Types.PathHop) (payload : Vector UInt8 geom.forwardPayloadLength) : EStateM String Interface.SeedStream (Vector UInt8 geom.packetLength)

Sphinx.Interface.wrap: newNIKEPacket with the client key and filler drawn from the seed stream.

Equations

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

def Cryptlib.Protocols.Sphinx.NIKESphinx.newNIKESURB (nike : Primitives.NIKE.NIKE.NIKE) (macS : Primitives.MAC.MAC) (kdfS : Primitives.KDF.KDF) (streamS : Primitives.StreamCipher.StreamCipher) (geom : Geometry.Geometry) (clientPrivateKey : ByteArray) (keyPayload : Vector UInt8 64) (filler : ByteArray) (path : Array Types.PathHop) : Except String (ByteArray × ByteArray)

Build a SURB. keyPayload is the 64-byte SPRP key and IV for the reply's final payload layer. Returns (surb, decryptionKeys).

Equations

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

theorem Cryptlib.Protocols.Sphinx.NIKESphinx.newNIKESURB_size (nike : Primitives.NIKE.NIKE.NIKE) (macS : Primitives.MAC.MAC) (kdfS : Primitives.KDF.KDF) (streamS : Primitives.StreamCipher.StreamCipher) (geom : Geometry.Geometry) (clientPrivateKey : ByteArray) (keyPayload : Vector UInt8 64) (filler : ByteArray) (path : Array Types.PathHop) (hvalid : geom.ValidForNIKE nike) (hmactag : macS.tagSize = Constants.macLength) (surb surbKeys : ByteArray) (h : newNIKESURB nike macS kdfS streamS geom clientPrivateKey keyPayload filler path = Except.ok (surb, surbKeys)) : surb.size = geom.surbLength

newNIKESURB's SURB is geom.surbLength bytes.

def Cryptlib.Protocols.Sphinx.NIKESphinx.wrapNIKESURB (nike : Primitives.NIKE.NIKE.NIKE) (macS : Primitives.MAC.MAC) (kdfS : Primitives.KDF.KDF) (streamS : Primitives.StreamCipher.StreamCipher) (geom : Geometry.Geometry) (path : List Types.PathHop) : EStateM String Interface.SeedStream (Vector UInt8 geom.surbLength × ByteArray)

Sphinx.Interface.newSURB: newNIKESURB with the client key, keyPayload and filler drawn from the seed stream.

Equations

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

def Cryptlib.Protocols.Sphinx.NIKESphinx.unwrapNIKE (nike : Primitives.NIKE.NIKE.NIKE) (cipher : Primitives.WideBlockCipher.WideBlockCipher) (macS : Primitives.MAC.MAC) (kdfS : Primitives.KDF.KDF) (streamS : Primitives.StreamCipher.StreamCipher) (geom : Geometry.Geometry) (privKey pkt : ByteArray) : Except String (Option ByteArray × Vector UInt8 32 × List Commands.RoutingCommand × Option (Vector UInt8 pkt.size))

Unwrap one layer: (payload, replayTag, cmds, forwardPkt).

Equations

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

theorem Cryptlib.Protocols.Sphinx.NIKESphinx.unwrapNIKE_hopPacket_nonterminal (nike : Primitives.NIKE.NIKE.NIKE) (cipher : Primitives.WideBlockCipher.WideBlockCipher) (macS : Primitives.MAC.MAC) (kdfS : Primitives.KDF.KDF) (streamS : Primitives.StreamCipher.StreamCipher) (geom : Geometry.Geometry) (path : Array Types.PathHop) (keys : Array HopKeys) (groupElements riKeyStream riPadding : Array ByteArray) (sprpKeys : Array Types.SPRPKey) (nrHops : ℕ) (s : ℕ → ByteArray × ByteArray) (t : ℕ → ByteArray) (clientSk : nike.PrivateKey) (f targetSk : ℕ → nike.PrivateKey) (hvalid : geom.ValidForNIKE nike) (hmactag : macS.tagSize = Constants.macLength) (hs0size : (s 0).1.size = (geom.nrHops - nrHops) * geom.perHopRoutingInfoLength) (hstep : ∀ j < nrHops, ∃ (riFragment0 : ByteArray), Common.commandsToBytes (if (nrHops - 1 - j == nrHops - 1) = true then geom.perHopRoutingInfoLength else geom.perHopRoutingInfoLength - geom.nextNodeHopLength) path[nrHops - 1 - j]!.commands = Except.ok riFragment0 ∧ (s (j + 1)).1 = Common.xorBytes (Common.zeroPadTo geom.perHopRoutingInfoLength (if (nrHops - 1 - j == nrHops - 1) = true then riFragment0 else riFragment0 ++ (Commands.RoutingCommand.nextNodeHop path[nrHops - 1 - j + 1]!.id (Common.toVec32 (s j).2)).toBytes) ++ (s j).1) riKeyStream[nrHops - 1 - j]! ∧ (s (j + 1)).2 = Util.Bytes.ofVector (macS.mac (Util.Bytes.ofVector keys[nrHops - 1 - j]!.headerMAC) (Common.v0AD ++ groupElements[nrHops - 1 - j]! ++ (s (j + 1)).1 ++ if nrHops - 1 - j > 0 then riPadding[nrHops - 1 - j - 1]! else ByteArray.empty))) (hgnsize : groupElements.size = nrHops) (hgesize : ∀ (j : ℕ) (hj : j < groupElements.size), groupElements[j].size = nike.publicKeySize) (hgcontent : ∀ i < nrHops, groupElements[i]! = Util.Bytes.ofVector (nike.encodePublicKey ↑(Primitives.NIKE.NIKE.telescopeElem nike clientSk f i)) ∧ keys[i]! = deriveHopKeys kdfS (Util.Bytes.ofVector (nike.encodeSharedSecret ↑(Primitives.NIKE.NIKE.telescopeSecret nike clientSk (targetSk i) f i))) ∧ nike.decodePrivateKey (Common.toVecN nike.privateKeySize keys[i]!.blindingFactor) = some (f i)) (hpadsize : ∀ i < nrHops, riPadding[i]!.size = (i + 1) * geom.perHopRoutingInfoLength) (hriKScontent : ∀ i < nrHops, riKeyStream[i]! = (streamS.keystream (Util.Bytes.ofVector keys[i]!.headerEncryption) (Util.Bytes.ofVector keys[i]!.headerEncryptionIV) (geom.routingInfoLength + geom.perHopRoutingInfoLength)).extract 0 (geom.routingInfoLength + geom.perHopRoutingInfoLength - (i + 1) * geom.perHopRoutingInfoLength)) (hriPadcontent : ∀ i < nrHops, riPadding[i]! = have totalRiLen := geom.routingInfoLength + geom.perHopRoutingInfoLength; have ks := streamS.keystream (Util.Bytes.ofVector keys[i]!.headerEncryption) (Util.Bytes.ofVector keys[i]!.headerEncryptionIV) totalRiLen; have ksLen := totalRiLen - (i + 1) * geom.perHopRoutingInfoLength; have thisPad0 := ks.extract ksLen totalRiLen; if i > 0 then Common.xorBytes (thisPad0.extract 0 riPadding[i - 1]!.size) riPadding[i - 1]! ++ thisPad0.extract riPadding[i - 1]!.size thisPad0.size else thisPad0) (htsize : ∀ j ≤ sprpKeys.size, (t j).size = (t 0).size) (ht0size : (t 0).size = geom.payloadTagLength + geom.forwardPayloadLength) (htstep : ∀ j < sprpKeys.size, t (j + 1) = Cryptlib.Protocols.Sphinx.NIKESphinx.payloadEncryptStep✝ cipher sprpKeys (t j) j) (hsprpkey : ∀ (i : ℕ) (hi : i < sprpKeys.size), sprpKeys[i].key = keys[i]!.payloadEncryption ∧ sprpKeys[i].iv = keys[i]!.headerEncryptionIV) (hsprp : sprpKeys.size = nrHops) (hgen : nrHops ≤ geom.nrHops) (h16 : 16 ≤ geom.payloadTagLength + geom.forwardPayloadLength) (k : ℕ) (hk : k + 1 < nrHops) (hcmdnn : ∀ c ∈ path[k]!.commands, c ≠ Commands.RoutingCommand.null) (hcmdnh : ∀ c ∈ path[k]!.commands, ∀ (id m : Vector UInt8 32), c ≠ Commands.RoutingCommand.nextNodeHop id m) (privKey : ByteArray) (hpp : nike.decodePrivateKey (Common.toVecN nike.privateKeySize privKey) = some (targetSk k)) : ∃ (replayTag : Vector UInt8 32) (cmds : List Commands.RoutingCommand) (hnewsize : (Cryptlib.Protocols.Sphinx.NIKESphinx.hopPacket✝ groupElements riPadding s t nrHops (k + 1)).size = (Cryptlib.Protocols.Sphinx.NIKESphinx.hopPacket✝ groupElements riPadding s t nrHops k).size), unwrapNIKE nike cipher macS kdfS streamS geom privKey (Cryptlib.Protocols.Sphinx.NIKESphinx.hopPacket✝ groupElements riPadding s t nrHops k) = Except.ok (none, replayTag, cmds, some (Vector.mk (Cryptlib.Protocols.Sphinx.NIKESphinx.hopPacket✝ groupElements riPadding s t nrHops (k + 1)).data hnewsize)) ∧ cmds = path[k]!.commands ++ [Commands.RoutingCommand.nextNodeHop path[k + 1]!.id (Common.toVec32 (s (nrHops - 1 - k)).2)]

Non-terminal hop: unwrapNIKE on hopPacket ... k (k+1 < nrHops) yields hopPacket ... (k+1), given the hop's private key decodes to targetSk k.

theorem Cryptlib.Protocols.Sphinx.NIKESphinx.unwrapNIKE_hopPacket_terminal (nike : Primitives.NIKE.NIKE.NIKE) (cipher : Primitives.WideBlockCipher.WideBlockCipher) (macS : Primitives.MAC.MAC) (kdfS : Primitives.KDF.KDF) (streamS : Primitives.StreamCipher.StreamCipher) (geom : Geometry.Geometry) (path : Array Types.PathHop) (keys : Array HopKeys) (groupElements riKeyStream riPadding : Array ByteArray) (sprpKeys : Array Types.SPRPKey) (nrHops : ℕ) (s : ℕ → ByteArray × ByteArray) (t : ℕ → ByteArray) (clientSk : nike.PrivateKey) (f targetSk : ℕ → nike.PrivateKey) (hvalid : geom.ValidForNIKE nike) (hmactag : macS.tagSize = Constants.macLength) (hs0size : (s 0).1.size = (geom.nrHops - nrHops) * geom.perHopRoutingInfoLength) (hstep : ∀ j < nrHops, ∃ (riFragment0 : ByteArray), Common.commandsToBytes (if (nrHops - 1 - j == nrHops - 1) = true then geom.perHopRoutingInfoLength else geom.perHopRoutingInfoLength - geom.nextNodeHopLength) path[nrHops - 1 - j]!.commands = Except.ok riFragment0 ∧ (s (j + 1)).1 = Common.xorBytes (Common.zeroPadTo geom.perHopRoutingInfoLength (if (nrHops - 1 - j == nrHops - 1) = true then riFragment0 else riFragment0 ++ (Commands.RoutingCommand.nextNodeHop path[nrHops - 1 - j + 1]!.id (Common.toVec32 (s j).2)).toBytes) ++ (s j).1) riKeyStream[nrHops - 1 - j]! ∧ (s (j + 1)).2 = Util.Bytes.ofVector (macS.mac (Util.Bytes.ofVector keys[nrHops - 1 - j]!.headerMAC) (Common.v0AD ++ groupElements[nrHops - 1 - j]! ++ (s (j + 1)).1 ++ if nrHops - 1 - j > 0 then riPadding[nrHops - 1 - j - 1]! else ByteArray.empty))) (hgnsize : groupElements.size = nrHops) (hgesize : ∀ (j : ℕ) (hj : j < groupElements.size), groupElements[j].size = nike.publicKeySize) (hgcontent : ∀ i < nrHops, groupElements[i]! = Util.Bytes.ofVector (nike.encodePublicKey ↑(Primitives.NIKE.NIKE.telescopeElem nike clientSk f i)) ∧ keys[i]! = deriveHopKeys kdfS (Util.Bytes.ofVector (nike.encodeSharedSecret ↑(Primitives.NIKE.NIKE.telescopeSecret nike clientSk (targetSk i) f i))) ∧ nike.decodePrivateKey (Common.toVecN nike.privateKeySize keys[i]!.blindingFactor) = some (f i)) (hpadsize : ∀ i < nrHops, riPadding[i]!.size = (i + 1) * geom.perHopRoutingInfoLength) (hriKScontent : ∀ i < nrHops, riKeyStream[i]! = (streamS.keystream (Util.Bytes.ofVector keys[i]!.headerEncryption) (Util.Bytes.ofVector keys[i]!.headerEncryptionIV) (geom.routingInfoLength + geom.perHopRoutingInfoLength)).extract 0 (geom.routingInfoLength + geom.perHopRoutingInfoLength - (i + 1) * geom.perHopRoutingInfoLength)) (htsize : ∀ j ≤ sprpKeys.size, (t j).size = (t 0).size) (ht0size : (t 0).size = geom.payloadTagLength + geom.forwardPayloadLength) (htstep : ∀ j < sprpKeys.size, t (j + 1) = Cryptlib.Protocols.Sphinx.NIKESphinx.payloadEncryptStep✝ cipher sprpKeys (t j) j) (hsprpkey : ∀ (i : ℕ) (hi : i < sprpKeys.size), sprpKeys[i].key = keys[i]!.payloadEncryption ∧ sprpKeys[i].iv = keys[i]!.headerEncryptionIV) (hsprp : sprpKeys.size = nrHops) (hgen : nrHops ≤ geom.nrHops) (h16 : 16 ≤ geom.payloadTagLength + geom.forwardPayloadLength) (k : ℕ) (hk : k + 1 = nrHops) (hcmdnn : ∀ c ∈ path[k]!.commands, c ≠ Commands.RoutingCommand.null) (hcmdnh : ∀ c ∈ path[k]!.commands, ∀ (id m : Vector UInt8 32), c ≠ Commands.RoutingCommand.nextNodeHop id m) (hcmdsurb : ∀ c ∈ path[k]!.commands, ∀ (id : Vector UInt8 16), c ≠ Commands.RoutingCommand.surbReply id) (payload : ByteArray) (hpayloadsize : payload.size = geom.forwardPayloadLength) (ht0content : t 0 = { data := Array.replicate geom.payloadTagLength 0 } ++ payload) (privKey : ByteArray) (hpp : nike.decodePrivateKey (Common.toVecN nike.privateKeySize privKey) = some (targetSk k)) : unwrapNIKE nike cipher macS kdfS streamS geom privKey (Cryptlib.Protocols.Sphinx.NIKESphinx.hopPacket✝ groupElements riPadding s t nrHops k) = Except.ok (some payload, Primitives.Hash.Sha512.sha512_256 groupElements[k]!, path[k]!.commands, none)

Terminal hop: unwrapNIKE on hopPacket ... (nrHops - 1) reveals payload, given the hop's private key decodes to targetSk k.

theorem Cryptlib.Protocols.Sphinx.NIKESphinx.unwrapChain_hopPacket (nike : Primitives.NIKE.NIKE.NIKE) (cipher : Primitives.WideBlockCipher.WideBlockCipher) (macS : Primitives.MAC.MAC) (kdfS : Primitives.KDF.KDF) (streamS : Primitives.StreamCipher.StreamCipher) (geom : Geometry.Geometry) (path : Array Types.PathHop) (keys : Array HopKeys) (groupElements riKeyStream riPadding : Array ByteArray) (sprpKeys : Array Types.SPRPKey) (nrHops : ℕ) (s : ℕ → ByteArray × ByteArray) (t : ℕ → ByteArray) (clientSk : nike.PrivateKey) (f targetSk : ℕ → nike.PrivateKey) (hvalid : geom.ValidForNIKE nike) (hmactag : macS.tagSize = Constants.macLength) (hs0size : (s 0).1.size = (geom.nrHops - nrHops) * geom.perHopRoutingInfoLength) (hstep : ∀ j < nrHops, ∃ (riFragment0 : ByteArray), Common.commandsToBytes (if (nrHops - 1 - j == nrHops - 1) = true then geom.perHopRoutingInfoLength else geom.perHopRoutingInfoLength - geom.nextNodeHopLength) path[nrHops - 1 - j]!.commands = Except.ok riFragment0 ∧ (s (j + 1)).1 = Common.xorBytes (Common.zeroPadTo geom.perHopRoutingInfoLength (if (nrHops - 1 - j == nrHops - 1) = true then riFragment0 else riFragment0 ++ (Commands.RoutingCommand.nextNodeHop path[nrHops - 1 - j + 1]!.id (Common.toVec32 (s j).2)).toBytes) ++ (s j).1) riKeyStream[nrHops - 1 - j]! ∧ (s (j + 1)).2 = Util.Bytes.ofVector (macS.mac (Util.Bytes.ofVector keys[nrHops - 1 - j]!.headerMAC) (Common.v0AD ++ groupElements[nrHops - 1 - j]! ++ (s (j + 1)).1 ++ if nrHops - 1 - j > 0 then riPadding[nrHops - 1 - j - 1]! else ByteArray.empty))) (hgnsize : groupElements.size = nrHops) (hgesize : ∀ (j : ℕ) (hj : j < groupElements.size), groupElements[j].size = nike.publicKeySize) (hgcontent : ∀ i < nrHops, groupElements[i]! = Util.Bytes.ofVector (nike.encodePublicKey ↑(Primitives.NIKE.NIKE.telescopeElem nike clientSk f i)) ∧ keys[i]! = deriveHopKeys kdfS (Util.Bytes.ofVector (nike.encodeSharedSecret ↑(Primitives.NIKE.NIKE.telescopeSecret nike clientSk (targetSk i) f i))) ∧ nike.decodePrivateKey (Common.toVecN nike.privateKeySize keys[i]!.blindingFactor) = some (f i)) (hpadsize : ∀ i < nrHops, riPadding[i]!.size = (i + 1) * geom.perHopRoutingInfoLength) (hriKScontent : ∀ i < nrHops, riKeyStream[i]! = (streamS.keystream (Util.Bytes.ofVector keys[i]!.headerEncryption) (Util.Bytes.ofVector keys[i]!.headerEncryptionIV) (geom.routingInfoLength + geom.perHopRoutingInfoLength)).extract 0 (geom.routingInfoLength + geom.perHopRoutingInfoLength - (i + 1) * geom.perHopRoutingInfoLength)) (hriPadcontent : ∀ i < nrHops, riPadding[i]! = have totalRiLen := geom.routingInfoLength + geom.perHopRoutingInfoLength; have ks := streamS.keystream (Util.Bytes.ofVector keys[i]!.headerEncryption) (Util.Bytes.ofVector keys[i]!.headerEncryptionIV) totalRiLen; have ksLen := totalRiLen - (i + 1) * geom.perHopRoutingInfoLength; have thisPad0 := ks.extract ksLen totalRiLen; if i > 0 then Common.xorBytes (thisPad0.extract 0 riPadding[i - 1]!.size) riPadding[i - 1]! ++ thisPad0.extract riPadding[i - 1]!.size thisPad0.size else thisPad0) (htsize : ∀ j ≤ sprpKeys.size, (t j).size = (t 0).size) (ht0size : (t 0).size = geom.payloadTagLength + geom.forwardPayloadLength) (htstep : ∀ j < sprpKeys.size, t (j + 1) = Cryptlib.Protocols.Sphinx.NIKESphinx.payloadEncryptStep✝ cipher sprpKeys (t j) j) (hsprpkey : ∀ (i : ℕ) (hi : i < sprpKeys.size), sprpKeys[i].key = keys[i]!.payloadEncryption ∧ sprpKeys[i].iv = keys[i]!.headerEncryptionIV) (hsprp : sprpKeys.size = nrHops) (hgen : nrHops ≤ geom.nrHops) (h16 : 16 ≤ geom.payloadTagLength + geom.forwardPayloadLength) (hcmdnn : ∀ i < nrHops, ∀ c ∈ path[i]!.commands, c ≠ Commands.RoutingCommand.null) (hcmdnh : ∀ i < nrHops, ∀ c ∈ path[i]!.commands, ∀ (id m : Vector UInt8 32), c ≠ Commands.RoutingCommand.nextNodeHop id m) (hcmdsurb : ∀ c ∈ path[nrHops - 1]!.commands, ∀ (id : Vector UInt8 16), c ≠ Commands.RoutingCommand.surbReply id) (payload : ByteArray) (hpayloadsize : payload.size = geom.forwardPayloadLength) (ht0content : t 0 = { data := Array.replicate geom.payloadTagLength 0 } ++ payload) (k : ℕ) (privKeys : List ByteArray) (_hk : k < nrHops) (_hprivlen : privKeys.length = nrHops - k) (_hpp : ∀ i < privKeys.length, nike.decodePrivateKey (Common.toVecN nike.privateKeySize privKeys[i]!) = some (targetSk (k + i))) : Interface.unwrapChainAux (unwrapNIKE nike cipher macS kdfS streamS geom) privKeys (Cryptlib.Protocols.Sphinx.NIKESphinx.hopPacket✝ groupElements riPadding s t nrHops k) = Except.ok (some payload)

Unwrapping hopPacket ... k through the remaining hops, with private keys decoding to targetSk (k+i), recovers payload.

theorem Cryptlib.Protocols.Sphinx.NIKESphinx.wrapNIKE_envelope_indep (nike : Primitives.NIKE.NIKE.NIKE) (cipher : Primitives.WideBlockCipher.WideBlockCipher) (macS : Primitives.MAC.MAC) (kdfS : Primitives.KDF.KDF) (streamS : Primitives.StreamCipher.StreamCipher) (geom : Geometry.Geometry) (hop0 hop1 : Types.PathHop) (rest0 rest1 : List Types.PathHop) (payload0 payload1 : Vector UInt8 geom.forwardPayloadLength) (st : Interface.SeedStream) (pkt0 pkt1 : Vector UInt8 geom.packetLength) (st0' st1' : Interface.SeedStream) (hvalid : geom.ValidForNIKE nike) (hmactag : macS.tagSize = Constants.macLength) : wrapNIKE nike cipher macS kdfS streamS geom (hop0 :: rest0) payload0 st = EStateM.Result.ok pkt0 st0' → wrapNIKE nike cipher macS kdfS streamS geom (hop1 :: rest1) payload1 st = EStateM.Result.ok pkt1 st1' → (Util.Bytes.ofVector pkt0).extract 2 (2 + nike.publicKeySize) = (Util.Bytes.ofVector pkt1).extract 2 (2 + nike.publicKeySize)

The envelope bytes depend only on the seed drawn from state.

theorem Cryptlib.Protocols.Sphinx.NIKESphinx.wrapNIKE_unfold (nike : Primitives.NIKE.NIKE.NIKE) (cipher : Primitives.WideBlockCipher.WideBlockCipher) (macS : Primitives.MAC.MAC) (kdfS : Primitives.KDF.KDF) (streamS : Primitives.StreamCipher.StreamCipher) (geom : Geometry.Geometry) (path : List Types.PathHop) (payload : Vector UInt8 geom.forwardPayloadLength) (i : ℕ) (str : ℕ → Vector UInt8 32) (pkt : Vector UInt8 geom.packetLength) (st' : Interface.SeedStream) (h : wrapNIKE nike cipher macS kdfS streamS geom path payload (i, str) = EStateM.Result.ok pkt st') : newNIKEPacket nike cipher macS kdfS streamS geom (Util.Bytes.ofVector (str i)) (Interface.seedBytes str (i + 1) (Interface.fillerLength geom path.length)) path.toArray (Util.Bytes.ofVector payload) = Except.ok (Util.Bytes.ofVector pkt)

A successful wrapNIKE, unfolded: one seed and the filler are drawn, and newNIKEPacket succeeds on them producing pkt.

theorem Cryptlib.Protocols.Sphinx.NIKESphinx.wrapNIKE_unwrapNIKE_complete_valid (nike : Primitives.NIKE.NIKE.NIKE) (cipher : Primitives.WideBlockCipher.WideBlockCipher) (macS : Primitives.MAC.MAC) (kdfS : Primitives.KDF.KDF) (streamS : Primitives.StreamCipher.StreamCipher) (geom : Geometry.Geometry) (hvalid : geom.ValidForNIKE nike) (hmactag : macS.tagSize = Constants.macLength) (h16 : 16 ≤ geom.payloadTagLength + geom.forwardPayloadLength) (path : List Types.PathHop) (privKeys : List ByteArray) (payload : Vector UInt8 geom.forwardPayloadLength) (st : Interface.SeedStream) (pkt : Vector UInt8 geom.packetLength) (st' : Interface.SeedStream) (hpath : path ≠ []) (hpriv : List.map (fun (x : Types.PathHop) => x.publicKey) path = List.map (Cryptlib.Protocols.Sphinx.NIKESphinx.nikeSelfPublicKeyBytes✝ nike) privKeys) (hcmds : ∀ hop ∈ path, ∀ c ∈ hop.commands, c ≠ Commands.RoutingCommand.null ∧ ∀ (id m : Vector UInt8 32), c ≠ Commands.RoutingCommand.nextNodeHop id m) (hsurb : ∀ c ∈ path[path.length - 1]!.commands, ∀ (id : Vector UInt8 16), c ≠ Commands.RoutingCommand.surbReply id) (hwrap : wrapNIKE nike cipher macS kdfS streamS geom path payload st = EStateM.Result.ok pkt st') : Interface.unwrapChainAux (unwrapNIKE nike cipher macS kdfS streamS geom) privKeys (Util.Bytes.ofVector pkt) = Except.ok (some (Util.Bytes.ofVector payload))

Completeness: NIKESphinxScheme's witness for Sphinx.Interface.unwrap_complete.

def Cryptlib.Protocols.Sphinx.NIKESphinx.nikeSphinxCore (nike : Primitives.NIKE.NIKE.NIKE) (cipher : Primitives.WideBlockCipher.WideBlockCipher) (macS : Primitives.MAC.MAC) (kdfS : Primitives.KDF.KDF) (streamS : Primitives.StreamCipher.StreamCipher) (geom : Geometry.Geometry) (hvalid : geom.ValidForNIKE nike) (hmactag : macS.tagSize = Constants.macLength) (h16 : 16 ≤ geom.payloadTagLength + geom.forwardPayloadLength) : Interface.Sphinx

The executable Sphinx.Interface.Sphinx instance for nike, without the re-blindable envelope structure (which needs noncomputable instances).

Equations

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

noncomputable def Cryptlib.Protocols.Sphinx.NIKESphinx.nikeSphinxSchemeOf (nike : Primitives.NIKE.NIKE.NIKE) (cipher : Primitives.WideBlockCipher.WideBlockCipher) (macS : Primitives.MAC.MAC) (kdfS : Primitives.KDF.KDF) (streamS : Primitives.StreamCipher.StreamCipher) (geom : Geometry.Geometry) (hvalid : geom.ValidForNIKE nike) (hmactag : macS.tagSize = Constants.macLength) (h16 : 16 ≤ geom.payloadTagLength + geom.forwardPayloadLength) : NIKESphinxScheme

NIKESphinxScheme for any NIKE. Noncomputable; use nikeSphinxCore for executable code.

Equations

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

noncomputable def Cryptlib.Protocols.Sphinx.NIKESphinx.nikeSphinxScheme (geom : Geometry.Geometry) : Except String NIKESphinxScheme

NIKESphinxScheme for the NIKE named by geom.nikeName, with AEZ, HMAC-SHA256, HKDF-SHA256-Expand and AES-256-CTR. Rejects a geom not valid for that NIKE.

Equations

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