使重复报销不可表示：一个面向人类与AI代理的经过验证的以太坊电子发票系统

中文摘要 AI 辅助

电子发票正在全球范围内取代纸质发票，但当今的中心化架构在消费端留下了三个未解决的问题：发票可以重复提交报销，收件人难以验证其真实性，以及数据被隔离在中央机构中，该机构既构成性能瓶颈又构成单点故障。本文介绍了基于区块链的以太坊电子发票系统的设计、形式化分析和实现。我们将发票生命周期形式化为一个带守卫的标记转换系统，并在标准密码学和共识假设下证明该系统保证：(i) 报销唯一性——一张发票最多被报销一次，即使在互不信任的组织之间也是如此；(ii) 面额完整性——任何经过验证的发票都与记录的发票匹配，除非keccak256第二原像抗性被破坏；(iii) 每个生命周期操作的授权健全性。核心不变量使用Solidity SMTChecker进行机器检查，证明所有可达交易序列的归纳有效性。该架构将每张发票建模为不可替代、不可交易的代币，其状态通过五个带守卫的子系统转换，采用基于锁的协议，使重复报销不可表示而不仅仅是可检测。我们将该设计实现为Solidity 0.8合约，并带有一个四角色Web应用程序，在私有以太坊网络上进行评估：签发成本为646,773 gas，完整报销成本低于135,000 gas，所有操作在O(1)时间内运行，单个节点可维持137次签发/秒。最后，经过验证的合约充当基于LLM的报销代理的安全保护层，即使代理的内部策略失败，也能可证明地拒绝不安全操作（重复、超限或伪造收据的索赔）。所有代码和基准测试均为开源。

英文摘要

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.

发表机构

• George Mason University（乔治梅森大学）
• College of Engineering and Computing（工程与计算学院）

机构由 AI 辅助整理，请以论文原文为准。