F-TLP — Time-lock puzzle

F-TLP (Time-lock puzzle) is part of Time and Applications in the UC functionality encyclopedia. Status: a canonical, well-established UC functionality.

A message you cannot read until you have done a fixed amount of work. The difficulty of modelling this composably is that “amount of work” is not a cryptographic notion — a functionality cannot count an adversary’s steps. The source’s answer is to make the work literal: the puzzle is a chain of \(\Gamma\) random states, each step of which is one call, and the message opens only to whoever holds the state at the end of the chain.

So the security is combinatorial rather than computational. Line 9 lays down a chain nobody can shortcut because the states are random and unrelated; line 17 walks it one step per call; line 20 opens the message only for the true endpoint. Nothing in the box appeals to how fast anybody computes.

Functionality

Reading the box: \(\mathcal{A}(\cdot)\) is a call on the adversary slot whose answer is used at lines 8 and 23 and discarded at line 12; require refuses the call, and the framework answers \(\textsf{rej}\), so no return is written for it; \(\mathbf{C}\) is the set of corrupted parties; \(\square\) marks a value never set and \(\bot\) an absence; \(\mathcal{S}\) and \(\mathcal{T}\) are the state and tag spaces; \(O\) is the parameter naming the puzzle’s owner.

Functionality \(\mathcal{F}_{\mathsf{TLP}}\)
\(\mathit{pid}\),   \(\mathbf{P}\),   \(\mathbf{N}\),   \(\mathbf{U} := \{(\mathcal{A},\mathsf{serves})\}\),   \(\mathit{par} := (O, \tau)\)
Initialize():
  1. \(\mathtt{next}[*] \gets \square\)// the state chain: one step per entry
  2. \(\mathtt{msg}[*,*] \gets \square\);  \(\mathtt{puz} \gets \square\)
  3. \(\mathtt{at}[*] \gets \square\)// how far each solver has walked
id.CreatePuzzle(Γ, msg)from id
  1. \(\textbf{require}\ \mathit{id}.P = O \ \wedge\ \mathtt{puz} = \square \ \wedge\ \Gamma \in \mathbb{N}\)// one puzzle per instance, and the owner's alone
  2. \(\textbf{if}\ O \notin \mathbf{C}\ \textbf{then}\)
  3. \(\mathit{tag} \gets_{\$} \mathcal{T}\);  \((\mathit{st}_{0}, \ldots, \mathit{st}_{\Gamma}) \gets_{\$} \mathcal{S}\)// distinct, and the chain is the box's own
  4. \(\textbf{if}\ O \in \mathbf{C}\ \textbf{then}\)
  5. \((\mathit{tag}, \mathit{st}_{0}, \ldots, \mathit{st}_{\Gamma}) \gets \mathcal{A}\bigl(\mathit{id}.\mathsf{CreatePuzzle}, \Gamma\bigr)\)
  6. \(\forall j < \Gamma : \mathtt{next}[\mathit{st}_{j}] \gets \mathit{st}_{j+1}\)
  7. \(\mathtt{msg}[\mathit{st}_{0}, \mathit{tag}] \gets (\mathit{st}_{\Gamma}, \mathit{msg})\)
  8. \(\mathtt{puz} \gets (\mathit{st}_{0}, \Gamma, \mathit{tag})\)
  9. \(\mathcal{A}\bigl(\mathit{id}.\mathsf{CreatedPuzzle},\ \mathtt{puz}\bigr)\)
  10. \(\textbf{return}\ \mathtt{puz}\)
id.Solve(st)from id
  1. \(\textbf{require}\ \mathtt{puz} \neq \square\)
  2. \(\textbf{if}\ \mathtt{next}[\mathit{st}] = \square\ \textbf{then}\)
  3. \(\mathtt{next}[\mathit{st}] \gets_{\$} \mathcal{S}\)// off the chain: a fresh step, going nowhere
  4. \(\mathtt{at}[\mathit{id}.P] \gets \mathtt{next}[\mathit{st}]\)// one step per call: the call is the clock
  5. \(\textbf{return}\ \mathtt{at}[\mathit{id}.P]\)
id.GetMsg(puz, st)from id
  1. parse \(\mathit{puz}\) as \((\mathit{st}_{0}, \Gamma, \mathit{tag})\)
  2. \(\textbf{if}\ \mathtt{msg}[\mathit{st}_{0}, \mathit{tag}] = (\mathit{st}, \mathit{msg})\) for some \(\mathit{msg}\ \textbf{then}\)
  3. \(\textbf{return}\ \mathit{msg}\)// only the true end of the chain opens it
  4. \(\textbf{if}\ O \in \mathbf{C}\ \textbf{then}\)
  5. \(\textbf{return}\ \mathcal{A}\bigl(\mathit{id}.\mathsf{GetMsg}, \mathit{puz}, \mathit{st}\bigr)\)
  6. \(\textbf{return}\ \bot\)
id.Leak()from id
  1. \(\textbf{if}\ O \in \mathbf{C}\ \textbf{then}\)
  2. \(\textbf{return}\ (\mathtt{puz}, \mathtt{next}, \mathtt{msg})\)
  3. \(\textbf{return}\ (\mathtt{puz}, \mathtt{at}[\mathit{id}.P])\)// the message stays shut until the chain is walked

The box is transcribed from Baum, David, Dowsley, Nielsen and Oechsner, TARDIS: a foundation of time-lock puzzles in UC, ePrint 2020/537, revision 20210808:072900, Figure 3, p. 16 — “Functionality \(\mathcal{F}_{\mathsf{tlp}}\) for time-lock puzzles”. The rendered page is at _src/baumetal2021-p16.png.

The clock is the call, and that is the translation to understand. The source is a ticked functionality: it keeps an inbox and an outbox, Solve appends to the inbox, and a Tick interface — driven by the paper’s global ticker — moves the inbox to the outbox so a party’s Output can collect it. One tick, one step. This framework has no ticker, so line 17 advances the chain on the Solve call itself, and the source’s Output interface disappears with the inbox it drained. The reachable behaviour is the same and the accounting is the same — \(\Gamma\) calls to walk a \(\Gamma\)-step chain — but who forces time to pass differs, and a reader comparing with the source should know that its steps are global ticks and these are the solver’s own activations. F-beacon, from the same group of authors, needed the identical translation.

Lines 5–8 are where honesty of the owner matters. For an honest owner the box draws the chain and tag itself; for a corrupt owner the adversary supplies them. The source requires the states be distinct in both cases, which is what stops a corrupt owner from building a chain with a shortcut — a repeated state would let a solver skip ahead. That distinctness is a condition on the adversary’s answer, and it is the one place a corrupt owner is constrained rather than trusted.

Line 16 is subtler than it looks. A Solve on a state that is not on any chain gets a fresh random successor, which is then recorded. So off-chain solving is possible, terminates, and leads nowhere: the walker gets states forever and never reaches an endpoint that opens anything at line 20. That is how the box says “solving a wrong puzzle is not detectably different from solving a right one until you finish”, which is a real property of time-lock puzzles and easy to omit.

Line 20 is the whole security property. The message opens only when the presented state is the recorded endpoint for that puzzle’s start and tag. There is no partial opening, no leak partway along the chain, and — for an honest owner — no adversary line that opens it early. Line 27 is the corresponding absence: another party’s leak carries the puzzle and its own position, never the message.

One thing the source has that this box does not model. In the source the message leaks to the adversary after \(\epsilon\Gamma\) steps for a parameter \(\epsilon < 1\) — the puzzle is not hiding all the way to the end, because a real adversary with more compute than the honest solver gets there sooner. That early-leak clause is the paper’s way of admitting a compute gap, and it is deliberately omitted here: modelling it needs a step counter per party and a second parameter, and adding it silently would understate what the box promises. This entry’s box is therefore stronger than the source’s, and a protocol proved against the source is not proved against this one. That is the most important caveat on the page.

Known realizations

From a trapdoor verifiable delay function, in the paper’s own construction. The owner uses the trapdoor to compute the VDF on a random start state for \(\Gamma\) steps, obtaining the endpoint and a proof, then masks the message with a random-oracle hash of the whole tuple and publishes \((\mathit{st}_0, \Gamma, \mathit{tag})\). A solver computes the \(\Gamma\) steps without the trapdoor, recovers the hash input, and unmasks. The theorem is stated in a hybrid model with a global ticker, a restricted programmable observable random oracle, and the VDF.

Rivest, Shamir and Wagner’s original construction — the stub’s other reference, and the origin of the primitive — is a technical report from 1996 and prints no functionality; it predates ideal-functionality notation. It is kept as the origin of the idea, not as a source for the box, the way F-OT keeps its Rabin reference.

What is built on it. F-beacon is realized from publicly verifiable time-lock puzzles by the same authors: everyone locks a random value, the values are opened after the delay, and the XOR is the beacon. That construction is the clearest argument for why a composable treatment of puzzles was worth having.

Properties

  • Hiding until the endpoint, with probability exactly \(1\) — in this box. Line 20 is the only path from \(\mathtt{msg}\) to a caller when the owner is honest, and it requires the recorded endpoint. But see the caveat above: the source additionally leaks the message after \(\epsilon\Gamma\) steps, and that clause is not modelled here.
  • \(\Gamma\) calls to open, exactly. Line 17 advances one step per call, and line 9’s chain has \(\Gamma\) links. No line skips.
  • No shortcut for a corrupt owner. Line 8’s states must be distinct, so even an adversary-chosen chain has full length.
  • Off-chain solving terminates and reveals nothing (lines 15–16). The walker cannot tell it is off the chain until it fails to open anything.
  • One puzzle per instance (line 4). Many puzzles are many instances, which is what makes the per-instance owner parameter sound.
  • No liveness. Nothing forces anyone to solve, and nothing bounds when they do.

Formal artifacts

No machine-checked formalization yet.

References:

  • Baum, David, Dowsley, Nielsen, and Oechsner. TARDIS: a foundation of time-lock puzzles in UC. In Advances in Cryptology – EUROCRYPT 2021, Part III, volume 12698 of LNCS, pages 429–459, 2021. Read at ePrint revision 20210808:072900. Figure 3, p. 16, the definition transcribed above, including its Output and Tick interfaces and the \(\epsilon\Gamma\) early-leak clause this box does not model. All five authors confirmed against the paper’s own title page; the venue and page range are as the stub recorded them.
  • Rivest, Shamir, and Wagner. Time-lock puzzles and timed-release crypto. Technical Report MIT/LCS/TR-684, MIT, 1996. Carried over from the stub’s reference list as the origin of the primitive. It prints no ideal functionality — at 1996 it predates the notation — and nothing on this page rests on it.