pith. sign in

arxiv: 2604.22602 · v1 · submitted 2026-04-24 · 💻 cs.CR

PASS: A Provenanced Access Subaccount System for Blockchain Wallets

Jay Yu , Shunfan Zhou , Hang Yin , Brian Seong This is my paper

Pith reviewed 2026-05-08 11:17 UTC · model grok-4.3

classification 💻 cs.CR
keywords blockchain walletsprovenancesubaccountsprivacycustodyenclavesformal verificationWalletConnect
0
0 comments X

The pith

PASS replaces private-key ownership in blockchain wallets with provenance-based subaccounts that trace custody back to deposits.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes that blockchain wallets can move beyond single-owner private-key control by introducing subaccounts whose access rights depend on verifiable provenance from original deposits. This matters for settings like AI agents, shared organizational custody, and payroll where multiple parties need coordinated action without exposing secrets or revealing internal transfers. An Inbox-Outbox mechanism makes every external action traceable while internal movements stay private and look like ordinary accounts. The authors formalize the design in Lean 4 to prove privacy, accessibility, and integrity invariants, then build a working prototype using secure enclaves and standard wallet interfaces. The results indicate that provenance-based wallets can be both secure and practical for real use.

Core claim

PASS defines a provenance-based access model in which assets held by a subaccount are usable only if the subaccount can demonstrate an unbroken custody chain back to a valid deposit; the Inbox-Outbox mechanism records external inflows and outflows to enforce this lineage while internal transfers between subaccounts remain hidden from external observers and indistinguishable from standard externally owned accounts.

What carries the argument

The Inbox-Outbox mechanism, which logs deposit provenance and external actions to enforce traceable custody while shielding internal transfers.

If this is right

  • Organizational and enterprise wallets can coordinate multiple users on shared assets without distributing private keys.
  • AI agent wallets gain traceable action histories while preserving privacy of internal state.
  • Existing wallet software and services such as WalletConnect remain compatible because internal operations look like ordinary account activity.
  • Formal proofs in Lean 4 guarantee that provenance integrity and transfer privacy hold under the stated model.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The approach could be adapted to other ledgers or smart-contract platforms that need auditable yet private multi-party access.
  • If enclaves prove reliable at scale, similar provenance tracking might apply to non-blockchain custody systems such as digital asset platforms.
  • Deployment data from the prototype could be used to test whether real-world transaction patterns still satisfy the indistinguishability property under heavy load.

Load-bearing premise

The enclave-backed implementation of the Inbox-Outbox mechanism can maintain verifiable provenance and privacy in live blockchain environments without creating new attack surfaces or performance problems that break the security claims.

What would settle it

An external observer or attacker can either move assets from a subaccount without a valid deposit provenance trace or distinguish an internal subaccount transfer from a normal externally owned account transaction.

Figures

Figures reproduced from arXiv: 2604.22602 by Brian Seong, Hang Yin, Jay Yu, Shunfan Zhou.

Figure 1
Figure 1. Figure 1: Overview of PASS. External deposits enter the Inbox and are claimed by sub￾accounts. Internal transfers are private and off-chain. Egress occurs via the Outbox, which signs and broadcasts on-chain transactions. All on-chain activity has clear prove￾nance; internal movements remain private. 3.1 High-level system model PASS is a multi-user wallet on a single EOA (sk, pk). The wallet maintains a finite set of… view at source ↗
Figure 2
Figure 2. Figure 2: Formal Model of PASS wallet functionality, including CreatePassWallet for initializing a fresh instance. On creation, pk is set to a chosen EOA address eoa, the TEE generates a hidden private key sk, and global data structures are initialized. External deposits enter I (Inbox), while subaccount transfers update L (Ledger) off￾chain. Withdrawals queue items in O (Outbox), and GSM operations are signed using… view at source ↗
Figure 3
Figure 3. Figure 3: PASS instantiation inside a zkVM: Inbox I and Outbox O transitions are applied to the Ledger L and Provenance H, producing new state commitments. The zkVM outputs a proof π, which the on-chain verifier checks before updating roots and enforcing outbox operations view at source ↗
read the original abstract

Blockchain wallets conventionally follow an ownership model where possession of a private key grants unilateral control. However, this assumption is brittle for emerging settings such as AI agent wallets, organizational custody, and enterprise payroll, where multiple actors must coordinate without exposing secrets or leaking internal activity. We present PASS, a Provenanced Access Subaccount System that replaces role-based or identity-based control with provenance-based control: assets can only be used by subaccounts that can trace custody back to a valid deposit. A simple Inbox-Outbox mechanism ensures all external actions have verifiable lineage, while internal transfers remain private and indistinguishable from ordinary EOAs. We formalize PASS in Lean 4 and prove core invariants, including privacy of internal transfers, asset accessibility, and provenance integrity. We implement a prototype with enclave backends on AWS Nitro Enclaves and dstack Intel TDX, integrate with WalletConnect, and benchmark throughput across wallet operations. These results show that provenance-based wallets are both implementable and efficient. PASS bridges today's gap between strict self-custody and flexible shared access, advancing the design space for practical, privacy-preserving custody.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 1 minor

Summary. The paper introduces PASS, a provenance-based access control system for blockchain wallets that uses an Inbox-Outbox mechanism to enforce verifiable lineage for external actions while preserving privacy for internal transfers. It claims to formalize the core model and invariants (privacy of internal transfers, asset accessibility, provenance integrity) in Lean 4, implement a prototype using AWS Nitro Enclaves and Intel TDX enclaves integrated with WalletConnect, and demonstrate efficiency via throughput benchmarks across wallet operations.

Significance. If the formalization and implementation claims hold, PASS provides a concrete advance in moving beyond rigid self-custody or role-based models toward provenance-driven shared custody suitable for AI agents and organizational settings, with the machine-checked Lean 4 proofs and enclave-backed prototype serving as notable strengths for verifiability and practicality.

major comments (2)
  1. [Formalization section] Formalization section (around the Lean 4 model and proofs of invariants): The proofs of privacy, accessibility, and provenance integrity treat the enclave backend as an idealized trusted primitive that correctly isolates subaccount state. However, the model does not encode attestation, side-channel resistance, or enclave compromise scenarios, so the proven invariants do not transfer to the AWS Nitro Enclaves and dstack Intel TDX deployments described in the implementation section; this is load-bearing for the security claims.
  2. [Implementation and Evaluation sections] Implementation and Evaluation sections: The prototype claims to enforce the proven invariants via enclave backends, yet no explicit mapping or refinement proof is provided linking the idealized Lean model to the concrete hardware and WalletConnect integration; without this, the efficiency benchmarks cannot be taken as evidence that the system preserves the claimed security properties in deployment.
minor comments (1)
  1. [Abstract] The abstract and introduction could more precisely state the exact invariants proven in Lean 4 (e.g., by naming the theorems) rather than summarizing them at a high level.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their thorough review and constructive comments. We address each major comment below and will revise the manuscript accordingly to improve clarity on the scope of our formal results and the relationship to the prototype.

read point-by-point responses

  1. Referee: [Formalization section] Formalization section (around the Lean 4 model and proofs of invariants): The proofs of privacy, accessibility, and provenance integrity treat the enclave backend as an idealized trusted primitive that correctly isolates subaccount state. However, the model does not encode attestation, side-channel resistance, or enclave compromise scenarios, so the proven invariants do not transfer to the AWS Nitro Enclaves and dstack Intel TDX deployments described in the implementation section; this is load-bearing for the security claims.

    Authors: We agree that the Lean 4 formalization abstracts the enclave as an idealized trusted primitive and does not encode attestation, side-channel resistance, or compromise scenarios. This is by design: the model focuses on proving the provenance, privacy, and accessibility invariants under the assumption of a correctly functioning trusted execution environment. The paper does not claim that the proofs cover hardware-specific threats. In revision we will add explicit text in the formalization section stating these modeling assumptions and noting that the invariants hold only relative to the enclave primitive. This will make the transfer to the AWS Nitro and Intel TDX deployments conditional on those platforms satisfying the assumed isolation properties. revision: yes

  2. Referee: [Implementation and Evaluation sections] Implementation and Evaluation sections: The prototype claims to enforce the proven invariants via enclave backends, yet no explicit mapping or refinement proof is provided linking the idealized Lean model to the concrete hardware and WalletConnect integration; without this, the efficiency benchmarks cannot be taken as evidence that the system preserves the claimed security properties in deployment.

    Authors: We acknowledge that the manuscript provides no formal refinement or mapping proof between the Lean model and the concrete enclave-based prototype with WalletConnect. The implementation section presents a practical realization that follows the model’s structure, with the enclave supplying the trusted primitive assumed in the formalization. The benchmarks measure throughput and are not offered as evidence of security preservation. In revision we will add an informal mapping subsection in the implementation section describing how model elements (Inbox/Outbox, subaccount state, provenance checks) are realized in the AWS Nitro / Intel TDX code, and we will revise the evaluation section to state explicitly that performance results assume the enclave upholds the model’s trusted primitive. A full machine-checked refinement proof is beyond the current scope and is noted as future work. revision: partial

Circularity Check

0 steps flagged

No circularity detected; formalization and implementation are independent

full rationale

The paper introduces PASS as a new construction using an Inbox-Outbox mechanism for provenance-based control, then separately formalizes the system in Lean 4 to prove invariants (privacy of internal transfers, asset accessibility, provenance integrity) and implements a prototype on specific enclave hardware with WalletConnect integration and benchmarks. No equations, definitions, or claims reduce by construction to their own inputs, fitted parameters renamed as predictions, or load-bearing self-citations. The Lean proofs and prototype are external to the initial definition and constitute independent verification steps. The paper is self-contained against its stated benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The central claim rests on standard blockchain ownership assumptions and introduces new mechanisms and entities without independent evidence outside the paper.

axioms (1)
  • domain assumption Conventional blockchain wallets grant unilateral control via private key possession
    This is the baseline model the paper contrasts with its provenance approach.
invented entities (1)
  • Provenanced Access Subaccount no independent evidence
    purpose: Enable traceable custody and access control based on deposit lineage
    Core new concept introduced to replace role-based or identity-based control.

pith-pipeline@v0.9.0 · 5493 in / 1356 out tokens · 38944 ms · 2026-05-08T11:17:30.571289+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

45 extracted references · 13 canonical work pages

  1. [1]

    a16z crypto: Helios: Ethereum light client.https://github.com/a16z/helios (2025), gitHub repository, accessed: 2025-09-14

    2025

  2. [2]

    Argent: Build with Argent (2023),https://docs.argent.xyz/

    2023

  3. [3]

    Cryptology ePrint Archive, Paper 2023/1217 (2023),https://eprint.iacr.org/ 2023/1217

    Arun, A., Setty, S., Thaler, J.: Jolt: SNARKs for virtual machines via lookups. Cryptology ePrint Archive, Paper 2023/1217 (2023),https://eprint.iacr.org/ 2023/1217

    2023

  4. [4]

    BIS Working Papers 1013, Bank for International Settlements (2023),https://www.bis.org/publ/work101 3.htm

    Auer, R., Farag, M., Lewrick, U., Orazem, L., Zoss, M.: Banking in the shadow of bitcoin? the institutional adoption of cryptocurrencies. BIS Working Papers 1013, Bank for International Settlements (2023),https://www.bis.org/publ/work101 3.htm

    2023

  5. [5]

    Cryptology ePrint Archive, Paper 2022/317 (2022).https: //doi.org/10.1145/3548606.3560556,https://eprint.iacr.org/2022/317

    Aumayr, L., Abbaszadeh, K., Maffei, M.: Thora: Atomic and privacy-preserving multi-channel updates. Cryptology ePrint Archive, Paper 2022/317 (2022).https: //doi.org/10.1145/3548606.3560556,https://eprint.iacr.org/2022/317

    work page doi:10.1145/3548606.3560556 2022

  6. [6]

    Cryptology ePrint Archive, Paper 2025/272 (2025),https://eprint.iacr.org/2025/272 PASS: A Provenanced Access Subaccount System for Blockchain Wallets 17

    Aumayr, L., Avarikioti, Z., Salem, I., Schmid, S., Yeo, M.: X-transfer: Enabling and optimizing cross-PCN transactions. Cryptology ePrint Archive, Paper 2025/272 (2025),https://eprint.iacr.org/2025/272 PASS: A Provenanced Access Subaccount System for Blockchain Wallets 17

    2025

  7. [7]

    arXiv e-prints 2412.02634(2024), arXiv:2412.02634 [cs.CR]

    Austgen, J., F´ abrega, A., Kelkar, M., Vilardell, D., Allen, S., Babel, K., Yu, J., Juels, A.: Liquefaction: Privately liquefying blockchain assets. arXiv e-prints 2412.02634(2024), arXiv:2412.02634 [cs.CR]

    work page arXiv 2024

  8. [8]

    Forbes (2025),https://www.forbes.com/sites/digital-assets/2025 /02/22/breaking-could-bybits-14b-hack-have-been-stopped-ledger-cz-r eact/

    Bambysheva, N.: Breaking: Could Bybit’s$1.5B hack have been stopped? Ledger, CZ react. Forbes (2025),https://www.forbes.com/sites/digital-assets/2025 /02/22/breaking-could-bybits-14b-hack-have-been-stopped-ledger-cz-r eact/

    2025

  9. [9]

    In: Proceedings of the 7th International Conference on Information Systems Security and Privacy (ICISSP)

    Brunner, D., Karame, G.O., Li, W., Tschorsch, F.: Who stores the private key? an exploratory study about user preferences of key management for blockchain-based applications. In: Proceedings of the 7th International Conference on Information Systems Security and Privacy (ICISSP). pp. 276–287. SciTePress (2021).https: //doi.org/10.5220/0010226102760287,htt...

    work page doi:10.5220/0010226102760287 2021

  10. [10]

    Ethereum whitepaper,https://ethereum.org/en/whitepaper/ (2014), accessed: 2024-10-16

    Buterin, V.: Ethereum: A next-generation smart contract and decentralized appli- cation platform. Ethereum whitepaper,https://ethereum.org/en/whitepaper/ (2014), accessed: 2024-10-16

    2014

  11. [11]

    Contributors, E.: Decentralized autonomous organizations (DAOs).https://ethe reum.org/en/dao/, accessed: 2024-11-13

    2024

  12. [12]

    Cutler, Craig Disselkoen, Aaron Eline, Shaobo He, Kyle Headley, Michael Hicks, Kesha Hietala, Eleftherios Ioannidis, John Kastner, Anwar Mamat, et al

    Cutler, J.W., Disselkoen, C., Eline, A., He, S., Headley, K., Hicks, M., Hietala, K., Ioannidis, E., Kastner, J., Mamat, A., McAdams, D., McCutchen, M., Rungta, N., Torlak, E., Wells, A.M.: Cedar: A new language for expressive, fast, safe, and analyzable authorization. arXiv preprint arXiv:2403.04651 (2024),https://arxi v.org/pdf/2403.04651

    work page arXiv 2024

  13. [13]

    ERC-4337 Documentation: UserOperation – ERC-4337 Documentation (2023),ht tps://www.erc4337.io/docs/understanding-ERC-4337/user-operation

    2023

  14. [14]

    Future Internet17(1), 7 (2024).https://doi.org/10.3390/fi17010007,https: //www.mdpi.com/1999-5903/17/1/7

    Erinle, Y., et al.: Shared-custodial wallet for multi-party crypto-asset management. Future Internet17(1), 7 (2024).https://doi.org/10.3390/fi17010007,https: //www.mdpi.com/1999-5903/17/1/7

    work page doi:10.3390/fi17010007 2024

  15. [15]

    FINCEN- 2020-0002; RIN 1506-AB41, 31 CFR Parts 1010, 1020

    Financial Crimes Enforcement Network, Department of the Treasury: Threshold for the requirement to collect, retain, and transmit information on funds transfers and transmittals of funds that begin or end outside the united states, and clarifica- tion of the requirement to collect, retain, and transmit information on transactions involving convertible virt...

    2020

  16. [16]

    Fireblocks: Governance and policy engine (2025),https://www.fireblocks.com /platforms/governance-and-policy-engine/

    2025

  17. [17]

    Goldman Sachs Research: Crypto: A new asset class? (2021),https://www.gold mansachs.com/insights/top-of-mind/crypto-a-new-asset-class

    2021

  18. [18]

    Intel: Performance Considerations of Intel®Trust Domain Extensions on 4th Gen- eration Intel®Xeon®Scalable Processors (2025),https://www.intel.com/cont ent/www/us/en/developer/articles/technical/trust-domain-extensions-o n-4th-gen-xeon-processors.html

    2025

  19. [19]

    Applied Economics pp

    Kong, B., Choi, M., Shin, J., Lee, D.: What wallet features do users want for their cryptocurrencies? conjoint analysis of user preferences in cryptocurrency wallets. Applied Economics pp. 1–15 (2025).https://doi.org/10.1080/00036846.2025. 2536752,https://doi.org/10.1080/00036846.2025.2536752 18 J. Yu et al

    work page doi:10.1080/00036846.2025 2025

  20. [20]

    Lean Community: Lean Documentation (2025),https://lean-lang.org/docume ntation/

    2025

  21. [21]

    loopring.io/

    Loopring: Loopring Smart Wallet Documentation (2023),https://docs-wallet. loopring.io/

    2023

  22. [22]

    In: Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security

    Mangipudi, E.V., Desai, U., Minaei, M., Mondal, M., Kate, A.: Uncovering impact of mental models towards adoption of multi-device crypto-wallets. In: Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security. pp. 3153–3167 (2023).https://doi.org/10.1145/3576915.3623218,https: //dl.acm.org/doi/10.1145/3576915.3623218

    work page doi:10.1145/3576915.3623218 2023

  23. [23]

    In: HASP

    McKeen, F., Alexandrovich, I., Berenzon, A., Rozas, C.V., Shafi, H., Shanbhogue, V., Savagaonkar, U.R.: Innovative instructions and software model for isolated execution. In: HASP. p. 10 (2013)

    2013

  24. [24]

    arXiv preprint arXiv:2101.06291 (2021),https://arxiv.org/abs/2101.06291

    Moosavi, M., Clark, J.: Lissy: Experimenting with on-chain order books. arXiv preprint arXiv:2101.06291 (2021),https://arxiv.org/abs/2101.06291

    work page arXiv 2021

  25. [25]

    Oasis Labs: Oasis protocol: Privacy-enabled blockchain platform.https://oasisp rotocol.org/(2024),https://oasisprotocol.org/, accessed: 2024-10-06

    2024

  26. [26]

    Patairya, D.K.: What are smart contract wallets? Cointelegraph (2024),https: //cointelegraph.com/explained/what-are-smart-contract-wallets

    2024

  27. [27]

    Cryptology ePrint Archive, Paper 2025/526 (2025),https://eprint.iacr.org/2025/526

    Patlan, A.S., Sheng, P., Hebbar, S.A., Mittal, P., Viswanath, P.: AI agents in cryp- toland: Practical attacks and no silver bullet. Cryptology ePrint Archive, Paper 2025/526 (2025),https://eprint.iacr.org/2025/526

    2025

  28. [28]

    Pertsev, A., Semenov, R., Storm, R.: Tornado cash privacy solution version 1.4 (2019),https://berkeley-defi.github.io/assets/material/Tornado%20Cash %20Whitepaper.pdf

    2019

  29. [29]

    Safe: How do Safe Smart Accounts work? (2025),https://docs.safe.global/a dvanced/smart-account-concepts

    2025

  30. [30]

    Schneider, M., Masti, R.J., Shinde, S., Capkun, S., Perez, R.: Sok: Hardware- supported trusted execution environments (2022),https://arxiv.org/abs/2205 .12742

    2022

  31. [31]

    Seehausen, V.: Eip-7702: A win for smart accounts in ethereum’s pectra upgrade? Safe Global Blog (2024),https://safe.global/blog/eip-7702-smart-account s-ethereum-pectra-upgrade

    2024

  32. [32]

    Seong, B., Gebheim, P.: Chainless apps: A modular framework for building apps with web2 capability and web3 trust (2025),https://arxiv.org/abs/2505.22989

    work page arXiv 2025

  33. [33]

    Sign-In with Ethereum Documentation: EIP-4361: Sign-In with Ethereum (2023), https://docs.login.xyz/general-information/siwe-overview/eip-4361

    2023

  34. [34]

    box/user-guides/voting/vote

    Snapshot Documentation: Voting on Snapshot (2023),https://docs.snapshot. box/user-guides/voting/vote

    2023

  35. [35]

    Tally: Gnosis Safe Overview (2025),https://docs.tally.xyz/set-up-and-tec hnical-documentation/using-governor-with-gnosis-safe/gnosis-safe

    2025

  36. [36]

    IEEE Access10, 93039–93054 (2022).https://doi.org/10.110 9/ACCESS.2022.3200051

    Thibault, L.T., Sarry, T., Hafid, A.S.: Blockchain scaling using rollups: A compre- hensive survey. IEEE Access10, 93039–93054 (2022).https://doi.org/10.110 9/ACCESS.2022.3200051

    work page arXiv 2022

  37. [37]

    Turnkey: Policy quickstart (2025),https://docs.turnkey.com/concepts/polici es/quickstart

    2025

  38. [38]

    Venly: Omnibus vs Segregated Wallets in Crypto (2025),https://docs.venly.i o/docs/omnibus-vs-segregated-wallets-in-crypto

    2025

  39. [39]

    arXiv preprint arXiv:2501.06781 (2025),https://arxiv.org/ pdf/2501.06781v1 PASS: A Provenanced Access Subaccount System for Blockchain Wallets 19

    Walters, S., Gao, S., Nerd, S., Da, F., Williams, W., Meng, T.C., Han, H., He, F., Zhang, A., Wu, M., Shen, T., Hu, M., Yan, J.: Eliza: A web3 friendly ai agent operating system. arXiv preprint arXiv:2501.06781 (2025),https://arxiv.org/ pdf/2501.06781v1 PASS: A Provenanced Access Subaccount System for Blockchain Wallets 19

    work page arXiv 2025

  40. [40]

    Wormhole Foundation: Guardians (2025),https://wormhole.com/docs/learn/ infrastructure/guardians/

    2025

  41. [41]

    Proceedings of the ACM on Human-Computer Interaction 8(CSCW2), 1–27 (2024).https://doi.org/10.1145/3642534,https://dl.acm.o rg/doi/10.1145/3642534

    Yu, Y., Chang, M., Reijers, W., McAuley, D.: How cryptocurrency users choose and secure their wallets. Proceedings of the ACM on Human-Computer Interaction 8(CSCW2), 1–27 (2024).https://doi.org/10.1145/3642534,https://dl.acm.o rg/doi/10.1145/3642534

    work page doi:10.1145/3642534 2024

  42. [42]

    Our goal is to prove that, under the PASS design, several critical security properties always hold

    Zhou, S., Wang, K., Yin, H.: Dstack: A Zero Trust Framework for Confidential Containers (2025),https://arxiv.org/abs/2509.11555 A Formal Verification We consider the formal model introduced in Section 3 of PASS as a state machine in Lean4. Our goal is to prove that, under the PASS design, several critical security properties always hold. We outline these ...

    work page arXiv 2025

  43. [43]

    Letting getAsset(W, α) return the assetαwithin stateWor⊥, we require∀α: totalBalance getAsset(W1, α) = totalBalance getAsset(W2, α)

    For every asset identifierα, the total balance of that asset inA 1 equals the total balance of the same asset inA 2. Letting getAsset(W, α) return the assetαwithin stateWor⊥, we require∀α: totalBalance getAsset(W1, α) = totalBalance getAsset(W2, α) . Theorem 2 (Privacy of Internal Transfers).If two PassAccount statesW 1 andW 2 differ only by internal tran...

  44. [44]

    For every addressu∈L, the user can access their full balance: checkBalance(s, α, u,balance(u)) =true

  45. [45]

    When checking against the user’s own balance, this is trivially satisfied sinceL[u][α]≥ L[u][α] for allu

    The sum of all accessible balances equals the total balance of the asset: X u∈L L[u][α] =totalBalance(α) Proof.We constructLas the set of all addresses with non-zero balances in the balance map forα: L={u| L[u][α]>0} For the first property, given anyu∈L, the definition ofcheckBalanceverifies if the user has sufficient balance for the specified amount. Whe...