拜占庭协议（BA）是分布式系统的核心基础组件，多实例执行下的安全性分析近年受到越来越多关注。然而现有敌手模型大多只考虑节点被腐化，忽视了通信信道被对抗性操纵带来的重要威胁。攻击者可通过信道攻击在多个协议执行实例之间对消息进行重排序，从而破坏协议的安全保证。本文提出首个将节点腐化与信道攻击相结合的敌手模型，并基于该模型为并行组合与并发组合下的拜占庭协议建立了新的安全阈值，给出互相匹配的不可能性与可能性结果，形成紧界。不可能性方面：即使采用认证拜占庭协议，当 n ≤ 3t 或 n ≤ 2c + 2t + 1 时，在并行组合下也无法保证安全，其中 t 为被腐化节点数，c 为通信信道数，n 为节点总数。可能性方面：作者证明当 n > max{3t, 2c+2t+1} 时，未认证拜占庭协议在并行与并发组合下存在安全协议。为此，作者首先给出通用黑盒编译器，可将任意单实例安全的 BA 协议转换为在并行与并发执行下安全，且不引入额外安全假设；为优化性能，进一步利用纠删码设计精化编译器，显著降低通信开销，尤其对长消息可达到相对原协议的常数倍乘性开销，从而保持相同的渐近通信复杂度。该工作为多实例协议的组合安全分析提供了首个同时涵盖节点腐化与信道重排序的模型与紧界，并给出可落地的通用与优化编译方案。

拜占庭容错（BFT）协议是分布式系统中最难设计和推理的组件之一。近年来，形式化验证领域发展出多种计算机辅助方法，能够对独立（standalone）BFT 协议的安全性与活性进行自动化验证；与此同时，分布式计算社区也尝试将复杂协议拆分为更简单的“构建块”进行组合，以降低设计新协议的概念复杂性。然而，到本文发表为止，还没有任何方法论能够将这两种研究路径统一起来，实现对任意复合式 BFT 协议的基础性（foundational）验证。本文提出了一种复合式拜占庭协议的组合验证方法，核心贡献是建立一套形式化框架，使协议设计者可以基于已验证的简单子协议模块，通过组合规则安全地构建更复杂的 BFT 协议，并自动继承或证明整体协议的期望正确性属性。作者综合运用了并发证明、协议组合理论和自动验证工具，给出了模块化推理规则，并展示了该方法在多个经典 BFT 协议变体上的可行性。这项工作填补了分布式系统形式化验证中的一个空白，有望将 BFT 协议的正确性证明从“一次性、手工程序化”转化为“可组合、可复用”的工程实践。对于研究分布式共识、区块链底层以及安全关键系统的人来说，本文提供了从组合视角系统性验证容错协议的新思路。