• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Set
        • Soft
        • C
        • Bv
        • Imp-language
        • Event-macros
        • Java
        • Bitcoin
          • Bip32
            • Bip32-wallet-structure
            • Bip32-key-trees
            • Bip32-key-serialization
            • Bip32-key-derivation
            • Bip32-executable-attachments
            • Bip32-extended-keys
            • Bip32-master-key-generation
          • Bech32
          • Bip39
          • Bip44
          • Base58
          • Bip43
          • Bytes
          • Base58check
          • Cryptography
          • Bip-350
          • Bip-173
        • Ethereum
        • Yul
        • Zcash
        • ACL2-programming-language
        • Prime-fields
        • Json
        • Syntheto
        • File-io-light
        • Cryptography
        • Number-theory
        • Lists-light
        • Axe
        • Builtins
        • Solidity
        • Helpers
        • Htclient
        • Typed-lists-light
        • Arithmetic-light
      • X86isa
      • Axe
      • Execloader
    • Math
    • Testing-utilities
  • Bitcoin

Bip32

Bitcoin Improvement Proposal (BIP) 32.

This is described at this page in the bitcoin/bips repository on GitHub, linked from Page `BIP 0032' of [Wiki]. We refer to the document at the first URL as `[BIP32]' in the documentation below.

As stated in the 'Conventions' section of [BIP32], the elliptic curve cryptography is based on the secp256k1 curve. In our model, the types for private and public keys are secp256k1-priv-key-p and secp256k1-pub-key-p.

The conversion functions described in the 'Conventions' section of [BIP32] are formalized as follows in our model of Bitcoin:

  • \mathsf{point} is secp256k1-mul with point secp256k1-point-generator; when the argument is a private key, we use secp256k1-priv-to-pub.
  • \mathsf{ser}_{32} is nat=>bebytes with width 4.
  • \mathsf{ser}_{256} is nat=>bebytes with width 32.
  • \mathsf{ser}_\mathsf{P} is secp256k1-point-to-bytes with the compression flag set.
  • \mathsf{parse}_{256} is bebytes=>nat.

The operations defined below should suffice to cover the use cases that BIP 32 should cater to:

  • Given a seed, bip32-master-tree is used to generate a singleton tree with the master private key at the root.
  • This master tree is extended as needed, via bip32-extend-tree.
  • For signing, private keys can be retrieved from the tree via bip32-get-priv-key-at-path. For calculating addresses, auditing, etc., public keys can be retrieved from the tree via bip32-get-pub-key-at-path.
  • For sharing (subtrees of) the master tree, bip32-export-key is used to serialize a (private or public) key. Then bip32-import-key is used to construct a separate (sub)tree rooted at that key.
  • (Sub)trees shared as just explained can be then operated upon via bip32-extend-tree for deriving more keys, bip32-get-priv-key-at-path for signing (unless the tree consists of public keys), bip32-get-pub-key-at-path for calculating addresses, auditing, etc., and bip32-export-key for further sharing.

Subtopics

Bip32-wallet-structure
Wallet structure.
Bip32-key-trees
Key trees.
Bip32-key-serialization
Key serialization.
Bip32-key-derivation
Key derivation functions.
Bip32-executable-attachments
Executable attachments for the BIP 32 formalization.
Bip32-extended-keys
Extended keys.
Bip32-master-key-generation
Master key generation.