[
[
['9','add','hl'],
['10','add','hl'],
['11','add','hl'],
['12','add','hl'],
['24','remove','slide-up'],
['21','add','slide-down']
],
[
['27','add','hl'],
['27','remove','hidden'],
['3','add','hidden'],
['9','remove','hl'],
['9','add','hidden'],
['10','remove','hl'],
['10','add','hidden'],
['11','remove','hl'],
['11','add','hidden'],
['12','remove','hl'],
['12','add','hidden']
],
[
['27','remove','hl'],
['7','add','hl'],
['8','add','hl'],
['88','add','hl'],
['14','add','hl'],
['15','add','hl'],
['42','remove','slide-up'],
['24','add','slide-down']
],
[
['48','add','hl'],
['48','remove','hidden'],
['49','add','hl'],
['49','remove','hidden'],
['7','remove','hl'],
['7','add','hidden'],
['8','remove','hl'],
['8','add','hidden'],
['88','remove','hl'],
['88','add','slide-left'],
['14','remove','hl'],
['14','add','hidden'],
['15','remove','hl'],
['15','add','hidden']
],
[
['48','remove','hl'],
['49','remove','hl'],
['5','add','hl'],
['6','add','hl'],
['48','add','hl'],
['87','add','hl'],
['58','remove','slide-up'],
['42','add','slide-down']
],
[
['9','add','hl'],
['9','remove','hidden'],
['88','add','hl'],
['88','remove','slide-left'],
['5','remove','hl'],
['5','add','hidden'],
['6','remove','hl'],
['6','add','hidden'],
['48','remove','hl'],
['48','add','hidden'],
['87','remove','hl'],
['87','add','slide-right']
],
[
['9','remove','hl'],
['88','remove','hl'],
['49','add','hl'],
['90','add','hl'],
['72','remove','slide-up'],
['58','add','slide-down']
],
[
['74','remove','hidden'],
['87','add','hl'],
['87','remove','slide-right'],
['78','add','hl'],
['78','remove','hidden'],
['91','add','hl'],
['91','remove','slide-left'],
['49','remove','hl'],
['49','add','hidden'],
['90','remove','hl'],
['90','add','slide-right']
],
[
['87','remove','hl'],
['78','remove','hl'],
['91','remove','hl']
]
]
The starting point is $\lib{ke-real}$, which outputs the protocol transcript $(\mat G, \vec x, \vec y, R)$ and corresponding output key $\alpha$.
We can apply the LWE assumption to replace $\vec y$ with a uniformly sampled vector. The standard three-hop maneuver is not shown.
Both $\vec x$ and $K$ are computed in a similar way: a multiplication (on the left) by $\vec a^\top$, followed by an addition of a noise term. We can therefore write both $\vec x$ and $K$ in terms of a single matrix expression, by appending $\vec y$ to the LWE matrix $\mat G$ and $e$ to the noise vector $\vec e_1$.
Now $(\vec x, K)$ are computed as (the transpose of) an LWE sample, using a uniformly sampled $(n+1) \times n$ LWE matrix $[\mat G \mid \vec y]$. We can therefore apply the LWE assumption to replace these values with uniform ones.
Now $K$ is distributed uniformly and used only to compute $R$. Thus, $R$ is a ciphertext in the OTP variant that uses addition mod $\qmod$, so it is distributed uniformly. The result of this change is $\lib{ke-rand}$, which completes the proof.
$\lib{ke-real}$
$\lib{ke-rand}$
$\mat G \gets (\Z_\qmod)^{n \times n}$
$\vec y \gets (\Z_\qmod)^n$
$\vec a \gets \mathcal E^n$
$\vec e_1^\top \gets \mathcal E^n$
$\vec x^\top := \vec a^\top \mat G + \vec e_1^\top$
$\vec b \gets \mathcal E^n$
$\vec e_2 \gets \mathcal E^n$
$\vec y := \mat G \vec b + \vec e_2$
$[\vec e_1^\top \mid e] \gets \mathcal E^{n+1}$
$[\vec x^\top \mid K] $
${}:= \vec a^\top [\mat G \mid \vec y] + [\vec e_1^\top\mid e]$
${}\gets (\Z_\qmod)^{n+1}$
$\vec x \gets (\Z_\qmod)^{n}$
$e \gets \mathcal E$
$K := \vec a^\top \vec y + e$
$\alpha \gets \bits$
$R $
${}:= K + \alpha\lfloor \qmod/2 \rfloor \pct \qmod$
${}\gets \Z_\qmod$
return $(\mat G, \vec x, \vec y, R, \alpha)$