Hybrid Sequence:
The starting point is $\lib{ots-real}^{\Sigma^*}$, and our goal is to make a sequence of interchangeable modifications until we eventually arrive at $\lib{ots-rand}^{\Sigma^*}$.
We can first apply the security of $\Sigma_1$ with a three-hop maneuver. The three hops are: (1) factor out the operations involving $\Sigma_1$, so that an instance of its library $\lib{ots-real}^{\Sigma_1}$ appears; (2) replace $\lib{ots-real}^{\Sigma_1}$ with $\lib{ots-rand}^{\Sigma_1}$; (3) inline $\lib{ots-rand}^{\Sigma_1}$. These changes have no effect on the calling program.
We can now apply the security property of $\Sigma_2$ in a similar three-step maneuver. The final result is $\lib{ots-rand}^{\Sigma^*}$, which completes the proof.
$\lib{ots-real}^{\Sigma^*}$
$\otsenc^*$($\ptxt$):
$\key \gets \Sigma_1.\K$ // ${} = \Sigma^*.\K$
// $(\ctxt_1,\ctxt_2) := \Sigma^*.\Enc(\key,\ptxt)$:
$\key' \gets \Sigma_2.\K$
$\ctxt_1 $
${}:= {}$
$\Sigma_1.\Enc(\key, \key')$
$\otsenc_1(\key')$
${}\gets \Sigma_1.\C$
$\ctxt_2 $
${}:= {}$
$\Sigma_2.\Enc(\key', \ptxt)$
$\otsenc_2(\ptxt)$
${}\gets \Sigma_2.\C$
return $(\ctxt_1, \ctxt_2)$
$\link$
$\lib{ots-real}^{\Sigma_1}$
$\otsenc_1$($\ptxt$):
$\key \gets \Sigma_1.\K$
$\ctxt := \Sigma_1.\Enc(\key, \ptxt)$
return $\ctxt$
$\lib{ots-rand}^{\Sigma_1}$
$\otsenc_1$($\ptxt$):
$\ctxt \gets \Sigma_1.\C$
return $\ctxt$
$\link$
$\lib{ots-real}^{\Sigma_2}$
$\otsenc_2$($\ptxt$):
$\key \gets \Sigma_2.\K$
$\ctxt := \Sigma_2.\Enc(\key, \ptxt)$
return $\ctxt$
$\lib{ots-rand}^{\Sigma_2}$
$\otsenc_2$($\ptxt$):
$\ctxt \gets \Sigma_2.\C$
return $\ctxt$