Increasing amounts of attention and money are paid to improving the security of hardware and software that are used to store digital assets, but no formal treatment has been given to the various design properties selected by different storage technology companies prior to the publication of this paper, which is the first formal model of Bitcoin ($BTC) hardware wallet operations. The properties and security parameters of Bitcoin wallets are identified and formally defined, and the scattered wallet and storage ecosystem is captured within certain shared assumptions. Lastly, the security of leading commercial wallets and possible attacks are analyzed.