本文针对带有链下组件的区块链智能合约语言，建立了一种形式化模型。链下组件是在区块链节点网络之外的指定位置执行的智能合约片段，但它们与链上合约状态保持同步。它们不仅响应链上状态的变化，还能将外部世界的事件（如股票价格、天气数据）通知给链上组件，甚至充当不同区块链之间的桥梁。这种架构为开发者提供了更大的灵活性，但也可能引入新的安全漏洞。为了具体研究这些问题，作者利用该模型，通过静态信息流控制（IFC）技术，考察了链上与链下组件之间数据的完整性和保密性保证问题。研究发现，即使在不存在循环构造的情况下，信息流控制也会失效，其原因在于链下组件作为独立线程运行，可以通过递归方法调用等方式编码出阻塞构造，从而绕过控制。作者在论文末尾讨论了若干可能的补救方向。该论文的核心贡献是对链下组件场景下信息流控制局限性的形式化证明，并提出了对区块链安全设计有指导意义的讨论。适合区块链安全研究者、形式化方法开发者以及智能合约语言设计者阅读。

该论文提出了一种名为 Accio 的链下支付协议，旨在解决现有基于中心节点（hub）的链下支付系统中存在的可扩展性、隐私性和效率问题。现有的 hub 类链下支付方案通常需要昂贵的零知识证明（NIZK）来实现不可链接性，且只能支持固定金额的支付，限制了其实用性。Accio 协议的核心创新在于：首先，支持可变金额的支付，允许用户在一次支付中发送任意数额的代币，而无需事先锁定固定金额；其次，通过优化设计实现了不可链接性（unlinkability），即收款节点无法将多笔支付关联到同一发送方或同一路径，且完全避免了 NIZK 的使用，显著降低了计算和通信开销；最后，Accio 基于 hub 架构，利用中心节点（hub）作为中介，连接多个支付通道，从而降低通道建立成本并提高网络连通性。论文详细描述了协议的设计原理、安全模型和具体构造，包括一种基于单向陷门置换的原子交换机制和一种新颖的匿名凭证系统。安全性分析表明，Accio 在标准模型下满足支付正确性、余额安全性和用户隐私（不可链接性）要求。性能评估通过原型实现和实验测试证明，Accio 的链下支付延迟仅为现有方案的几十分之一，且适用于大规模的微支付场景。该工作对于区块链支付通道网络（如闪电网络）的隐私增强和效率提升具有重要理论意义和实际应用价值。