• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Debugging
    • Projects
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Error-checking
        • Apt
        • Abnf
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Prime-field-constraint-systems
        • Soft
        • Bv
        • Imp-language
        • Event-macros
        • Bitcoin
        • Ethereum
        • Yul
        • Zcash
        • ACL2-programming-language
        • Prime-fields
        • Java
        • C
        • Syntheto
        • Number-theory
        • Cryptography
          • R1cs
          • Interfaces
            • Definterface-hmac
            • Definterface-encrypt-block
            • Definterface-hash
            • Definterface-encrypt-init
            • Definterface-pbkdf2
            • Aes-256-cbc-pkcs7-interface
            • Aes-192-cbc-pkcs7-interface
            • Aes-128-cbc-pkcs7-interface
            • Aes-256-interface
            • Aes-192-interface
            • Aes-128-interface
            • Pbkdf2-hmac-sha-512-interface
              • Keccak-256-interface
              • Keccak-512-interface
              • Sha-256-interface
              • Ripemd-160-interface
              • Sha-512-interface
              • Pbkdf2-hmac-sha-256-interface
              • Hmac-sha-512-interface
              • Hmac-sha-256-interface
              • Secp256k1-interface
              • Secp256k1-ecdsa-interface
            • Sha-2
            • Keccak
            • Kdf
            • Mimc
            • Padding
            • Hmac
            • Elliptic-curves
            • Attachments
            • Elliptic-curve-digital-signature-algorithm
          • Lists-light
          • File-io-light
          • Json
          • Built-ins
          • Solidity
          • Axe
          • Std-extensions
          • Htclient
          • Typed-lists-light
          • Arithmetic-light
        • X86isa
        • Execloader
        • Axe
      • Testing-utilities
      • Math
    • Interfaces

    Pbkdf2-hmac-sha-512-interface

    PBKDF2-HMAC-SHA-512 interface.

    PBKDF2 stands for Password-Based Key Derivation Function 2. It is defined in IETF RFC 8018.

    We instantiate PBKDF2 with the pseudorandom function HMAC-SHA-512.

    See also:

    • PBKDF2-HMAC-SHA-512 executable specification
    • attaching PBKDF2-HMAC-SHA-512 executable specification to this interface

    Definitions and Theorems

    Theorem: byte-list-of-pbkdf2-hmac-sha-512

    (defthm
     byte-list-of-pbkdf2-hmac-sha-512
     (byte-listp (pbkdf2-hmac-sha-512 password salt iterations length)))

    Theorem: len-of-pbkdf2-hmac-sha-512

    (defthm
      len-of-pbkdf2-hmac-sha-512
      (equal (len (pbkdf2-hmac-sha-512 password salt iterations length))
             (pos-fix length)))

    Theorem: pbkdf2-hmac-sha-512-of-byte-list-fix-password

    (defthm
         pbkdf2-hmac-sha-512-of-byte-list-fix-password
         (equal (pbkdf2-hmac-sha-512 (byte-list-fix password)
                                     salt iterations length)
                (pbkdf2-hmac-sha-512 password salt iterations length)))

    Theorem: pbkdf2-hmac-sha-512-byte-list-equiv-congruence-on-password

    (defthm
     pbkdf2-hmac-sha-512-byte-list-equiv-congruence-on-password
     (implies
      (byte-list-equiv password password-equiv)
      (equal
           (pbkdf2-hmac-sha-512 password salt iterations length)
           (pbkdf2-hmac-sha-512 password-equiv salt iterations length)))
     :rule-classes :congruence)

    Theorem: pbkdf2-hmac-sha-512-of-byte-list-fix-salt

    (defthm
         pbkdf2-hmac-sha-512-of-byte-list-fix-salt
         (equal (pbkdf2-hmac-sha-512 password (byte-list-fix salt)
                                     iterations length)
                (pbkdf2-hmac-sha-512 password salt iterations length)))

    Theorem: pbkdf2-hmac-sha-512-byte-list-equiv-congruence-on-salt

    (defthm
     pbkdf2-hmac-sha-512-byte-list-equiv-congruence-on-salt
     (implies
      (byte-list-equiv salt salt-equiv)
      (equal
           (pbkdf2-hmac-sha-512 password salt iterations length)
           (pbkdf2-hmac-sha-512 password salt-equiv iterations length)))
     :rule-classes :congruence)

    Theorem: pbkdf2-hmac-sha-512-of-pos-fix-iterations

    (defthm
         pbkdf2-hmac-sha-512-of-pos-fix-iterations
         (equal (pbkdf2-hmac-sha-512 password salt (pos-fix iterations)
                                     length)
                (pbkdf2-hmac-sha-512 password salt iterations length)))

    Theorem: pbkdf2-hmac-sha-512-pos-equiv-congruence-on-iterations

    (defthm
     pbkdf2-hmac-sha-512-pos-equiv-congruence-on-iterations
     (implies
      (acl2::pos-equiv iterations iterations-equiv)
      (equal
           (pbkdf2-hmac-sha-512 password salt iterations length)
           (pbkdf2-hmac-sha-512 password salt iterations-equiv length)))
     :rule-classes :congruence)

    Theorem: pbkdf2-hmac-sha-512-of-pos-fix-length

    (defthm
         pbkdf2-hmac-sha-512-of-pos-fix-length
         (equal (pbkdf2-hmac-sha-512 password
                                     salt iterations (pos-fix length))
                (pbkdf2-hmac-sha-512 password salt iterations length)))

    Theorem: pbkdf2-hmac-sha-512-pos-equiv-congruence-on-length

    (defthm
     pbkdf2-hmac-sha-512-pos-equiv-congruence-on-length
     (implies
      (acl2::pos-equiv length length-equiv)
      (equal
           (pbkdf2-hmac-sha-512 password salt iterations length)
           (pbkdf2-hmac-sha-512 password salt iterations length-equiv)))
     :rule-classes :congruence)

    Theorem: true-listp-of-pbkdf2-hmac-sha-512

    (defthm
      true-listp-of-pbkdf2-hmac-sha-512
      (true-listp (pbkdf2-hmac-sha-512 password salt iterations length))
      :rule-classes :type-prescription)

    Theorem: consp-of-pbkdf2-hmac-sha-512

    (defthm
         consp-of-pbkdf2-hmac-sha-512
         (consp (pbkdf2-hmac-sha-512 password salt iterations length))
         :rule-classes :type-prescription)