Documentation

Cryptlib.Protocols.Sphinx.geometry

Sphinx packet geometry #

Every fixed byte offset of the header, routing-info, and packet layout, computed from a hop count, a payload size, and a NIKE or KEM.

source
structure Cryptlib.Protocols.Sphinx.Geometry.Geometry :
Type
  • packetLength : ℕ
  • nrHops : ℕ
  • headerLength : ℕ
  • routingInfoLength : ℕ
  • perHopRoutingInfoLength : ℕ
  • surbLength : ℕ
  • sphinxPlaintextHeaderLength : ℕ
  • payloadTagLength : ℕ
  • forwardPayloadLength : ℕ
  • userForwardPayloadLength : ℕ
  • nextNodeHopLength : ℕ
  • sprpKeyMaterialLength : ℕ
  • nikeName : String

    The NIKE scheme name; empty for a KEM geometry.

  • kemName : String

    The KEM scheme name; empty for a NIKE geometry.

Instances For
    source
    def Cryptlib.Protocols.Sphinx.Geometry.instReprGeometry.repr :
    Geometry → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[instance_reducible]
      instance Cryptlib.Protocols.Sphinx.Geometry.instReprGeometry :
      Repr Geometry
      Equations
      source
      def Cryptlib.Protocols.Sphinx.Geometry.instDecidableEqGeometry.decEq (x✝ x✝¹ : Geometry) :
      Decidable (x✝ = x✝¹)
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[instance_reducible]
        instance Cryptlib.Protocols.Sphinx.Geometry.instDecidableEqGeometry :
        DecidableEq Geometry
        Equations
        source
        @[instance_reducible]
        instance Cryptlib.Protocols.Sphinx.Geometry.instInhabitedGeometry :
        Inhabited Geometry
        Equations
        source
        def Cryptlib.Protocols.Sphinx.Geometry.ofNIKE (nikeSchemeName : String) (userForwardPayloadLength : ℕ) (withSURB : Bool) (nrHops : ℕ) :
        Except String Geometry

        Geometry for a NIKE named nikeSchemeName, with the given user payload length.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Cryptlib.Protocols.Sphinx.Geometry.ofKEM (kemSchemeName : String) (userForwardPayloadLength : ℕ) (withSURB : Bool) (nrHops : ℕ) :
          Except String Geometry

          Geometry for a KEM named kemSchemeName, with the given user payload length.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Cryptlib.Protocols.Sphinx.Geometry.ofNIKETargetSize (nikeSchemeName : String) (targetPacketLength : ℕ) (withSURB : Bool) (nrHops : ℕ) :
            Except String Geometry

            Geometry for a NIKE whose total packet length is targetPacketLength. Fails if it is smaller than the fixed overhead.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Cryptlib.Protocols.Sphinx.Geometry.ofKEMTargetSize (kemSchemeName : String) (targetPacketLength : ℕ) (withSURB : Bool) (nrHops : ℕ) :
              Except String Geometry

              As ofNIKETargetSize, for a KEM.

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

                Checks that exactly one scheme name is set, that it names a registered scheme, and that the header dimensions are nonzero.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  @[instance_reducible]
                  instance Cryptlib.Protocols.Sphinx.Geometry.instToStringGeometry :
                  ToString Geometry
                  Equations
                  • One or more equations did not get rendered due to their size.
                  source
                  @[reducible]
                  def Cryptlib.Protocols.Sphinx.Geometry.Geometry.ValidForNIKE (geom : Geometry) (nike : Primitives.NIKE.NIKE.NIKE) :
                  Prop

                  geom has the field values buildNIKE gives for nike.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    @[reducible]
                    def Cryptlib.Protocols.Sphinx.Geometry.Geometry.ValidForKEM (geom : Geometry) (kem : Primitives.KEM.KEM.KEM) :
                    Prop

                    geom has the field values buildKEM gives for kem.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      def Cryptlib.Protocols.Sphinx.Geometry.ofNIKEWith (label : String) (nike : Primitives.NIKE.NIKE.NIKE) (userForwardPayloadLength : ℕ) (withSURB : Bool) (nrHops : ℕ) :
                      Geometry

                      As ofNIKE, for a NIKE given directly rather than by name. label is only stored.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        theorem Cryptlib.Protocols.Sphinx.Geometry.ofNIKEWith_validForNIKE (label : String) (nike : Primitives.NIKE.NIKE.NIKE) (userForwardPayloadLength : ℕ) (withSURB : Bool) (nrHops : ℕ) :
                        (ofNIKEWith label nike userForwardPayloadLength withSURB nrHops).ValidForNIKE nike

                        ofNIKEWith nike is valid for nike.

                        source
                        theorem Cryptlib.Protocols.Sphinx.Geometry.ofNIKEWith_payloadTagLength (label : String) (nike : Primitives.NIKE.NIKE.NIKE) (userForwardPayloadLength : ℕ) (withSURB : Bool) (nrHops : ℕ) :
                        (ofNIKEWith label nike userForwardPayloadLength withSURB nrHops).payloadTagLength = Constants.payloadTagLength

                        ofNIKEWith sets payloadTagLength.

                        source
                        def Cryptlib.Protocols.Sphinx.Geometry.ofKEMWith (label : String) (kem : Primitives.KEM.KEM.KEM) (userForwardPayloadLength : ℕ) (withSURB : Bool) (nrHops : ℕ) :
                        Geometry

                        As ofNIKEWith, for a KEM.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          source
                          theorem Cryptlib.Protocols.Sphinx.Geometry.ofKEMWith_validForKEM (label : String) (kem : Primitives.KEM.KEM.KEM) (userForwardPayloadLength : ℕ) (withSURB : Bool) (nrHops : ℕ) :
                          (ofKEMWith label kem userForwardPayloadLength withSURB nrHops).ValidForKEM kem
                          source
                          theorem Cryptlib.Protocols.Sphinx.Geometry.ofKEMWith_payloadTagLength (label : String) (kem : Primitives.KEM.KEM.KEM) (userForwardPayloadLength : ℕ) (withSURB : Bool) (nrHops : ℕ) :
                          (ofKEMWith label kem userForwardPayloadLength withSURB nrHops).payloadTagLength = Constants.payloadTagLength
                          source
                          theorem Cryptlib.Protocols.Sphinx.Geometry.ofNIKE_validForNIKE (nikeSchemeName : String) (userForwardPayloadLength : ℕ) (withSURB : Bool) (nrHops : ℕ) (geom : Geometry) (nike : Primitives.NIKE.NIKE.NIKE) (h : ofNIKE nikeSchemeName userForwardPayloadLength withSURB nrHops = Except.ok geom) (hn : Primitives.NIKE.byName nikeSchemeName = some nike) :
                          geom.ValidForNIKE nike
                          source
                          theorem Cryptlib.Protocols.Sphinx.Geometry.ofKEM_validForKEM (kemSchemeName : String) (userForwardPayloadLength : ℕ) (withSURB : Bool) (nrHops : ℕ) (geom : Geometry) (kem : Primitives.KEM.KEM.KEM) (h : ofKEM kemSchemeName userForwardPayloadLength withSURB nrHops = Except.ok geom) (hk : Primitives.KEM.byName kemSchemeName = some kem) :
                          geom.ValidForKEM kem
                          source
                          theorem Cryptlib.Protocols.Sphinx.Geometry.ofKEM_payloadTagLength (kemSchemeName : String) (userForwardPayloadLength : ℕ) (withSURB : Bool) (nrHops : ℕ) (geom : Geometry) (h : ofKEM kemSchemeName userForwardPayloadLength withSURB nrHops = Except.ok geom) :
                          geom.payloadTagLength = Constants.payloadTagLength

                          ofKEM sets payloadTagLength.

                          source
                          theorem Cryptlib.Protocols.Sphinx.Geometry.ofNIKE_payloadTagLength (nikeSchemeName : String) (userForwardPayloadLength : ℕ) (withSURB : Bool) (nrHops : ℕ) (geom : Geometry) (h : ofNIKE nikeSchemeName userForwardPayloadLength withSURB nrHops = Except.ok geom) :
                          geom.payloadTagLength = Constants.payloadTagLength

                          ofNIKE sets payloadTagLength.

                          source
                          theorem Cryptlib.Protocols.Sphinx.Geometry.ofNIKETargetSize_packetLength (nikeSchemeName : String) (targetPacketLength : ℕ) (withSURB : Bool) (nrHops : ℕ) (geom : Geometry) (h : ofNIKETargetSize nikeSchemeName targetPacketLength withSURB nrHops = Except.ok geom) :
                          geom.packetLength = targetPacketLength

                          ofNIKETargetSize produces a geometry with exactly the target packet length.

                          source
                          theorem Cryptlib.Protocols.Sphinx.Geometry.ofKEMTargetSize_packetLength (kemSchemeName : String) (targetPacketLength : ℕ) (withSURB : Bool) (nrHops : ℕ) (geom : Geometry) (h : ofKEMTargetSize kemSchemeName targetPacketLength withSURB nrHops = Except.ok geom) :
                          geom.packetLength = targetPacketLength

                          As ofNIKETargetSize_packetLength, for a KEM.