发表机构
University of Minnesota（明尼苏达大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
针对双向全加密协议易被检测的问题，提出新安全定义并构造可证明安全的BiFEPs，覆盖数据流与数据报，经Rust实现验证。
AI 中文摘要
全加密协议（FEPs）提供加密通道，使所有协议生成的字节在计算上与均匀随机字符串不可区分。先前多项工作探索了单向FEPs的安全定义与构造：在这些协议中，一方仅作为发送方，另一方仅作为接收方。然而，大多数应用需要双向信息交换，且网络对手可以观察两个方向的通信及其共享生命周期。由于双向通道的语义涉及更复杂的共享状态，两个单向通道的“朴素”组合可能导致可被检测的双向协议，检测依据包括两个方向之间的依赖关系，如流量不平衡、通道关闭、故障或连接拆除。为解决此问题，我们为双向FEPs引入新的形式化安全定义，涵盖精确塑形、投递、协议状态完整性、私有半关闭和跨方向隔离，同时公开可能随机化的“发送调度”和“关闭纪元”。我们证明朴素组合无法满足这些定义，导致实际检测攻击。随后，我们为数据流和数据报两种设置构造了可证明安全的双向FEPs（BiFEPs）。对于数据流，我们将两个方向分离的FEPs与一个“包装”层结合，防止基于单向与双向连接状态不匹配的检测。对于数据报，我们添加带重放保护和容忍丢失关闭的加密DATA/FIN/ACK。我们通过Rust实现验证了设计，并表明所调查的已部署协议均未提供完整的BiFEP安全属性集。
英文摘要
Fully encrypted protocols (FEPs) provide encrypted channels that make all protocol-generated bytes computationally indistinguishable from uniform random strings. Several previous works have explored security definitions and constructions of unidirectional FEPs: protocols in which one party acts only as a sender, and the other acts only as a receiver. However, most applications require two-way information exchange, and a network adversary can observe communication in both directions and their shared lifetime. Because the semantics of bidirectional channels involve more complex shared state, it is possible that the ``naïve'' composition of two unidirectional channels can result in a two-way protocol that can be detected based on dependencies between the two directions, such as traffic imbalance, channel closure, failures, or connection tear-down. To address this issue, we introduce new formal security definitions for bidirectional FEPs that capture exact shaping, delivery, protocol-state integrity, private half-close, and cross-direction isolation, while revealing a public ``sending schedule'' and ``closing epoch'' that may be randomized. We show that the trivial composition fails to meet these definitions, leading to practical detection attacks. We then construct provably secure bidirectional FEPs (BiFEPs) for both the datastream and datagram settings. For datastream, we combine two direction-separated FEPs with a ``wrapper'' layer that prevents detection based on the mismatch between uni- and bi-directional connection states. For datagram, we add encrypted DATA/FIN/ACK with replay protection and loss-tolerant close. We validate the design through a Rust implementation and show that none of the surveyed deployed protocols provides the full set of BiFEP security properties.
