Documentation

Cryptlib.Protocols.Sphinx.kem_sphinx_theorems

KEM-Sphinx #

Sphinx over a generic KEM. Unlike NIKE-Sphinx, each hop gets an independent encapsulation (no blinding), and each non-terminal hop's routing-info block carries the next hop's ciphertext in its last kem.ciphertextSize bytes.

source
def Cryptlib.Protocols.Sphinx.KEMSphinx.createKEMHeader (kem : Primitives.KEM.KEM.KEM) (macS : Primitives.MAC.MAC) (kdfS : Primitives.KDF.KDF) (streamS : Primitives.StreamCipher.StreamCipher) (geom : Geometry.Geometry) (ephemeralSeeds : Array (Vector UInt8 32)) (filler : ByteArray) (path : Array Types.PathHop) :
Except String (ByteArray × Array Types.SPRPKey)

Build a KEM-Sphinx header. ephemeralSeeds seeds one encapsulation per hop.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Cryptlib.Protocols.Sphinx.KEMSphinx.kemEncap_kemDecap_of_honest (kem : Primitives.KEM.KEM.KEM) (skBytes : ByteArray) (seedV : Vector UInt8 32) (ctBytes ssBytes : ByteArray) (hrel : kem.Reliable (kem.stateFromSeed seedV)) (henc : Cryptlib.Protocols.Sphinx.KEMSphinx.kemEncap✝ kem (Cryptlib.Protocols.Sphinx.KEMSphinx.kemSelfPublicKeyBytes✝ kem skBytes) seedV = Except.ok (ctBytes, ssBytes)) :
    Cryptlib.Protocols.Sphinx.KEMSphinx.kemDecap✝ kem skBytes ctBytes = Except.ok ssBytes

    If pkBytes is skBytes's own public key and encapsulation succeeds, decapsulating with skBytes recovers the same shared secret.

    source
    theorem Cryptlib.Protocols.Sphinx.KEMSphinx.kemRiFragment_content_terminal (kem : Primitives.KEM.KEM.KEM) (geom : Geometry.Geometry) (path : Array Types.PathHop) (kemElements : Array ByteArray) (macBytes : ByteArray) (nrHops i : ℕ) (_hi : i < nrHops) (hterm : i = nrHops - 1) (hcle : kem.ciphertextSize ≤ geom.perHopRoutingInfoLength) (hcmdnn : ∀ c ∈ path[i]!.commands, c ≠ Commands.RoutingCommand.null) (riFragment : ByteArray) (h : Cryptlib.Protocols.Sphinx.KEMSphinx.kemRiFragment✝ kem geom path kemElements macBytes nrHops i = Except.ok riFragment) :
    Commands.parseAll (riFragment.extract 0 (geom.perHopRoutingInfoLength - kem.ciphertextSize)) = Except.ok path[i]!.commands ∧ riFragment.extract (geom.perHopRoutingInfoLength - kem.ciphertextSize) geom.perHopRoutingInfoLength = { data := Array.replicate kem.ciphertextSize 0 }

    Terminal hop: the fragment's leading perHop - ctSize bytes parse to the hop's commands and the trailing ctSize bytes are zero.

    source
    theorem Cryptlib.Protocols.Sphinx.KEMSphinx.kemRiFragment_content_nonterminal (kem : Primitives.KEM.KEM.KEM) (geom : Geometry.Geometry) (path : Array Types.PathHop) (kemElements : Array ByteArray) (macBytes : ByteArray) (nrHops i : ℕ) (hi : i < nrHops) (hterm : i ≠ nrHops - 1) (hperhop : geom.nextNodeHopLength + kem.ciphertextSize ≤ geom.perHopRoutingInfoLength) (hnnh : geom.nextNodeHopLength = Constants.nextNodeHopLength) (hknsize : kemElements.size = nrHops) (hksize : ∀ (j : ℕ) (hj : j < kemElements.size), kemElements[j].size = kem.ciphertextSize) (hcmdnn : ∀ c ∈ path[i]!.commands, c ≠ Commands.RoutingCommand.null) (riFragment : ByteArray) (h : Cryptlib.Protocols.Sphinx.KEMSphinx.kemRiFragment✝ kem geom path kemElements macBytes nrHops i = Except.ok riFragment) :
    Commands.parseAll (riFragment.extract 0 (geom.perHopRoutingInfoLength - kem.ciphertextSize)) = Except.ok (path[i]!.commands ++ [Commands.RoutingCommand.nextNodeHop path[i + 1]!.id (Common.toVec32 macBytes)]) ∧ riFragment.extract (geom.perHopRoutingInfoLength - kem.ciphertextSize) geom.perHopRoutingInfoLength = kemElements[i + 1]!

    Non-terminal hop: the fragment's leading perHop - ctSize bytes parse to the hop's commands followed by NextNodeHop (next hop's ID, macBytes), and the trailing ctSize bytes are the next hop's ciphertext.

    source
    theorem Cryptlib.Protocols.Sphinx.KEMSphinx.createKEMHeader_hdr_size (kem : Primitives.KEM.KEM.KEM) (macS : Primitives.MAC.MAC) (kdfS : Primitives.KDF.KDF) (streamS : Primitives.StreamCipher.StreamCipher) (geom : Geometry.Geometry) (ephemeralSeeds : Array (Vector UInt8 32)) (filler : ByteArray) (path : Array Types.PathHop) (hdr : ByteArray) (sprpKeys : Array Types.SPRPKey) (hvalid : geom.ValidForKEM kem) (hmactag : macS.tagSize = Constants.macLength) (h : createKEMHeader kem macS kdfS streamS geom ephemeralSeeds filler path = Except.ok (hdr, sprpKeys)) :
    hdr.size = geom.headerLength

    createKEMHeader's header is geom.headerLength bytes.

    source
    def Cryptlib.Protocols.Sphinx.KEMSphinx.newKEMPacket (kem : Primitives.KEM.KEM.KEM) (cipher : Primitives.WideBlockCipher.WideBlockCipher) (macS : Primitives.MAC.MAC) (kdfS : Primitives.KDF.KDF) (streamS : Primitives.StreamCipher.StreamCipher) (geom : Geometry.Geometry) (ephemeralSeeds : Array (Vector UInt8 32)) (filler : ByteArray) (path : Array Types.PathHop) (payload : ByteArray) :
    Except String ByteArray

    Build a KEM-Sphinx packet.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Cryptlib.Protocols.Sphinx.KEMSphinx.newKEMPacket_size (kem : Primitives.KEM.KEM.KEM) (cipher : Primitives.WideBlockCipher.WideBlockCipher) (macS : Primitives.MAC.MAC) (kdfS : Primitives.KDF.KDF) (streamS : Primitives.StreamCipher.StreamCipher) (geom : Geometry.Geometry) (ephemeralSeeds : Array (Vector UInt8 32)) (filler : ByteArray) (path : Array Types.PathHop) (payload pkt : ByteArray) (hvalid : geom.ValidForKEM kem) (hmactag : macS.tagSize = Constants.macLength) (h : newKEMPacket kem cipher macS kdfS streamS geom ephemeralSeeds filler path payload = Except.ok pkt) (hpay : payload.size = geom.forwardPayloadLength) :
      pkt.size = geom.packetLength

      newKEMPacket's packet is geom.packetLength bytes.

      source
      def Cryptlib.Protocols.Sphinx.KEMSphinx.wrapKEM (kem : Primitives.KEM.KEM.KEM) (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)

      newKEMPacket with per-hop seeds and filler drawn from the seed stream.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Cryptlib.Protocols.Sphinx.KEMSphinx.newKEMSURB (kem : Primitives.KEM.KEM.KEM) (macS : Primitives.MAC.MAC) (kdfS : Primitives.KDF.KDF) (streamS : Primitives.StreamCipher.StreamCipher) (geom : Geometry.Geometry) (ephemeralSeeds : Array (Vector UInt8 32)) (keyPayload : Vector UInt8 64) (filler : ByteArray) (path : Array Types.PathHop) :
        Except String (ByteArray × ByteArray)

        Build a KEM-Sphinx SURB.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem Cryptlib.Protocols.Sphinx.KEMSphinx.newKEMSURB_size (kem : Primitives.KEM.KEM.KEM) (macS : Primitives.MAC.MAC) (kdfS : Primitives.KDF.KDF) (streamS : Primitives.StreamCipher.StreamCipher) (geom : Geometry.Geometry) (ephemeralSeeds : Array (Vector UInt8 32)) (keyPayload : Vector UInt8 64) (filler : ByteArray) (path : Array Types.PathHop) (hvalid : geom.ValidForKEM kem) (hmactag : macS.tagSize = Constants.macLength) (surb surbKeys : ByteArray) (h : newKEMSURB kem macS kdfS streamS geom ephemeralSeeds keyPayload filler path = Except.ok (surb, surbKeys)) :
          surb.size = geom.surbLength

          newKEMSURB's header is geom.headerLength bytes.

          source
          def Cryptlib.Protocols.Sphinx.KEMSphinx.wrapKEMSURB (kem : Primitives.KEM.KEM.KEM) (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)

          newKEMSURB with per-hop seeds, keyPayload and filler drawn from the seed stream.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Cryptlib.Protocols.Sphinx.KEMSphinx.unwrapKEM (kem : Primitives.KEM.KEM.KEM) (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))

            Process one hop: returns (payload, replayTag, cmds, forwardPkt). The forwarded packet carries the next-hop ciphertext copied from the decrypted routing-info block.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem Cryptlib.Protocols.Sphinx.KEMSphinx.unwrapKEM_hopPacket_nonterminal (kem : Primitives.KEM.KEM.KEM) (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 NIKESphinx.HopKeys) (kemElements riKeyStream riPadding : Array ByteArray) (sprpKeys : Array Types.SPRPKey) (nrHops : ℕ) (s : ℕ → ByteArray × ByteArray) (t : ℕ → ByteArray) (hvalid : geom.ValidForKEM kem) (hmactag : macS.tagSize = Constants.macLength) (hs0size : (s 0).1.size = (geom.nrHops - nrHops) * geom.perHopRoutingInfoLength) (hstep : ∀ j < nrHops, ∃ (riFragment : ByteArray), Cryptlib.Protocols.Sphinx.KEMSphinx.kemRiFragment✝ kem geom path kemElements (s j).2 nrHops (nrHops - 1 - j) = Except.ok riFragment ∧ (s (j + 1)).1 = Common.xorBytes (riFragment ++ (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 ++ kemElements[nrHops - 1 - j]! ++ (s (j + 1)).1 ++ if nrHops - 1 - j > 0 then riPadding[nrHops - 1 - j - 1]! else ByteArray.empty))) (hknsize : kemElements.size = nrHops) (hksize : ∀ (j : ℕ) (hj : j < kemElements.size), kemElements[j].size = kem.ciphertextSize) (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) (hkeyscontent : ∀ i < nrHops, ∃ (seed : Vector UInt8 32) (ss : ByteArray), kem.Reliable (kem.stateFromSeed seed) ∧ Cryptlib.Protocols.Sphinx.KEMSphinx.kemEncap✝ kem path[i]!.publicKey seed = Except.ok (kemElements[i]!, ss) ∧ keys[i]! = NIKESphinx.deriveHopKeys kdfS ss) (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.KEMSphinx.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 : Cryptlib.Protocols.Sphinx.KEMSphinx.kemSelfPublicKeyBytes✝ kem privKey = path[k]!.publicKey) :
              ∃ (replayTag : Vector UInt8 32) (cmds : List Commands.RoutingCommand) (hnewsize : (Cryptlib.Protocols.Sphinx.KEMSphinx.hopPacket✝ kemElements riPadding s t nrHops (k + 1)).size = (Cryptlib.Protocols.Sphinx.KEMSphinx.hopPacket✝ kemElements riPadding s t nrHops k).size), unwrapKEM kem cipher macS kdfS streamS geom privKey (Cryptlib.Protocols.Sphinx.KEMSphinx.hopPacket✝ kemElements riPadding s t nrHops k) = Except.ok (none, replayTag, cmds, some (Vector.mk (Cryptlib.Protocols.Sphinx.KEMSphinx.hopPacket✝ kemElements 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: given the honest key pairing at hop k (k+1 < nrHops), unwrapKEM maps hopPacket ... k to hopPacket ... (k+1).

              source
              theorem Cryptlib.Protocols.Sphinx.KEMSphinx.unwrapKEM_hopPacket_terminal (kem : Primitives.KEM.KEM.KEM) (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 NIKESphinx.HopKeys) (kemElements riKeyStream riPadding : Array ByteArray) (sprpKeys : Array Types.SPRPKey) (nrHops : ℕ) (s : ℕ → ByteArray × ByteArray) (t : ℕ → ByteArray) (hvalid : geom.ValidForKEM kem) (hmactag : macS.tagSize = Constants.macLength) (hs0size : (s 0).1.size = (geom.nrHops - nrHops) * geom.perHopRoutingInfoLength) (hstep : ∀ j < nrHops, ∃ (riFragment : ByteArray), Cryptlib.Protocols.Sphinx.KEMSphinx.kemRiFragment✝ kem geom path kemElements (s j).2 nrHops (nrHops - 1 - j) = Except.ok riFragment ∧ (s (j + 1)).1 = Common.xorBytes (riFragment ++ (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 ++ kemElements[nrHops - 1 - j]! ++ (s (j + 1)).1 ++ if nrHops - 1 - j > 0 then riPadding[nrHops - 1 - j - 1]! else ByteArray.empty))) (hknsize : kemElements.size = nrHops) (hksize : ∀ (j : ℕ) (hj : j < kemElements.size), kemElements[j].size = kem.ciphertextSize) (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) (hkeyscontent : ∀ i < nrHops, ∃ (seed : Vector UInt8 32) (ss : ByteArray), kem.Reliable (kem.stateFromSeed seed) ∧ Cryptlib.Protocols.Sphinx.KEMSphinx.kemEncap✝ kem path[i]!.publicKey seed = Except.ok (kemElements[i]!, ss) ∧ keys[i]! = NIKESphinx.deriveHopKeys kdfS ss) (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.KEMSphinx.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 : Cryptlib.Protocols.Sphinx.KEMSphinx.kemSelfPublicKeyBytes✝ kem privKey = path[k]!.publicKey) :
              unwrapKEM kem cipher macS kdfS streamS geom privKey (Cryptlib.Protocols.Sphinx.KEMSphinx.hopPacket✝ kemElements riPadding s t nrHops k) = Except.ok (some payload, Primitives.Hash.Sha512.sha512_256 kemElements[k]!, path[k]!.commands, none)

              Terminal hop: given the honest key pairing at hop k (k + 1 = nrHops) and t 0 a zero tag followed by payload, unwrapKEM on hopPacket ... k recovers payload.

              source
              theorem Cryptlib.Protocols.Sphinx.KEMSphinx.unwrapChain_hopPacket (kem : Primitives.KEM.KEM.KEM) (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 NIKESphinx.HopKeys) (kemElements riKeyStream riPadding : Array ByteArray) (sprpKeys : Array Types.SPRPKey) (nrHops : ℕ) (s : ℕ → ByteArray × ByteArray) (t : ℕ → ByteArray) (hvalid : geom.ValidForKEM kem) (hmactag : macS.tagSize = Constants.macLength) (hs0size : (s 0).1.size = (geom.nrHops - nrHops) * geom.perHopRoutingInfoLength) (hstep : ∀ j < nrHops, ∃ (riFragment : ByteArray), Cryptlib.Protocols.Sphinx.KEMSphinx.kemRiFragment✝ kem geom path kemElements (s j).2 nrHops (nrHops - 1 - j) = Except.ok riFragment ∧ (s (j + 1)).1 = Common.xorBytes (riFragment ++ (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 ++ kemElements[nrHops - 1 - j]! ++ (s (j + 1)).1 ++ if nrHops - 1 - j > 0 then riPadding[nrHops - 1 - j - 1]! else ByteArray.empty))) (hknsize : kemElements.size = nrHops) (hksize : ∀ (j : ℕ) (hj : j < kemElements.size), kemElements[j].size = kem.ciphertextSize) (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) (hkeyscontent : ∀ i < nrHops, ∃ (seed : Vector UInt8 32) (ss : ByteArray), kem.Reliable (kem.stateFromSeed seed) ∧ Cryptlib.Protocols.Sphinx.KEMSphinx.kemEncap✝ kem path[i]!.publicKey seed = Except.ok (kemElements[i]!, ss) ∧ keys[i]! = NIKESphinx.deriveHopKeys kdfS ss) (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.KEMSphinx.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, Cryptlib.Protocols.Sphinx.KEMSphinx.kemSelfPublicKeyBytes✝ kem privKeys[i]! = path[k + i]!.publicKey) :
              Interface.unwrapChainAux (unwrapKEM kem cipher macS kdfS streamS geom) privKeys (Cryptlib.Protocols.Sphinx.KEMSphinx.hopPacket✝ kemElements riPadding s t nrHops k) = Except.ok (some payload)

              Unwrapping hopPacket ... k with the remaining private keys for path[k], path[k+1], ... recovers payload.

              source
              theorem Cryptlib.Protocols.Sphinx.KEMSphinx.wrapKEM_unfold (kem : Primitives.KEM.KEM.KEM) (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 : wrapKEM kem cipher macS kdfS streamS geom path payload (i, str) = EStateM.Result.ok pkt st') :
              ∃ (seeds : Array (Vector UInt8 32)), seeds.size = path.length ∧ (∀ j < path.length, seeds[j]! = str (i + j)) ∧ newKEMPacket kem cipher macS kdfS streamS geom seeds (Interface.seedBytes str (i + path.toArray.size) (Interface.fillerLength geom path.length)) path.toArray (Util.Bytes.ofVector payload) = Except.ok (Util.Bytes.ofVector pkt)

              A successful wrapKEM call drew per-hop seeds str (i + j) and the filler from the seed stream, and newKEMPacket succeeded on them producing pkt.

              source
              theorem Cryptlib.Protocols.Sphinx.KEMSphinx.wrapKEM_unwrapKEM_complete_valid (kem : Primitives.KEM.KEM.KEM) (cipher : Primitives.WideBlockCipher.WideBlockCipher) (macS : Primitives.MAC.MAC) (kdfS : Primitives.KDF.KDF) (streamS : Primitives.StreamCipher.StreamCipher) (geom : Geometry.Geometry) (hvalid : geom.ValidForKEM kem) (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.KEMSphinx.kemSelfPublicKeyBytes✝ kem) 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) (hrel : ∀ j < path.length, kem.Reliable (kem.stateFromSeed (st.2 (st.1 + j)))) (hwrap : wrapKEM kem cipher macS kdfS streamS geom path payload st = EStateM.Result.ok pkt st') :
              Interface.unwrapChainAux (unwrapKEM kem cipher macS kdfS streamS geom) privKeys (Util.Bytes.ofVector pkt) = Except.ok (some (Util.Bytes.ofVector payload))

              Completeness: unwrapping a wrapKEM packet hop by hop recovers the payload. Requires geom.ValidForKEM kem and 16 ≤ geom.payloadTagLength + geom.forwardPayloadLength.

              source
              def Cryptlib.Protocols.Sphinx.KEMSphinx.kemSphinxSchemeOf (kem : Primitives.KEM.KEM.KEM) (cipher : Primitives.WideBlockCipher.WideBlockCipher) (macS : Primitives.MAC.MAC) (kdfS : Primitives.KDF.KDF) (streamS : Primitives.StreamCipher.StreamCipher) (geom : Geometry.Geometry) (hvalid : geom.ValidForKEM kem) (hmactag : macS.tagSize = Constants.macLength) (h16 : 16 ≤ geom.payloadTagLength + geom.forwardPayloadLength) :
              KEMSphinxScheme

              A KEMSphinxScheme for any KEM, MAC, KDF, stream cipher and wide-block cipher.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def Cryptlib.Protocols.Sphinx.KEMSphinx.kemSphinxScheme (geom : Geometry.Geometry) :
                Except String KEMSphinxScheme

                A KEMSphinxScheme for the KEM geom.kemName names, with AEZ, HMAC-SHA256, HKDF-SHA256-Expand and AES-256-CTR. Rejects a geom that fails the validity checks.

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

                  Wrap-resistance fails #

                  KEM-Sphinx has no blinding step. A holder of privKey can compute the header keystream for any ciphertext, so every target routing-info block is reachable.

                  source
                  theorem Cryptlib.Protocols.Sphinx.KEMSphinx.unwrapKEM_routingInfoBlock_not_wrap_resistant (streamS : Primitives.StreamCipher.StreamCipher) (key iv target : ByteArray) :
                  ∃ (raw : ByteArray), Common.xorBytes raw (streamS.keystream key iv target.size) = target

                  KEM-Sphinx is not wrap-resistant: for any routing-info block target, some pre-decryption bytes decrypt to exactly target.