• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Acre
    • Milawa
    • Smtlink
    • Aleobft
    • Abnf
    • Vwsim
    • Isar
    • Wp-gen
    • Dimacs-reader
    • Pfcs
    • Legacy-defrstobj
    • Proof-checker-array
    • Soft
    • Farray
    • Rp-rewriter
    • Instant-runoff-voting
    • Imp-language
    • Sidekick
    • Leftist-trees
    • C
    • Java
    • Taspi
    • Bitcoin
    • Des
    • Ethereum
    • X86isa
    • Sha-2
    • Yul
    • Riscv
    • Zcash
    • Proof-checker-itp13
    • Regex
    • ACL2-programming-language
    • Json
    • Jfkr
    • Equational
    • Cryptography
      • R1cs
      • Interfaces
      • Sha-2
      • Keccak
      • Kdf
      • Mimc
      • Padding
      • Hmac
      • Elliptic-curves
      • Attachments
      • Elliptic-curve-digital-signature-algorithm
    • Poseidon
    • Where-do-i-place-my-book
    • Bigmems
    • Builtins
    • Axe
    • Execloader
    • Solidity
    • Leo
    • Paco
    • Concurrent-programs
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Cryptography

Sha-2

A formal specification of the SHA-2 hash functions

The SHA-2 library contains executable formal specifications of several hash functions: SHA-224, SHA-256, SHA-384, and SHA-512. These algorithms are described in NIST publication FIPS PUB 180-4.

The library also includes tests of the specifications.

The following include-book commands may be helpful to bring in the library:

(include-book "kestrel/crypto/sha-2/sha-224" :dir :system)
(include-book "kestrel/crypto/sha-2/sha-256" :dir :system)
(include-book "kestrel/crypto/sha-2/sha-384" :dir :system)
(include-book "kestrel/crypto/sha-2/sha-512" :dir :system)

Or one can do:

(include-book "kestrel/crypto/sha-2/top" :dir :system)

The SHA-2 library contains two sets of interface functions: core functions that take lists of bits and additional convenience functions that take lists of bytes. All of the functions return the hash (or message digest) as a list of bytes. For both inputs and outputs, bytes are interpreted in a big-endian fashion. More precisely, a sequence of bytes can be converted to a sequence of bits by taking the bits from the first byte, starting with the most significant bit, then the bits of the next byte, and so on.

The interface functions are:

• (sha-224 bits) applies SHA-224 to the given list of bits, returning the hash as a list of 28 bytes.
• (sha-224-bytes bytes) applies SHA-224 to the given list of bytes, returning the hash as a list of 28 bytes.
• (sha-256 bits) applies SHA-256 to the given list of bits, returning the hash as a list of 32 bytes.
• (sha-256-bytes bytes) applies SHA-256 to the given list of bytes, returning the hash as a list of 32 bytes.
• (sha-384 bits) applies SHA-384 to the given list of bits, returning the hash as a list of 48 bytes.
• (sha-384-bytes bytes) applies SHA-384 to the given list of bytes, returning the hash as a list of 48 bytes.
• (sha-512 bits) applies SHA-512 to the given list of bits, returning the hash as a list of 64 bytes.
• (sha-512-bytes bytes) applies SHA-512 to the given list of bytes, returning the hash as a list of 64 bytes.

See the comments in the source files for more information.