• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
      • Isar
      • Wp-gen
      • Dimacs-reader
      • Pfcs
      • Legacy-defrstobj
      • Proof-checker-array
      • Soft
      • C
      • Farray
      • Rp-rewriter
      • Instant-runoff-voting
      • Imp-language
      • Sidekick
      • Leftist-trees
      • Java
      • Taspi
      • 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
      • Riscv
      • Des
      • Ethereum
      • X86isa
      • Sha-2
      • Yul
      • Zcash
      • Proof-checker-itp13
      • Regex
      • ACL2-programming-language
      • Json
      • Jfkr
      • Equational
      • Cryptography
      • Poseidon
      • Where-do-i-place-my-book
      • Axe
      • Bigmems
      • Builtins
      • Execloader
      • Aleo
      • Solidity
      • Paco
      • Concurrent-programs
      • Bls12-377-curves
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • 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.