Added Proofs for lax parsing

This commit is contained in:
2023-05-02 17:36:07 +02:00
parent 419018dec3
commit 8a7b0d4d75
9 changed files with 210 additions and 30 deletions

View File

@@ -1,7 +1,7 @@
\subsection{UF-NMA $\Rightarrow$ \cma (ROM)} \label{proof:uf-nma_implies_suf-cma}
\subsection{UF-NMA $\Rightarrow$ $\text{\cma}_{\text{EdDSA with strict parsing}}$ (ROM)} \label{proof:uf-nma_implies_suf-cma}
% TODO: "intuition for the proof" vs. "intuition of the proof"?
This section shows that the UF-NMA security of EdDSA signature scheme implies the \cma security of EdDSA signature scheme using the Random Oracle Model. The section starts by first providing an intuition for the proof followed by the detailed security proof.
This section shows that the UF-NMA security of EdDSA implies the \cma security of EdDSA with strict parsing using the random oracle model. The section starts by first providing an intuition for the proof followed by the detailed security proof.
\begin{theorem}
\label{theorem:adv_uf-nma}
@@ -164,14 +164,80 @@ The proof starts by providing an algorithm which generates correctly distributed
To prove (\ref{eq:adv_uf-nma}), we define an adversary $\adversary{B}$ attacking $\text{UF-NMA}$ that simulates $\adversary{A}$'s view in $G_3$. Adversary $\adversary{B}$ formally defined in figure \ref{fig:adversarybuf-nma} is run in the $\text{UF-NMA}$ game and adversary $\adversary{B}$ simulates \Osign for adversary $\adversary{A}$. \Osign is simulated perfectly.
Finally, consider $\adversary{A}$ output $(\m^*, \signature^* \assign (\encoded{R}, S))$. It is known that $2^c S \groupelement{B} = 2^c \groupelement{R} + 2^c H'(\encoded{R}|\encoded{A}|m) \groupelement{A}$. Since the signature for the message $\m^*$ has not been queried in the \Osign oracle the output of $H'(\encoded{R}|\encoded{A}|m)$ has not been set by the adversary $\adversary{B}$ but was forwarded from the $H$ hash oracle. For this reason $H'(\encoded{R}|\encoded{A}|m) = H(\encoded{R}|\encoded{A}|m)$. Therefore,
Finally, consider $\adversary{A}$ output $(\m^*, \signature^* \assign (\encoded{R^*}, S^*))$. It is known that $2^c S^* \groupelement{B} = 2^c \groupelement{R^*} + 2^c H'(\encoded{R^*}|\encoded{A}|m^*) \groupelement{A}$. When using strict parsing any the decoded $S$ from the signature it is known that $0 \leq S < L$. Therefore there is only one valid encoded $S$ for each $R$, $\m$ pair that satisfies the equation. This means that from no new and valid signature can be generated by only changing the $S$ value of an already valid signature. Hence, also $R$ or $m$ has to be altered to generate a new valid signature from another one. Since $R$ and $m$ are inputs to the hash query, which is used to generate the challenge, the result for this hash query are forwarded from the $H$ hash oracle provided to the adversary $\adversary{B}$. For this reason $H'(\encoded{R^*}|\encoded{A}|m^*) = H(\encoded{R^*}|\encoded{A}|m^*)$. Therefore,
\begin{align*}
2^c S \groupelement{B} &= 2^c \groupelement{R} + 2^c H'(\encoded{R}|\encoded{A}|m) \groupelement{A}\\
\Leftrightarrow 2^c S \groupelement{B} &= 2^c \groupelement{R} + 2^c H(\encoded{R}|\encoded{A}|m) \groupelement{A}.
2^c S^* \groupelement{B} &= 2^c \groupelement{R^*} + 2^c H'(\encoded{R^*}|\encoded{A}|m^*) \groupelement{A}\\
\Leftrightarrow 2^c S^* \groupelement{B} &= 2^c \groupelement{R^*} + 2^c H(\encoded{R^*}|\encoded{A}|m^*) \groupelement{A}.
\end{align*}
Meaning that the forged signature from adversary $\adversary{A}$ is also a valid signature in the UF-NMA game.
\item This proves theorem \ref{theorem:adv_uf-nma}.
\end{proof}
\subsection{UF-NMA $\Rightarrow$ $\text{EUF-CMA}_{\text{EdDSA with lax parsing}}$ (ROM)}
This section shows that the UF-NMA security of EdDSA implies the EUF-CMA security of EdDSA with lax parsing using the random oracle model. This proof is very similar to the proof of the SUF-CMA security of EdDSA with strict parsing. The modification of the games are the same as in the proof above with the only difference being the win condition, which is $\verify(\groupelement{A}, \m^*,\signature^*) \wedge \m^* \notin Q$. For this reason this proofs starts at showing the existence of an adversary $\adversary{B}$ breaking UF-NMA security.
\begin{theorem}
\label{theorem:adv2_uf-nma}
Let $\adversary{A}$ be an adversary against EUF-CMA, making at most $\hashqueries$ hash queries and $\oraclequeries$ oracle queries. Then,
\[ \advantage{\adversary{A}}{\text{EUF-CMA}}(\secparamter) = \advantage{\adversary{B}}{\text{UF-NMA}}(\secparamter) - \frac{\oraclequeries \hashqueries}{2^{-\log_2(\lceil \frac{2^{2b} - 1}{L} \rceil 2^{-2b})}}. \]
\end{theorem}
\paragraph{\underline{Formal Proof}}
\begin{proof}
\item
\begin{align}
\prone{G_3^{\adversary{A}}} = \advantage{\adversary{B}}{\text{UF-NMA}}(\secparamter). \label{eq:adv2_uf-nma}
\end{align}
\begin{figure}
\hrule
\begin{multicols}{2}
\large
\begin{algorithmic}[1]
\Statex \underline{\textbf{Adversary} $\adversary{B}^{H(\inp)}(\groupelement{A})$}
\State $(\m^*, \signature^*) \randomassign \adversary{A}^{H'(\inp), \sign(\inp)}(\groupelement{A})$
\State \Return $(\m^*, \signature^*)$
\end{algorithmic}
\columnbreak
\begin{algorithmic}[1]
\Statex \underline{\oracle \sign($m \in \messagespace$)}
\State $(R,\textbf{ch},S) \randomassign \simalg(\groupelement{A})$
\State $\textbf{if } \sum[\encoded{R} | \encoded{A} | m] \neq \bot \textbf{ then}$
\State \quad $bad \assign true$
\State \quad $abort$
\State $\sum[\encoded{R} | \encoded{A} | m] = \textbf{ch}$
\State $\signature \assign (\encoded{R}, S)$
\State $Q \assign Q \cup \{\m\}$
\State \Return $\signature$
\end{algorithmic}
\end{multicols}
\begin{algorithmic}[1]
\Statex \underline{\oracle $H'(m \in \{0,1\}^*)$}
\State $\textbf{if } \sum[m] = \bot \textbf{ then}$
\State \quad $\sum[m] \assign H(m)$
\State \Return $\sum[m]$
\end{algorithmic}
\hrule
\caption{Adversary $\adversary{B}$ breaking $\text{UF-NMA}$}
\label{fig:adversary_b_suf-nma}
\end{figure}
To prove (\ref{eq:adv2_uf-nma}), we define an adversary $\adversary{B}$ attacking $\text{UF-NMA}$ that simulates $\adversary{A}$'s view in $G_3$. Adversary $\adversary{B}$ formally defined in figure \ref{fig:adversary_b_suf-nma} is run in the $\text{UF-NMA}$ game and adversary $\adversary{B}$ simulates \Osign for adversary $\adversary{A}$. \Osign is simulated perfectly.
Finally, consider $\adversary{A}$ output $(\m^*, \signature^* \assign (\encoded{R^*}, S^*))$. It is known that $2^c S^* \groupelement{B} = 2^c \groupelement{R^*} + 2^c H'(\encoded{R^*}|\encoded{A}|m^*) \groupelement{A}$. The same argument as in the proof above cannot be used since the lax parser could map multiple $2b$-bit bitstrings onto the same $S^* \pmod L$. Therefore the adversary $\adversary{A}$ could generate a new valid signature from a by \Osign generated one by simply choosing a different bitstring representation of the same $S^* \pmod L$. Since in this case $\sum[\encoded{R^*}|\encoded{A}|m^*]$ was set by the adversary $\adversary{B}$ this signature is not valid for the UF-NMA challenger. But since we are in the EUF-CMA setting we require the adversary $\adversary{A}$ to output a signature for a message $m^*$ for that it has not requested a signature via the \Osign oracle. Since the signature for the message $m^*$ has not been queried in the Sign oracle the output of $H'(\encoded{R^*}|\encoded{A}|m^*)$ has not been set by the adversary B but was forwarded from the $H$ hash oracle. For this reason $H'(\encoded{R^*}|\encoded{A}|m^*) = H(\encoded{R^*}|\encoded{A}|m^*)$. Therefore,
\begin{align*}
2^c S^* \groupelement{B} &= 2^c \groupelement{R^*} + 2^c H'(\encoded{R^*}|\encoded{A}|m^*) \groupelement{A}\\
\Leftrightarrow 2^c S^* \groupelement{B} &= 2^c \groupelement{R^*} + 2^c H(\encoded{R^*}|\encoded{A}|m^*) \groupelement{A}.
\end{align*}
Meaning that the forged signature from adversary $\adversary{A}$ is also a valid signature in the UF-NMA game.
\item This proves theorem \ref{theorem:adv2_uf-nma}.
\end{proof}