Closing the Loop: Bidirectional Fully Encrypted Protocols
Researchers show naively composing unidirectional fully encrypted protocols is detectable and construct provably secure bidirectional FEPs, validated in Rust.
The paper introduces formal security definitions for bidirectional fully encrypted protocols (BiFEPs), covering exact shaping, delivery, protocol-state integrity, private half-close, and cross-direction isolation. It shows trivially composing two unidirectional FEPs enables detection attacks via cross-direction dependencies like traffic imbalance and connection tear-down. The authors construct provably secure BiFEPs for datastream and datagram settings, validated with a Rust implementation; no surveyed deployed protocol provides the full set of properties.
- Naive composition of unidirectional FEPs detectable via traffic imbalance and tear-down patterns
- New definitions cover shaping, protocol-state integrity, private half-close, cross-direction isolation
- Provably secure constructions for both datastream and datagram settings
- Rust implementation; no deployed protocol satisfies all BiFEP properties
Full article248 words · extracted from arxiv.org · click to collapse
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.
Text extracted automatically; images, tables and formatting may be missing. Original: https://arxiv.org/abs/2609.17397