\Init\text{-}\KeyGen(1^\lambda) \to I_{\mathsf{CKA}}\in\mathcal{I}_{\mathsf{CKA}}: On input the security parameter 1^\lambda, output an initial key I_{\mathsf{CKA}}\in\mathcal{I}_{\mathsf{CKA}}.

One possible schedule: either party may send repeatedly without waiting for a reply.

\begin{array}{rcccl} & \textsf{Party A} & & \textsf{Party B} & \\ & \boxed{\InitA} & \xleftarrow{\hspace{1.5em}I\hspace{1.5em}}\boxed{\Init\text{-}\KeyGen}\xrightarrow{\hspace{1.5em}I\hspace{1.5em}} & \boxed{\InitB} & \\ & \Big\downarrow\mathrlap{\,\scriptstyle\mathsf{st}} & & \Big\downarrow\mathrlap{\,\scriptstyle\mathsf{st}} & \\ & \boxed{\SendA} & \xrightarrow{\hspace{7em}\rho_1\hspace{7em}} & \boxed{\RecB} & \\ & \Big\downarrow\mathrlap{\,\scriptstyle\mathsf{st}} & & \Big\downarrow\mathrlap{\,\scriptstyle\mathsf{st}} & \\ & \boxed{\SendA} & \xrightarrow{\hspace{7em}\rho_2\hspace{7em}} & \boxed{\RecB} & \\ & \Big\downarrow\mathrlap{\,\scriptstyle\mathsf{st}} & & \Big\downarrow\mathrlap{\,\scriptstyle\mathsf{st}} & \\ & \boxed{\RecA} & \xleftarrow{\hspace{7em}\rho_3\hspace{7em}} & \boxed{\SendB}\mathrlap{\to(t,I_\B)} & \phantom{\to(t,I_\B)} \\ & \Big\downarrow\mathrlap{\,\scriptstyle\mathsf{st}} & & \Big\downarrow\mathrlap{\,\scriptstyle\mathsf{st}} & \\ & \boxed{\RecA} & \xleftarrow{\hspace{7em}\rho_4\hspace{7em}} & \boxed{\SendB} & \\ & \Big\downarrow\mathrlap{\,\scriptstyle\mathsf{st}} & & \Big\downarrow\mathrlap{\,\scriptstyle\mathsf{st}} & \\ \phantom{(t,I_\A)\gets} & \mathllap{(t,I_\A)\gets}\boxed{\RecA} & \xleftarrow{\hspace{7em}\rho_5\hspace{7em}} & \boxed{\SendB} & \\ & & I_\A\overset{?}{=}I_\B & & \end{array}

For each party X\in\{\A,\B\}, let \mathsf{St}_X be its state space and R_X the space of randomness values returned by its leaking-send algorithm. The game is parametrised by

• \mathsf{vuln}^{\mathsf{corr}}_X:\mathsf{St}_X\to\mathcal P_{\mathrm{fin}}(\mathbb N), the epochs exposed by corruption of a state \mathsf{st}\in\mathsf{St}_X;

• \boxed{\mathsf{vuln}^{\mathsf{rleak}}_X:\mathsf{St}_X\times R_X\to\mathcal P_{\mathrm{fin}}(\mathbb N)}, the epochs exposed by leaking the randomness r\in R_X of a send operation from state \mathsf{st}\in\mathsf{St}_X.

Epochs exposed by corruption and randomness leakage

The game state consists of:

• \stA, \stB: local protocol states for parties A and B.

• \mathsf{Key}[\A,t], \mathsf{Key}[\B,t]: keys output by A and B for epoch t, retained in the game after local erasure.

• \mathsf{Msg}[\A,n], \mathsf{Msg}[\B,n]: n-th messages sent by A and B, with their sending epochs.

• n_\A, n_\B: numbers of successful sends by A and B.

• t^\mathsf{cur}_\A, t^\mathsf{cur}_\B: current epochs of A and B.

• \mathsf{Exposed}\subseteq\mathbb{N}: epochs exposed by corruption and randomness leakage oracle calls.

• \mathsf{Challenged}\subseteq\mathbb{N}: epochs t for which \OChall(t) has returned a key.

• \mathsf{correct}: whether all correctness assertions have held.

Protocol states, key and message tables, and exposed and challenged epochs

\begin{array}{l} \pcommentline{\text{Send from A to B}} \\ ((t_{I_\A},I_\A),\rho,t^\mathsf{snd}_\A,\stA') \sample \SendA(\stA); \\ \pcommentline{\text{Correctness: no rollback of current epoch}} \\ \mathsf{assert}\;t^\mathsf{snd}_\A\ge t^\mathsf{cur}_\A; \\ t^\mathsf{cur}_\A\gets t^\mathsf{snd}_\A; \\ \pif\;(t_{I_\A},I_\A)\ne(\bot,\bot)\;\pthen \\ \quad\pcommentline{\text{Correctness: epoch output only once}} \\ \quad\mathsf{assert}\;\mathsf{Key}[\A,t_{I_\A}]=\bot; \\ \quad\pcommentline{\text{Correctness: keys agree when both defined}} \\ \quad\mathsf{assert}\;\mathsf{Key}[\B,t_{I_\A}]\in\{I_\A,\bot\}; \\ \quad\mathsf{Key}[\A,t_{I_\A}]\gets I_\A; \\ \pcommentline{\text{Correctness: keys known through sending epoch}} \\ \mathsf{assert}\;\forall t\in\{1,\ldots,t^\mathsf{snd}_\A\},\; \mathsf{Key}[\A,t]\ne\bot; \\ \pcommentline{\text{Record message for delivery}} \\ \mathsf{Msg}[\A,{+}{+}n_\A]\gets(\rho,t^\mathsf{snd}_\A); \\ \stA\gets\stA'; \\ \Return(t^\mathsf{snd}_\A,t_{I_\A},\rho) \end{array}

A's send oracle and correctness checks

\begin{array}{l} \pcommentline{\text{Send from B to A}} \\ ((t_{I_\B},I_\B),\rho,t^\mathsf{snd}_\B,\stB') \sample \SendB(\stB); \\ \pcommentline{\text{Correctness: no rollback of current epoch}} \\ \mathsf{assert}\;t^\mathsf{snd}_\B\ge t^\mathsf{cur}_\B; \\ t^\mathsf{cur}_\B\gets t^\mathsf{snd}_\B; \\ \pif\;(t_{I_\B},I_\B)\ne(\bot,\bot)\;\pthen \\ \quad\pcommentline{\text{Correctness: epoch output only once}} \\ \quad\mathsf{assert}\;\mathsf{Key}[\B,t_{I_\B}]=\bot; \\ \quad\pcommentline{\text{Correctness: keys agree when both defined}} \\ \quad\mathsf{assert}\;\mathsf{Key}[\A,t_{I_\B}]\in\{I_\B,\bot\}; \\ \quad\mathsf{Key}[\B,t_{I_\B}]\gets I_\B; \\ \pcommentline{\text{Correctness: keys known through sending epoch}} \\ \mathsf{assert}\;\forall t\in\{1,\ldots,t^\mathsf{snd}_\B\},\; \mathsf{Key}[\B,t]\ne\bot; \\ \pcommentline{\text{Record message for delivery}} \\ \mathsf{Msg}[\B,{+}{+}n_\B]\gets(\rho,t^\mathsf{snd}_\B); \\ \stB\gets\stB'; \\ \Return(t^\mathsf{snd}_\B,t_{I_\B},\rho) \end{array}

B's send oracle and correctness checks

\begin{array}{l} \pcommentline{\text{Send from A to B; reveal randomness}} \\ ((t_{I_\A},I_\A),\rho,t^\mathsf{snd}_\A,\stA',r) \sample \SendARLeak(\stA); \\ \pcommentline{\text{Vulnerable epochs following randomness leakage}} \\ \boxed{\mathsf{vuln}\gets\mathsf{vuln}^{\mathsf{rleak}}_\A(\stA,r)}; \\ \pcommentline{\text{Reject exposure of challenged epochs}} \\ \req\;\mathsf{vuln}\cap\mathsf{Challenged}=\emptyset; \\ \mathsf{Exposed}\gets\mathsf{Exposed}\cup\mathsf{vuln}; \\ \pcommentline{\text{Correctness: no rollback of current epoch}} \\ \mathsf{assert}\;t^\mathsf{snd}_\A\ge t^\mathsf{cur}_\A; \\ t^\mathsf{cur}_\A\gets t^\mathsf{snd}_\A; \\ \pif\;(t_{I_\A},I_\A)\ne(\bot,\bot)\;\pthen \\ \quad\pcommentline{\text{Correctness: epoch output only once}} \\ \quad\mathsf{assert}\;\mathsf{Key}[\A,t_{I_\A}]=\bot; \\ \quad\pcommentline{\text{Correctness: keys agree when both defined}} \\ \quad\mathsf{assert}\;\mathsf{Key}[\B,t_{I_\A}]\in\{I_\A,\bot\}; \\ \quad\mathsf{Key}[\A,t_{I_\A}]\gets I_\A; \\ \pcommentline{\text{Correctness: keys known through sending epoch}} \\ \mathsf{assert}\;\forall t\in\{1,\ldots,t^\mathsf{snd}_\A\},\; \mathsf{Key}[\A,t]\ne\bot; \\ \pcommentline{\text{Record message for delivery}} \\ \mathsf{Msg}[\A,{+}{+}n_\A]\gets(\rho,t^\mathsf{snd}_\A); \\ \stA\gets\stA'; \\ \Return(t^\mathsf{snd}_\A,t_{I_\A},\rho,r) \end{array}

A's leaking-send oracle and exposure guard

\begin{array}{l} \pcommentline{\text{Send from B to A; reveal randomness}} \\ ((t_{I_\B},I_\B),\rho,t^\mathsf{snd}_\B,\stB',r) \sample \SendBRLeak(\stB); \\ \pcommentline{\text{Vulnerable epochs following randomness leakage}} \\ \boxed{\mathsf{vuln}\gets\mathsf{vuln}^{\mathsf{rleak}}_\B(\stB,r)}; \\ \pcommentline{\text{Reject exposure of challenged epochs}} \\ \req\;\mathsf{vuln}\cap\mathsf{Challenged}=\emptyset; \\ \mathsf{Exposed}\gets\mathsf{Exposed}\cup\mathsf{vuln}; \\ \pcommentline{\text{Correctness: no rollback of current epoch}} \\ \mathsf{assert}\;t^\mathsf{snd}_\B\ge t^\mathsf{cur}_\B; \\ t^\mathsf{cur}_\B\gets t^\mathsf{snd}_\B; \\ \pif\;(t_{I_\B},I_\B)\ne(\bot,\bot)\;\pthen \\ \quad\pcommentline{\text{Correctness: epoch output only once}} \\ \quad\mathsf{assert}\;\mathsf{Key}[\B,t_{I_\B}]=\bot; \\ \quad\pcommentline{\text{Correctness: keys agree when both defined}} \\ \quad\mathsf{assert}\;\mathsf{Key}[\A,t_{I_\B}]\in\{I_\B,\bot\}; \\ \quad\mathsf{Key}[\B,t_{I_\B}]\gets I_\B; \\ \pcommentline{\text{Correctness: keys known through sending epoch}} \\ \mathsf{assert}\;\forall t\in\{1,\ldots,t^\mathsf{snd}_\B\},\; \mathsf{Key}[\B,t]\ne\bot; \\ \pcommentline{\text{Record message for delivery}} \\ \mathsf{Msg}[\B,{+}{+}n_\B]\gets(\rho,t^\mathsf{snd}_\B); \\ \stB\gets\stB'; \\ \Return(t^\mathsf{snd}_\B,t_{I_\B},\rho,r) \end{array}

B's leaking-send oracle and exposure guard

\begin{array}{l} \pcommentline{\text{Deliver B's message n to A}} \\ \req\;\mathsf{Msg}[\B,n]\ne\bot; \\ (\rho,t^\mathsf{snd}_\B)\gets\mathsf{Msg}[\B,n]; \\ r\getsval\RecA(\stA,\rho); \\ \pcommentline{\text{Correctness: honest delivery succeeds}} \\ \pif\;r=\bot\;\pthen\; \mathsf{correct}\gets\mathsf{false};\;\Return\bot; \\ ((t_{I_\B},I_\B),t^\mathsf{rcv}_\A,\stA')\gets r; \\ \pcommentline{\text{Correctness: receive epoch matches sender}} \\ \mathsf{assert}\;t^\mathsf{rcv}_\A=t^\mathsf{snd}_\B; \\ t^\mathsf{cur}_\A\gets \max(t^\mathsf{cur}_\A,t^\mathsf{rcv}_\A); \\ \pif\;(t_{I_\B},I_\B)\ne(\bot,\bot)\;\pthen \\ \quad\pcommentline{\text{Correctness: epoch output only once}} \\ \quad\mathsf{assert}\;\mathsf{Key}[\A,t_{I_\B}]=\bot; \\ \quad\pcommentline{\text{Correctness: keys agree when both defined}} \\ \quad\mathsf{assert}\;\mathsf{Key}[\B,t_{I_\B}]\in\{I_\B,\bot\}; \\ \quad\mathsf{Key}[\A,t_{I_\B}]\gets I_\B; \\ \pcommentline{\text{Correctness: keys known through current epoch}} \\ \mathsf{assert}\;\forall t\in\{1,\ldots,t^\mathsf{cur}_\A\},\; \mathsf{Key}[\A,t]\ne\bot; \\ \stA\gets\stA'; \\ \Return(t^\mathsf{rcv}_\A,t_{I_\B}) \end{array}

Delivery of a recorded message to A

\begin{array}{l} \pcommentline{\text{Deliver A's message n to B}} \\ \req\;\mathsf{Msg}[\A,n]\ne\bot; \\ (\rho,t^\mathsf{snd}_\A)\gets\mathsf{Msg}[\A,n]; \\ r\getsval\RecB(\stB,\rho); \\ \pcommentline{\text{Correctness: honest delivery succeeds}} \\ \pif\;r=\bot\;\pthen\; \mathsf{correct}\gets\mathsf{false};\;\Return\bot; \\ ((t_{I_\A},I_\A),t^\mathsf{rcv}_\B,\stB')\gets r; \\ \pcommentline{\text{Correctness: receive epoch matches sender}} \\ \mathsf{assert}\;t^\mathsf{rcv}_\B=t^\mathsf{snd}_\A; \\ t^\mathsf{cur}_\B\gets \max(t^\mathsf{cur}_\B,t^\mathsf{rcv}_\B); \\ \pif\;(t_{I_\A},I_\A)\ne(\bot,\bot)\;\pthen \\ \quad\pcommentline{\text{Correctness: epoch output only once}} \\ \quad\mathsf{assert}\;\mathsf{Key}[\B,t_{I_\A}]=\bot; \\ \quad\pcommentline{\text{Correctness: keys agree when both defined}} \\ \quad\mathsf{assert}\;\mathsf{Key}[\A,t_{I_\A}]\in\{I_\A,\bot\}; \\ \quad\mathsf{Key}[\B,t_{I_\A}]\gets I_\A; \\ \pcommentline{\text{Correctness: keys known through current epoch}} \\ \mathsf{assert}\;\forall t\in\{1,\ldots,t^\mathsf{cur}_\B\},\; \mathsf{Key}[\B,t]\ne\bot; \\ \stB\gets\stB'; \\ \Return(t^\mathsf{rcv}_\B,t_{I_\A}) \end{array}

Delivery of a recorded message to B

\begin{array}{l} \pcommentline{\text{Return a real or random epoch key}} \\ \pcommentline{\text{Reject exposed or previously challenged epochs}} \\ \req\;t\notin\mathsf{Exposed}\cup\mathsf{Challenged}; \\ \pcommentline{\text{Use either party's derived key}} \\ \pif\;\mathsf{Key}[\A,t]\ne\bot\;\pthen \\ \quad K\gets\mathsf{Key}[\A,t]; \\ \pelse \\ \quad K\gets\mathsf{Key}[\B,t]; \\ \pcommentline{\text{A party must have derived the key}} \\ \req\;K\ne\bot; \\ \pcommentline{\text{Replace the key in the random case}} \\ \pif\;b=1\;\pthen\;K\sample I; \\ \pcommentline{\text{Record this epoch to prevent another challenge}} \\ \mathsf{Challenged}\gets\mathsf{Challenged}\cup\{t\}; \\ \Return K \end{array}

Real or random key challenge for an unexposed epoch

\begin{array}{l} \pcommentline{\text{Vulnerable epochs following corruption of A}} \\ \mathsf{vuln}\gets\mathsf{vuln}^{\mathsf{corr}}_\A(\stA); \\ \pcommentline{\text{Reject exposure of challenged epochs}} \\ \req\;\mathsf{vuln}\cap\mathsf{Challenged}=\emptyset; \\ \pcommentline{\text{Record exposed epochs}} \\ \mathsf{Exposed}\gets\mathsf{Exposed}\cup\mathsf{vuln}; \\ \Return\stA \end{array}

A's state-corruption oracle and exposure guard

\begin{array}{l} \pcommentline{\text{Vulnerable epochs following corruption of B}} \\ \mathsf{vuln}\gets\mathsf{vuln}^{\mathsf{corr}}_\B(\stB); \\ \pcommentline{\text{Reject exposure of challenged epochs}} \\ \req\;\mathsf{vuln}\cap\mathsf{Challenged}=\emptyset; \\ \pcommentline{\text{Record exposed epochs}} \\ \mathsf{Exposed}\gets\mathsf{Exposed}\cup\mathsf{vuln}; \\ \Return\stB \end{array}

B's state-corruption oracle and exposure guard

\Ocor=\{\mathsf{O\text{-}Unif},\OSendA,\OSendB, \ORecA(n),\ORecB(n)\}

\begin{array}{ll} \mathsf{O\text{-}Unif} & \text{Sample uniform randomness.} \\ \OSendA & \text{Trigger A to send a message to B.} \\ \OSendB & \text{Trigger B to send a message to A.} \\ \ORecA(n) & \text{Deliver B's recorded message }n\text{ to A.} \\ \ORecB(n) & \text{Deliver A's recorded message }n\text{ to B.} \end{array}

Correctness oracle interface

Correctness oracle implementation

Correctness adversary

\Osec=\Ocor\cup \{\OSendARLeak,\OSendBRLeak,\OChall(t),\OCorrA,\OCorrB\}

In addition to \Ocor:

\begin{array}{ll} \OSendARLeak & \text{Trigger A to send and reveal the randomness used.} \\ \OSendBRLeak & \text{Trigger B to send and reveal the randomness used.} \\ \OChall(t) & \text{Real or random key challenge for epoch }t\text{.} \\ \OCorrA & \text{Reveal A's current local state.} \\ \OCorrB & \text{Reveal B's current local state.} \end{array}

Security oracle interface

Security oracle implementation

Security adversary