PaperlayerView exact revision on arXiv

Source-linked AI summary

Closing the Loop: Bidirectional Fully Encrypted Protocols

Baigang Chen, Nicholas Hopper

arXiv:2609.17397v1cs.CR

TL;DR

Unidirectional FEPs do not model how two directions and their shared session lifetime can interact, leaving a gap for bidirectional communication. The paper defines and constructs BiFEPs for datastreams and datagrams, then evaluates implementations and surveyed protocols. Its tests pass, but none of the surveyed protocols provides the full property set.

  • Problem

    Unidirectional FEP definitions model one direction at a time, leaving bidirectional exchanges and shared session behavior outside their scope.

    Source: §I · p. 1

  • Method

    The paper formalizes BiFEP security and constructs datastream and datagram protocols that coordinate traffic shaping, authenticated state, and private termination.

    Source: §XI · p. 13

  • Results

    The implementation passed adversarial security tests, with cover expansion from 2.0× at half load to 1.09× near saturation, and none of the surveyed protocols satisfies the full property set.

    Source: §XI · p. 13

  • Takeaways & Limitations

    Bidirectional fully encrypted communication requires coordinating traffic behavior and termination across the session, beyond independently protecting two unidirectional channels.

    Source: §XI · p. 13

    Deployment assumes authenticated shared keys and agreed public parameters, and full deployments also need congestion control, NAT traversal, safe sizing, and application-data reliability.

    Source: §IX · p. 12

Abstract

from arXiv · show

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\"ive'' 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.

I. INTRODUCTION

Fully encrypted bytes can still leave observable protocol structure and metadata, while unidirectional FEP definitions do not capture dependencies between two directions. The paper motivates bidirectional security definitions and constructions that shape traffic and coordinate private close under a public schedule and close grid.

I. INTRODUCTION

  • Protocol fingerprints and observable metadata can let an observer classify, throttle, or block encrypted traffic, even when protocol-controlled bytes look random.Lengths, timing, responses to active probes, and high-entropy traffic can remain distinctive.Source: §I · p. 1
  • Parallel unidirectional FEPs can expose a private half-close when one direction goes silent while the other continues, motivating a joint bidirectional security object.Cross-direction reactions can also enable active probes.Source: §I · p. 1
  • The datastream construction continues scheduled traffic after half-close and closes only at a permitted public epoch, hiding the exact private close time.For datagrams, encrypted FIN and ACK bits are retransmitted, and both directions must provide authenticated evidence before closing.Source: §I · pp. 1–2
  • The paper formalizes bidirectional security goals and constructs datastream and datagram BiFEPs with exact per-direction schedules and encrypted close coordination.The constructions expose only the public schedule and quantized close epochs.Source: §I · p. 2

II. BACKGROUND

  • Prior FEP notions cover same-length random transcript indistinguishability and active integrity for one direction at a time, while related channel-security work does not require a random wire image.The paper uses a datastream FEP and an atomic datagram FEP as inner layers.Source: §II · p. 2

A. Endpoints, epochs, and schedules

  • Each direction has a public emission schedule, while visible closure uses a shared public grid independent of application data and private state.Schedules may be randomized but can remain distinctive, and endpoint-specific close grids can create one-directional tails.Source: A. Endpoints, epochs, and schedules · pp. 2–3

B. Adversary

The model gives the adversary visibility and control over both directions while limiting the FEP claim to protocol-controlled payload bytes. It requires shaped, integrity-protected bidirectional behavior and shows why naive composition fails, then wraps independently keyed unidirectional datastream FEPs.

B. Adversary

  • The adversary observes network and transport metadata and may delay, drop, reorder, modify, or otherwise manipulate traffic; the FEP claim covers only protocol-controlled payload bytes.Deployed transports may intentionally expose protocol structure and do not aim for the studied FEP guarantees.Source: B. Adversary · p. 3

C. Goals

  • The goals require reliable admitted-data delivery, exact scheduled lengths, random-looking live payloads, authenticated state transitions, invisible half-close, and full close only in the public grid.Dropping or modifying traffic may delay delivery or prevent termination without violating integrity unless forged events or transitions are accepted.Source: C. Goals · p. 3

D. Security notions

  • Passive security compares honest transcripts with same-length uniform outputs, while active security additionally monitors for accepted forgeries, replay, post-FIN data, and premature close.Unlike unidirectional games, the bidirectional definition fixes lengths to a public schedule and hides earlier local half-closes.Source: D. Security notions · p. 3
  • Two channels can each satisfy unidirectional FEP definitions yet fail passive BiFEP security when one direction falls silent after a half-close.In the example, the test checks whether the request direction emits zero bytes after epoch 2; the bidirectional definition instead requires 1,024 bytes in both directions through epoch 8.Source: D. Security notions · pp. 3–4

IV. BIDIRECTIONAL DATASTREAM CONSTRUCTION

  • For datastreams, an authenticated wrapper around an independently keyed unidirectional FEP encodes data, cover, and close control as encrypted objects.The inner layer never closes; the wrapper governs FIN processing and visible termination while the inner layer continues scheduled output.Source: §IV · p. 4

A. State and initialization

Each direction maintains its own wrapper and inner-layer state, with independent keys and counters. Protected wrapper frames encode application data, cover, or close control before the inner layer produces scheduled ciphertext.

A. State and initialization

  • Each direction has separate send and receive state, including keys, counters, buffers, FIN tracking, and a visible-close bit.The endpoint state also tracks private failure and peer-FIN status.Source: A. State and initialization · p. 4
  • Initialization samples independent keys for both directions and layers, then zeros counters and bits, empties buffers, and opens each write state.No key or state variable is shared across directions or layers.Source: A. State and initialization · p. 4

B. Protected objects

  • A wrapper frame is DATA, DUMMY, or FIN: DATA carries one application chunk, DUMMY carries random cover bytes, and FIN has an empty payload.Application input is chunked canonically; an empty DATA message remains distinct from no input, which produces cover.Source: B. Protected objects · p. 4
  • Protected objects bind type, payload, sequence position, and direction; their length prefix remains inside the inner encrypted stream, hiding object boundaries on the wire.The figure depicts sender-side layering for one direction, with independent keys in reverse and wrapper structure hidden as inner-layer plaintext.Source: B. Protected objects · p. 4, Figure 1 · p. 4

C. Close state and the FIN-drain invariant

The datastream close rule separates private FIN readiness from visible termination, which occurs on the public close schedule. The sender preserves exact epoch lengths while draining FIN only after its full record has been released.

C. Close state and the FIN-drain invariant

  • Both endpoints keep their full schedules through the closing epoch; termination becomes visible only at the next public bucket after private readiness.Close output requires the local FIN to be drained and the peer FIN to be authenticated, with output restricted to closing epochs.Source: C. Close state and the FIN-drain… · p. 5

D. Scheduled datastream sender

  • Algorithm 1 returns exactly ΓX(t) ciphertext bytes in each live epoch, and its loop terminates after finitely many iterations.Each iteration appends a nonempty protected record, so the output buffer grows until the scheduled prefix can be released.Source: D. Scheduled datastream sender · p. 5
  • The sender enters finDrained only after every byte of the inner record containing FIN has been released.The final FIN byte's absolute ciphertext position is tracked by finlim; ordered release ensures the transition occurs only when out ≥ finlim.Source: D. Scheduled datastream sender · p. 5, C. Close state and the FIN-drain… · p. 5
  • Epoch boundaries need not align with inner-record boundaries, and correctness does not depend on transport read, write, or TCP-segment boundaries.The wrapper releases arbitrary ciphertext prefixes rather than requiring whole-record release.Source: D. Scheduled datastream sender · p. 5

E. Datastream receiver and failure discipline

The datastream receiver processes complete protected objects in order and keeps failures private, while the epoch coordinator delays visible close until scheduled traffic and receive processing are complete. Directional state remains isolated apart from the declared close conjunction.

E. Datastream receiver and failure discipline

  • The receiver buffers input fragments and processes complete length-delimited objects in order, accepting only authenticated objects at the expected sequence number.On failure it removes the object, sets private bad, and ends the call without advancing the sequence number or searching for a later boundary.Source: E. Datastream receiver and failure… · pp. 5–6
  • Inner-receiver failure is permanently fail-stop, while wrapper failure ends only the current call; neither changes output length or visible close.Recovery requires a new higher-layer session.Source: E. Datastream receiver and failure… · p. 6

F. Epoch operation and absorbing close

  • Both endpoints send and process received traffic before applying absorbing close, preserving all scheduled bytes in the closing epoch and none afterward.A closed endpoint subsequently ignores inputs and returns an empty output with its close bit set.Source: F. Epoch operation and absorbing close · p. 6
  • Cross-direction isolation is structural: the two directions share no keys, counters, or buffers, and their only joint value is the declared close conjunction.The construction's companion datagram protocol uses the same epoch interface and coordinator while accommodating atomic, reorderable, duplicable, or lost packets.Source: F. Epoch operation and absorbing close · p. 6, §V · p. 6

A. Atomic shaped channel

The datagram construction shapes each packet to its public scheduled length, then uses encrypted semantic frames and authenticated close coordination to handle reordering, replay, and loss. Its close rule requires authenticated FIN/ACK evidence, while linger can defer visible closure.

A. Atomic shaped channel

  • Each atomic channel sender returns exactly the requested UDP payload length, using a transmitted uniform nonce and authenticated encryption for messages that fit.AES-256-GCM gives h = 28: lengths 0–28 are unauthenticated uniform chaff, 29 bytes is the smallest authenticated null, and base DATA needs 31 + |m| bytes.Source: A. Atomic shaped channel · p. 6

B. Semantic frame and endpoint state

  • The semantic frame encrypts a flag byte, sender sequence number, and application payload; both nonce and sequence must be fresh for acceptance.Exact replay sets permit reordering while rejecting repeated ciphertexts and duplicate semantic positions.Source: B. Semantic frame and endpoint state · pp. 6–7, D. Datagram receiver, replay, and close · p. 7
  • Sequence-space exhaustion backpressures inputs requiring new frames and switches the sender to scheduled chaff, without erasing readiness already obtained.The semantic wrapper adds nine bytes, making the smallest semantic datagram 40 bytes and the maximum application payload at public length p equal to p −40.Source: B. Semantic frame and endpoint state · p. 7

C. Datagram sender

  • After local half-close the sender repeats FIN, and after peer FIN it repeats ACK within the existing schedule and linger phase.DATA and FIN are mutually exclusive; DATA+ACK can continue before local half-close, and FIN+ACK carries both close signals.Source: C. Datagram sender · p. 7

D. Datagram receiver, replay, and close

  • Figure 3's one-bucket linger carries B's epoch-5 FIN+ACK beyond the dropped epochs 3–4 ACK window, allowing both endpoints to close.Under immediate bucket close, B closes at epoch 4 and A remains live indefinitely.Source: Figure 3 · p. 8, D. Datagram receiver, replay, and close · p. 8
  • Replay protection admits each semantic datagram's DATA and control meaning at most once despite reordering or duplication.FIN and ACK bits are monotone, and DATA first arriving after authenticated peer FIN is rejected.Source: D. Datagram receiver, replay, and close · pp. 7–8
  • Close safety requires the four authenticated FIN/ACK conditions, while linger can only defer visible close; packet loss may prevent termination.An endpoint remains live through a public number of additional close buckets and retransmits its acknowledgment, allowing a later ACK-bearing datagram to repair an isolated loss.Source: D. Datagram receiver, replay, and close · pp. 7–8

VI. SECURITY ANALYSIS

The security analysis proves BiFEP guarantees for datastream and datagram constructions under stated cryptographic, key, sequence, and schedule assumptions. The Rust implementation and evaluation provide a concrete instantiation, while the security claims leave statistical traffic-analysis resistance to schedule selection.

VI. SECURITY ANALYSIS

  • Under stated assumptions, the datastream construction provides bidirectional shaping, correctness, wrapper-state integrity, and active BiFEP security with leakage LBD.Assumptions include a correct, actively secure inner datastream FEP, secure wrapper AEAD, independent keys, nonrepeating sequence numbers, and private failure state.Source: §VI · p. 8
  • Under stated assumptions, the datagram construction provides exact bidirectional shaping, authenticated atomic delivery before peer FIN, replay-safe wrapper integrity, and active BiFEP security with leakage LBD.Close liveness additionally requires timely acceptance of required FIN/ACK evidence while endpoints remain live, eligible control epochs and sequence space, and a permitted close bucket.Source: §VI · p. 8
  • Datagram close liveness can fail only when no eligible linger frame is accepted because of loss or modification, a schedule below the 40-byte control minimum, or sequence exhaustion.When a fresh FIN+ACK frame emitted during linger is accepted, the peer becomes ready and its close follows the public close rule.Source: §VI · pp. 8–9
  • The guarantees are conditional on fixed public epoch timing and generator profile, with LBD revealing realized lengths and close buckets.The security games do not establish resistance to statistical traffic analysis; selecting a resistant schedule distribution is outside their scope.Source: §VI · p. 9

VII. IMPLEMENTATION

  • The reference implementation contains approximately 20.4k lines of Rust, including 2,195 datastream-construction lines and 989 datagram-construction lines.It uses AES-256-GCM, with datastream sessions ending before counter exhaustion to prevent nonce reuse under a fixed key.Source: §VII · p. 9
  • The datastream baseline uses ΓA=1200 and ΓB=1000 bytes per epoch with close buckets every fourth epoch over a 64-epoch horizon.The datagram instantiation uses a 40-byte minimum semantic datagram and a configured limit of Nsess = 232 semantic datagrams per direction.Source: §VII · p. 9
  • The close-loss evaluation sweeps linger depths L ∈{0, . . . , 3}, while conformance and active and passive datagram suites use L=0.Adapters coordinate both sends, both receive-processing steps, then absorbing close; instrumentation and artifact I/O are excluded from byte accounting.Source: §VII · p. 9
  • Implementation resource policies bound sender queues and per-call receive input at 8 MiB, and oversized inputs receive backpressure without changing state or scheduled output.An incomplete wrapper object is limited to 1 MiB and 64 receive calls, after which the receiver enters a permanent non-delivering state.Source: §VII · p. 9

VIII. EVALUATION

The evaluation combines deterministic conformance tests, active-attack trials, passive byte diagnostics, and timing measurements. The tested implementations preserved scheduled behavior and resisted tested attacks, while finite-sample diagnostics detected no byte-level artifact but do not establish computational indistinguishability.

A. Methodology and evidence classes

  • Deterministic oracle tests, loopback byte-accounting runs, passive byte-level tests, and timed scheduler runs assess distinct aspects of implementation behavior.The cryptographic claims follow from the paper’s analysis.Source: A. Methodology and evidence classes · p. 10

B. Datastream conformance and close (RQ1)

  • All 62,119 assertions passed, and all 10,642 per-direction live-epoch measurements matched their scheduled lengths exactly.The deterministic suite covered 143 scenarios, 491 trials, and 5,321 logical epochs.Source: B. Datastream conformance and close… · p. 10

C. Active integrity (RQ2)

  • Across 360 datastream trials, attacks forged no DATA or FIN and caused no premature close; 60 datagram mutations blocked target delivery, and 60 replays produced no duplicate output.For single-direction datastream mutations, the reverse-direction workload completed unchanged, while the targeted direction could stall.Source: C. Active integrity (RQ2) · p. 10

D. Passive diagnostics (RQ3)

  • Byte entropy ranged from 7.999279 to 7.999749 bits/byte, and the largest absolute correlation was 0.004668; finite-sample tests detected no byte-level artifact but do not establish computational indistinguishability.No tested 16-byte datastream block repeated, and all 1,024 authenticated datagram nonces were distinct.Source: D. Passive diagnostics (RQ3) · pp. 10–11
  • On the fixed 1,200/1,000-byte schedule, each epoch emits 2,200 bytes and cover expansion reaches 1.09×.The figure plots cover expansion and delivered goodput against offered load.Source: Figure 4 · p. 11

E. Processing cost and cover bandwidth (RQ4)

The evaluation measures prototype cost, close behavior under loss, half-close leakage, wall-clock scheduling, and specification-level support in deployed transports. It also identifies operating costs and deployment boundaries for BiFEPs.

E. Processing cost and cover bandwidth (RQ4)

  • Across 7,680 live epochs, each stream operation delivered 1,100 bytes and emitted 2,200 scheduled bytes; the lower-median stream results were 37.0 µs per epoch and 28.2 MiB/s application goodput.At idle, all 2,200 scheduled bytes per epoch were cover; expansion was 2.0× at half load and 1.09× at the largest tested load. At 50% load, increasing the symmetric schedule from 200 to 12,800 bytes per epoch raised median epoch cost from 20 µs to 234 µs.Source: E. Processing cost and cover bandwidth… · p. 11

F. Close under loss (RQ1/RQ2)

  • With L=1, every tested loss pattern with k ≤5 ended in bilateral close, while one-sided ACK loss at k=6 left A open.Each increment of L delayed otherwise successful close, including lossless controls, by one public bucket; the observed closes respected the four authenticated conditions.Source: F. Close under loss (RQ1/RQ2) · pp. 11–12

G. Naive composition versus BiFEP

  • Naive composition exposed both half-close times and their order, whereas BiFEP kept both directions scheduled through the shared close bucket.The comparison used close requests at epochs 2 and 6 on the baseline 1,200/1,000-byte schedule.Source: G. Naive composition versus BiFEP · p. 12

H. Wall-clock scheduling fidelity

  • Across tested wall-clock periods, 77–89% of endpoint-epochs started more than 2 ms late, and overruns fell from 56% at 5 ms to none at 50 and 100 ms.All 150 ten-epoch trials matched the logical oracle without skipped or merged late epochs; measurements characterize only the tested host and scheduler.Source: H. Wall-clock scheduling fidelity · p. 12, Figure 5 · p. 12

I. Comparison with deployed transports

  • No surveyed specification mandates the conjunction of bidirectional shaping, idle cover in both directions, hidden half-close, and scheduled close.The comparison is specification-level; deployed transports expose different public structures or make padding and cover optional.Source: §I · p. 12, Table VIII · p. 13

IX. DISCUSSION AND LIMITATIONS

  • Full deployment additionally requires congestion control, NAT traversal, fragmentation-safe sizing, and application-data reliability within the public schedule.The construction assumes authenticated shared keys and agreed public parameters; integrating fully encrypted key exchange remains future work.Source: §IX · p. 12
  • BiFEP’s schedule trades bandwidth, latency, and processing costs: excess capacity adds cover, longer intervals may increase buffering delay, and very short intervals can overrun processing capacity.The evaluation host had deadline overruns at 5, 10, and 20 ms, but none at 50 or 100 ms.Source: §IX · pp. 12–13
  • The implementation’s replay set grows linearly with accepted semantic datagrams; a bounded anti-replay window limits memory but can reject packets reordered beyond that window.The stated session bound is not intended as a feasible replay-set size.Source: §IX · p. 13

X. RELATED WORK

Prior work addresses one-way FEPs, obfuscated transports, and selected channel or traffic-analysis properties, but does not combine bidirectional traffic and termination into one FEP security object. The paper introduces that framework and constructions, evaluates them, and reports that no surveyed deployed protocol meets the full property set.

X. RELATED WORK

  • Prior work studied channel state, fragmentation, and secure termination without requiring a random wire shape; traffic-analysis defenses instead select schedules and quantify their cost.TLS/QUIC wire-image management and ECH reduce selected visible information but do not seek a uniform wire image; BiFEP targets subsequent bidirectional traffic and termination.Source: §X · p. 13

XI. CONCLUSION

  • BiFEP is presented as the first framework treating both traffic directions and session termination as one security object, with datastream and datagram constructions.The constructions include traffic shaping, authenticated protocol state, and privacy-preserving termination.Source: §XI · p. 13
  • None of the surveyed deployed protocols satisfies the full BiFEP property set, following Rust evaluation and specification-level analysis.The implementation passed tests for adversarial mutation, dropping, and replay; cover expansion ranged from 2.0× at half load to 1.09× near saturation.Source: §XI · p. 13

ETHICAL CONSIDERATIONS

  • The work aims to protect network-session metadata against surveillance and reports using synthetic traffic and systems under the authors’ control, with no human subjects, user data, or third-party networks.The authors acknowledge dual-use risks and state that they believe privacy and access benefits outweigh them.Source: ETHICAL CONSIDERATIONS · p. 14

GENERATIVE AI ASSISTANCE DISCLOSURE

  • The authors disclose that OpenAI Codex and Anthropic Claude assisted with paper polishing, implementation, and evaluation, while the authors reviewed and are responsible for every claim, proof, and artifact.Source: GENERATIVE AI ASSISTANCE DISCLOSURE · p. 14

OPEN SCIENCE

  • The source code and evaluation artifacts are available in an anonymous repository.Source: OPEN SCIENCE · p. 15

APPENDIX A FORMAL SECURITY GAMES AND CONCRETE BOUNDS

The appendix specifies correctness and challenge experiments for the bidirectional security definitions. Its passive and active games track endpoint state and close behavior while modeling synchronized and modified traffic.

A. Correctness

  • Datastream correctness requires exact preservation of admitted data, eventual delivery under reliable in-order delivery and continued scheduling, one authenticated FIN after prior data, and close only after both half-closes in Ecl.Source: A. Correctness · p. 15
  • Datagram correctness is atomic and at-most-once for accepted DATA before peer FIN; loss, duplication, and reordering are allowed, while close liveness depends on accepted FIN/ACK evidence and both endpoints remaining live.The stated correctness condition also requires every sender output to respect the UDP payload bound; linger keeps retransmitting FIN/ACK through L further public close buckets when eligible epochs and sequence space remain.Source: A. Correctness · p. 15

B. Passive challenge

  • The passive challenge initializes a real shadow execution with public parameters and processes epoch queries in order, running both sends before both receives and applying close afterward.Source: B. Passive challenge · p. 15
  • At finalization, the challenger discloses the two first absorbing close epochs; the passive random branch depends on the public leakage bound rather than secret real-output lengths.Source: B. Passive challenge · p. 15

C. Active datastream challenge

  • The active game records the real shadow sent stream and tracks synchronization by direction, using the receive input’s longest prefix that matches the shown stream.Source: C. Active datastream challenge · p. 15
  • The active datastream game orders one send per live endpoint before receives, with arbitrary fragmentation, coalescing, delay, insertion, and deletion represented across receive strings.Source: C. Active datastream challenge · p. 15
  • On first deviation, the active challenger processes only the common synchronized prefix in the random world, permanently desynchronizes that direction, and monitors for forged state or early close.Active security requires negligible distinguishing advantage and negligible probability of the bad event in the real branch.Source: C. Active datastream challenge · p. 15

D. Wrapper-state integrity game

The integrity game logs honestly generated protected frames and checks accepted frames and deliveries against that record. It flags semantic violations, while the datagram argument bounds fresh accepted frames by directional forgery and nonce-collision probabilities.

D. Wrapper-state integrity game

  • For every direction and semantic sequence, the send oracle logs the complete honestly generated protected frame for later comparison.The instrumentation exposes generated and accepted frames but is not part of the protocol interface.Source: D. Wrapper-state integrity game · p. 16
  • The receive oracle checks accepted frames, requires delivered payloads to match the ordered logged DATA frames, and flags first visible close when its predicate or public epoch condition fails.The monotone bad flag covers frame, DATA, FIN/ACK, replay, post-FIN-DATA, and early-close violations.Source: D. Wrapper-state integrity game · p. 16
  • In the datastream argument, absent inner plaintext failure or a fresh wrapper-ciphertext forgery, accepted frames match the unique logged frame and the deterministic state machine governs subsequent state.Source: D. Wrapper-state integrity game · p. 16
  • The monitor flags mismatched or repeated sequence frames, DATA after peer FIN, and FIN/ACK state changes without the corresponding logged flag.Source: D. Wrapper-state integrity game · p. 16
  • For datagrams, an unlogged fresh accepted semantic frame is an atomic FEP-CCA forgery; the bad-event probability is bounded by directional forgery probabilities plus transmitted-nonce collision probability.Source: D. Wrapper-state integrity game · p. 16

E. Active datagram challenge

The active datagram challenge treats packets atomically and allows recovery after modified or lost packets, while an integrity monitor constrains accepted DATA/FIN/ACK and close behavior. The appendix specifies close safety and the evaluation sweeps’ coverage.

E. Active datagram challenge

  • The active datagram challenge uses atomic synchronization: shown datagrams advance the shadow receiver, while new adversarial datagrams are opened only in the real world.Independent queries permit recovery after a modified or lost datagram; replay protection prevents repeated honest outputs from redelivering DATA.Source: E. Active datagram challenge · p. 16

A. Datastream sender and FIN drain

  • Datastream FIN becomes drained only after the entire containing inner ciphertext has left the endpoint API, distinguishing queued or encrypted FIN from publicly drained FIN.The sender tracks the inner FIN position and released output to determine that point.Source: A. Datastream sender and FIN drain · p. 17
  • Wrapper failure leaves the expected sequence unchanged; invalid semantics such as DATA after peer FIN, duplicate or non-empty FIN, and unknown tags produce neither DATA nor close.Source: A. Datastream sender and FIN drain · p. 17

B. Datagram close safety

  • No adversary can cause visible datagram close before the required FIN/ACK evidence, public linger window, and public close epoch, except with the atomic channel’s forgery probability.Readiness requires an application FIN request, authenticated peer FIN and peer ACK, and an emitted ACK; dropping or replaying traffic cannot set a missing readiness bit.Source: B. Datagram close safety · p. 17
  • Datagram close liveness is conditional: loss or modification, schedules below 40 bytes, or sequence exhaustion can strand a peer when required evidence is not accepted.Linger retransmits FIN/ACK through L additional public close buckets when eligible epochs and sequence space remain.Source: B. Datagram close safety · p. 17

APPENDIX C DETAILED EVALUATION MATRICES

  • Evaluation matrices cover datastream delivery and semantic probes, two-direction mutation trials, datagram lengths from 0 through 1500 plus the format maximum, and load, linger, and timing sweeps.The datagram active trials rotate bit flips, truncation, extension, and uniform replacement, checking delivery, recovery, and replay rejection.Source: Appendix C · p. 17
Loading 2609.17397v1…