cronokirby

Cait-Sith Security (1): Echo Broadcast

One sub-component used a couple of times is a combined broadcast commitment functionality, implemented via echo broadcast.

In a nutshell, the idea behind echo broadcast is to ensure that a party sends the same message to all others. We accomplish this by sending a hash of all the messages we've received to everyone else, thus enabling us to realize if a different message was sent in the first round.

Definition (Echo Broadcast Protocol): The broadcast protocol P[EchoBroadcast]\mathscr{P}[\text{EchoBroadcast}] is defined as follows:

P[EchoBroadcast] Pi (1)StartBroadcasti(x):‾↱i(⋆,x,0)WaitBroadcasti(x):‾x^_∙↰i(⋆,0)coni←Hash(x^_∙)↱i(⋆,coni,1)return x_∙EndBroadcasti():‾con^_∙↰i(⋆,1)if ∃j.con^j≠coni:stop(⋆,1)F[SyncComm]⊗F[Hash]Leakage:={Hash,stop}\boxed{ \begin{matrix} \colorbox{FBCFE8}{\large $\mathscr{P}[\text{EchoBroadcast}]$ }\cr \cr \boxed{ \small{ \begin{aligned} &\colorbox{FBCFE8}{\large $P_i$ }\cr \cr &\underline{ (1)\text{StartBroadcast}_i(x): }\cr &\enspace \Rsh_i(\star, x, 0) \cr \cr &\underline{ \text{WaitBroadcast}_i(x): }\cr &\enspace \hat{x}\_\bullet \Lsh_i(\star, 0) \cr &\enspace \text{con}_i \gets \text{Hash}(\hat{x}\_\bullet) \cr &\enspace \Rsh_i(\star, \text{con}_i, 1) \cr &\enspace \texttt{return } x\_{\bullet} \cr \cr &\underline{ \text{EndBroadcast}_i(): }\cr &\enspace \hat{\text{con}}\_\bullet \Lsh_i(\star, 1) \cr &\enspace \texttt{if } \exists j.\enspace \hat{\text{con}}_j \neq \text{con}_i: \cr &\enspace\enspace \texttt{stop}(\star, 1) \cr \end{aligned} } } \quad \begin{matrix} F[\text{SyncComm}]\cr \otimes\cr F[\text{Hash}]\cr \end{matrix}\cr \cr \text{Leakage} := \{\text{Hash}, \texttt{stop}\} \end{matrix} }

□\square

We model this hash function as a random oracle here.

The functionality that this implements is basically what you'd expect. The parties have to set their broadcast value, and then the functionality forces them to send it to all others. However, there is a sort of catch, in that adversaries can set a "trap" value, which will cause an abort later if the wrong broadcast value is set after the trap. This reflects the fact that adversaries can send their confirmation message early, thus potentially causing an abort later.

In practice this won't matter for our purpose of using broadcasts for commitments, because the commitment values will be random, and thus not trappable.

Definition (Ideal Broadcast Protocol):

The protocol capturing the ideal behavior of broadcast is defined as follows:

P[IdealBroadcast] Pi (1)StartBroadcasti(x):‾SetBroadcasti(x)SendBroadcasti(⋆)WaitBroadcasti():‾x_∙←GetBroadcasti(⋆)Synci(⋆)return x_∙EndBroadcasti():‾WaitSynci(⋆)if BadBroadcasti():stop(⋆,1)F[Broadcast] xi,sent_ij,trap_ij←⊥(1)SetBroadcasti(x):‾xi←xSendBroadcasti(S):‾assert xi≠⊥sent_ij←true (∀j∈S)GetBroadcasti(S):‾wait_(i,0) sent_ji (∀j∈S)return [xj∣j∈S]Trap(j,m_∙):‾assert ∀i. mi=⊥∨(trap_ij=⊥∧xi=⊥)trap_ij←miBadBroadcasti():‾return ∃j. trap_ji≠⊥∧trap_ji≠x_j⊗F[Sync(1)]⊗F[Stop]Leakage:={Trap,stop}\boxed{ \begin{matrix} \colorbox{FBCFE8}{\large $\mathscr{P}[\text{IdealBroadcast}]$ }\cr \cr \boxed{ \small{ \begin{aligned} &\colorbox{FBCFE8}{\large $P_i$ }\cr \cr &\underline{ (1)\text{StartBroadcast}_i(x): }\cr &\enspace \text{SetBroadcast}_i(x) \cr &\enspace \text{SendBroadcast}_i(\star) \cr \cr &\underline{ \text{WaitBroadcast}_i(): }\cr &\enspace x\_{\bullet} \gets \text{GetBroadcast}_i(\star) \cr &\enspace \text{Sync}_i(\star) \cr &\enspace \texttt{return } x\_{\bullet} \cr \cr &\underline{ \text{EndBroadcast}_i(): }\cr &\enspace \text{WaitSync}_i(\star) \cr &\enspace \texttt{if } \text{BadBroadcast}_i(): \cr &\enspace\enspace \texttt{stop}(\star, 1) \cr \end{aligned} } } \quad \begin{matrix} \boxed{ \small{ \begin{aligned} &\colorbox{FBCFE8}{\large $F[\text{Broadcast}]$ }\cr \cr &x_i, \text{sent}\_{ij}, \text{trap}\_{ij} \gets \bot\cr \cr &\underline{ (1)\text{SetBroadcast}_i(x): }\cr &\enspace x_i \gets x \cr \cr &\underline{ \text{SendBroadcast}_i(S): }\cr &\enspace \texttt{assert } x_i \neq \bot \cr &\enspace \text{sent}\_{ij} \gets \texttt{true}\ (\forall j \in S) \cr \cr &\underline{ \text{GetBroadcast}_i(S): }\cr &\enspace \texttt{wait}\_{(i, 0)}\ \text{sent}\_{ji}\ (\forall j \in S) \cr &\enspace \texttt{return } [x_j \mid j \in S] \cr \cr &\underline{ \textcolor{ef4444}{\text{Trap}(j, m\_\bullet)}: }\cr &\enspace \texttt{assert } \forall i.\ m_i = \bot \lor (\text{trap}\_{i j} = \bot \land x_i = \bot) \cr &\enspace \text{trap}\_{i j} \gets m_i \cr \cr &\underline{ \text{BadBroadcast}_i(): }\cr &\enspace \texttt{return } \exists j.\ \text{trap}\_{j i} \neq \bot \land \text{trap}\_{j i} \neq x\_j \cr \end{aligned} } }\cr \otimes\cr F[\text{Sync}(1)]\cr \otimes\cr F[\text{Stop}]\cr \end{matrix}\cr \cr \text{Leakage} := \{\text{Trap}, \texttt{stop}\} \end{matrix} }

□\square

Another little detail is that the ideal functionality reflects the fact that the original broadcast had two rounds, via the synchronization mechanism.

Lemma:

For a negligible ϵ\epsilon, and any combination of malicious parties:

P[EchoBroadcast]⇝ϵP[IdealBroadcast]\mathscr{P}[\text{EchoBroadcast}] \overset{\epsilon}{\leadsto} \mathscr{P}[\text{IdealBroadcast}]

Proof:

As per usual, we unroll Inst(P[EchoBroadcast])\text{Inst}(\mathscr{P}[\text{EchoBroadcast}]), to get:

ΓH0 (1)StartBroadcasti(x):‾…⊗ΓM0 =1(↱k,↰k,Hash)∘F[SyncComm]⊗F[Hash]\begin{matrix} \boxed{ \small{ \begin{aligned} &\colorbox{FBCFE8}{\large $\Gamma^0_H$ }\cr \cr &\underline{ (1)\text{StartBroadcast}_i(x): }\cr &\enspace \ldots \cr \end{aligned} } } \otimes \boxed{\colorbox{FBCFE8}{\large $\Gamma^0_M$ } = 1 \begin{pmatrix} \Rsh_k ,\cr \Lsh_k ,\cr \text{Hash} \end{pmatrix} } \cr \circ \cr F[\text{SyncComm}] \otimes F[\text{Hash}] \end{matrix}

having split the game into an honest part, and a malicious part, long with the ideal functionalities. The malicious part will slowly become our simulator.

Our next step will be to modify the honest part to send both the hash of their messages, and an entire vector confirmation. The malicious part will ignore this new information, giving us an identical game.

ΓH1 …WaitBroadcasti():‾x^_∙↰i(⋆,0)hi←Hash(x^_∙)↱i(⋆,(hi,x^_∙),1)EndBroadcasti():‾(h^_∙,x⃗_∙)↰i(⋆,1)if ∃j.h^j≠hi:stop(⋆,1)⊗ΓM1 ↱k(S,h_∙,1):‾↱k(S,(h_∙,⊥),1)↰k(S,1):‾(h^_∙,…)↰k(S,1)return [h^j∣j∈S]⊗1(↱k,↰k,Hash)∘F[SyncComm]⊗F[Hash]\begin{matrix} \boxed{ \small{ \begin{aligned} &\colorbox{FBCFE8}{\large $\Gamma^1_H$ }\cr &\ldots\cr \cr &\underline{ \text{WaitBroadcast}_i(): }\cr &\enspace \hat{x}\_\bullet \Lsh_i(\star, 0) \cr &\enspace h_i \gets \text{Hash}(\hat{x}\_\bullet) \cr &\enspace \colorbox{bae6fd}{$ \Rsh_i(\star, (h_i, \hat{x}\_\bullet), 1) $} \cr \cr &\underline{ \text{EndBroadcast}_i(): }\cr &\enspace \colorbox{bae6fd}{$ (\hat{h}\_\bullet, \vec{x}\_\bullet) \Lsh_i(\star, 1) $} \cr &\enspace \texttt{if } \exists j.\enspace \hat{h}_j \neq h_i: \cr &\enspace\enspace \texttt{stop}(\star, 1) \cr \end{aligned} } } \otimes \begin{matrix} \boxed{ \small{ \begin{aligned} &\colorbox{bae6fd}{\large $\Gamma^1_M$ }\cr \cr &\underline{ \Rsh_k(S, h\_\bullet, 1): }\cr &\enspace \Rsh_k(S, (h\_\bullet, \bot), 1) \cr \cr &\underline{ \Lsh_k(S, 1): }\cr &\enspace (\hat{h}\_\bullet, \ldots)\Lsh_k(S, 1) \cr &\enspace \texttt{return } [\hat{h}_j \mid j \in S] \cr \end{aligned} } } \cr \otimes \cr 1(\Rsh_k, \Lsh_k, \text{Hash}) \end{matrix} \cr \circ \cr F[\text{SyncComm}] \otimes F[\text{Hash}] \end{matrix}

Now, we can have the honest parties omit their hash completely, only sending the vector. This requires moving some of the hashing logic into the malicious part, and the verification check at the end, but otherwise gives us an identical game.

ΓH2 …WaitBroadcasti():‾↱i(⋆,x,0)x^_∙↰i(⋆,0)↱i(⋆,(⊥,x^_∙),1)EndBroadcasti():‾(h^_∙,x⃗_∙)↰i(⋆,1)if ∃j.(h^j≠⊥∧h^j≠Hash(x⃗i)) ∨(x⃗j≠⊥∧Hash(x⃗j)≠Hash(x⃗i)):stop(⋆,1)⊗ΓM2 ↱k(S,h_∙,1):‾↱k(S,(h_∙,⊥),1)↰k(S,1):‾(h^_∙,x⃗_∙)↰k(S,1)if h^j=⊥:assert x⃗j≠⊥h^j←Hash(x⃗j)return [h^j∣j∈S]⊗1(↱k,↰k,Hash)∘F[SyncComm]⊗F[Hash]\begin{matrix} \boxed{ \small{ \begin{aligned} &\colorbox{FBCFE8}{\large $\Gamma^2_H$ }\cr &\ldots\cr \cr &\underline{ \text{WaitBroadcast}_i(): }\cr &\enspace \Rsh_i(\star, x, 0) \cr &\enspace \hat{x}\_\bullet \Lsh_i(\star, 0) \cr &\enspace \colorbox{bae6fd}{$ \Rsh_i(\star, (\bot, \hat{x}\_\bullet), 1) $} \cr \cr &\underline{ \text{EndBroadcast}_i(): }\cr &\enspace (\hat{h}\_\bullet, \vec{x}\_\bullet) \Lsh_i(\star, 1) \cr &\enspace \colorbox{bae6fd}{$ \texttt{if } \exists j.\enspace \begin{matrix} (\hat{h}_j \neq \bot \land \hat{h}_j \neq \text{Hash}(\vec{x}_i))\ \lor\cr (\vec{x}_j \neq \bot \land \text{Hash}(\vec{x}_j) \neq \text{Hash}(\vec{x}_i)) \end{matrix} : $} \cr &\enspace\enspace \texttt{stop}(\star, 1) \cr \end{aligned} } } \otimes \begin{matrix} \boxed{ \small{ \begin{aligned} &\colorbox{FBCFE8}{\large $\Gamma^2_M$ }\cr \cr &\underline{ \Rsh_k(S, h\_\bullet, 1): }\cr &\enspace \Rsh_k(S, (h\_\bullet, \bot), 1) \cr \cr &\colorbox{bae6fd}{$\underline{ \Lsh_k(S, 1): }$}\cr &\enspace (\hat{h}\_\bullet, \vec{x}\_\bullet)\Lsh_k(S, 1) \cr &\enspace \texttt{if } \hat{h}_j = \bot: \cr &\enspace\enspace \texttt{assert } \vec{x}_j \neq \bot \cr &\enspace\enspace \hat{h}_j \gets \text{Hash}(\vec{x}_j) \cr &\enspace \texttt{return } [\hat{h}_j \mid j \in S] \cr \end{aligned} } } \cr \otimes \cr 1(\Rsh_k, \Lsh_k, \text{Hash}) \end{matrix} \cr \circ \cr F[\text{SyncComm}] \otimes F[\text{Hash}] \end{matrix}

Because we're using a random oracle. Nowe, we can extract preimages by snopping on the hash queries made by the adversary, and send those instead.

ΓH3 …WaitBroadcasti():‾x^_∙↰i(⋆,0)↱i(⋆,(⊥,x^_∙),1)EndBroadcasti():‾(h^_∙,x⃗_∙)↰i(⋆,1)if ∃j.(h^j≠⊥∧h^j≠Hash(x⃗i)) ∨(x⃗j≠⊥∧Hash(x⃗j)≠Hash(x⃗i)):stop(⋆,1)⊗ΓM3 μ[…]←⊥Hash(x_∙):‾h←Hash(x_∙)μ[h]←x_∙return hh_ij←⊥↱k(S,h_∙,1):‾assert ∀j∈S. hj≠⊥for j∈S∩M:h_kj←hjfor j∈S∩H:if μ[hj]≠⊥:↱k({j},(⊥,μ[hj]),1)else:↱k({j},(hj,⊥),1)↰k(S,1):‾(…,x⃗_∙)↰k(S∩H,1)wait_(k,1) ∀j∈S∩M. h_jk≠⊥return [Hash(x⃗_j)∣j∈S∩Hh_jk∣j∈S∩M]⊗1(↱k,↰k,Hash)∘F[SyncComm]⊗F[Hash]\begin{matrix} \boxed{ \small{ \begin{aligned} &\colorbox{FBCFE8}{\large $\Gamma^3_H$ }\cr &\ldots\cr \cr &\colorbox{bae6fd}{$\underline{ \text{WaitBroadcast}_i(): }$}\cr &\enspace \hat{x}\_\bullet \Lsh_i(\star, 0) \cr &\enspace \Rsh_i(\star, (\bot, \hat{x}\_\bullet), 1) \cr \cr &\colorbox{bae6fd}{$\underline{ \text{EndBroadcast}_i(): }$}\cr &\enspace (\hat{h}\_\bullet, \vec{x}\_\bullet) \Lsh_i(\star, 1) \cr &\enspace \texttt{if } \exists j.\enspace \begin{matrix} (\hat{h}_j \neq \bot \land \hat{h}_j \neq \text{Hash}(\vec{x}_i))\ \lor\cr (\vec{x}_j \neq \bot \land \text{Hash}(\vec{x}_j) \neq \text{Hash}(\vec{x}_i)) \end{matrix} : \cr &\enspace\enspace \texttt{stop}(\star, 1) \cr \end{aligned} } } \otimes \begin{matrix} \boxed{ \small{ \begin{aligned} &\colorbox{bae6fd}{\large $\Gamma^3_M$ }\cr \cr &\mu[\ldots] \gets \bot\cr &\underline{ \text{Hash}(x\_\bullet): }\cr &\enspace h \gets \text{Hash}(x\_\bullet) \cr &\enspace \mu[h] \gets x\_\bullet \cr &\enspace \texttt{return } h \cr \cr &h\_{ij} \gets \bot\cr &\underline{ \Rsh_k(S, h\_\bullet, 1): }\cr &\enspace \texttt{assert } \forall j \in S.\ h_j \neq \bot \cr &\enspace \texttt{for } j \in S \cap \mathcal{M}: \cr &\enspace\enspace h\_{kj} \gets h_j \cr &\enspace \texttt{for } j \in S \cap \mathcal{H}: \cr &\enspace\enspace \texttt{if } \mu[h_j] \neq \bot: \cr &\enspace\enspace\enspace \Rsh_k(\{j\}, (\bot, \mu[h_j]), 1) \cr &\enspace\enspace \texttt{else}: \cr &\enspace\enspace\enspace \Rsh_k(\{j\}, (h_j, \bot), 1) \cr & \cr &\underline{ \Lsh_k(S, 1): }\cr &\enspace (\ldots, \vec{x}\_\bullet)\Lsh_k(S \cap \mathcal{H}, 1) \cr &\enspace \texttt{wait}\_{(k, 1)}\ \forall j \in S \cap \mathcal{M}.\ h\_{jk} \neq \bot \cr &\enspace \texttt{return }\begin{bmatrix} \text{Hash}(\vec{x}\_j) &\mid& j \in S \cap \mathcal{H}\cr h\_{jk} &\mid& j \in S \cap \mathcal{M}\cr \end{bmatrix} \cr \cr \end{aligned} } } \cr \otimes \cr 1(\Rsh_k, \Lsh_k, \text{Hash}) \end{matrix} \cr \circ \cr F[\text{SyncComm}] \otimes F[\text{Hash}] \end{matrix}

Now, except with negligible probability, a hash with no pre-image will cause the final verification check made by honest parties to fail, so we can instead cause an abort when the adversary tries to send such a hash, allowing us to always extract a pre-image, or to abort:

ΓH4 …WaitBroadcasti():‾x^_∙↰i(⋆,0)↱i(⋆,x^_∙,1)EndBroadcasti():‾x⃗_∙↰i(⋆,1)if ∃j.Hash(x⃗j)≠Hash(x⃗i):stop(⋆,1)⊗ΓM4 …↱k(S,h_∙,1):‾…for j∈S∩H:if μ[hj]≠⊥:↱k({j},μ[hj],1)else:stop(⋆,1)↰k(S,1):‾x⃗_∙↰k(S∩H,1)…⊗1(↱k,↰k,Hash)∘F[SyncComm]⊗F[Hash]\begin{matrix} \boxed{ \small{ \begin{aligned} &\colorbox{FBCFE8}{\large $\Gamma^4_H$ }\cr &\ldots\cr \cr &\underline{ \text{WaitBroadcast}_i(): }\cr &\enspace \hat{x}\_\bullet \Lsh_i(\star, 0) \cr &\enspace \colorbox{bae6fd}{$ \Rsh_i(\star, \hat{x}\_\bullet, 1) $} \cr \cr &\underline{ \text{EndBroadcast}_i(): }\cr &\enspace \colorbox{bae6fd}{$ \vec{x}\_\bullet \Lsh_i(\star, 1) $} \cr &\enspace \colorbox{bae6fd}{$ \texttt{if } \exists j.\enspace \text{Hash}(\vec{x}_j) \neq \text{Hash}(\vec{x}_i) : $} \cr &\enspace\enspace \texttt{stop}(\star, 1) \cr \end{aligned} } } \otimes \begin{matrix} \boxed{ \small{ \begin{aligned} &\colorbox{FBCFE8}{\large $\Gamma^4_M$ }\cr \cr &\ldots\cr \cr &\underline{ \Rsh_k(S, h\_\bullet, 1): }\cr &\enspace \ldots \cr &\enspace \texttt{for } j \in S \cap \mathcal{H}: \cr &\enspace\enspace \texttt{if } \mu[h_j] \neq \bot: \cr &\enspace\enspace\enspace \colorbox{bae6fd}{$ \Rsh_k(\{j\}, \mu[h_j], 1) $} \cr &\enspace\enspace \texttt{else}: \cr &\enspace\enspace\enspace \colorbox{bae6fd}{$ \texttt{stop}(\star, 1) $} \cr & \cr &\underline{ \Lsh_k(S, 1): }\cr &\enspace \colorbox{bae6fd}{$ \vec{x}\_\bullet\Lsh_k(S \cap \mathcal{H}, 1) $} \cr &\enspace \ldots \cr \cr \end{aligned} } } \cr \otimes \cr 1(\Rsh_k, \Lsh_k, \text{Hash}) \end{matrix} \cr \circ \cr F[\text{SyncComm}] \otimes F[\text{Hash}] \end{matrix}

At this point, we've actually written a simulator for a protocol P0\mathscr{P}^0, which is like our initial protocol, except that the parties send their entire vector, rather than their hash. This shows that P[EchoBroadcast]⇝P0\mathscr{P}[\text{EchoBroadcast}] \leadsto \mathscr{P}^0.

We can unroll Inst(P0)\text{Inst}(\mathscr{P}^0) to get:

ΓH5 …WaitBroadcasti():‾↱i(⋆,x,0)x^_∙↰i(⋆,0)↱i(⋆,x^_∙,1)EndBroadcasti():‾x⃗_∙↰i(⋆,1)if ∃j.Hash(x⃗j)≠Hash(x⃗i):stop(⋆,1)⊗ΓM5 =1(↱k,↰k,Hash)∘F[SyncComm]⊗F[Hash]\begin{matrix} \boxed{ \small{ \begin{aligned} &\colorbox{FBCFE8}{\large $\Gamma^5_H$ }\cr &\ldots\cr \cr &\underline{ \text{WaitBroadcast}_i(): }\cr &\enspace \Rsh_i(\star, x, 0) \cr &\enspace \hat{x}\_\bullet \Lsh_i(\star, 0) \cr &\enspace \Rsh_i(\star, \hat{x}\_\bullet, 1) \cr \cr &\underline{ \text{EndBroadcast}_i(): }\cr &\enspace \vec{x}\_\bullet \Lsh_i(\star, 1) \cr &\enspace \texttt{if } \exists j.\enspace \text{Hash}(\vec{x}_j) \neq \text{Hash}(\vec{x}_i) : \cr &\enspace\enspace \texttt{stop}(\star, 1) \cr \end{aligned} } } \otimes \boxed{\colorbox{FBCFE8}{\large $\Gamma^5_M$ } = 1 \begin{pmatrix} \Rsh_k ,\cr \Lsh_k ,\cr \text{Hash} \end{pmatrix} } \cr \circ \cr F[\text{SyncComm}] \otimes F[\text{Hash}] \end{matrix}

Except with negligible probability, the hashes won't collide, so we can replace the hash based check with an actual check of equality.

ΓH6 …EndBroadcasti():‾…if ∃j.x⃗j≠x⃗i:stop(⋆,1)⊗ΓM6 =ΓM5∘F[SyncComm]⊗F[Hash]\begin{matrix} \boxed{ \small{ \begin{aligned} &\colorbox{FBCFE8}{\large $\Gamma^6_H$ }\cr &\ldots\cr &\underline{ \text{EndBroadcast}_i(): }\cr &\enspace \ldots \cr &\enspace \colorbox{bae6fd}{$ \texttt{if } \exists j.\enspace \vec{x}_j \neq \vec{x}_i : $} \cr &\enspace\enspace \texttt{stop}(\star, 1) \cr \end{aligned} } } \otimes \boxed{\colorbox{FBCFE8}{\large $\Gamma^6_M$ } = \Gamma^5_M} \cr \circ \cr F[\text{SyncComm}] \otimes F[\text{Hash}] \end{matrix}

Now, we employ a classic trick, and are trying to get rid of F[SyncComm]F[\text{SyncComm}]. Our strategy to do this will be to inline all of the variables in a common mutable functionality:

ΓH7 (1)StartBroadcasti(x):‾x^_ij←xWaitBroadcasti():‾wait_(i,0) ∀j. x^_ji≠⊥x⃗_ij←x^_∙isync_ij←trueEndBroadcasti():‾wait_(i,1) ∀j. sync_ji≠⊥if ∃j.x⃗_ji≠x^_∙i:stop(⋆,1)⊗ΓM7 ↱k(S,m_∙,0):‾assert ∀j∈S. mj≠⊥∧x^_kj=⊥x^_kj←mj (∀j∈S)↱k(S,m_∙,1):‾assert ∀j∈S. mj≠⊥∧x⃗_kj=⊥x⃗_kj←mj (∀j∈S)sync_kj←true (∀j∈S)↰k(S,0):‾wait_(k,0) ∀j∈S. x^_jk≠⊥return [x^_jk∣j∈S]↰k(S,1):‾wait_(k,1) ∀j∈S. sync_jk≠⊥return [x⃗_jk∣j∈S]⊗F[SyncComm]⊗F[Hash]∘pub x^_ij,x⃗_ij,sync_ij←⊥⊗F[Stop]\begin{matrix} \boxed{ \small{ \begin{aligned} &\colorbox{bae6fd}{\large $\Gamma^7_H$ }\cr \cr &\underline{ (1)\text{StartBroadcast}_i(x): }\cr &\enspace \hat{x}\_{ij} \gets x \cr \cr &\underline{ \text{WaitBroadcast}_i(): }\cr &\enspace \texttt{wait}\_{(i, 0)}\ \forall j.\ \hat{x}\_{ji} \neq \bot \cr &\enspace \vec{x}\_{ij} \gets \hat{x}\_{\bullet i} \cr &\enspace \text{sync}\_{ij} \gets \texttt{true} \cr \cr &\underline{ \text{EndBroadcast}_i(): }\cr &\enspace \texttt{wait}\_{(i, 1)}\ \forall j.\ \text{sync}\_{ji} \neq \bot \cr &\enspace \texttt{if } \exists j.\enspace \vec{x}\_{ji} \neq \hat{x}\_{\bullet i} : \cr &\enspace\enspace \texttt{stop}(\star, 1) \cr \end{aligned} } } \otimes \begin{matrix} \boxed{ \small{ \begin{aligned} &\colorbox{bae6fd}{\large $\Gamma^7_M$ }\cr \cr &\underline{ \Rsh_k(S, m\_\bullet, 0): }\cr &\enspace \texttt{assert } \forall j \in S.\ m_j \neq \bot \land \hat{x}\_{kj} = \bot \cr &\enspace \hat{x}\_{kj} \gets m_j\ (\forall j \in S) \cr \cr &\underline{ \Rsh_k(S, m\_\bullet, 1): }\cr &\enspace \texttt{assert } \forall j \in S.\ m_j \neq \bot \land \vec{x}\_{kj} = \bot \cr &\enspace \vec{x}\_{kj} \gets m_j\ (\forall j \in S) \cr &\enspace \text{sync}\_{kj} \gets \texttt{true}\ (\forall j \in S) \cr \cr &\underline{ \Lsh_k(S, 0): }\cr &\enspace \texttt{wait}\_{(k, 0)}\ \forall j \in S.\ \hat{x}\_{jk} \neq \bot \cr &\enspace \texttt{return } [\hat{x}\_{j k} \mid j \in S] \cr \cr &\underline{ \Lsh_k(S, 1): }\cr &\enspace \texttt{wait}\_{(k, 1)}\ \forall j \in S.\ \text{sync}\_{jk} \neq \bot \cr &\enspace \texttt{return } [\vec{x}\_{jk} \mid j \in S] \cr \end{aligned} } } \cr \otimes \cr F[\text{SyncComm}] \otimes F[\text{Hash}] \end{matrix} \cr \circ \cr \boxed{ \small{ \begin{aligned} \texttt{pub } \hat{x}\_{ij}, \vec{x}\_{ij}, \text{sync}\_{ij} \gets \bot \end{aligned} } } \otimes F[\text{Stop}] \end{matrix}

Next, we can split the verification check into an honest check, and a malicious check.

ΓH8 …EndBroadcasti():‾…if ∃j∈H.x^_∙j≠x^_∙i:stop(⋆,1)if ∃j∈M.x⃗_ji≠x^_∙i:stop(⋆,1)⊗ΓM8 =ΓM7⊗F[SyncComm]⊗F[Hash]∘pub x^_ij,x⃗_ij,sync_ij←⊥⊗F[Stop]\begin{matrix} \boxed{ \small{ \begin{aligned} &\colorbox{FBCFE8}{\large $\Gamma^8_H$ }\cr &\ldots\cr \cr &\underline{ \text{EndBroadcast}_i(): }\cr &\enspace \ldots \cr &\enspace \colorbox{bae6fd}{$ \texttt{if } \exists j \in \mathcal{H}.\enspace \hat{x}\_{\bullet j} \neq \hat{x}\_{\bullet i} : $} \cr &\enspace\enspace \texttt{stop}(\star, 1) \cr &\enspace \colorbox{bae6fd}{$ \texttt{if } \exists j \in \mathcal{M}.\enspace \vec{x}\_{ji} \neq \hat{x}\_{\bullet i} : $} \cr &\enspace\enspace \texttt{stop}(\star, 1) \cr \end{aligned} } } \otimes \begin{matrix} \boxed{ \small{ \begin{aligned} &\colorbox{FBCFE8}{\large $\Gamma^8_M$ } = \Gamma^7_M\cr \end{aligned} } } \cr \otimes \cr F[\text{SyncComm}] \otimes F[\text{Hash}] \end{matrix} \cr \circ \cr \boxed{ \small{ \begin{aligned} \texttt{pub } \hat{x}\_{ij}, \vec{x}\_{ij}, \text{sync}\_{ij} \gets \bot \end{aligned} } } \otimes F[\text{Stop}] \end{matrix}

The only reason the honest check will fail is if the adversary sends to different messages to honest parties, causing their confirmations to differ. We can detect that in ΓM\Gamma_M instead, replacing the honest check.

ΓH9 (1)StartBroadcasti(x):‾x^_ij←xsent_ij←trueWaitBroadcasti():‾wait_(i,0) ∀j. x^_ij≠⊥x⃗_ij←x^_∙isync_ij←trueEndBroadcasti():‾wait_(i,1) ∀j. sync_ji≠⊥if ∃j∈M.x⃗_ji≠x^_∙i:stop(⋆,1)⊗ΓM9 xk←⊥↱k(S,m_∙,0):‾assert ∀j∈S. mj≠⊥∧x^_kj=⊥for j∈S∩H:if xk=⊥:xk←mjelif xk≠mj:stop({j},1)x^_kj←mj (∀j∈S)…⊗F[SyncComm]⊗F[Hash]∘pub x^_ij,x⃗_ij,sent_ij,sync_ij←⊥⊗F[Stop]\begin{matrix} \boxed{ \small{ \begin{aligned} &\colorbox{FBCFE8}{\large $\Gamma^9_H$ }\cr \cr &\underline{ (1)\text{StartBroadcast}_i(x): }\cr &\enspace \hat{x}\_{ij} \gets x \cr &\enspace \text{sent}\_{ij} \gets \texttt{true} \cr \cr &\underline{ \text{WaitBroadcast}_i(): }\cr &\enspace \texttt{wait}\_{(i, 0)}\ \forall j.\ \hat{x}\_{ij} \neq \bot \cr &\enspace \vec{x}\_{ij} \gets \hat{x}\_{\bullet i} \cr &\enspace \text{sync}\_{ij} \gets \texttt{true} \cr \cr &\underline{ \text{EndBroadcast}_i(): }\cr &\enspace \texttt{wait}\_{(i, 1)}\ \forall j.\ \text{sync}\_{ji} \neq \bot \cr &\enspace \texttt{if } \exists j \in \mathcal{M}.\enspace \vec{x}\_{ji} \neq \hat{x}\_{\bullet i} : \cr &\enspace\enspace \texttt{stop}(\star, 1) \cr \end{aligned} } } \otimes \begin{matrix} \boxed{ \small{ \begin{aligned} &\colorbox{FBCFE8}{\large $\Gamma^9_M$ }\cr \cr &\colorbox{bae6fd}{$ x_k \gets \bot $}\cr &\underline{ \Rsh_k(S, m\_\bullet, 0): }\cr &\enspace \texttt{assert } \forall j \in S.\ m_j \neq \bot \land \hat{x}\_{kj} = \bot \cr &\enspace \colorbox{bae6fd}{$ \texttt{for } j \in S \cap \mathcal{H}: $} \cr &\enspace\enspace \colorbox{bae6fd}{$ \texttt{if } x_k = \bot:\enspace x_k \gets m_j $} \cr &\enspace\enspace \colorbox{bae6fd}{$ \texttt{elif } x_k \neq m_j:\enspace \texttt{stop}(\{j\}, 1) $} \cr &\enspace \hat{x}\_{kj} \gets m_j\ (\forall j \in S) \cr \cr & \ldots \cr \end{aligned} } } \cr \otimes \cr F[\text{SyncComm}] \otimes F[\text{Hash}] \end{matrix} \cr \circ \cr \boxed{ \small{ \begin{aligned} \texttt{pub } \hat{x}\_{ij}, \vec{x}\_{ij}, \text{sent}\_{ij}, \text{sync}\_{ij} \gets \bot \end{aligned} } } \otimes F[\text{Stop}] \end{matrix}

Now, the only thing that can cause a malicious failure is if a bad x⃗_ij\vec{x}\_{ij} value is set. We can capture this with a trap value.

ΓH10 (1)Broadcasti(x):‾x^_ij←xsent_ij←trueWaitBroadcasti():‾wait_(i,0) ∀j. x^_ij≠⊥x⃗_ij←x^_∙isync_ij←trueEndBroadcasti():‾wait_(i,1) ∀j. sync_ji≠⊥if trap_∙i≠⊥∧trap_∙i≠x^_∙i:stop(⋆,1)⊗ΓM10 …↱k(S,m_∙,1):‾assert ∀j∈S. mj≠⊥∧x⃗_kj=⊥for j∈S∩H:if trap_∙j=⊥:trap_∙j←mjelif trap_∙j≠mj:stop({j},1)x⃗_kj←mj (∀j∈S)sync_kj←true (∀j∈S)⊗F[SyncComm]⊗F[Hash]∘pub x^_ij,trap_ij,x⃗_ij,sent_ij,sync_ij←⊥⊗F[Stop]\begin{matrix} \boxed{ \small{ \begin{aligned} &\colorbox{FBCFE8}{\large $\Gamma^{10}_H$ }\cr \cr &\underline{ (1)\text{Broadcast}_i(x): }\cr &\enspace \hat{x}\_{ij} \gets x \cr &\enspace \text{sent}\_{ij} \gets \texttt{true} \cr \cr &\underline{ \text{WaitBroadcast}_i(): }\cr &\enspace \texttt{wait}\_{(i, 0)}\ \forall j.\ \hat{x}\_{ij} \neq \bot \cr &\enspace \vec{x}\_{ij} \gets \hat{x}\_{\bullet i} \cr &\enspace \text{sync}\_{ij} \gets \texttt{true} \cr \cr &\underline{ \text{EndBroadcast}_i(): }\cr &\enspace \texttt{wait}\_{(i, 1)}\ \forall j.\ \text{sync}\_{ji} \neq \bot \cr &\enspace \colorbox{bae6fd}{$ \texttt{if } \text{trap}\_{\bullet i} \neq \bot \land \text{trap}\_{\bullet i} \neq \hat{x}\_{\bullet i} : $} \cr &\enspace\enspace \texttt{stop}(\star, 1) \cr \end{aligned} } } \otimes \begin{matrix} \boxed{ \small{ \begin{aligned} &\colorbox{FBCFE8}{\large $\Gamma^{10}_M$ }\cr \cr &\ldots\cr \cr &\underline{ \Rsh_k(S, m\_\bullet, 1): }\cr &\enspace \texttt{assert } \forall j \in S.\ m_j \neq \bot \land \vec{x}\_{kj} = \bot \cr &\enspace \colorbox{bae6fd}{$ \texttt{for } j \in S \cap \mathcal{H}: $} \cr &\enspace\enspace \colorbox{bae6fd}{$ \texttt{if } \text{trap}\_{\bullet j} = \bot:\enspace \text{trap}\_{\bullet j} \gets m_j $} \cr &\enspace\enspace \colorbox{bae6fd}{$ \texttt{elif } \text{trap}\_{\bullet j} \neq m_j:\enspace \texttt{stop}(\{j\}, 1) $} \cr &\enspace \vec{x}\_{kj} \gets m_j\ (\forall j \in S) \cr &\enspace \text{sync}\_{kj} \gets \texttt{true}\ (\forall j \in S) \cr \end{aligned} } } \cr \otimes \cr F[\text{SyncComm}] \otimes F[\text{Hash}] \end{matrix} \cr \circ \cr \boxed{ \small{ \begin{aligned} \texttt{pub } \hat{x}\_{ij}, \text{trap}\_{ij}, \vec{x}\_{ij}, \text{sent}\_{ij}, \text{sync}\_{ij} \gets \bot \end{aligned} } } \otimes F[\text{Stop}] \end{matrix}

Since we can't equivocate, simplify variables.

ΓH11 (1)Broadcasti(x):‾SetBroadcasti(x)SendBroadcasti(⋆)WaitBroadcasti():‾x_∙←GetBroadcasti(⋆)Synci(⋆)EndBroadcasti():‾WaitSynci(⋆)if BadBroadcasti():stop(⋆,1)⊗ΓM11 xk,x^_ij,x⃗_ij←⊥↱k(S,m_∙,0):‾assert ∀j∈S. mj≠⊥∧x^_kj=⊥for j∈S∩H:if xk=⊥:xk←mjSetBroadcastk(xk)elif xk≠mj:stop({j},1)x^_kj←mj (∀j∈S∩M)SendBroadcastk(S∩H)↱k(S,m_∙,1):‾assert ∀j∈S. mj≠⊥∧x⃗_kj=⊥for j∈S∩H:if trap_∙j=⊥:Trap(j,mj)elif trap_∙j≠mj:stop({j},1)x⃗_kj←mj (∀j∈S)Synck(S)↰k(S,0):‾wait_(k,0) ∀j∈S∩M. x^_jk≠⊥x^_jk←GetBroadcastk({j}) (∀j∈S∩H)return [x^_jk∣j∈S]↰k(S,1):‾WaitSynck()x⃗_jk←GetBroadcastk(⋆) (∀j∈S∩H)return [x⃗_jk∣j∈S]⊗F[SyncComm]⊗F[Hash]∘F[Broadcast]′ xi,sent_ij,trap_ij←⊥(1)SetBroadcasti(x):‾xi←xGetBroadcasti(S):‾wait_(i,0) sent_ji (∀j∈S)return [xj∣j∈S]Trap(j,m_∙):‾assert trap_∙j=⊥trap_ij←miBadBroadcast(j,m_∙):‾return ∃i. trap_ij≠⊥∧trap_ij≠x_i⊗F[Sync(1)]⊗F[Stop]\begin{matrix} \boxed{ \small{ \begin{aligned} &\colorbox{bae6fd}{\large $\Gamma^{11}_H$ }\cr \cr &\underline{ (1)\text{Broadcast}_i(x): }\cr &\enspace \text{SetBroadcast}_i(x) \cr &\enspace \text{SendBroadcast}_i(\star) \cr \cr &\underline{ \text{WaitBroadcast}_i(): }\cr &\enspace x\_{\bullet} \gets \text{GetBroadcast}_i(\star) \cr &\enspace \text{Sync}_i(\star) \cr \cr &\underline{ \text{EndBroadcast}_i(): }\cr &\enspace \text{WaitSync}_i(\star) \cr &\enspace \texttt{if } \text{BadBroadcast}_i(): \cr &\enspace\enspace \texttt{stop}(\star, 1) \cr \end{aligned} } } \otimes \begin{matrix} \boxed{ \small{ \begin{aligned} &\colorbox{FBCFE8}{\large $\Gamma^{11}_M$ }\cr \cr &\colorbox{bae6fd}{$ x_k, \hat{x}\_{ij}, \vec{x}\_{ij} \gets \bot $}\cr &\underline{ \Rsh_k(S, m\_\bullet, 0): }\cr &\enspace \texttt{assert } \forall j \in S.\ m_j \neq \bot \land \hat{x}\_{kj} = \bot \cr &\enspace \texttt{for } j \in S \cap \mathcal{H}: \cr &\enspace\enspace \texttt{if } x_k = \bot: \cr &\enspace\enspace\enspace x_k \gets m_j \cr &\enspace\enspace\enspace \colorbox{bae6fd}{$ \text{SetBroadcast}_k(x_k) $} \cr &\enspace\enspace \texttt{elif } x_k \neq m_j:\enspace \texttt{stop}(\{j\}, 1) \cr &\enspace \hat{x}\_{kj} \gets m_j\ (\forall j \in S \cap \mathcal{M}) \cr &\enspace \colorbox{bae6fd}{$ \text{SendBroadcast}_k(S \cap \mathcal{H}) $} \cr \cr &\underline{ \Rsh_k(S, m\_\bullet, 1): }\cr &\enspace \texttt{assert } \forall j \in S.\ m_j \neq \bot \land \vec{x}\_{kj} = \bot \cr &\enspace \texttt{for } j \in S \cap \mathcal{H}: \cr &\enspace\enspace \texttt{if } \text{trap}\_{\bullet j} = \bot: \cr &\enspace\enspace\enspace \colorbox{bae6fd}{$ \text{Trap}(j, m_j) $} \cr &\enspace\enspace \texttt{elif } \text{trap}\_{\bullet j} \neq m_j:\enspace \texttt{stop}(\{j\}, 1) \cr &\enspace \vec{x}\_{kj} \gets m_j\ (\forall j \in S) \cr &\enspace \colorbox{bae6fd}{$ \text{Sync}_k(S) $} \cr \cr &\underline{ \Lsh_k(S, 0): }\cr &\enspace \texttt{wait}\_{(k, 0)}\ \forall j \in S \cap M.\ \hat{x}\_{jk} \neq \bot \cr &\enspace \colorbox{bae6fd}{$ \hat{x}\_{jk} \gets \text{GetBroadcast}_k(\{j\})\ (\forall j \in S \cap \mathcal{H}) $} \cr &\enspace \texttt{return } [\hat{x}\_{j k} \mid j \in S] \cr \cr &\underline{ \Lsh_k(S, 1): }\cr &\enspace \colorbox{bae6fd}{$ \text{WaitSync}_k() $} \cr &\enspace \colorbox{bae6fd}{$ \vec{x}\_{jk} \gets \text{GetBroadcast}_k(\star)\ (\forall j \in S \cap \mathcal{H}) $} \cr &\enspace \texttt{return } [\vec{x}\_{jk} \mid j \in S] \cr \end{aligned} } } \cr \otimes \cr F[\text{SyncComm}] \otimes F[\text{Hash}] \end{matrix} \cr \circ \cr \boxed{ \small{ \begin{aligned} &\colorbox{FBCFE8}{\large $F[\text{Broadcast}]'$ }\cr \cr &x_i, \text{sent}\_{ij}, \text{trap}\_{ij} \gets \bot\cr \cr &\underline{ (1)\text{SetBroadcast}_i(x): }\cr &\enspace x_i \gets x \cr \cr &\underline{ \text{GetBroadcast}_i(S): }\cr &\enspace \texttt{wait}\_{(i, 0)}\ \text{sent}\_{ji}\ (\forall j \in S) \cr &\enspace \texttt{return } [x_j \mid j \in S] \cr \cr &\underline{ \text{Trap}(j, m\_\bullet): }\cr &\enspace \texttt{assert } \text{trap}\_{\bullet j} = \bot \cr &\enspace \text{trap}\_{i j} \gets m_i \cr \cr &\underline{ \text{BadBroadcast}(j, m\_\bullet): }\cr &\enspace \texttt{return } \exists i.\ \text{trap}\_{i j} \neq \bot \land \text{trap}\_{i j} \neq x\_i \cr \end{aligned} } } \otimes F[\text{Sync}(1)] \otimes F[\text{Stop}] \end{matrix}

As suggested by the introduction of this broadcast functionality, we now have a new protocol P1\mathscr{P}^1, and have shown that P0⇝P1\mathscr{P}^0 \leadsto \mathscr{P}^1 by our game hopping. We're not quite done yet, because the trapping here is a bit too strong, in that the adversary can trap even after a broadcast value has been set. We can simulate this freedom away.

Next, unroll again.

ΓH12 (1)StartBroadcasti(x):‾…⊗ΓM12 =1(SetBroadcastk,GetBroadcastk,BadBroadcastk,Synck,Trap)∘F[Broadcast]′⊗F[Sync(1)]⊗F[Stop]\begin{matrix} \boxed{ \small{ \begin{aligned} &\colorbox{FBCFE8}{\large $\Gamma^{12}_H$ }\cr \cr &\underline{ (1)\text{StartBroadcast}_i(x): }\cr &\enspace \ldots \cr \end{aligned} } } \otimes \boxed{\colorbox{FBCFE8}{\large $\Gamma^{12}_M$ } = 1 \begin{pmatrix} \text{SetBroadcast}_k ,\cr \text{GetBroadcast}_k ,\cr \text{BadBroadcast}_k ,\cr \text{Sync}_k ,\cr \text{Trap} \end{pmatrix} } \cr \circ \cr F[\text{Broadcast}]' \otimes F[\text{Sync}(1)] \otimes F[\text{Stop}] \end{matrix}

Traps that happen after a broadcast can be simulated by triggering an abort ourselves in the simulator.

ΓH13 =ΓH12⊗ΓM13 Trap(j,m_∙):‾for i∈H:if ∃k. x←nowait GetBroadcastk({i}):if mi≠x:stop({j},1)returnTrap(j,m_∙)∘F[Broadcast]⊗F[Sync(1)]⊗F[Stop]\begin{matrix} \boxed{ \small{ \begin{aligned} &\colorbox{FBCFE8}{\large $\Gamma^{13}_H$ } = \Gamma^{12}_H\cr \end{aligned} } } \otimes \boxed{ \small{ \begin{aligned} &\colorbox{FBCFE8}{\large $\Gamma^{13}_M$ }\cr \cr &\colorbox{bae6fd}{$ \underline{ \text{Trap}(j, m\_{\bullet}): }$}\cr &\enspace \texttt{for } i \in \mathcal{H}: \cr &\enspace\enspace \texttt{if } \exists k.\ x \gets \texttt{nowait } \text{GetBroadcast}_k(\{i\}): \cr &\enspace\enspace\enspace \texttt{if } m_i \neq x: \cr &\enspace\enspace\enspace\enspace \texttt{stop}(\{j\}, 1) \cr &\enspace\enspace\enspace\enspace \texttt{return} \cr &\enspace \text{Trap}(j, m\_\bullet) \cr \end{aligned} } } \cr \circ \cr F[\text{Broadcast}] \otimes F[\text{Sync}(1)] \otimes F[\text{Stop}] \end{matrix}

This is a simulator for P[IdealBroadcast]\mathscr{P}[\text{IdealBroadcast}], which concludes our proof, via the logic:

P[EchoBroadcast]⇝P0⇝P1⇝P[IdealBroadcast]\mathscr{P}[\text{EchoBroadcast}] \leadsto \mathscr{P}^0 \leadsto \mathscr{P}^1 \leadsto \mathscr{P}[\text{IdealBroadcast}]

■\blacksquare

Commitments

Our main application of broadcast will be to define a commitment protocol. The basic idea is that you commit to a value by hashing it, along with a random salt, and then broadcast that commitment. Later, you can open the value by sending it along with the salt.

Definition (Commitment Protocol):

P[Commit] Pi xi,ri←⊥(1)SetCommiti(x):‾xi←x,ri←$012λSetBroadcasti(Hash(xi,ri))Commiti():‾SendBroadcasti(⋆)WaitCommiti():‾return WaitBroadcasti()Openi():‾assert xi≠⊥↱i(⋆,(xi,ri),2)WaitOpeni():‾c_∙←WaitCommiti()EndBroadcasti()(x^_∙,r^_∙)↰i(⋆,2)if ∃j. Hash(x^j,r^j)≠cj:stop(⋆,2)return x^_∙F[Stop]⊚F[SyncComm]⊗F[Hash]Leakage:={Hash,stop}⊲P[EchoBroadcast]\boxed{ \begin{matrix} \colorbox{FBCFE8}{\large $\mathscr{P}[\text{Commit}]$ }\cr \cr \boxed{ \small{ \begin{aligned} &\colorbox{FBCFE8}{\large $P_i$ }\cr \cr &x_i, r_i \gets \bot\cr \cr &\underline{ (1)\text{SetCommit}_i(x): }\cr &\enspace x_i \gets x, \quad r_i \xleftarrow{\$} \texttt{01}^{2 \lambda} \cr &\enspace \text{SetBroadcast}_i(\text{Hash}(x_i, r_i)) \cr \cr &\underline{ \text{Commit}_i(): }\cr &\enspace \text{SendBroadcast}_i(\star) \cr \cr &\underline{ \text{WaitCommit}_i(): }\cr &\enspace \texttt{return } \text{WaitBroadcast}_i() \cr \cr &\underline{ \text{Open}_i(): }\cr &\enspace \texttt{assert } x_i \neq \bot \cr &\enspace \Rsh_i(\star, (x_i, r_i), 2) \cr \cr &\underline{ \text{WaitOpen}_i(): }\cr &\enspace c\_\bullet \gets \text{WaitCommit}_i() \cr &\enspace \text{EndBroadcast}_i() \cr &\enspace (\hat{x}\_{\bullet}, \hat{r}\_{\bullet}) \Lsh_i(\star, 2) \cr &\enspace \texttt{if } \exists j.\ \text{Hash}(\hat{x}_j, \hat{r}_j) \neq c_j: \cr &\enspace\enspace \texttt{stop}(\star, 2) \cr &\enspace \texttt{return } \hat{x}\_{\bullet} \cr \cr \end{aligned} } } \quad \begin{matrix} F[\text{Stop}]\cr \circledcirc\cr F[\text{SyncComm}]\cr \otimes\cr F[\text{Hash}]\cr \end{matrix}\cr \cr \text{Leakage} := \{\text{Hash}, \texttt{stop}\} \end{matrix} } \lhd \mathscr{P}[\text{EchoBroadcast}]

□\square

The ideal functionality this is supposed to implement is relatively straightforward. You set a commit value, and can wait for others to commit as well. Finally, you can open, which doesn't allow you to actually change the value you've committed to, it just makes it now visible to others. We also have the usual abort points remaining in the protocol.

Definition (Ideal Commitment):

P[IdealCommit] Pi (1)SetCommiti(x):‾SetCommiti(x)Commiti():‾Commiti(⋆)WaitCommiti():‾WaitCommiti(⋆)Synci(⋆)Openi():‾Openi(⋆)WaitOpeni():‾WaitCommiti()WaitSynci(⋆)return WaitOpeni(⋆)F[Commit] xi,com_ij,open_ij←⊥(1)SetCommiti(x):‾xi←xCommiti(S):‾com_ij←true (∀j∈S)WaitCommiti(S):‾wait_(i,0)∀j∈S. com_jiOpeni(S):‾assert xi≠⊥open_ij←true(∀j∈S)WaitOpeni(S):‾wait_(i,2)∀j∈S. open_jireturn x_∙⊗F[Sync(1)]⊚F[Stop]Leakage:={Hash,stop}\boxed{ \begin{matrix} \colorbox{FBCFE8}{\large $\mathscr{P}[\text{IdealCommit}]$ }\cr \cr \boxed{ \small{ \begin{aligned} &\colorbox{FBCFE8}{\large $P_i$ }\cr \cr &\underline{ (1)\text{SetCommit}_i(x): }\cr &\enspace \text{SetCommit}_i(x) \cr \cr &\underline{ \text{Commit}_i(): }\cr &\enspace \text{Commit}_i(\star) \cr \cr &\underline{ \text{WaitCommit}_i(): }\cr &\enspace \text{WaitCommit}_i(\star) \cr &\enspace \text{Sync}_i(\star) \cr \cr &\underline{ \text{Open}_i(): }\cr &\enspace \text{Open}_i(\star) \cr \cr &\underline{ \text{WaitOpen}_i(): }\cr &\enspace \text{WaitCommit}_i() \cr &\enspace \text{WaitSync}_i(\star) \cr &\enspace \texttt{return } \text{WaitOpen}_i(\star) \cr \end{aligned} } } \quad \begin{matrix} \boxed{ \small{ \begin{aligned} &\colorbox{FBCFE8}{\large $F[\text{Commit}]$ }\cr \cr &x_i, \text{com}\_{ij}, \text{open}\_{ij} \gets \bot\cr \cr &\underline{ (1)\text{SetCommit}_i(x): }\cr &\enspace x_i \gets x \cr \cr &\underline{ \text{Commit}_i(S): }\cr &\enspace \text{com}\_{ij} \gets \texttt{true}\ (\forall j \in S) \cr \cr &\underline{ \text{WaitCommit}_i(S): }\cr &\enspace \texttt{wait}\_{(i, 0)} \forall j \in S.\ \text{com}\_{ji} \cr \cr &\underline{ \text{Open}_i(S): }\cr &\enspace \texttt{assert } x_i \neq \bot \cr &\enspace \text{open}\_{ij} \gets \texttt{true} (\forall j \in S) \cr \cr &\underline{ \text{WaitOpen}_i(S): }\cr &\enspace \text{wait}\_{(i, 2)} \forall j \in S.\ \text{open}\_{ji} \cr &\enspace \texttt{return } x\_\bullet \cr \end{aligned} } }\cr \otimes\cr F[\text{Sync}(1)]\cr \circledcirc\cr F[\text{Stop}] \end{matrix}\cr \cr \text{Leakage} := \{\text{Hash}, \texttt{stop}\} \end{matrix} }

□\square

Lemma:

For some negligible ϵ\epsilon, and any combination of malicious parties, we have:

P[Commit⇝ϵP[IdealCommit]\begin{matrix} \mathscr{P}[\text{Commit} \overset{\epsilon}{\leadsto} \mathscr{P}[\text{IdealCommit}] \end{matrix}

Proof:

First, we have P[Commit]⇝P0\mathscr{P}[\text{Commit}] \leadsto \mathscr{P}^0, where P0\mathscr{P}^0 replaces P[EchoBroadcast]\mathscr{P}[\text{EchoBroadcast}] with P[IdealBroadcast]\mathscr{P}[\text{IdealBroadcast}], and we start from there.

We unroll Inst(P0)\text{Inst}(\mathscr{P}^0) to get:

ΓH0 (1)SetCommiti(x):‾…⊗ΓM0 =1(SetBroadcastk,SendBroadcastk,GetBroadcastk,BadBroadcastk,Trap,Synck,WaitSynck,↱k,↰k,Hash,stop)∘F[Broadcast]⊗F[Sync(1)]⊗F[SyncComm]⊗F[Hash]⊚F[Stop]\begin{matrix} \boxed{ \small{ \begin{aligned} &\colorbox{FBCFE8}{\large $\Gamma^0_H$ }\cr \cr &\underline{ (1)\text{SetCommit}_i(x): }\cr &\enspace \ldots \cr \end{aligned} } } \otimes \boxed{\colorbox{FBCFE8}{\large $\Gamma^0_M$ } = 1 \begin{pmatrix} \text{SetBroadcast}_k ,\cr \text{SendBroadcast}_k ,\cr \text{GetBroadcast}_k ,\cr \text{BadBroadcast}_k ,\cr \text{Trap} ,\cr \text{Sync}_k ,\cr \text{WaitSync}_k ,\cr \Rsh_k ,\cr \Lsh_k ,\cr \text{Hash} ,\cr \texttt{stop} \end{pmatrix} } \cr \circ \cr F[\text{Broadcast}] \otimes F[\text{Sync}(1)] \otimes F[\text{SyncComm}] \otimes F[\text{Hash}] \circledcirc F[\text{Stop}] \end{matrix}

Now, a trap value needs to be provided before the commitment value is known. However, for honest parties, these commitment values are in all likelihood freshly sampled, because of the entropy in rr. This means that trapping honest values is useless, since except with negligible probability, it has no effect.

ΓH1 =ΓH0⊗ΓM1 …Trap(j,m_∙):‾comi←xi≠⊥(∀i∈M)comi←nowait GetBroadcastk({i})≠⊥(∀i∈H)assert ∀i. mi=⊥∨(trap_ij=⊥∧¬comi)∀i∈H. mi←⊥Trap(j,m_∙)∘F[Broadcast]⊗F[Sync(1)]⊗F[SyncComm]⊗F[Hash]⊚F[Stop]\begin{matrix} \boxed{ \begin{aligned} &\colorbox{FBCFE8}{\large $\Gamma^1_H$ } = \Gamma^0_H \end{aligned} } \otimes \boxed{ \small{ \begin{aligned} &\colorbox{FBCFE8}{\large $\Gamma^1_M$ }\cr &\ldots\cr &\colorbox{bae6fd}{$ \underline{ \text{Trap}(j, m\_\bullet): }$}\cr &\enspace \text{com}_i \gets x_i \neq \bot (\forall i \in \mathcal{M}) \cr &\enspace \text{com}_i \gets \texttt{nowait } \text{GetBroadcast}_k(\{i\})\neq \bot (\forall i \in \mathcal{H}) \cr &\enspace \texttt{assert } \forall i.\ m_i = \bot \lor (\text{trap}\_{i j} = \bot \land \neg \text{com}_i) \cr &\enspace \forall i \in \mathcal{H}.\ m_i \gets \bot \cr &\enspace \text{Trap}(j, m\_{\bullet}) \cr \end{aligned} } } \cr \circ \cr F[\text{Broadcast}] \otimes F[\text{Sync}(1)] \otimes F[\text{SyncComm}] \otimes F[\text{Hash}] \circledcirc F[\text{Stop}] \end{matrix}

We can now replace F[Broadcast]F[\text{Broadcast}] with a function F[Broadcast′]F[\text{Broadcast}'], in which trapping isn't possible, because we can simulate the effects ourself.

ΓH2 =ΓH1⊗ΓM2 …ck,trap_ij,badk←⊥Trap(j,m_∙):‾comi←ci≠⊥(∀i∈M)comi←nowait GetBroadcastk({i})≠⊥(∀i∈H)assert ∀i. mi=⊥∨(trap_ij=⊥∧¬comi)∀i∈H. mi←⊥trap_ij←miSetBroadcastk(c):‾ck←cif ∃j. trap_jk≠⊥∧trap_jk≠c:badj←trueif j∈H: stop({j},1)BadBroadcastk():‾return badk∘F[Broadcast′]⊗F[Sync(1)]⊗F[SyncComm]⊗F[Hash]⊚F[Stop]\begin{matrix} \boxed{ \begin{aligned} &\colorbox{FBCFE8}{\large $\Gamma^2_H$ } = \Gamma^1_H \end{aligned} } \otimes \boxed{ \small{ \begin{aligned} &\colorbox{FBCFE8}{\large $\Gamma^2_M$ }\cr &\ldots\cr &\colorbox{bae6fd}{$ c_k, \text{trap}\_{ij}, \text{bad}_k \gets \bot$} \cr \cr &\underline{ \text{Trap}(j, m\_\bullet): }\cr &\enspace \text{com}_i \gets c_i \neq \bot (\forall i \in \mathcal{M}) \cr &\enspace \text{com}_i \gets \texttt{nowait } \text{GetBroadcast}_k(\{i\})\neq \bot (\forall i \in \mathcal{H}) \cr &\enspace \texttt{assert } \forall i.\ m_i = \bot \lor (\text{trap}\_{i j} = \bot \land \neg \text{com}_i) \cr &\enspace \forall i \in \mathcal{H}.\ m_i \gets \bot \cr &\enspace \colorbox{bae6fd}{$ \text{trap}\_{ij} \gets m_i $} \cr \cr &\colorbox{bae6fd}{$ \underline{ \text{SetBroadcast}_k(c): }$}\cr &\enspace c_k \gets c \cr &\enspace \texttt{if } \exists j.\ \text{trap}\_{jk} \neq \bot \land \text{trap}\_{jk} \neq c: \cr &\enspace\enspace \text{bad}_j \gets \texttt{true} \cr &\enspace\enspace \texttt{if } j \in \mathcal{H}:\ \texttt{stop}(\{j\}, 1) \cr \cr &\colorbox{bae6fd}{$ \underline{ \text{BadBroadcast}_k(): }$}\cr &\enspace \texttt{return } \text{bad}_k \cr \end{aligned} } } \cr \circ \cr F[\text{Broadcast}'] \otimes F[\text{Sync}(1)] \otimes F[\text{SyncComm}] \otimes F[\text{Hash}] \circledcirc F[\text{Stop}] \end{matrix}

From this we see that we're in fact simulating a protocol P1\mathscr{P}^1, which is like P[IdealBroadcast]\mathscr{P}[\text{IdealBroadcast}], except that trapping is not possible. Let's unroll that protocol, to get:

ΓH3 (1)SetCommiti(x):‾…⊗ΓM3 =1(SetBroadcastk,SendBroadcastk,GetBroadcastk,,Synck,WaitSynck,↱k,↰k,Hash,stop)∘F[Broadcast′]⊗F[Sync(1)]⊗F[SyncComm]⊗F[Hash]⊚F[Stop]\begin{matrix} \boxed{ \small{ \begin{aligned} &\colorbox{FBCFE8}{\large $\Gamma^3_H$ }\cr \cr &\underline{ (1)\text{SetCommit}_i(x): }\cr &\enspace \ldots \cr \end{aligned} } } \otimes \boxed{\colorbox{FBCFE8}{\large $\Gamma^3_M$ } = 1 \begin{pmatrix} \text{SetBroadcast}_k ,\cr \text{SendBroadcast}_k ,\cr \text{GetBroadcast}_k ,\cr ,\cr \text{Sync}_k ,\cr \text{WaitSync}_k ,\cr \Rsh_k ,\cr \Lsh_k ,\cr \text{Hash} ,\cr \texttt{stop} \end{pmatrix} } \cr \circ \cr F[\text{Broadcast}'] \otimes F[\text{Sync}(1)] \otimes F[\text{SyncComm}] \otimes F[\text{Hash}] \circledcirc F[\text{Stop}] \end{matrix}

At the end of WaitOpeni\text{WaitOpen}_i, we check that the opened values match the commitments. Because honest parties will always open the right values, we can instead limit the check to malicious parties.

ΓH4 WaitOpeni(x):‾c_∙←WaitCommiti()EndBroadcasti()(x^_∙,r^_∙)↰i(⋆,2)if ∃j∈M. Hash(x^j,r^j)≠cj:stop(⋆,2)return x^_∙⊗ΓM4 =ΓM3∘F[Broadcast′]⊗F[Sync(1)]⊗F[SyncComm]⊗F[Hash]⊚F[Stop]\begin{matrix} \boxed{ \small{ \begin{aligned} &\colorbox{FBCFE8}{\large $\Gamma^4_H$ }\cr \cr &\underline{ \text{WaitOpen}_i(x): }\cr &\enspace c\_\bullet \gets \text{WaitCommit}_i() \cr &\enspace \text{EndBroadcast}_i() \cr &\enspace (\hat{x}\_{\bullet}, \hat{r}\_{\bullet}) \Lsh_i(\star, 2) \cr &\enspace \colorbox{bae6fd}{$ \texttt{if } \exists j \in \mathcal{M}.\ \text{Hash}(\hat{x}_j, \hat{r}_j) \neq c_j: $} \cr &\enspace\enspace \texttt{stop}(\star, 2) \cr &\enspace \texttt{return } \hat{x}\_{\bullet} \cr \end{aligned} } } \otimes \boxed{\colorbox{FBCFE8}{\large $\Gamma^4_M$ } = \Gamma^3_M } \cr \circ \cr F[\text{Broadcast}'] \otimes F[\text{Sync}(1)] \otimes F[\text{SyncComm}] \otimes F[\text{Hash}] \circledcirc F[\text{Stop}] \end{matrix}

Now, because of the entropy of the rr values, in all likelihood the random oracle will not have been queried at that value before, and so we can instead assume that the value is random, and then backfill it later. Thus, we have honest parties broadcast completely random commitments, and then program the random oracle after they open the commitment.

ΓH5 xi,ci←⊥…(1)SetCommiti(x):‾xi←xci←$012λSetBroadcasti(ci)Openi():‾assert xi≠⊥ri←$012λ↱i(⋆,(xi,ri),2)WaitOpeni(x):‾c_∙←WaitCommiti()EndBroadcasti()(x^_∙,r^_∙)↰i(⋆,2)if ∃j∈M. Hash(x^j,r^j)≠cj:stop(⋆,2)return x^_∙⊗ΓH5 …Hash(x,r):‾if ∃k∈M,j∈H. nowait↰k({j},2)=(x,r):if ∃k∈M,j∈H. nowait GetBroadcast({j})→cj:return cjreturn Hash(x,r)∘F[Broadcast′]⊗F[Sync(1)]⊗F[SyncComm]⊗F[Hash]⊚F[Stop]\begin{matrix} \boxed{ \small{ \begin{aligned} &\colorbox{FBCFE8}{\large $\Gamma^5_H$ }\cr \cr &\colorbox{bae6fd}{$ x_i, c_i \gets \bot $}\cr &\ldots\cr \cr &\colorbox{bae6fd}{$ \underline{ (1)\text{SetCommit}_i(x): }$}\cr &\enspace x_i \gets x \cr &\enspace c_i \xleftarrow{\$} \texttt{01}^{2 \lambda} \cr &\enspace \text{SetBroadcast}_i(c_i) \cr \cr &\underline{ \text{Open}_i(): }\cr &\enspace \texttt{assert } x_i \neq \bot \cr &\enspace \colorbox{bae6fd}{$ r_i \xleftarrow{\$} \texttt{01}^{2\lambda} $} \cr &\enspace \Rsh_i(\star, (x_i, r_i), 2) \cr \cr &\underline{ \text{WaitOpen}_i(x): }\cr &\enspace c\_\bullet \gets \text{WaitCommit}_i() \cr &\enspace \text{EndBroadcast}_i() \cr &\enspace (\hat{x}\_{\bullet}, \hat{r}\_{\bullet}) \Lsh_i(\star, 2) \cr &\enspace \texttt{if } \exists j \in \mathcal{M}.\ \text{Hash}(\hat{x}_j, \hat{r}_j) \neq c_j: \cr &\enspace\enspace \texttt{stop}(\star, 2) \cr &\enspace \texttt{return } \hat{x}\_{\bullet} \cr \end{aligned} } } \otimes \boxed{ \small{ \begin{aligned} &\colorbox{FBCFE8}{\large $\Gamma^5_H$ }\cr &\ldots\cr \cr &\colorbox{bae6fd}{$ \underline{ \text{Hash}(x, r): }$}\cr &\enspace \texttt{if } \exists k \in \mathcal{M}, j \in \mathcal{H}.\ \texttt{nowait}\Lsh_k(\{j\}, 2) = (x, r): \cr &\enspace\enspace \texttt{if } \exists k \in \mathcal{M}, j \in \mathcal{H}.\ \texttt{nowait } \text{GetBroadcast}(\{j\}) \to c_j: \cr &\enspace\enspace\enspace \texttt{return } c_j \cr &\enspace \texttt{return } \text{Hash}(x, r) \cr \end{aligned} } } \cr \circ \cr F[\text{Broadcast}'] \otimes F[\text{Sync}(1)] \otimes F[\text{SyncComm}] \otimes F[\text{Hash}] \circledcirc F[\text{Stop}] \end{matrix}

Next, except with negligible probability we can extract preimages of commitments, since a commitment that hasn't come from the hash function will fail with probability ≤2−2λ\leq 2^{-2\lambda}.

ΓH6 =ΓH5⊗ΓH6 μ[∙],xk,rk←⊥…SetBroadcastk(h):‾assert h∈μ(xk,rk)←μ[h]SetBroadcastk(h)Hash(x,r):‾h←Hash′(x,r)μ[h]←(x,r)return hHash′(x,r):‾…∘F[Broadcast′]⊗F[Sync(1)]⊗F[SyncComm]⊗F[Hash]⊚F[Stop]\begin{matrix} \boxed{ \small{ \begin{aligned} &\colorbox{FBCFE8}{\large $\Gamma^6_H$ } = \Gamma^5_H\cr \end{aligned} } } \otimes \boxed{ \small{ \begin{aligned} &\colorbox{FBCFE8}{\large $\Gamma^6_H$ }\cr &\mu[\bullet], x_k, r_k \gets \bot\cr &\ldots\cr \cr &\colorbox{bae6fd}{$ \underline{ \text{SetBroadcast}_k(h): }$}\cr &\enspace \texttt{assert } h \in \mu \cr &\enspace (x_k, r_k) \gets \mu[h] \cr &\enspace \text{SetBroadcast}_k(h) \cr \cr &\colorbox{bae6fd}{$ \underline{ \text{Hash}(x, r): }$}\cr &\enspace h \gets \text{Hash}'(x, r) \cr &\enspace \mu[h] \gets (x, r) \cr &\enspace \texttt{return } h \cr &\underline{ \text{Hash}'(x, r): }\cr &\enspace \ldots \cr \end{aligned} } } \cr \circ \cr F[\text{Broadcast}'] \otimes F[\text{Sync}(1)] \otimes F[\text{SyncComm}] \otimes F[\text{Hash}] \circledcirc F[\text{Stop}] \end{matrix}

Next, instead of checking for bad openings inside honest parties, we can instead have malicious parties directly cause a stop once they send a bad value.

ΓH7 …WaitOpeni():‾c_∙←WaitCommiti()EndBroadcasti()(x^_∙,r^_∙)↰i(⋆,2)if ∃j. Hash(x^j,r^j)≠cj:stop(⋆,2)return x^_∙⊗ΓH7 μ[∙],xk,rk←⊥…↱k(S,(x^_∙,r^_∙)):‾for j∈S∩H. Hash(x^j,r^j)≠Hash(xk,rk):stop({j},2)↱k(S,(x^_∙,r^_∙))∘F[Broadcast′]⊗F[Sync(1)]⊗F[SyncComm]⊗F[Hash]⊚F[Stop]\begin{matrix} \boxed{ \small{ \begin{aligned} &\colorbox{FBCFE8}{\large $\Gamma^7_H$ }\cr &\ldots\cr \cr &\underline{ \text{WaitOpen}_i(): }\cr &\enspace c\_\bullet \gets \text{WaitCommit}_i() \cr &\enspace \text{EndBroadcast}_i() \cr &\enspace (\hat{x}\_{\bullet}, \hat{r}\_{\bullet}) \Lsh_i(\star, 2) \cr &\enspace \colorbox{#fca5a5}{$ \texttt{if } \exists j.\ \text{Hash}(\hat{x}_j, \hat{r}_j) \neq c_j: $} \cr &\enspace\enspace \colorbox{#fca5a5}{$ \texttt{stop}(\star, 2) $} \cr &\enspace \texttt{return } \hat{x}\_{\bullet} \cr \end{aligned} } } \otimes \boxed{ \small{ \begin{aligned} &\colorbox{FBCFE8}{\large $\Gamma^7_H$ }\cr &\mu[\bullet], x_k, r_k \gets \bot\cr &\ldots\cr \cr &\colorbox{bae6fd}{$ \underline{ \Rsh_k(S, (\hat{x}\_\bullet, \hat{r}\_\bullet)): }$}\cr &\enspace \texttt{for } j \in S \cap \mathcal{H}.\ \text{Hash}(\hat{x}_j, \hat{r}_j) \neq \text{Hash}(x_k, r_k): \cr &\enspace\enspace \texttt{stop}(\{j\}, 2) \cr &\enspace \Rsh_k(S, (\hat{x}\_\bullet, \hat{r}\_\bullet)) \cr \end{aligned} } } \cr \circ \cr F[\text{Broadcast}'] \otimes F[\text{Sync}(1)] \otimes F[\text{SyncComm}] \otimes F[\text{Hash}] \circledcirc F[\text{Stop}] \end{matrix}

(red parts deleted).

Now, because random oracles are collision resistant, we get the same result to check full equality rather than hash equality.

ΓH8 =ΓH7⊗ΓH8 …↱k(S,(x^_∙,r^_∙),2):‾for j∈S∩H. (x^j,r^j)≠(xk,rk):stop({j},2)↱k(S,(x^_∙,r^_∙))∘F[Broadcast′]⊗F[Sync(1)]⊗F[SyncComm]⊗F[Hash]⊚F[Stop]\begin{matrix} \boxed{ \small{ \begin{aligned} &\colorbox{FBCFE8}{\large $\Gamma^8_H$ } = \Gamma^7_H\cr \end{aligned} } } \otimes \boxed{ \small{ \begin{aligned} &\colorbox{FBCFE8}{\large $\Gamma^8_H$ }\cr &\ldots\cr \cr &\underline{ \Rsh_k(S, (\hat{x}\_\bullet, \hat{r}\_\bullet), 2): }\cr &\enspace \colorbox{bae6fd}{$ \texttt{for } j \in S \cap \mathcal{H}.\ (\hat{x}_j, \hat{r}_j) \neq (x_k, r_k): $} \cr &\enspace\enspace \texttt{stop}(\{j\}, 2) \cr &\enspace \Rsh_k(S, (\hat{x}\_\bullet, \hat{r}\_\bullet)) \cr \end{aligned} } } \cr \circ \cr F[\text{Broadcast}'] \otimes F[\text{Sync}(1)] \otimes F[\text{SyncComm}] \otimes F[\text{Hash}] \circledcirc F[\text{Stop}] \end{matrix}

At this point, the malicious party can't actually send honest parties an opened value that's any different than the one they used to generate their initial broadcast hash. We can now rewrite the adversary to use the ideal commitment functionality instead.

ΓH9 (1)SetCommiti(x):‾SetCommiti(x)Commiti():‾Commiti(⋆)WaitCommiti():‾WaitCommiti(⋆)Synci(⋆)Openi():‾Openi(⋆)WaitOpeni():‾WaitCommiti()WaitSynci(⋆)return WaitOpeni(⋆)⊗ΓH9 …SetBroadcastk(h):‾assert h∈μhk←hSetCommitk(μ[h])SendBroadcastk(S):‾h^_kj←hk (∀j∈S∩m)Commitk(S)GetBroadcastk(S):‾WaitCommitk(S)for j∈S∩H. cj=⊥:cj←$012λreturn [cj∣j∈S∩Hh^_jk∣j∈S∩M]↱k(S,m^_∙,2):‾(x^_∙,r^_∙)←m^_∙for j∈S∩H. (x^j,r^j)≠(xk,rk):stop({j},2)S←S/{j}m_kj←(∀j∈S∩M)Openk(S)↰k(S,2):‾xr_∙←WaitOpenk(S)return [xrj∣j∈S∩Hm_kj∣j∈S∩M]Hash(x,r):‾h←Hash′(x,r)μ[h]←(x,r)return hHash′(x,r):‾if ∃k∈M,j∈H. nowait↰k({j},2)=(x,r):if ∃k∈M,j∈H. nowait GetBroadcast({j})→cj:return cjreturn Hash(x,r)⊗1(Synck,WaitSynck,stop)⊗F[Hash]∘F[IdealCommit]⊗F[Sync(1)]⊚F[Stop]\begin{matrix} \boxed{ \small{ \begin{aligned} &\colorbox{bae6fd}{\large $\Gamma^9_H$ }\cr \cr &\underline{ (1)\text{SetCommit}_i(x): }\cr &\enspace \text{SetCommit}_i(x) \cr \cr &\underline{ \text{Commit}_i(): }\cr &\enspace \text{Commit}_i(\star) \cr \cr &\underline{ \text{WaitCommit}_i(): }\cr &\enspace \text{WaitCommit}_i(\star) \cr &\enspace \text{Sync}_i(\star) \cr \cr &\underline{ \text{Open}_i(): }\cr &\enspace \text{Open}_i(\star) \cr \cr &\underline{ \text{WaitOpen}_i(): }\cr &\enspace \text{WaitCommit}_i() \cr &\enspace \text{WaitSync}_i(\star) \cr &\enspace \texttt{return } \text{WaitOpen}_i(\star) \cr \end{aligned} } } \otimes \begin{matrix} \boxed{ \small{ \begin{aligned} &\colorbox{bae6fd}{\large $\Gamma^9_H$ }\cr &\ldots\cr \cr &\underline{ \text{SetBroadcast}_k(h): }\cr &\enspace \texttt{assert } h \in \mu \cr &\enspace h_k \gets h \cr &\enspace \text{SetCommit}_k(\mu[h]) \cr \cr &\underline{ \text{SendBroadcast}_k(S): }\cr &\enspace \hat{h}\_{kj} \gets h_k \ (\forall j \in S \cap \mathcal{m}) \cr &\enspace \text{Commit}_k(S) \cr \cr &\underline{ \text{GetBroadcast}_k(S): }\cr &\enspace \text{WaitCommit}_k(S) \cr &\enspace \texttt{for } j \in S \cap \mathcal{H}.\ c_j = \bot: \cr &\enspace\enspace c_j \xleftarrow{\$} \texttt{01}^{2\lambda} \cr &\enspace \texttt{return } \begin{bmatrix} c_j &\mid j \in S \cap \mathcal{H} \cr \hat{h}\_{jk} &\mid j \in S \cap \mathcal{M} \end{bmatrix} \cr \cr &\underline{ \Rsh_k(S, \hat{m}\_\bullet, 2): }\cr &\enspace (\hat{x}\_\bullet, \hat{r}\_\bullet) \gets \hat{m}\_\bullet \cr &\enspace \texttt{for } j \in S \cap \mathcal{H}.\ (\hat{x}_j, \hat{r}_j) \neq (x_k, r_k): \cr &\enspace\enspace \texttt{stop}(\{j\}, 2) \cr &\enspace\enspace S \gets S / \{j\} \cr &\enspace m\_{kj} \gets (\forall j \in S \cap \mathcal{M}) \cr &\enspace \text{Open}_k(S) \cr \cr &\underline{ \Lsh_k(S, 2): }\cr &\enspace \text{xr}\_\bullet \gets \text{WaitOpen}_k(S) \cr &\enspace \texttt{return } \begin{bmatrix} \text{xr}_j &\mid j \in S \cap \mathcal{H}\cr m\_{kj} &\mid j \in S \cap \mathcal{M} \end{bmatrix} \cr \cr &\underline{ \text{Hash}(x, r): }\cr &\enspace h \gets \text{Hash}'(x, r) \cr &\enspace \mu[h] \gets (x, r) \cr &\enspace \texttt{return } h \cr \cr &\underline{ \text{Hash}'(x, r): }\cr &\enspace \texttt{if } \exists k \in \mathcal{M}, j \in \mathcal{H}.\ \texttt{nowait}\Lsh_k(\{j\}, 2) = (x, r): \cr &\enspace\enspace \texttt{if } \exists k \in \mathcal{M}, j \in \mathcal{H}.\ \texttt{nowait } \text{GetBroadcast}(\{j\}) \to c_j: \cr &\enspace\enspace\enspace \texttt{return } c_j \cr &\enspace \texttt{return } \text{Hash}(x, r) \cr \end{aligned} } }\cr \otimes\cr 1(\text{Sync}_k, \text{WaitSync}_k, \texttt{stop}) \otimes F[\text{Hash}] \end{matrix} \cr \circ \cr F[\text{IdealCommit}] \otimes F[\text{Sync}(1)] \circledcirc F[\text{Stop}] \end{matrix}

This is fact a simulator over P[IdealCommit]\mathscr{P}[\text{IdealCommit}], concluding our proof.

■\blacksquare