• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • 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
          • Mmp-trees
          • Semaphore
          • Database
          • Cryptography
            • Rlp
            • Transactions
            • Hex-prefix
            • Basics
            • Addresses
          • Yul
          • Zcash
          • ACL2-programming-language
          • Prime-fields
          • Java
          • C
          • Syntheto
          • Number-theory
          • Cryptography
          • Lists-light
          • File-io-light
          • Json
          • Built-ins
          • Solidity
          • Axe
          • Std-extensions
          • Htclient
          • Typed-lists-light
          • Arithmetic-light
        • X86isa
        • Execloader
        • Axe
      • Testing-utilities
      • Math
    • Ethereum

    Cryptography

    Cryptography in Ethereum.

    Ethereum uses a number of cryptographic functions that are described in external standards. Our Ethereum model uses cryptographic functions from these cryptographic libraries.

    Our current Ethereum model uses the following cryptographic functions. Most of these links go to the interface documentation first, and most of the interface documents have links to executable specifications.

    • keccak-256-bytes, which corresponds to \mathtt{KEC} [YP:3].
    • sha-256-bytes
    • sha-512-bytes
    • RIPEMD-160 (link coming)
    • hmac-sha-512
    • pbkdf2-hmac-sha-512
    • secp256k1-priv-to-pub, which corresponds to \mathtt{ECDSAPUBKEY} [YP:F] (modulo a different but isomorphic data representation, namely byte arrays for the former, and ecurve::secp256k1-priv-key and ecurve::secp256k1-pub-key values for the latter).
    • secp256k1-sign-det-rec, which corresponds to \mathtt{ECDSASIGN} [YP:F] in essence, but see make-signed-transaction for details.