F-fsAEAD — Forward-secure AEAD, one epoch

F-fsAEAD (Forward-secure AEAD, one epoch) is part of Cryptographic Library and Symmetric Primitives in the UC functionality encyclopedia. Status: a canonical, well-established UC functionality.

Introduced as one piece of a decomposition of the Signal protocol, alongside F-secmsg and F-CKE. A one-directional stream of numbered messages inside a single epoch, with two deletion interfaces — one for the sender, one for the receiver — and the security content is entirely in what those two make unreachable.

Functionality

Reading the box: \(\mathit{id}_{\mathcal{F}}.\mathsf{Full}\mathsf{Op}()\) as \(\mathit{id}\) is a call this functionality makes on another, in the caller’s name; \(\square\) marks a slot never filled and \(\bot\) a refusal or a failure; require refuses the call, and the framework answers \(\textsf{rej}\), so no return is written for it. \(\mathtt{I}\) is a program fetched from a code library and run, with state \(\mathtt{st}\) persisting across calls; \(\mathtt{Off}\) is the set of message numbers that can no longer be read.

Functionality \(\mathcal{F}_{\mathsf{fsAEAD}}\)
\(\mathit{pid}\),   \(\mathbf{P} := \{P_0, P_1\}\),   \(\mathbf{N}\),   \(\mathbf{U} := \{(\mathcal{A},\mathsf{serves}),\,(\mathcal{F}_{\mathsf{Lib}},\mathsf{serves})\}\),   \(\mathit{par} := \bot\)
Initialize():
  1. \(\mathtt{I} \gets \square\);  \(\mathtt{st} \gets \bot\)// the uploaded code, and its running state
  2. \(\mathtt{S} \gets \square\);  \(\mathtt{n} \gets 0\)// the sender for this epoch, and its counter
  3. \(\mathtt{Rec}[*] \gets \square\)// \((\mathit{msg}, c, N)\) per message number
  4. \(\mathtt{Bad} \gets \varnothing\);  \(\mathtt{Off} \gets \varnothing\)// triples that failed; numbers no longer readable
  5. \(\mathtt{stop} \gets 0\);  \(\mathtt{got} \gets 0\);  \(\mathtt{corr} \gets 0\)
id.Encrypt(msg, N)from id′
  1. \(\textbf{require}\ \mathit{id}.P \in \mathcal{F}_{\mathsf{fsAEAD}}.\mathbf{P} \ \wedge\ \mathtt{stop} = 0\)// a sender that has deleted cannot encrypt
  2. \(\textbf{if}\ \mathtt{S} = \square\ \textbf{then}\)
  3. \(\mathtt{S} \gets \mathit{id}.P\)// the first activation fixes the direction
  4. \(\mathtt{I} \gets \mathit{id}_{\mathcal{F}_{\mathsf{Lib}}}.\mathsf{FullCode}() \text{ as } \mathit{id}\)
  5. \(\textbf{require}\ \mathit{id}.P = \mathtt{S}\)
  6. \(\mathtt{n} \gets \mathtt{n} + 1\)
  7. \(\textbf{if}\ \mathtt{corr} = 0\ \textbf{then}\)
  8. \((\mathtt{st}, c) \gets \mathtt{I}\bigl(\mathtt{st}, \mathsf{Encrypt}, \mathit{id}.P, N, |\mathit{msg}|\bigr)\)// the length only, and no message number
  9. \(\textbf{if}\ \mathtt{corr} = 1\ \textbf{then}\)
  10. \((\mathtt{st}, c) \gets \mathcal{A}\bigl(\mathit{id}.\mathsf{Encrypt}, \mathit{id}.P, \mathtt{n}, N, \mathit{msg}\bigr)\)
  11. \(\mathtt{Rec}[\mathtt{n}] \gets (\mathit{msg}, c, N)\)
  12. \(\textbf{return}\ c\)// the number travels in the protocol's header
id.StopEncrypting()from id′
  1. \(\textbf{require}\ \mathtt{S} \neq \square \ \wedge\ \mathit{id}.P = \mathtt{S}\)
  2. \(\mathtt{stop} \gets 1\)
  3. \(\textbf{return}\) ok
id.Decrypt(c, j, N)from id′
  1. \(\textbf{require}\ \mathit{id}.P \in \mathcal{F}_{\mathsf{fsAEAD}}.\mathbf{P} \ \wedge\ \mathtt{S} \neq \square \ \wedge\ \mathit{id}.P \neq \mathtt{S}\)
  2. \(\textbf{if}\ j \in \mathtt{Off} \ \vee\ (c, j, N) \in \mathtt{Bad}\ \textbf{then}\)
  3. \(\textbf{return}\ \bot\)// deleted, or already found unauthentic
  4. \(\textbf{if}\ \mathtt{corr} = 0\ \textbf{then}\)
  5. \((\mathtt{st}, v) \gets \mathtt{I}\bigl(\mathtt{st}, \mathsf{Authenticate}, \mathit{id}.P, c, j, N\bigr)\)
  6. \(\textbf{if}\ \mathtt{corr} = 1\ \textbf{then}\)
  7. \((\mathtt{st}, v) \gets \mathcal{A}\bigl(\mathit{id}.\mathsf{Decrypt}, \mathsf{Inject}, \mathit{id}.P, c, j, N\bigr)\)
  8. \(\textbf{if}\ v = \bot\ \textbf{then}\)
  9. \(\mathtt{Bad} \gets \mathtt{Bad} \cup \{(c, j, N)\}\)
  10. \(\textbf{return}\ \bot\)
  11. \(\mathtt{Off} \gets \mathtt{Off} \cup \{j\}\);  \(\mathtt{got} \gets 1\)// read once, then gone
  12. \(\textbf{if}\ \mathtt{corr} = 1\ \textbf{then}\)
  13. \(\textbf{return}\ v\)
  14. \(\textbf{require}\ \mathtt{Rec}[j] \neq \square\)
  15. \((\mathit{msg}, \cdot, \cdot) \gets \mathtt{Rec}[j]\)
  16. \(\textbf{return}\ \mathit{msg}\)
id.StopDecrypting(j^{*})from id′
  1. \(\textbf{require}\ \mathtt{S} \neq \square \ \wedge\ \mathit{id}.P \neq \mathtt{S} \ \wedge\ \mathtt{got} = 1\)
  2. \(\mathtt{Off} \gets \mathtt{Off} \cup \{j : j > j^{*}\}\)// everything above the mark, at once
  3. \(\textbf{return}\) ok
id.Leak()from id′
  1. \(\textbf{require}\ \mathit{id}.P \in \mathcal{F}_{\mathsf{fsAEAD}}.\mathbf{P}\)
  2. \(\mathtt{corr} \gets 1\);  \(L \gets \varnothing\)
  3. \(\textbf{if}\ \mathtt{S} \neq \square \ \wedge\ \mathit{id}.P \neq \mathtt{S}\ \textbf{then}\)
  4. \(L \gets \{(j, \mathtt{Rec}[j]) : \mathtt{Rec}[j] \neq \square \wedge j \notin \mathtt{Off}\}\)// a receiver's unread messages, and only those
  5. \(\textbf{return}\ (\mathtt{st},\ L)\)// a sender leaks no message at all

The box is transcribed from Canetti, Jain, Swanberg and Varia, Universally composable end-to-end secure messaging, ePrint 2022/376, revision 20230519:151937 (the newest of five postings), Figure 15, p. 41 — the functionality \(\mathcal{F}_{\mathsf{fs\_aead}}\), captioned “The Forward-Secure Encryption Functionality”.

Retitled to name the scope the source states in its first line: the functionality “processes encryptions and decryptions for a single epoch”. A whole conversation is a sequence of these, keyed by epoch_id in the session identifier and stitched together by F-secmsg; one instance carries one direction of one epoch.

Four lines carry the forward secrecy, and it is worth reading them as a pair of one-way doors:

  • Line 19 closes the sender’s door. After StopEncrypting, line 6 refuses every further encryption in this instance. In the protocol this is the sender deleting the epoch’s sending state, and the box models deletion as loss of ability rather than as loss of stored data — which is the only way a functionality can express it.
  • Line 38 closes the receiver’s, in bulk. StopDecrypting takes a mark \(j^{*}\) and makes everything above it unreadable at once. This is the interface a real receiver uses when it advances an epoch: messages still in flight from the old epoch are abandoned. Note the asymmetry with line 32, which retires numbers one at a time as they are read.
  • Line 43 is where the two doors pay off. A corrupt sender’s adversary gets the code’s state and nothing else — leakage is empty, because everything it sent is gone from its side. A corrupt receiver’s gets exactly the messages that are still readable: recorded and not in \(\mathtt{Off}\). So the plaintext of a message that has been read, or that the receiver has abandoned, is unreachable by corrupting either party.
  • Line 31 makes reading destructive. A successful decryption adds \(j\) to \(\mathtt{Off}\), so the same number cannot be decrypted twice and its plaintext leaves the corruption leak at the same moment. Replay protection and forward secrecy are the same line here.

Two more things the box says:

  • Line 13 hands the uploaded code the length and the associated data, and not the message number. The counter is incremented at line 12 and used only to index \(\mathtt{Rec}\) and to answer decryptions. So the ciphertext’s distribution is independent of position in the stream — which is a real constraint on any protocol realizing this, and stronger than the AEAD module one layer down, whose code does receive a number in the corrupt branch.
  • Line 8 fixes the direction on first use. Whoever encrypts first is the sender for the life of the instance, and line 21 refuses a decryption from that party. There is no interface to swap.

Where the source needed a decision, and two places its text is under-determined:

Source Box Why
Honest decryption “output \((\texttt{Decrypt}, c, \mathsf{msg\_num}, N, m)\)” Line 34, a require on \(\mathtt{Rec}[j] \neq \square\), then line 36 \(m\) is unbound if no message was ever recorded under \(j\), and the uploaded code’s Authenticate can accept such a \((c, j, N)\). Reading the output as the recorded plaintext is the only coherent option; the require is added so that the case where there is none is refused rather than answered with an unset value. The same under-determination appears one module down, and there the paper’s own \(\mathcal{F}_{\mathsf{SM}}\) resolves it the same way.
Encrypt outputs \((\texttt{Encrypt}, c)\); Decrypt takes \(\mathsf{msg\_num}\) as an input Line 17 returns \(c\) alone The number is not returned, so the receiver must learn it elsewhere — in the protocol it rides in the header. Returning it would make the box more informative than the source and would hide the fact that the header is unauthenticated by this module.
A Corrupt interface that reports \((\mathsf{state}_{\mathcal{I}}, \mathit{pid}, \mathsf{leakage})\) to \(\mathcal{A}\) and relays \(\mathcal{A}\)’s simulated state \(S\) back to its caller Lines 40–44, \(\mathsf{Leak}\) Corruption is the framework’s here, so the report becomes the leak. The relay half has no counterpart: a corrupted party’s protocol state is the adversary’s to fabricate directly in this framework.
StopDecrypting ends the activation if “no messages have been successfully decrypted by \(\mathit{pid}_i\)” \(\mathtt{got}\), set at line 31 and tested at line 37 The condition is about this receiver having consumed at least one message, which is exactly what line 32 records. Without the flag the test would have to inspect \(\mathtt{Off}\), which StopDecrypting itself writes to, and would then be satisfiable by calling it twice.
Leakage is \(\{(\mathit{pid}_{\mathsf{sender}}, h = (\mathsf{epoch\_id}, \mathsf{msg\_num}, N), c, m)\}\) Line 43’s \((j, \mathtt{Rec}[j])\) The same content: the epoch identifier is the instance here, and \(\mathtt{Rec}[j]\) holds \((\mathit{msg}, c, N)\).
Session identifier \(\mathit{sid}.\mathit{fs} = (\text{“}\mathit{fs\_aead}\text{”}, (\mathit{pid}_0, \mathit{pid}_1), \mathsf{epoch\_id})\), and inputs from other machines ignored The process id, and \(\mathbf{P} := \{P_0, P_1\}\) Clean, and it carries the one-epoch scope.
\(\mathcal{F}_{\mathsf{lib}}\) supplies \(\mathcal{I}\) \(\mathbf{U}\) on the header line No page here, and load-bearing for the same reason as one module down: code fixed in advance is what lets an honest-case ciphertext be produced without the simulator holding the plaintext.

Known realizations

  • \(\Pi_{\mathsf{fs\_aead}}\), Figure 30, p. 75 of the same paper, with its internal adversary in Figure 31 and simulator in Figures 32–33. It builds this box from F-AEAD and the message key exchange \(\mathcal{F}_{\mathsf{mKE}}\) (Figure 28, p. 73), one instance of each per message — which is why the AEAD box refuses a second encryption.
  • Upwards, this box plus the epoch key exchange realizes the secure-messaging functionality. The modular structure is the paper’s contribution rather than any single protocol, and the composition theorems are what make the stack a proof.

Properties

  • Confidentiality, with probability exactly \(0\) of leakage while both peers are honest: no call on the adversary slot in the honest branch carries a plaintext, and line 13 hands the code only \(\lvert \mathit{msg} \rvert\) and \(N\).
  • Forward secrecy, sender side, with probability exactly \(0\): line 42’s guard excludes the sender, so corrupting it leaks \(\mathtt{st}\) and no message — before or after StopEncrypting.
  • Forward secrecy, receiver side, bounded by \(\mathtt{Off}\): corrupting the receiver leaks exactly the messages recorded and not retired. Retirement happens on a successful read (line 31) or in bulk on StopDecrypting (line 38). Everything else is unreachable.
  • Authenticity, conditional on the uploaded code, with a permanent rejection: line 29 records a failed triple in \(\mathtt{Bad}\), and line 22 makes that permanent — a \((c, j, N)\) once rejected can never later be accepted, in either the honest or the corrupt branch.
  • Ordering is not enforced. Numbers may be decrypted in any order, and gaps are permitted: line 22’s only test is membership of \(\mathtt{Off}\) and \(\mathtt{Bad}\). What StopDecrypting gives is not in-order delivery but the ability to declare a suffix abandoned.

Formal artifacts

No machine-checked formalization yet.

References:

  • Canetti, Jain, Swanberg, and Varia. Universally composable end-to-end secure messaging. In Advances in Cryptology – CRYPTO 2022, volume 13508 of LNCS, 2022. Figure 15, p. 41 of revision 20230519:151937, the newest of five postings — the definition transcribed above; Figure 2, p. 18 for the code library; Figures 28–29, pp. 73–74 for the message key exchange and the AEAD module it is built from; Figure 30, p. 75 for the protocol.