Resource Locks and Fast Unlock for Shared Balances in Certificate-Based Payment Systems

Resource Locks and Fast Unlock for Shared Balances in Certificate-Based Payment Systems

arXiv:2610.41207v1 [cs.DC] 30 Oct 2026

Lingkang Shangguan, Student Member, IEEE The University of Sydney lsha0379@uni.sydney.edu.au Version 1.0

Abstract Certificate-based payment systems such as FastPay settle a payment with one round of signatures from a quorum of validators and avoid global ordering. The client collects the signatures, and validators never talk to each other. We observe that this client-driven design is complete only as long as no lock is ever undone. Each account has a single writer, a conflict can only come from that writer’s own misbehavior, and the account stays locked as the penalty. Stablecoin payments routinely need balances that several accounts debit: treasuries, merchant pools, allowances and subscriptions. There, honest accounts race, locks must be undone, and a quorum certificate held privately by a client can be silently overridden. We prove that no unlock rule is safe in this setting unless certificate formation is visible to validators. We present a hybrid protocol. Personal accounts keep the client-driven FastPay path unchanged. A shared resource is a balance with its own version number and a set of authorized accounts. Transactions on shared resources are submitted to any validator and certified by a two-phase broadcast, Echo then Ready. The admission check requires both the sender’s nonce and the resource’s nonce to be free. Without contention, this path needs no consensus. When concurrent debits split the votes in any proportion, validators detect the split themselves, freeze the affected resource version, and resolve it with one agreement instance scoped to that version. Losing transactions return their sender nonce. We prove consistency, no overdraft, validity, finality and liveness. The protocol composes with the PDCC reconfiguration protocol.

1

Introduction

Payment systems built on Byzantine consistent broadcast [4, 2, 7] achieve sub-second settlement and horizontal scalability because validators never agree on a global order. In FastPay [2], a client sends its signed transfer to all validators, collects 2f + 1 signatures into a certificate, and broadcasts the certificate. Validators do not communicate with each other, so each payment costs O(n) messages. The design rests on two facts. First, each account has a single writer, and the account nonce orders that writer’s transfers. Asset transfer with single-owner accounts has consensus number one [10]. Second, an honest validator signs at most one transfer per nonce and never revokes that signature. Together these make a certificate final the moment it exists, even if only the client holds it, because no conflicting certificate can ever be formed. If the owner equivocates, the account stays locked, and only the owner is harmed. Delegating signature collection to the client is therefore safe, and it is what makes the system fast.

1

When client-driven certification breaks. Stablecoin workloads need balances debited by several accounts: a corporate treasury with several payers, a merchant pool debited by refunds and payouts, delegated allowances and subscriptions, and custodial wallets operated by many signing workers. Guerraoui et al. [10] show that an account shared by k owners has consensus number k. Concretely, two honest accounts can debit the same balance at the same time and split the validators’ votes, so that neither reaches a quorum and the balance is stuck. This is not a penalty anyone deserves. The lock must be undone. Undoing a lock is exactly what the client-driven design cannot support. Before releasing a stuck balance, validators must know that no transaction on it has already been certified. In a client-driven design a certificate may exist only in a client’s hands. A Byzantine validator can sign one transaction privately and another publicly, so the validators’ joint view can show a split while a certificate exists. We prove (Proposition 2) that no unlock rule over validators’ reports is safe in this setting. This holds even if validators broadcast their votes to each other. The protocol, not the client, has to record that a certificate was formed. Our design. undone.

We keep the fast path where it is safe and add visibility only where locks may be

• Personal path. A transaction that debits the sender’s own account runs the FastPay protocol unchanged: client-driven, O(n) messages, no unlock. • Shared path. A shared resource has a balance, its own version number (the resource nonce) and a set of authorized accounts. A transaction debiting it can be submitted to any validator. A validator admits it only if the sender’s nonce and the resource nonce are both free, and then broadcasts an Echo. A validator that has seen 2f + 1 echoes for a transaction stores them and broadcasts Ready, and 2f + 1 readies make the transaction final. This is Bracha’s two-phase broadcast [3] applied per resource version, with no consensus. • Fast unlock. If a resource version is not resolved in time, validators freeze it, report what they echoed and stored, and run one validated agreement instance [5, 1] for that version. The selection rule admits only a transaction whose echo quorum someone stored, which includes every final transaction. Losing transactions are dead, and their sender nonces are released for reuse. Contributions. 1. A characterization of when client-driven certification is complete (single writer, no unlock), and a proof that no unlock rule is safe without visible certification (§4). 2. A hybrid protocol with dual-nonce admission: personal transactions on the FastPay path, shared transactions on an Echo/Ready path (§5). 3. Fast unlock: in-protocol detection, freeze and per-version agreement, with nonce release for losing transactions (§6). 4. Proofs of consistency, no overdraft, validity, finality and liveness (§7). 5. Integration with PDCC reconfiguration [14] (§9). 6. An open-source TLA+ model, exhaustively checked with TLC, which also reproduces the counterexample of the impossibility result (§10).

2

Background

Certificate-based payments. FastPay [2] and its successors settle each payment by Byzantine consistent broadcast on a per-account basis; credits commute and need no ordering. PDCC [14] 2

describes the resulting architecture as per-account certificate payments combined with a periodic settlement consensus that commits checkpoints and reconfigurations. Stuck accounts. An equivocating sender can split votes on its own nonce. FastPay leaves the account stuck. Sui [15] keeps such owned objects locked until the end of the epoch. Reliable broadcast. Bracha’s broadcast [3] includes an additional Ready all-to-all phase after the echo phase to ensure that if an honest party delivers the message, then a quorum has seen a quorum of echo messages. Astro [7] applies Byzantine reliable broadcast to build payment systems. Validated agreement. In validated Byzantine agreement [5] all honest validators decide on a common value satisfying a predicate Valid; PBFT-style protocols [6, 16] implement this in the partial synchrony model with a transferable decision proof and randomized protocols [1] in the asynchronous model.

3

Model

Validators, faults, network. In a configuration, a committee of n = 3f + 1 validators runs the protocol; at most f are Byzantine. A quorum is any 2f + 1 validators; two quorums share at least one honest validator, and a quorum contains at least f + 1 honest validators. Accounts and clients may be Byzantine and collude with Byzantine validators. Signatures are unforgeable. Safety holds under asynchrony. Liveness assumes partial synchrony [9]: after an unknown GST, messages between honest parties arrive within ∆. Configurations change through PDCC (§9). Accounts and shared resources. An account a has a personal balance and a nonce. A shared resource ρ has a balance, a version (the resource nonce) and an authorization set Auth(ρ) of accounts allowed to debit it, with |Auth(ρ)| ≥ 2 in practice. Slots. A nonce slot consists of a pair (a, i) and a resource slot consists of a pair (ρ, v). A transaction consumes one sender nonce slot and, if it debits a shared resource, also one resource slot. Transactions. A transaction T is signed by its sender a and carries a nonce i, so ns(T ) = (a, i). It is of one of two kinds. • A personal transaction debits a’s personal balance. • A shared transaction debits a shared resource ρ at version v, requires a ∈ Auth(ρ), and has rs(T ) = (ρ, v). Both kinds may credit any accounts or resources. Credits are not versioned. Execution order. A validator executes the transactions of account a in nonce order and the transactions of resource ρ in version order. A nonce slot is consumed when a transaction on it is executed. A resource slot is resolved when a transaction on it is executed or the slot is released; resolving (ρ, v) opens (ρ, v + 1).

3

Properties. Consistency. No two executed transactions share a slot. All honest validators resolve every resource slot the same way. No overdraft. No balance in an honest validator’s state becomes negative. Validity. An executed transaction is signed by its sender, the sender is authorized for the resource it debits, and an honest validator found the debit covered. Finality. A final transaction is eventually executed by every honest validator, and no transaction conflicting with it is ever executed. Liveness. After GST: a personal transaction from an honest account is eventually final; every resource slot on which an honest validator saw an echo is eventually resolved; and an honest account whose shared transaction loses can reuse its nonce.

4

When Client-Driven Certification Is Complete

In client-driven certification, a transaction is final when a quorum of validators has signed it. Validators send their signatures to whoever collects them and need not see each other’s. Lemma 1. If honest validators sign at most one transaction per slot and never release a slot, then client-driven certification is safe even if certificates are known only to clients. Proof. Two certificates for conflicting transactions would come from two quorums, which share an honest validator that signed both on the same slot. Note that this guarantee depends on never releasing a slot. If a slot is at some point released and re-signed, it becomes possible to contradict a certificate created but never shown to validators. Proposition 2. Let n = 3f + 1, f ≥ 1, and let a transaction be final once a quorum has signed it, even if signatures are additionally broadcast among validators. Then no function Select that maps the reports of a quorum of validators on a slot (each stating which transaction the reporter signed) to a transaction or ⊥ can ever release or reassign the slot without contradicting some final transaction. Proof. Let f = 1 with honest h1 , h2 , h3 and Byzantine b, and conflicting A, B on one slot. In execution X, h1 , h2 sign A and h3 signs B. b broadcasts a signature for B and privately gives the client of A a signature for A, so {h1 , h2 , b} certifies A. In execution Y , h1 signs A, h2 , h3 sign B, and b signs B, so {h2 , h3 , b} certifies B. The quorum {h1 , h3 , b} reports A, B, B in both executions, and every broadcast it received is the same in both. Select must output A in X and B in Y , a contradiction. For general f , let h1 , h3 and b each stand for a group of f validators and h2 for one validator. Personal transactions are never released, so Lemma 1 covers them. Shared transactions must sometimes be released, so Proposition 2 applies to them and they need visible certification.

5

Protocol

Validator state. For each nonce slot σ, validator p stores lockp [σ], the transaction that currently holds the slot at p, or ⊥. For each resource slot s it stores echoedp [s], pcp [s] (a stored echo quorum or ⊥), frozenp [s], and the resolution. It also stores the set deadp of transactions known to have lost (§6). 4

Admission.

Validator p admits transaction T if all of the following hold:

1. T is signed by its sender a, and a ∈ Auth(ρ) if T debits ρ; 2. T ∈ / deadp ; 3. user nonce: nonce i − 1 of a is consumed at p, and lockp [(a, i)] ∈ {⊥, T }; 4. resource nonce (shared only): (ρ, v − 1) is resolved at p, and both echoedp [(ρ, v)] = ⊥ and ¬frozenp [(ρ, v)] hold; 5. the debited balance in p’s view covers the amount and fees. On admission, p sets lockp [(a, i)] ← T and, for a shared transaction, echoedp [(ρ, v)] ← T , in one atomic step.

5.1

Personal path

The personal path is FastPay. The client sends T to all validators; each validator that admits T returns ⟨Vote, T ⟩; a quorum of votes is a certificate Cert(T ), which is final; validators execute T on receiving Cert(T ). Nonce locks taken by personal transactions are never released.

5.2

Shared path

1. Submit. The client sends T to any validator. If it does not see T become final within a timeout, it sends T to another validator. 2. Echo. A validator that receives T (from a client or inside an Echo) and admits it broadcasts ⟨Echo, T ⟩p to all validators, including T . 3. Ready. A validator p that holds Echos for T from a quorum, with ¬frozenp [rs(T )], stores the quorum as pcp [rs(T )] ← PC(T ) and broadcasts ⟨Ready, T ⟩p . 4. Final. Readys for T from a quorum form RC(T ), and T is final. Validators also send Readys to the client and recipients, who can verify RC(T ). A validator executes T on holding RC(T ). A transaction on the shared path is therefore final after three message delays: submit, echo, ready. It involves no leader and no consensus. Definition 1 (Final). A personal transaction is final when Cert(T ) exists. A shared transaction is final when RC(T ) exists.

6

Fast Unlock

Triggers. Unlocking is triggered inside the protocol. Validator p freezes resource slot s when any of the following holds and s is unresolved: 1. Timeout: τ has elapsed since p first saw an Echo on s. A validator forwards the first Echo it sees on each slot, so every honest validator starts the timer. 2. Split: p holds Echos on s from a quorum of distinct validators and no transaction among them has a quorum; it may wait a short grace period first. 3. Amplification: p received Freeze reports on s from f + 1 validators. Triggers affect only liveness and latency. A Byzantine validator cannot freeze a slot at an honest validator alone, because amplification needs f + 1 reports.

5

Algorithm 1 Shared path and fast unlock at validator p 1: upon receiving T or ⟨Echo, T ⟩ with T admissible do 2: take locks on ns(T ) and rs(T ); broadcast ⟨Echo, T ⟩p 3: end upon 4: upon Echos for T from a quorum and ¬frozenp [rs(T )] do 5: pcp [rs(T )] ← PC(T ); broadcast ⟨Ready, T ⟩p 6: end upon 7: upon Readys for T from a quorum do 8: execute T 9: end upon 10: upon a trigger for unresolved s do 11: frozenp [s] ← true; broadcast ⟨Freeze, s, echoedp [s], pcp [s]⟩p 12: end upon 13: upon a freeze set Fp for s do 14: propose (Fp , Select(Fp )) to VBAs 15: end upon 16: upon VBAs decides (F ∗ , d∗ ) with proof π do 17: forward π; execute d∗ or release s; mark the others dead and free their nonce locks 18: end upon

Freeze.

To freeze s, p sets frozenp [s] ← true and broadcasts ⟨Freeze, s, echoedp [s], pcp [s]⟩p .

Afterwards p neither echoes on s nor sends Ready for any transaction on s. Freezing is irrevocable. Selection. A freeze set F for s consists of well-formed Freeze reports on s from a quorum of distinct validators. ( T if some report in F contains a valid PC(T ), Select(F ) = ⊥ otherwise. Agreement. Validator p proposes (Fp , Select(Fp )) to the agreement instance VBAs with predicate Valid(F, d) ⇐⇒ F is a freeze set for s and d = Select(F ). Any validated agreement with a transferable decision proof π works. In a PDCC system, a dedicated instance of its leaderless PBFT-style settlement protocol serves, since any validator may propose. Pending unlocks can also be batched into the next settlement round, at the cost of waiting for it. Resolution.

On deciding (F ∗ , d∗ ) with proof π, validators forward π and proceed as follows.

• If d∗ = T , they execute T . It consumes T ’s nonce slot and resolves s. • If d∗ = ⊥, they release s: the balance is unchanged and (ρ, v + 1) opens. • Every transaction T ′ ̸= d∗ on s is dead. Each validator adds it to dead and, if lock[ns(T ′ )] = T ′ , resets the nonce lock to ⊥. The sender can reuse nonce i for a new transaction.

6

7

Correctness

We say a transaction has a quorum if a quorum of validators admitted it, that is, if Cert(T ) or PC(T ) exists. Lemma 3 (One echo per resource slot). An honest validator echoes at most one transaction on each resource slot, and none after freezing it. Proof. echoedp [s] is set on admission and never reset, and admission requires ¬frozenp [s], which is irrevocable. Lemma 4 (Unique echo quorum). At most one transaction per resource slot has an echo quorum. Proof. Two echo quorums share an honest validator, which contradicts Lemma 3. Lemma 5 (Visibility). If a shared T on s is final, then Select(F ) = T for every freeze set F for s. Proof. RC(T ) and F come from two quorums, which share an honest validator q. q sends Ready only while s is unfrozen and only after storing PC(T ). Since freezing is irrevocable, its report in F contains PC(T ), and Select(F ) = T by Lemma 4. Lemma 6 (No late finality). If a freeze set F for s exists and Select(F ) ̸= T , then T is never final. Proof. Suppose RC(T ) exists, formed at any time. Its quorum shares an honest validator q with F . Since q is in F , it froze s. Since it sent Ready for T , it did so before freezing, so it had stored PC(T ) and reported it in F . Then Select(F ) = T by Lemma 4. Lemma 7 (Dead transactions). A dead transaction is never final and never executed. Proof. T ′ is dead only if VBAs decided (F ∗ , d∗ ) with d∗ ̸= T ′ , where d∗ = Select(F ∗ ). By Lemma 6, T ′ is never final. The only other way to execute a shared transaction is to be the decision, and the decision is unique by agreement of VBAs . Lemma 8 (Nonce slots). If T ̸= T ′ share a nonce slot and both have a quorum, at least one of them is dead. Proof. The two quorums share an honest validator q, which admitted both. Admission sets lockq [σ] and requires it to be ⊥ or the same transaction. So q admitted one of them, say X, then reset the lock before admitting the other. A lock is reset only when the transaction holding it becomes dead, so X is dead. Theorem 9 (Resource slot agreement). All honest validators resolve each resource slot s the same way. Proof. A validator resolves s by executing a final T or by applying VBAs ’s decision. Two final transactions on s would have two echo quorums, contradicting Lemma 4. The decision is unique, and it equals Select(F ∗ ). If T is final, the decision is T by Lemma 5. If the decision is d∗ , no T ̸= d∗ becomes final later by Lemma 6. Theorem 10 (Consistency). No two executed transactions share a slot.

7

Proof. For resource slots this follows from Theorem 9. For a nonce slot, every executed transaction has a quorum: a personal one through Cert(T ), a final shared one because RC(T ) implies a stored PC(T ), and a decided shared one because Select returns a transaction only if a report contains its PC(T ). If two executed transactions shared a nonce slot, one of them would be dead by Lemma 8, and dead transactions are not executed by Lemma 7. Theorem 11 (Validity and no overdraft). Every executed transaction was signed by its sender, the sender was authorized for the debited resource, and the debit is executed only when the executing validator’s balance covers it. Proof. Every executed transaction has a quorum, so at least f + 1 honest validators admitted it, checking the signature, the authorization and the balance in their view. Debits of a balance are ordered (nonce order for personal balances, version order for resources), and honest validators agree on them by Theorems 9 and 10. Credits only grow, and every credit an honest admitter counted was executed by it and is eventually executed by everyone (Lemma 12). A validator executes a debit only when its own view covers it, buffering it until then. Lemma 12 (Propagation). If an honest validator executes T or releases a slot, every honest validator eventually does the same. Proof. Each such step is backed by self-verifying evidence (Cert(T ), RC(T ) or a decision proof π), which honest validators forward. The evidence for a slot is applied after the previous nonce and version. The validator that applied it had applied the previous ones, so induction on nonce and version concludes. Theorem 13 (Finality). A final transaction is eventually executed by every honest validator, and no transaction that shares a slot with it is ever executed. Proof. By Lemma 12 and Theorem 10. Theorem 14 (Liveness). Assume partial synchrony and that VBA terminates after GST. 1. A personal transaction from an honest account becomes final. 2. A resource slot on which an honest validator saw an Echo is eventually resolved. 3. If an honest account’s shared transaction T is dead, every honest validator eventually releases the nonce lock that T holds there. Proof. (1) An honest account never signs two transactions with one nonce, so after GST every honest validator admits T once its previous nonce is consumed and the balance it relies on has arrived (Lemma 12). The 2f + 1 honest votes form Cert(T ). (2) The first honest validator to see an Echo on s forwards it, so all honest validators start the timer. If s is not resolved within τ after GST, every honest validator freezes, each receives at least 2f + 1 Freeze reports, and each proposes a valid value. Termination of VBAs resolves s. (3) The decision proof π reaches every honest validator, each of which marks T dead and resets lock[ns(T )] if it holds T . Remark 1 (Accounts that equivocate). An account that signs two personal transactions with the same nonce may lock its own nonce forever, as in FastPay. If it signs a personal and a shared transaction with the same nonce, the shared one may die and release its locks, while the personal one keeps its own. Lemma 8 still prevents both from executing. In neither case is another account’s resource affected beyond one released version. 8

8

Cost Path

Messages per transaction

Delays to finality

Consensus

Personal (FastPay) Shared, no contention Shared, contended slot

O(n) O(n2 /B) with batches of B as above + one VBA

2 (certificate at client) 3 τ + 1 + VBA

never never that slot only

Table 1: Cost of each path. The quadratic message pattern of the shared path is the price of visible certification (Proposition 2), and only shared resources pay it. Two standard techniques make it small in bytes. Digests and batching. The validator that first receives a transaction broadcasts its body once. Echo and Ready messages carry only digests and cover a batch of B transactions. A validator that receives an Echo for an unknown digest fetches the body from the echoing validator. Admission, freezing and selection are per slot. If a batch contains a transaction that a validator does not admit, the validator echoes the batch with that position marked as rejected, so the remaining transactions are unaffected. A simple byte model. Let |tx| be the size of the transaction, h the size of the Echo or Ready header with its signature, and σ the size of a signature. Then the approximate number of bytes sent per transaction by all of the validators is personal: n |tx| + n σ + n |Cert|,

shared: n |tx| +

2 n2 h . B

With aggregated signatures, certificates have constant size plus an n-bit signer bitmap. For illustration, with n = 100, |tx| = 250 B, h = 100 B and B = 1000, the shared-path overhead is 2n2 h/B = 2 kB per transaction against 25 kB for disseminating the body, about 8%. These figures are an analytical model, not measurements; measuring them on a prototype is future work. Computation. Per batch, each validator verifies O(n) echo and ready signatures, so the pertransaction verification cost is O(n/B), plus one aggregate verification per received certificate.

9

Reconfiguration with PDCC

PDCC [14] tags certificates with the configuration c in which they are formed. A validator accepts only certificates of its installed configuration (PDCC Invariant I), and it installs c + 1 when the settlement consensus commits a checkpoint payload containing a certified reconfiguration proposal. Applied naively, this rule can lose a final transaction: a personal certificate or a ready certificate formed in c may still be in transit, or held only by a client, when c + 1 is installed, and c + 1 then rejects it. We close this gap with a two-step transition. The first step seals c, and the second installs c + 1 from a quorum of closing reports. All objects below are tagged with c, and quorums are counted in Mc .

9

Seal. When the settlement consensus commits a checkpoint containing a valid reconfiguration proposal for c → c + 1, every honest validator of Mc seals c. It stops admitting transactions, sending Ready and acknowledging anything in c, and freezes every unresolved resource slot. Since all honest validators deliver the same committed checkpoint, they all seal. Closing report.

After sealing, validator p sends a signed closing report CRp containing

• every transaction p executed since the last committed checkpoint, with the certificate or decision proof that justified it; • for every nonce slot, the non-dead transaction holding lockp , if any, together with p’s signature on it; • for every unresolved resource slot s, its Freeze content (echoedp [s], pcp [s]). Install. The next settlement proposal that installs c + 1 must contain closing reports C from a quorum of Mc ; this is part of its validity predicate. The new state is computed deterministically from the last checkpoint and C. 1. Every transaction listed as executed in some report of C, with valid evidence, is executed. 2. For every unresolved resource slot s, the reports of C form a freeze set Fs . The slot is resolved as Select(Fs ): that transaction is executed, or the slot is released. Transactions on s other than Select(Fs ) are dead. 3. Every nonce slot σ for which some report lists a lock becomes inherited with the set Lσ of non-dead transactions reported on it. One committed proposal resolves every frozen slot simultaneously. The settlement consensus acts as the validated agreement for all of them, and no per-slot instance is needed at reconfiguration. Inherited nonce slots in c + 1. For an inherited slot σ, validators of Mc+1 accept a personal certificate Certc (T ) from configuration c, verified against Mc in the configuration history, if and only if T ∈ Lσ . If |Lσ | = 1, they also admit the single transaction in Lσ in c + 1, and no other transaction on σ. If |Lσ | ≥ 2, the sender equivocated, and the slot accepts only an old certificate for a member of Lσ , exactly as an equivocated slot in FastPay. This relaxes PDCC Invariant I for inherited slots only. Every other certificate from c is still rejected. Lemma 15 (No final transaction is lost). If T is final in c, then after installing c + 1 either T is executed or T is a personal transaction, ns(T ) is inherited and T ∈ Lns(T ) , so that Certc (T ) is accepted in c + 1. Proof. A final T was admitted by a quorum, hence by at least f + 1 honest validators. Every quorum contains at least one of them, so C contains a report CRq from an honest q that admitted T . All admissions in c precede sealing, so q’s report reflects T : either q executed T and lists it as executed, or q still holds the lock. If T is shared and unexecuted at q, then s = rs(T ) is unresolved at q, and Fs is a freeze set. By Lemma 5, Select(Fs ) = T , so T is executed at installation. If T is personal and unexecuted at q, q’s lock on ns(T ) is T , because personal locks are never reset, so T ∈ Lns(T ) . Lemma 16 (No conflict across configurations). No two executed transactions share a slot, across configurations.

10

Proof. Within c this is Theorem 10. At installation, executed transactions carry evidence that they are final or decided, and resource slots are resolved by Select on a freeze set. Lemmas 5 and 6 apply verbatim, because sealing is a freeze of every unresolved slot. After installation, a nonce slot that is not inherited had no lock at any reporter in C. By the argument of Lemma 15, no transaction on it has a quorum in c. For an inherited slot, two transactions T ̸= T ′ executed on it would both belong to Lσ , or one would be admitted fresh in c + 1 while |Lσ | = 1. Two members of Lσ with a certificate in c would contradict Lemma 8, since neither is dead. A fresh admission in c + 1 is restricted to the unique member of Lσ , which is the only one that can hold a certificate from c. Liveness and cost. Under PDCC’s overlap assumption, at least Qc honest members of Mc remain to send closing reports, so the installing proposal can be formed. Between sealing and installation, configuration c admits no new transactions, so payments pause for one settlement round at each reconfiguration. Shortening this pause, for instance by sealing per account range, is left to future work.

10

Mechanized Verification

We model the protocol in TLA+ [12] and check it exhaustively with the TLC model checker. The specification, configurations and run script are open source at https://github.com/sglk123/ resource-lock-tla. Model. There are n = 4 validators in this model, with three honest and one Byzantine (f = 1). The Byzantine validator signs all messages (public and private) on all transactions and thus is included in all quorums. In a freeze set it may report any existing echo quorum. The workload consists of four transactions that cover all §3 conflict patterns: • A and B, shared transactions from different accounts racing on the same resource version; • P , a personal transaction with the same sender nonce as A, so that the account equivocates across the two paths; • C, a shared transaction on another resource with the same sender nonce as A, which reuses the nonce after A loses. Unlock triggers are abstracted away: any honest validator may freeze any slot at any time. This over-approximates the triggers of §6, which only restrict when a freeze happens. Validated agreement is abstracted as a single atomic decision Select(F ) over some freeze set F , which captures its agreement and external-validity properties. Properties. We check the conjunction of: Consistency (no two executed transactions share a slot); finality safety (no executed transaction conflicts with a final one); unlock respects finality (the decision on a slot is never a transaction other than a final one); dead transactions are never final ; and at most one echo quorum per resource slot. Results. The full protocol satisfies all properties over the complete reachable state space; TLC generated 346 million states, of which 41.3 million are distinct, and terminated in about six minutes on a laptop. In the variant in which a shared transaction is final once an echo quorum exists, TLC finds a counterexample of depth six that matches Proposition 2. Two honest validators echo A, which together with the Byzantine validator’s private signature is an echo quorum, so A is final. One of the two freezes before storing that quorum, and the unlock decides ⊥, contradicting A. 11

Variant Protocol (Echo + Ready) Finality at bare echo quorum

Distinct states

Depth

41,333,964 —

30 6

Result no violation (exhaustive) violation found

Table 2: TLC results (n = 4, f = 1, four transactions). Scope. Model checking covers this instance exhaustively, not all n and workloads; the general case is established by the proofs of §7. Reconfiguration (§9) and liveness are not part of the current model and are covered by the proofs only.

11

Related Work

FastPay [2] introduced client-driven certificate payments; Astro [7] payments over Byzantine reliable broadcast. Guerraoui et al. [10] give the consensus number of asset transfer. Sui [15] separates owned objects (consistent broadcast) from shared objects (consensus) and locks equivocated owned objects until the end of the epoch. Bracha [3] introduced the echo/ready structure we use per resource version. Fast Byzantine consensus [13, 11] studies the committee size needed for deciding from a single round of votes, of which Proposition 2 is a payment-specific instance. PDCC [14] and dynamic BFT [8] handle reconfiguration.

12

Conclusion

Client-driven certification is complete exactly when locks are never undone. Shared balances require undoing locks, and therefore require the protocol itself to record certification. Our hybrid keeps personal payments on the FastPay path. It certifies shared-resource payments by a leaderless echo/ready broadcast with dual-nonce admission, and resolves contention with agreement on the single contended version. Agreement is paid for only where writers actually contend.

References [1] Ittai Abraham, Dahlia Malkhi, and Alexander Spiegelman. Asymptotically optimal validated asynchronous Byzantine agreement. In Proceedings of the 2019 ACM Symposium on Principles of Distributed Computing (PODC), 2019. [2] Mathieu Baudet, George Danezis, and Alberto Sonnino. FastPay: High-performance Byzantine fault tolerant settlement. In Proceedings of the 2nd ACM Conference on Advances in Financial Technologies (AFT), 2020. [3] Gabriel Bracha. Asynchronous Byzantine agreement protocols. Information and Computation, 75(2):130–143, 1987. [4] Christian Cachin, Rachid Guerraoui, and Luı́s Rodrigues. Introduction to Reliable and Secure Distributed Programming. Springer, 2nd edition, 2011. [5] Christian Cachin, Klaus Kursawe, Frank Petzold, and Victor Shoup. Secure and efficient asynchronous broadcast protocols. In Advances in Cryptology – CRYPTO 2001, 2001.

12

[6] Miguel Castro and Barbara Liskov. Practical Byzantine fault tolerance. In 3rd Symposium on Operating Systems Design and Implementation (OSDI), 1999. [7] Daniel Collins, Rachid Guerraoui, Jovan Komatovic, Petr Kuznetsov, Matteo Monti, Matej Pavlovic, Yvonne-Anne Pignolet, Dragos-Adrian Seredinschi, Andrei Tonkikh, and Athanasios Xygkis. Online payments by merely broadcasting messages. In 50th IEEE/IFIP International Conference on Dependable Systems and Networks (DSN), 2020. [8] Sisi Duan and Haibin Zhang. Foundations of dynamic BFT. In IEEE Symposium on Security and Privacy (S&P), 2022. [9] Cynthia Dwork, Nancy Lynch, and Larry Stockmeyer. Consensus in the presence of partial synchrony. Journal of the ACM, 35(2), 1988. [10] Rachid Guerraoui, Petr Kuznetsov, Matteo Monti, Matej Pavlovic, and Dragos-Adrian Seredinschi. The consensus number of a cryptocurrency. In Proceedings of the 2019 ACM Symposium on Principles of Distributed Computing (PODC), 2019. [11] Petr Kuznetsov, Andrei Tonkikh, and Yan X. Zhang. Revisiting optimal resilience of fast Byzantine consensus. In Proceedings of the 2021 ACM Symposium on Principles of Distributed Computing (PODC), 2021. [12] Leslie Lamport. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, 2002. [13] Jean-Philippe Martin and Lorenzo Alvisi. Fast Byzantine consensus. IEEE Transactions on Dependable and Secure Computing, 3(3), 2006. [14] Lingkang Shangguan. Transaction-driven dynamic reconfiguration for certificate-based payment systems. arXiv:2601.09146, 2026. [15] The Sui Team. The Sui smart contracts platform. Whitepaper, Mysten Labs, 2022. [16] Maofan Yin, Dahlia Malkhi, Michael K. Reiter, Guy Golan Gueta, and Ittai Abraham. HotStuff: BFT consensus with linearity and responsiveness. In Proceedings of the 2019 ACM Symposium on Principles of Distributed Computing (PODC), 2019.

13

Related documents

• CVE-2026-86405 — CRITICAL 9.8#1267409
• Inner layer security reinforcement for instant payment systems: a dual layer encryption-steganography evaluation in Brunei's digital payment context.#334830
• Identity Based Authenticated Key Agreement Protocol — Sundaram Ganapathy S (US20100211779A1)#607379
• Model Sinergitas Antar Lembaga Dalam Pengelolaan Zakat Bagi Mustahiq Pedagang Kaki Lima (PKL)#1020917
• TLS 1.3 Authentication and Integrity-Only Cipher Suites#213528