Documentation

Cryptlib.Protocols.Sphinx.constants

Sphinx packet format constants #

Scheme-dependent lengths are computed in geometry.lean.

source
def Cryptlib.Protocols.Sphinx.Constants.nodeIDLength :
Nat
Equations
Instances For
    source
    def Cryptlib.Protocols.Sphinx.Constants.recipientIDLength :
    Nat
    Equations
    Instances For
      source
      def Cryptlib.Protocols.Sphinx.Constants.surbIDLength :
      Nat
      Equations
      Instances For
        source
        def Cryptlib.Protocols.Sphinx.Constants.commandTagLength :
        Nat

        The one-byte tag every routing command starts with.

        Equations
        Instances For
          source
          def Cryptlib.Protocols.Sphinx.Constants.macLength :
          Nat

          HMAC-SHA256 tag width.

          Equations
          Instances For
            source
            def Cryptlib.Protocols.Sphinx.Constants.streamIVLength :
            Nat

            AES-256-CTR IV width.

            Equations
            Instances For
              source
              def Cryptlib.Protocols.Sphinx.Constants.sprpKeyLength :
              Nat

              AEZ key and nonce widths.

              Equations
              Instances For
                source
                def Cryptlib.Protocols.Sphinx.Constants.sprpIVLength :
                Nat
                Equations
                Instances For
                  source
                  def Cryptlib.Protocols.Sphinx.Constants.nextNodeHopLength :
                  Nat

                  1 (tag) + nodeIDLength + macLength.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    def Cryptlib.Protocols.Sphinx.Constants.surbReplyLength :
                    Nat

                    1 (tag) + surbIDLength.

                    Equations
                    Instances For
                      source
                      def Cryptlib.Protocols.Sphinx.Constants.adLength :
                      Nat

                      The two-byte version prefix on every header.

                      Equations
                      Instances For
                        source
                        def Cryptlib.Protocols.Sphinx.Constants.payloadTagLength :
                        Nat

                        Width of the all-zero tag a correctly decrypted payload ends in.

                        Equations
                        Instances For
                          source
                          def Cryptlib.Protocols.Sphinx.Constants.sphinxPlaintextHeaderLength :
                          Nat
                          Equations
                          Instances For
                            source
                            def Cryptlib.Protocols.Sphinx.Constants.sprpKeyMaterialLength :
                            Nat

                            One SPRP key plus IV.

                            Equations
                            Instances For