Wallets and authorization

In this section, we review wallet accounts and spending authorization. We use Lean to model wallet authority and specify a decidable spending policy.

Our main reference is the PASS wallet model.

In PASS #

pass-wallet/pass-lean4-proofs models assets, wallet accounts, and transaction processing. In PassAccount.lean at 2a488ac, PassAccount holds assets, an inbox, an outbox, and transaction history.

processInternalTx requires both checkBalance and checkAllow before processing a transfer or withdrawal. checkBalance looks up the asset and the sender's funds. At this revision, checkAllow always returns true. It is a policy hook, not an implemented spending restriction.

Withdrawals enter the outbox. outboxSubmit builds different transactions for native Ether and contract tokens: the Ether branch uses transaction value, while the token branch targets a contract and places recipient and amount in call data. An internal wallet record and an on-chain transaction are distinct stages in this source.

Spending policy #

For example, an agent controls an account with 0.01 ETH but may pay at most 0.003 ETH to an approved recipient.

Our model concentrates on the policy decision before payment. It assigns an account and asset to an agent, with a per-payment limit and permitted recipients:

structure Wallet where
  owner : AgentId
  account : AccountId
  asset : AssetId
  perCallLimit : Amount asset
  recipients : List AccountId
  deriving DecidableEq, Repr

A request supplies the exact payer, recipient, asset, and amount. CanSpend states the policy checks:

def CanSpend (wallet : Wallet) (actor : AgentId) (request : SpendRequest) : Prop :=
  actor = wallet.owner ∧
  request.payer = wallet.account ∧
  request.asset = wallet.asset ∧
  request.amount.units ≤ wallet.perCallLimit.units ∧
  request.payee ∈ wallet.recipients ∧
  request.payer.network = request.asset.network ∧
  request.payee.network = request.asset.network

This is our concrete policy for the role occupied by PASS's checkAllow hook; it is not a claim that PASS implements these checks. The actor identifier is already authenticated, and the policy is a fixed input. Key custody and signing are outside this decision.

AP2 payment authorization extends this study to signed evidence that a merchant and payment provider can verify for a particular checkout.

In the example, the owner may pay 0.003 ETH to the permitted recipient. One wei above the limit, another actor, another payer, or another recipient is rejected. decide (CanSpend wallet owner request) evaluates the proposition. No balance changes when the policy is checked. Repeated payments each below the limit can exceed that amount in total: a per-payment limit is not a session budget.

For comparison, Coinbase's Agentic Wallet controls describe per-call and per-session limits. Those product documents describe configuration; PASS supplies the implementation examined in this note.