PaperlayerView exact revision on arXiv

Source-linked AI summary

Making Duplicate Reimbursement Unrepresentable: A Verified Ethereum E-Invoice System for Humans and AI Agents

Jia Cai

arXiv:2609.37819v1cs.CRcs.AIcs.CE

TL;DR

Centralized e-invoice systems leave duplicate reimbursement, difficult authenticity verification, and siloed invoice data unresolved on the consumption side. The paper formalizes and implements a verified Ethereum invoice system with a lock-based reimbursement protocol. It proves reimbursement uniqueness and face integrity under stated assumptions, and reports a lifecycle-complete implementation with bounded operating costs and a deployment boundary shaped by storage growth.

  • Problem

    Centralized e-invoice systems leave consumption-side duplicate reimbursement and siloed invoice state unresolved.

    Source: §I · p. 1

  • Method

    The paper models invoices as non-tradable tokens in a guarded lifecycle and uses a lock-based reimbursement protocol in a verified Ethereum contract.

    Source: §I · p. 2, G. Subsystem 5: Declaration and… · pp. 5–6

  • Results

    The paper proves reimbursement occurs at most once and verified invoice faces match recorded faces under the stated hash assumption, with core state invariants machine-checked.

    Source: §I · p. 2, §VII · pp. 6–7

  • Takeaways & Limitations

    The contract makes duplicate reimbursement unrepresentable and serves as a safety envelope that rejects unsafe agent actions even when the agent policy fails.

    Source: G. Subsystem 5: Declaration and… · p. 6, §X · p. 8

    Storage growth of roughly 1–2 KB per invoice face favors the commitment-on-chain variant at national volumes.

    Source: §XI · p. 10

Abstract

from arXiv · show

Electronic invoices are replacing paper invoices worldwide, but today's centralized architectures leave three problems unsolved on the consumption side: an invoice can be submitted for reimbursement repeatedly, authenticity is difficult for recipients to verify, and data is siloed at a central authority that forms both a performance bottleneck and a single point of failure. This paper presents the design, formal analysis, and implementation of a complete blockchain-based electronic invoice system on Ethereum. We formalize the invoice lifecycle as a guarded labeled transition system and prove, under standard cryptographic and consensus assumptions, that the system guarantees: (i) reimbursement uniqueness--an invoice is reimbursed at most once, even across mutually distrusting organizations; (ii) face integrity--any verified invoice matches the recorded one unless keccak256 second-preimage resistance is broken; and (iii) authorization soundness for every lifecycle operation. The core invariants are machine-checked using Solidity SMTChecker, proving inductive validity across all reachable transaction sequences. The architecture models each invoice as a non-fungible, non-tradable token whose state transitions through five guarded subsystems, employing a lock-based protocol that makes duplicate reimbursement unrepresentable rather than merely detectable. We implement the design as a Solidity 0.8 contract with a four-role web application and evaluate it on a private Ethereum network: issuing costs 646,773 gas, full reimbursement costs under 135,000 gas, all operations run in O(1) time, and a single node sustains 137 issuances/s. Finally, the verified contract serves as a safety envelope for LLM-based reimbursement agents, provably rejecting unsafe actions (duplicate, over-limit, or forged-receipt claims) even when the agent's internal policy fails. All code and benchmarks are open-source.

I. INTRODUCTION

Centralized e-invoice systems leave duplicate reimbursement, costly authenticity checks, and siloed invoice state unresolved on the consumption side. This paper proposes a lifecycle-complete blockchain design, contrasting it with prior work that often covers issuance or VAT settlement rather than consumption-side controls.

I. INTRODUCTION

  • Duplicate claims can cross employers or channels, while manually maintained registers are error-prone, unauditable, and ineffective across organizations.Recipients also face costly authenticity checks and centralized data bottlenecks.Source: §I · p. 1
  • A unique on-chain invoice with one-way reimbursement rules makes duplicate reimbursement unrepresentable rather than merely detectable.The paper encodes lifecycle rules in an Ethereum smart contract that participants cannot bypass.Source: §I · p. 2
  • The paper contributes a lifecycle-complete design, formal security analysis, machine-checked invariants, an open-source implementation, evaluation, and an agent case study.The design spans blank-invoice distribution through red-flush correction and lock-based reimbursement.Source: §I · p. 2

II. RELATED WORK

  • Prior blockchain e-invoice systems address issuance, validation, or VAT settlement, but do not model ownable invoice tokens or prevent duplicate reimbursement.Tradable invoice tokens for financing pursue a different design goal from non-tradable legal tax documents.Source: §II · p. 2
  • The proposed system positions itself as an open-source, auditable, lifecycle-complete design with proved security properties and reproducible cost measurements.The paper contrasts this with conceptual or single-scenario academic work and proprietary industrial designs.Source: §II · p. 2

III. PRELIMINARIES AND THREAT MODEL

The paper relies on Ethereum’s replicated contract state and explicit cryptographic and consensus assumptions. Its threat model treats registered account holders, including autonomous agents, as adversaries while excluding specified off-chain concerns.

A. Blockchain and Smart Contracts

  • Ethereum orders signed transactions through consensus, records state changes immutably, meters execution in gas, and exposes events for reconstructing asset history.Permanent, globally replicated storage means corrections must be recorded as transactions, while contract invariants prevent unauthorized state changes through unavailable functions.Source: A. Blockchain and Smart Contracts · pp. 2–3

B. Cryptographic Primitives

  • Security assumes keccak256 second-preimage and collision resistance, unforgeable ECDSA signatures, and consensus safety under the stated proof-of-work or PBFT fault thresholds.These assumptions yield a single, totally ordered, globally agreed state.Source: B. Cryptographic Primitives · p. 3

C. Threat Model

  • The adversary controls arbitrary registered enterprise keys and may submit transactions adaptively, but cannot forge honest signatures, break the hash assumptions, or violate consensus safety.Fictitious sales, key theft, and storage confidentiality are outside the guarantees’ scope.Source: C. Threat Model · p. 3

IV. FORMAL MODEL

The formal model represents the contract as a deterministic guarded transition system over global state. Its invoice automaton and operation guards specify which lifecycle changes are allowed and when transactions revert.

IV. FORMAL MODEL

  • The model treats the contract as a deterministic transition system over a global state.Executions are finite sequences of operations from the genesis state.Source: §IV · pp. 3–4
  • Global state is a tuple of registration, ownership, status, credit-note, declaration, invoice-face, digest, and lock mappings, initialized empty at genesis.An undefined owner corresponds to status NONE.Source: §IV · p. 3
  • The lifecycle automaton has states NONE, BLANK, ISSUED, LOCKED, REIMBURSED, and REVERSED, with contract operations as transition labels.REIMBURSED and REVERSED are terminal states.Source: §IV · pp. 3–4
  • Fig. 1 depicts the invoice lifecycle automaton, marking terminal states with double borders and showing a frozen credit note in gold.Tax declaration is an orthogonal one-way flag omitted from the diagram.Source: Figure 1 · p. 4
  • Each operation is a guarded command whose sender and arguments are checked against global state before effects are applied.A failed guard reverts the transaction without changing state; the rules match the contract’s require clauses and state writes.Source: §IV · p. 4

A. Actors and Functional Requirements

Four roles participate in an invoice lifecycle covered by five functional subsystems. The architecture places authoritative lifecycle rules in a smart contract and leaves dashboards as stateless clients.

A. Actors and Functional Requirements

  • The lifecycle assigns distinct responsibilities to the bureau, seller, buyer, and third-party verifiers.The bureau admits enterprises and creates blanks; sellers issue and correct invoices, buyers verify and reimburse, and third parties verify without trusting either party.Source: A. Actors and Functional Requirements · p. 4
  • Five subsystems cover blank distribution, issuance, voiding and red-flush correction, query and verification, and tax declaration and reimbursement.The requirements include permissioned participation, auditability, adequate throughput, and no trusted intermediary on the consumption side.Source: A. Actors and Functional Requirements · p. 4

C. Architecture

  • The smart contract is the sole trust boundary, while role dashboards submit signed transactions and reconstruct history as stateless clients.No application server holds authoritative state.Source: Figure 2 · p. 4, C. Architecture · p. 4

B. Is a Blockchain Warranted?

  • Electronic invoicing fits the blockchain applicability test through shared state, multiple writers, mutual distrust, and absence of a perfect trusted third party.A consortium is the natural fit for identified enterprises under a regulator, with public-chain design retained as a more adversarial baseline.Source: B. Is a Blockchain Warranted? · p. 4

VI. SMART CONTRACT DESIGN

The design treats invoices as non-tradable tokens and uses guarded lifecycle operations to preserve their identity and record issuance and correction. Bureau-approved blank distribution, atomic issuance, and linked red-flush transactions cover the lifecycle through correction.

A. Invoices as Non-Tradable, Non-Fungible Tokens

  • Invoices are unique, indivisible ERC-721-style tokens with no public transfer function; ownership changes only through lifecycle operations.This prevents invoice resale and gray-market circulation at the type-system level.Source: A. Invoices as Non-Tradable,… · p. 4
  • Transition rules require all guards to hold; a failed guard reverts without effect.The rules are specified per invoice and mirror the contract's guards and state writes.Source: Table III · p. 5

B. Data Model

  • Each invoice stores party snapshots, amounts, category and item details, status, credit and red-flush links, issuance time, and a face digest.Registry-controlled enterprise registration and on-chain tax calculation constrain the recorded face; monetary values use unsigned cents and credit invoices use a separate flag.Source: B. Data Model · p. 5

C. Subsystem 1: Application and Distribution

  • Enterprises request numbered blank invoices, and the bureau may approve fewer than requested, minting the granted range directly to the applicant.Ledger distribution makes each outstanding blank attributable to its holder without a high-availability distribution platform.Source: C. Subsystem 1: Application and… · p. 5

D. Subsystem 2: Issuance and Circulation

  • Issuance atomically checks the holder, party registration and distinctness, and valid amounts, then records the face and digest and transfers ownership to the buyer.The operation snapshots both parties and computes tax in the same transaction.Source: D. Subsystem 2: Issuance and Circulation · p. 5

E. Subsystem 3: Void and Red-Flush

  • To correct an issued invoice, only its original seller can use a held blank to create a linked credit note, reverse the original, and deliver the note to the buyer.The original and correction remain permanently visible, avoiding a centralized-system “void and reprint” pattern.Source: E. Subsystem 3: Void and Red-Flush · p. 5

F. Subsystem 4: Query and Verification

The contract supports independent invoice verification and auditable reimbursement workflows. It records face digests, provides seller-controlled tax declaration, and uses a recoverable lock before reimbursement.

F. Subsystem 4: Query and Verification

  • A verifier can hash a purported invoice face and query the on-chain digest index to check whether it matches the recorded face, without trusting or contacting either party or a central platform.Indexed events also allow reconstruction of an invoice's full history.Source: F. Subsystem 4: Query and Verification · p. 5

G. Subsystem 5: Declaration and Lock-Based Reimbursement

  • Only the seller can mark output tax declared, exactly once; a bureau policy switch can require declaration before reimbursement.This encodes a rule that otherwise exists only on paper.Source: G. Subsystem 5: Declaration and… · p. 5
  • If a red-flush guard fails, both invoices remain unchanged.The control flow reverts rather than partially applying the correction.Source: Figure 3 · p. 6
  • A two-phase reimbursement protocol locks an eligible issued, non-credit invoice to a claim id, then lets only the locker reimburse it or release it after a failed claim.The lock makes the invoice unavailable to competing claims while approval is pending, and the claim id gives auditors an on-chain join to the expense claim.Source: G. Subsystem 5: Declaration and… · p. 6

VII. SECURITY ANALYSIS

The security analysis proves that lifecycle guards enforce reimbursement uniqueness, face integrity, and authorization, while red-flush preserves signed value. The results rely on the specified system model and assumptions.

VII. SECURITY ANALYSIS

  • REIMBURSED and REVERSED are terminal states: no later transition changes either status.The operation guards cannot be satisfied when an invoice is in either state.Source: §VII · p. 6
  • An invoice can be reimbursed at most once in any execution, so no two reimbursements succeed across organizations or accounts, even under concurrency.Consensus safety serializes concurrent attempts; the first lock changes the invoice state so later lock attempts revert.Source: §VII · pp. 6–7
  • A successful reimbursement must be called by the account that most recently locked the invoice while holding it, with no intervening unlock.The sender field cannot be spoofed under the stated EUF-CMA assumption.Source: §VII · p. 7
  • A verified invoice face equals the recorded face except with negligible probability, assuming second-preimage resistance of the hash function.Producing a different face that verifies would require a second preimage for the recorded digest.Source: §VII · p. 7
  • After red-flush, the original and credit note have signed values summing to zero; the original is permanently reversed and the credit note cannot be reimbursed or red-flushed further.The theorem establishes value conservation and that the credit note is frozen.Source: §VII · p. 7

A. Machine-Checked Verification

The state-machine invariants are proved inductively across reachable transaction sequences, with five verification conditions reported safe and no counterexamples. The implementation includes a separate verification model and a four-role web application.

A. Machine-Checked Verification

  • The Solidity SMTChecker proves the modeled invariants inductively over all reachable transaction sequences and invoice numbers, abstracting invoice-face strings and hashing.The model preserves the registry, ownership, and guarded transitions; a ghost counter directly encodes reimbursement uniqueness.Source: A. Machine-Checked Verification · p. 7
  • Five verification conditions were proved safe, covering reimbursement uniqueness and authorization, credit/reversed-invoice exclusions, and red-flush value conservation and monotonicity.Weakening the reimbursement guard produced a counterexample trace, while 23 deployed-bytecode tests corroborated the properties.Source: A. Machine-Checked Verification · p. 7

VIII. IMPLEMENTATION

  • The security goals are refuted by the theorems and per-operation guards, with the state-machine goals additionally machine-checked.The implementation includes a separate SMTChecker model and a 23-case suite covering subsystem paths and adversarial cases.Source: A. Machine-Checked Verification · p. 7, §VIII · p. 7
  • The implementation is a Solidity 0.8.24 contract with guard-first access control, indexed events, and no external calls or unbounded state-changing loops except bureau-bounded range minting.The React/ethers.js application provides bureau, seller, buyer, and verifier dashboards; buyers verify invoice digests and drive the lock–reimburse–unlock protocol.Source: §VIII · pp. 7–8

IX. EVALUATION

The evaluation reports successful adversarial and end-to-end tests, O(1) core-operation costs, and single-node throughput of about 137 invoices per second. The measurements use a local development setup, so real-network consensus overhead is additional.

A. Setup

  • The evaluation used Hardhat’s in-process EVM and a local JSON-RPC node; real-network consensus overhead is additional to the reported execution measurements.Gas costs are described as deterministic EVM properties, while latency and throughput reflect the single-node configuration.Source: A. Setup · p. 8

B. Functional Correctness

  • All 23 tests passed, including adversarial access-control, duplicate-reimbursement, and forged-face cases, and the full lifecycle was exercised through the web application.The live local-chain run visibly rejected a duplicate reimbursement attempt.Source: B. Functional Correctness · p. 8

C. Gas Cost and Complexity

  • Under 135,000 gas covers lock plus reimburse, about a fifth of issuance; every core operation is O(1) in invoice count N.Issuance and red-flush dominate gas because they store a full invoice face; batch granting alone is linear in its bureau-chosen batch size k.Source: C. Gas Cost and Complexity · p. 8, Figure 5 · p. 8

D. Latency and Throughput

  • 137 invoices/s were sustained on a single development node, with 100 concurrent issuance transactions completing in 0.73 s.Mean end-to-end latency was 1.6–3.2 ms per operation, with p95 ≤8.2 ms; the paper identifies consensus configuration as the deployment constraint.Source: D. Latency and Throughput · p. 8

X. AUTONOMOUS AGENTS OVER A VERIFIED INVOICE LEDGER

The paper treats the verified contract as the safety boundary for autonomous reimbursement agents: agents may propose arbitrary calls, but contract guards preserve lifecycle guarantees. The implemented runtime separates reasoning, policy filtering, and on-chain enforcement.

X. AUTONOMOUS AGENTS OVER A VERIFIED INVOICE LEDGER

  • The contract is the already-verified guardrail for agents acting as registered accounts, so the stated safety properties require neither trust in the LLM nor an additional mechanism.The agent stack has a reasoner propose actions, a deterministic policy filter them, and the contract as final authority.Source: §X · p. 8, Figure 6 · p. 9
  • No agent behavior can reimburse an invoice more than once, verify a face differing from the recorded one, or perform an unauthorized lifecycle transition.The proof treats signed transactions from registered agent accounts as arbitrary transaction sequences covered by the machine-checked results.Source: §X · p. 9
  • A broken agent can fail to reimburse valid claims or select the wrong authorized invoice; the contract does not provide liveness or decision quality.The system therefore retains a policy layer and human escalation path; prompt injection may waste gas or misdirect effort but cannot cross authorization or uniqueness boundaries.Source: §X · p. 9

A. Agent Architecture and Implementation

  • The reimbursement runtime checks receipt digest, invoice state and ownership, claim amount, and a per-claim spending ceiling before executing lock–reimburse.A deterministic matcher is the default; an optional LLM reasoner is schema-constrained, with invalid invoice identifiers discarded.Source: A. Agent Architecture and Implementation · p. 9

B. Case Study

The case study reports that legitimate claims were reimbursed while duplicate, over-limit, and forged claims were rejected, including duplicate reimbursement when the policy was deliberately bypassed. The discussion identifies privacy and transaction-authenticity boundaries, and the conclusion points to future work and reproducible artifacts.

B. Case Study

  • Duplicate, over-limit, and forged claims were rejected by the policy, while the contract rejected a duplicate when the policy was replaced with one that approves everything.Changing the LLM reasoner can change invoice matching, but not the reported safety outcomes; twelve additional offline tests exercised the agents and policy-bypass path.Source: B. Case Study · p. 9

XI. DISCUSSION AND LIMITATIONS

  • Invoice faces are stored in plaintext contract storage, which the paper considers acceptable on permissioned consortium chains with restricted read access but not on public chains.Proposed alternatives include on-chain commitments with off-chain faces, selective encryption, and zero-knowledge proofs.Source: §XI · p. 9
  • The guarantees cover invoice integrity and lifecycle, not whether the underlying sale is real; a seller can still invoice a fictitious transaction.The paper suggests anchoring order, logistics, and payment digests at issuance and integrating payment systems to address this gap.Source: §XI · p. 9
  • The proposed production path is a tax-authority consortium chain, with a layer-2 rollup anchored to a public chain as an alternative.Storage growth of roughly 1–2 KB per face favors the commitment-on-chain variant at national volumes.Source: §XI · pp. 9–10

XII. CONCLUSION

  • Invoice numbering, red-flush semantics, and declaration follow Chinese VAT practice, while the state machine itself is jurisdiction-neutral.The conclusion identifies privacy, transaction-evidence anchoring, richer agent autonomy, and multi-node consortium evaluation as future work.Source: §XI · p. 10, §XII · p. 10

ARTIFACT AVAILABILITY

  • The contract, verification model, web application, agent runtime, tests, and reproduction scripts are available under the MIT license.The verification script and agent demo reproduce the machine-checked result and case study, respectively.Source: ARTIFACT AVAILABILITY · p. 10
Loading 2609.37819v1…