Documentation

Cryptlib.Primitives.KDF.Argon2

Argon2 (RFC 9106), version 0x13 #

Argon2d, Argon2i and Argon2id, the memory-hard password hash. RFC 9106 recommends Argon2id.

Memory is one ByteArray of 1 KiB blocks, block j of lane l at l * laneLength + j. Words are 64-bit little-endian and are loaded into locals for the permutation, since an Array UInt64 would box every word. Lanes are filled one after another: within a slice no lane reads another lane's current segment, so the order does not change the result.

source
inductive Cryptlib.Primitives.KDF.Argon2.Variant :
Type
Instances For
    source
    def Cryptlib.Primitives.KDF.Argon2.instReprVariant.repr :
    Variant → Nat → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[instance_reducible]
      instance Cryptlib.Primitives.KDF.Argon2.instReprVariant :
      Repr Variant
      Equations
      source
      @[instance_reducible]
      instance Cryptlib.Primitives.KDF.Argon2.instBEqVariant :
      BEq Variant
      Equations
      source
      def Cryptlib.Primitives.KDF.Argon2.instBEqVariant.beq :
      Variant → Variant → Bool
      Equations
      Instances For
        source
        @[instance_reducible]
        instance Cryptlib.Primitives.KDF.Argon2.instDecidableEqVariant :
        DecidableEq Variant
        Equations
        source
        def Cryptlib.Primitives.KDF.Argon2.Variant.code :
        Variant → Nat

        The type field y of RFC 9106 §3.2.

        Equations
        Instances For
          source
          structure Cryptlib.Primitives.KDF.Argon2.Params :
          Type
          • variant : Variant
          • parallelism : Nat

            p, the number of lanes.

          • tagLength : Nat

            T, the tag length in bytes.

          • memoryKiB : Nat

            m, the memory size in KiB.

          • passes : Nat

            t, the number of passes.

          • secret : ByteArray

            K, the optional secret.

          • ad : ByteArray

            X, the optional associated data.

          Instances For
            source
            def Cryptlib.Primitives.KDF.Argon2.version :
            Nat
            Equations
            Instances For
              source
              def Cryptlib.Primitives.KDF.Argon2.hPrime (t : Nat) (x : ByteArray) :
              ByteArray

              RFC 9106 §3.3: the variable-length hash H'^T.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def Cryptlib.Primitives.KDF.Argon2.hPrime.go (t r : Nat) :
                Nat → ByteArray → ByteArray → ByteArray
                Equations
                Instances For
                  source
                  def Cryptlib.Primitives.KDF.Argon2.validate (p : Params) (password salt : ByteArray) :
                  Except String Unit

                  RFC 9106 §3.1 bounds on the parameters, in bytes and KiB.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    def Cryptlib.Primitives.KDF.Argon2.hash (p : Params) (password salt : ByteArray) :
                    Except String ByteArray

                    RFC 9106 §3.2: the Argon2 tag of password and salt.

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