Add income theorem statements

1 files changed, 35 insertions, 3 deletions

diff --git a/games/games.tex b/games/games.tex
index 265cbf3..8d2255f 100644
--- a/games/games.tex
+++ b/games/games.tex
@@ -22,8 +22,9 @@
 \title{Taler Security Proofs}
 \date{\today}
 
-\newtheorem{lemma}{Lemma}
-\newtheorem{theorem}{Theorem}
+\newtheorem{lemma}{Lemma}[section]
+\newtheorem{theorem}[lemma]{Theorem}
+\newtheorem{corollary}[lemma]{Corollary}
 
 \theoremstyle{definition}
 \newtheorem{definition}{Definition}[section]
@@ -523,6 +524,8 @@ the aid of authorities who can witness the attack, like our auditor.
 
 \subsection{Unforgeability} % Exculpability?
 
+TODO: Copy in definitions
+
 \begin{theorem}
 In the random oracle model,
 if the RSA known-target inversion problem (RSA-KTI) is hard, then
@@ -567,7 +570,29 @@ RSA-KTI cannot be hard by \cite[Theorem 12]{RSA-FDH-KTIvCTI}.
 
 \subsection{Income Transparency}
 
-\begin{proof}[Proof-sketch]
+\begin{definition}
+A {\em key exchange failure} consists of two key pairs
+ $A = a G$ and $B = b G$ such that $b A \neq a B$.
+\comment{Find this in literature?  Is it related to contributory behavior?}
+\end{definition}
+
+\begin{theorem}
+Assume Taler is polynomially-secure against
+\begin{enumerate}
+\item one-more forgery attacks,
+\item collisions in the hash function the refresh protocol uses
+ to commit to planchets, and
+\item key exchange failures in the ECDH operation used in the refresh.
+\end{enumerate}
+Then Taler is polynomially-secure against profitable attacks on
+income transperency in the sense that
+any probabilistic polynomially time adversary $\cal A$ has at best
+$1\over\kappa \epsilon(k)$ odds of winning the income transparency
+game where $\epsilon(k)$ is $k$ is a security parameter distinct
+from $\kappa$.
+\end{theorem}
+
+\begin{proof}
 In our actual refresh operation, our commitment phase sends only the
 hash of the planchets to reduce bandwidth.  We could however commit
 to the full planchets without damaging anything else, including
@@ -614,6 +639,13 @@ It follows that
  $P[{b \over w'} \ge (1-{1\over\kappa})] = 1/2 > {1\over\kappa}$.
 \end{proof}
 
+\begin{corollary}
+In the random oracle model,
+if the RSA known-target inversion problem (RSA-KTI) is hard, then
+Taler is polynomially-secure against profitable attacks on
+ income transperency.
+\end{corollary}
+
 We observe that $t C' = c' T$ provides a delicate requirement for
 implementations:  An exchange might do the scalar multiplication by
 the basepoint $T = t G$ differently than the abritrary scalar