Pending Issues

What this paper leaves open, gathered from the places the body raises it, together with what its review does and does not cover. Presentation and typesetting are not listed.

Dummy completeness stops at responsive calls.  Theorem 4.29 hypothesises systems whose cores place no responsive call. The dummy’s relay is refused at the first such call and answers \(\none \) where a real adversary would answer with substance, so the regrouping fails. Recovering completeness needs a matching notion on the environment’s side, and we do not give one.

Games have no responsive theory.  All three property-transfer results inherit that condition from Theorem 4.29. A game system whose \(\F \) reaches the slot through \(\Adv ^{!}\) sits outside all three and must have its dummy-only hypothesis established directly. Four of this paper’s own functionalities decline the hypothesis for exactly this reason and argue their transfers by hand.

The quantifier order has no converse.  Definition 4.11 fixes the simulator before the environment, and implies the weaker reading in which the simulator may depend on both. The converse we do not prove. Whether the two notions separate is open.

Blocked pairs are not characterized.  Tightness keeps a blocked comparison faithful for the private members, but it constrains no member of \(I\), and an interface member admitting a bare used name is reachable by a hosted fake instance. Pinning those, or admitting only \(\Zpid \cup \Apid \) where the environment reaches them directly, would close it. We give no general sufficient condition and no characterization.

What spawning would cost.  Admissibility withholds the whole name closure, which is more than a comparison strictly needs. Letting a simulator spawn functionalities at identities \(\varphi \) does not occupy would leave only \(\IDs (\varphi ) \setminus \IDs (\pi )\) to withhold — empty for the usual pairing. What that relaxation costs in composition is not worked out.

Trace atomicity is not temporal consistency.  Every trace entry is assembled atomically, and every append in the paper was checked. Whether an entry’s timestamp and the set fetched alongside it agree in time is a different property, secured by responsiveness rather than by atomicity. The two are easy to conflate and the paper nowhere separates them in one place.

What the review covers.  Six of twenty-one audit units were examined in full, chosen leaves-first by criticality, and in a single pass rather than the two independent ones the protocol asks for. Every defect found clustered on one mechanism — what a bundle places outward, and whether it may use its hosted members while answering a responsive call — and all were fixed. The exposure is therefore in what one pass did not look for; the realization of the authenticated channel is where a further pass should go, being the unit that actually contained defects.