The framework parameterizes adversary, simulator, and environment by polynomial circuit depth and represents a timed primitive's changing hardness rather than treating it as perfectly hidden until an instantaneous expiry.

1. definition

   Residual complexity

   formally defined

   A puzzle has residual complexity (d, r) when every depth-d adversary guesses a random puzzle solution with probability at most r; the paper calls 1−r the remaining hardness and uses the curve across depths as a leakage profile.

   Residual complexity and critical time
2. definition

   Critical time

   formally defined and designer parameterized

   Given a designer-chosen unacceptable guessing threshold, the critical time is the first depth at which residual complexity crosses it. Timed privacy is claimed only before that point, which may conservatively precede honest completion.

   Residual complexity and critical time
3. methodological property

   Falsifiable leakage assumptions

   explicitly argued

   Rather than asserting an opaque generic step, the framework's depth-indexed guessing bounds can in principle be falsified by a sampling and guessing algorithm that outperforms the assumed residual-complexity curve.

   Leaky algebraic solving and fine-grained motivation · Residual complexity and critical time
4. definition group

   Depth-bounded machines and indistinguishability

   formally defined

   The model bounds circuit depth while retaining polynomial size, extends this accounting to interactive circuits, and defines indistinguishability relative to a depth-bounded distinguisher.

   Depth-bounded circuits and indistinguishability
5. security definition (d_a, d_s, d_e)-depth-secure MPC formally defined

   A protocol is depth-secure when a d_s-depth simulator makes real and ideal executions indistinguishable to every d_a-depth adversary and d_e-depth environment; the paper gives a concurrent UC-like model and a separate sequential model.

   Depth-bounded real/ideal MPC

   1. modeling constraint

      Simulator budget is security-critical

      explicitly justified

      Constraining simulator depth prevents a vacuous proof in which the simulator solves a time-lock puzzle to learn information unavailable to the real adversary; meaningful parameters require the simulation budget to remain below relevant adversary and environment depths.

      Depth-bounded real/ideal MPC · Sequential and lockstep composition
   2. security property

      Temporary privacy with matched leakage

      formally modeled

      Leaky ideal functionalities reveal information in phases so that a simulator learns no more than the adversary at the corresponding depth; outputs may become public after the timed protection has served its purpose.

      Leaky functionalities and temporary privacy

The paper tracks how simulator work reduces the adversary depth covered by the result, increases the composite simulator budget, and limits the environment to the weaker component bound.

1. theorem

   Concurrent composition (Theorem 3)

   proved

   If π is (d_a,d_s,d_e)-secure and ρ is (d'_a,d'_s,d'_e)-secure, their concurrent composition is (d_a−d'_s, d_s+d'_s, min(d_e,d'_e))-secure, under the theorem's meaningful-depth conditions.

   Concurrent composition theorem
2. theorem

   Sequential composition (Theorem 4)

   proved

   When π invokes ρ sequentially, the general bound is (d_a−d'_s, d_s·d'_s, min(d_e,d'_e)); if the caller's simulator never rewinds across the invocation, Corollary 1 improves the simulator term to d_s+d'_s.

   Sequential and lockstep composition
3. corollary

   Lockstep and serial structure

   proved or claimed as specified

   Lockstep execution lets multiple subprotocol simulators run in parallel so degradation depends on the largest relevant simulator depth rather than summing all of them. For serially separated executions, the paper states that independent analyses need not degrade one another.

   Sequential and lockstep composition · Boundary with arbitrary-polynomial MPC
4. boundary

   Boundary with standard arbitrary-polynomial MPC

   explicitly characterized

   Depth-bounded protocols may use or run beside standard MPC through the stated composition bounds. The reverse direction has no general black-box theorem; it is supported in the special case where the timed subprotocol's inputs and outputs may all be revealed when it terminates.

   Boundary with arbitrary-polynomial MPC

Generate an algebraic puzzle Z with random solution r, mask the intended solution χ as γ=H(r) xor χ, and publish (Z,γ). Solving recovers r and then χ; only the final masking step uses the random oracle.

1. theorem

   Compiler guarantee (Theorem 5)

   proved

   The compiled construction's critical time is no earlier than the last point at which the base algebraic solution still hides on the order of the security parameter in bits; the proof links this hidden information to negligible guessing probability.

   One-random-oracle compiler
2. simulation technique

   Late equivocation

   analyzed in random oracle model

   A simulator can initially use a random puzzle solution and later program the random oracle so the puzzle opens to the required value. This requires a small timing advantage and guarantees privacy only until the critical time.

   Simulation-equivocation and temporary-privacy boundary

The paper uses auctions to demonstrate how temporary privacy, non-malleability, simulator budgeting, and composition loss interact in a concrete multi-party protocol.

1. protocol Single-round single-item auction specified and proved under assumptions

   Each party unfair-broadcasts a time-lock puzzle containing its bid before t_bid, solves all timely puzzles in parallel by t_end, and outputs all bids and the maximum. Puzzle parameters require the critical time to follow the bid deadline.

   Single-round auction functionality and protocol

   1. theorem

      Single-auction security (Theorem 6)

      proved under named assumptions

      Given an equivocable, non-malleable time-lock puzzle and a bounded unfair-broadcast simulator, the protocol realizes the auction functionality with adversary depth reduced by the broadcast-simulation cost and simulator depth covering puzzle generation plus equivocation.

      Single-round auction functionality and protocol · Deferred model details and proofs
   2. assumption

      Non-malleability blocks bid adaptation

      explicitly required

      The proof requires a corrupt bidder not to transform honest parties' unsolved puzzles into related bid puzzles. Appendix F reduces indistinguishability of real and simulated executions to concurrent puzzle non-malleability, with a CCA-based alternative discussed.

      Single-round auction functionality and protocol · Deferred model details and proofs
2. protocol Simultaneous multi-round auction specified and composition analyzed

   A round runs one single-item auction per item in lockstep, and rounds are then composed serially. Because concurrent composition weakens the adversary-depth guarantee, the bid deadline and puzzle hardness must be retuned.

   Simultaneous multi-round auction composition

   1. theorem

      SMRA security (Theorem 7)

      proved

      If the single-auction protocol is (d_a,d_s,d_e)-secure, one lockstep SMRA round is (d_a−d_s,2d_s,d_e)-secure; with appropriate parameterization and end-of-round revelation, the full serial SMRA implements its functionality in the arbitrary-polynomial regime.

      Simultaneous multi-round auction composition