path: root/games/games.tex

\documentclass[a4paper]{scrartcl}

\usepackage[utf8]{inputenc}
\usepackage{amsmath,amssymb,amsthm}
\usepackage{pifont}
\usepackage{url}
\usepackage[left=20mm,top=20mm]{geometry}
\usepackage{booktabs}
\usepackage{hyperref}
\usepackage{subcaption}
\usepackage{mathpazo}
\usepackage{mathtools}
\usepackage{mdframed}
% \usepackage[amsmath,thmmarks]{ntheorem}
\usepackage[usenames,dvipsnames,svgnames,table]{xcolor}

\def\Z{\mathbb{Z}}

% not amsthm
% \theoremseparator{.} % normal theorem

\title{Taler Security Proofs}
\date{\today}

\newtheorem{lemma}{Lemma}
\newtheorem{theorem}{Theorem}

\theoremstyle{definition}
\newtheorem{definition}{Definition}[section]

\begin{document}


%\newcommand{randsel}{\ensuremath{\xrightarrow[\text{world}]{\text{hello}}}}
\newcommand{\randsel}[0]{\ensuremath{\xleftarrow{\text{\$}}}}

% oracles
\newcommand{\ora}[1]{\ensuremath{\mathcal{O}\mathsf{#1}}}
% oracle set
\newcommand{\oraSet}[1]{\ensuremath{\mathcal{O}\textsc{#1}}}
% algorithm
\newcommand{\algo}[1]{\ensuremath{\mathsf{#1}}}
% party
\newcommand{\prt}[1]{\ensuremath{\mathcal{#1}}}
% long-form variable
\newcommand{\V}[1]{\ensuremath{\mathit{#1}}}

\maketitle

\section{Model and Syntax}

The exchange is one entity, there is only one exchange, there are many clients
and a client can act as a merchant, a customer or both (no further distinction other than naming in the role).
By convention, names for private keys begin with $pk$ and $sk$ for secret keys.

We track $\V{countWithdraw}[\V{pkClient}]$ for each client.  The private keys of coins given to clients are stored as
$\V{wallet}[\V{pkClient}]$.  Contracts are created during deposit are tracked
as $\V{contractHashes}[\V{pkClient}]$.  The exchange keeps track of $\V{spent}[\V{pkCoin}]$ and $\V{refreshCommit}[\V{pkCoin}]$ and $\V{refreshFail}[\V{pkCoin}]$.


Simplification:  No partial spending, only one denomination.

\subsection{Algorithms}
The Taler e-cash system is defined by the following algorithms.

\begin{itemize}
  \item \algo{EKeygen}():  Probabilistic algorithm executed by the exchange, outputs a key pair $(\V{skE}, \V{pkE})$.

  \item \algo{CKeygen}():  Probabilistic algorithm executed by customers, outputs a key pair $(\V{skU}, \V{pkU})$.
  \item \algo{Withdraw}(\prt{E}(\V{skE}, \V{pkE}, \prt{U}(\V{skU}, \V{pkU})):  Interactive protocol between exchange and user.

    Increases $countWithdraw[pkU]$ by one, adds the resulting coin to the wallet $wallet[pkU]$.
  \item \algo{Spend}(contract, pkClient, skCoin, pkReceiver):  Probabilistic algorithm. Signs a deposit permission for a particular contract.
    Adds $contract$ to $contractHashes[pkClient]$.
  \item \algo{Deposit}(\prt{E}(\V{skE}, \V{pkE}), \prt{M}(\V{skU}, \V{depositPermission})):
  Interactive protocol between the exchange and a customer (acting as merchant).

  Marks the coin with public key $pkCoin$ in the deposit permission as $spent[pkCoin] := 1$.

  On double-spending, return the protocol transcript of the deposit/refresh.  On success, returns exchange's signature over the request.
  \item \algo{Refresh}(\prt{E}(\V{skE}, \V{pkE}), \prt{U}(\V{skU}, \V{pkU}, \V{skCoin})):
  Interactive protocol between exchange and user.  Marks the coin with secret key $skCoin$ as spent.  If the user plays honestly,
    they will store the unlinkable change they obtain in their wallet.  If \prt{U} plays dishonestly, the coin will be marked
    as spent without anything in return.
  \item \algo{Link}(\prt{E}(\V{skE}, \V{pkE}), \prt{U}(\V{skU}, \V{pkU}, \V{skCoin})):
  Interactive protocol between exchange and user.
  If \V{skCoin} is the secret key of a coin that was refreshed, adds a coin that resulted from the refresh to the user's wallet.
\end{itemize}

\subsection{Oracles}

We define the following oracles:

\begin{itemize}
  \item $\ora{AddClient}()$:
    Creates a new client, sets $countWithdraw$ for the client to $0$, sets $wallet[pkClient] := \{\}$.
    Returns the public key of the client.

  \item $\ora{WithdrawAsUser}(pkClient)$:  Do a withdraw from the perspective of a user.  The adversary
    controls the user, the simulator the exchange.

  \item $\ora{WithdrawAsExchange}(pkClient)$:  Do a withdraw from the perspective of a exchange.  The adversary
    controls the exchange, the user is simulated.

  \item $\ora{RefreshAsUser}$  Do a withdraw from the perspective of a user, i.e. the adversary sends messages that the user would send.

    The adversary obtains the protocol transcript from the \algo{Refresh} protocol.

  \item $\ora{RefreshAsExchange}$  Do a withdraw from the perspective of the exchange, i.e. the adversary sends messages that the exchange would send.

    The adversary obtains the protocol transcript from the \algo{Refresh} protocol.

  \item $\ora{Spend}(contractHash, pkSpender, pkCoin, pkReceiver)$
    Make a customer sign a deposit permission.  Returns the deposit permission on success, or $\bot$ if the $skSpender$ does not have enough coins.

  \item $\ora{Share}(pkSender, pkReceiver)$:

    Shares one random, previously unshared coin in the wallet of $pkSender$ with $pkReceiver$.

  \item $\ora{CorruptClient}(pkClient)$:

    Used by the adversary to corrupt a client.  Marks the client as corrupted and gives the adversary the
    client's private key, wallet and signed contract hashes.
\end{itemize}

\begin{mdframed}
The difference between algorithms and interactive protocols
is that the ``pure'' algorithms only deal with data, while the interactive protocols
take ``handles'' to parties that are communicating in the protocol.  The adversary can
always execute algorithms that don't depend on handles to communication partners.
However the adversary can't run the interactive protocols directly, instead it must
rely on the interaction oracles for it.  Different interaction oracles might allow the
adversary to play different roles in the same interactive protocol.

While most algorithms in Taler are not probabilistic, we still say that they are, since
somebody else might come up with an instantiation of Taler that uses probabilistic algorithms,
and then the games should still apply.

All algorithms need to be polynomial time, but this is already implied by the
definition of the adversary and simulator.

While we do have a \algo{Deposit} protocol that's used in some of the games, having a deposit oracle is not necessary
since it does not give the adversary any additional power.
\end{mdframed}



\section{Games}

\newcommand{\comment}[1]{\\ {\small \textcolor{blue}{({#1})}}}


\subsection{Anonymity}
Anonymity game with adversary $\prt{A}$.
Let \oraSet{Anon} stand for access to the oracles \ora{AddClient}, \ora{WithdrawAsExchange}, \ora{Spend},
\ora{RefreshAsExchange}, \ora{Share}, \ora{CorruptClient}

\bigskip
\noindent $\mathit{Exp}_{\prt{A}}^{anon}(1^\lambda, \kappa)$:
\vspace{-0.5\topsep}
\begin{enumerate}
  \setlength\itemsep{0em}
  \item $(\V{skE}, \V{pkE}, \V{skM}, \V{pkM}) \leftarrow \prt{A}()$ \\
    Our adversary controls the exchange and a merchant.
    \comment{Note that this only means that \prt{A} has the exchange secret key, it
    does not automatically receive transcripts and it does not have access to any exchange data structures \textit{unless} indicated by the oracles}
  \item $(\V{pkU}_0, \V{pkU}_1, \V{contract}_0, \V{contract}_1) \leftarrow \prt{A}^{\oraSet{Anon}}()$ \\
    Our adversary creates two users and two contract,
    along with some coins open which it calls oracles freely.
  \item Return 0 either if $\V{pkU}_1$ or $\V{pkU}_2$ are not distinct
    registered users, or if any coins are left in a unfinished spent
    state without either completing the spend through a deposit or refreshing the coin.
    \footnote{In general, there is lag during which coins remain in an
    unfinished spent state, but our wallet will not use those cons in
    another transaction until refreshing them.}
  \item $b \randsel{} \{0,1\}$
    \comment{Random bit selected by challenger}
  \item Select unspent coins $\V{pkC}_0$ and $\V{pkC}_1$ from
    the wallets of $\V{pkU}_0, \V{pkU}_1$, respectively.  Return 0
    if either $\V{pkU}_0$ or $\V{pkU}_1$ has no unspent coin.
  \item $\V{dp_1} \leftarrow \algo{Spend}(\V{contract}_b, \V{pkU}_b, \V{pkC}_b, \V{pkM})$, \\
        $\V{dp_2} \leftarrow \algo{Spend}(\V{contract}_{(1-b)}, \V{pkU}_{(1-b)}, \V{pkC}_{(1-b)}, \V{pkM})$ \\
    Spend these two coins without revealing the customer's identity to the adversary.
  \item $\algo{Deposit}(\prt{E}(\V{skE}, \V{pkE}), \prt{A}(dp_1))$, \\
        $\algo{Deposit}(\prt{E}(\V{skE}, \V{pkE}), \prt{A}(dp_2))$ \\
    Deposit these two coins with the adversary controlled merchant.
  \item $b' \leftarrow \prt{A}^{\oraSet{Anon}}()$
    \comment{Ask adversary to find out mapping between users and contracts as determined by $b$}
  \item Let $\cal U \supseteq \{ \V{pkU}_1, \V{pkU}_2 \}$ consist
    of the users who know, or could learn through linking, either
    $\V{skC}_0$ or $\V{skC}_1$, aka these coin's {\em ownership set}.
    Return 0 if $\cal U$ contains either any user corrupted by \prt{A}
    or any user who ran the linking protocol.
    \comment{TODO: Add linking protocol to \oraSet{Anon}, but simplify this text if the linking protocol can be restrited to corrupted users}
  \item if $b = b'$ return 1, otherwise return 0
\end{enumerate}


\paragraph{Intuition:}  Users are anonymous if there is no adversary that can win this game,
since then two users can spend money, but the adversary is not able to say who purchased what.

\paragraph{Todo:}  Show that/how in our model, this also implies that anonymous purchases are independent from \emph{each other}.

\begin{mdframed}
There are two kinds of games found for anonymity in the
literature, one is based in indistinguishability (between two users or coins) and
the other one on simulation.  The latter is claimed to be more powerful in \cite{izabachene2013divisible}.

Note that our game lets both users spend, which means we don't need to ``magically'' come up for
a fresh coin for the only user who just spent one.  If only one coin is spend and we don't replace it,
the adversary can exhaust wallets to see who spent.  We can avoid this, since we have contract identifiers
and can rely on those.

The ``\dots AsUser'' oracles are not given to the adversary, since they play as the exchange and thus
allowing them to talk to themselves does not make sense.
\end{mdframed}

%\subsection{Unforgeability}
%\begin{enumerate}
%  \setlength\itemsep{0em}
%  \item $(skExchange, pkExchange) \leftarrow \algo{EKeygen}()$ 
%  \item $(r_1, r_2) = \prt{A}^{\ora{*}}()$
%    \comment{Two different receipts for deposit from the exchange / relayed by merchant}
%  \item return $1$ if $r_1, r_2 \neq \bot$, $r_1 \neq r_2$ and $r_1 = S(pkExchange, pkCoin, h_1)$ but $r_2 = S(pkExchange, pkCoin, h_2)$
%    with $h_1 \neq h_2$ for some $pkCoin$.
%\end{enumerate}

%Is this the right game?  We could also base it on not being able to spend more than was withdrawn.  Note that in the game above, we only look
%at receipts and the coin doesn't even need to be valid directly.

\subsection{Fairness}
Intuition: Adversary wins if a non-corrupted user can't obtain a proof-of-spending or unlinkable change.

Let \oraSet{Fair} stand for access to the oracles \ora{AddClient}, \ora{WithdrawAsExchange}, \ora{Spend},
\ora{RefreshAsExchange}, \ora{Share}, \ora{CorruptClient}

\bigskip
\noindent $\mathit{Exp}_{\prt{A}}^{fair}(1^\lambda, \kappa)$:
\vspace{-0.5\topsep}
\begin{enumerate}
  \setlength\itemsep{0em}
  \item $(skE, pkE) \leftarrow \mathrm{EKeygen}()$ 
  \item $C_0 \leftarrow \prt{A}^{\oraSet{Fair}}(pkExchange)$
  \item Let $U$ be the user that has $C_0$ in their wallet.  If no such $U$ exists, return 0.
  \item Let $C_0, \dots, C_n$ be the coins reachable via \algo{Link} from $C_0$.
    \comment{When $C_0$ was not refreshed, $n=0$ and $C_n = C_0$}
  \item If $U$ was corrupted or \ora{Share} was called with any of $C_0, \dots, C_n$, return 0.
  \item $R \rightarrow \algo{Refresh}(\prt{B}(skExchange, pkExchange), \prt{U}(U, C_n))$
  \item If $R$ indicates a successful refresh, return $0$.
    If $R$ indicates double spending with contract $h$ and $h \in contractHashes[U]$, return 0.
    Otherwise return 1.
\end{enumerate}

\paragraph{Note:}  This also covers the case where the deposit receipt from the exchange is forged by the merchant.


\subsection{Unforgability} % Exculpability?

Let \oraSet{Forge} stand for access to the oracles \ora{AddClient}, \ora{WithdrawAsExchange}, \ora{Spend},
\ora{RefreshAsExchange}, \ora{Share}, \ora{CorruptClient} ???

\bigskip
\noindent $\mathit{Exp}_{\prt{A}}^{forge}(1^\lambda, \kappa)$:
\vspace{-0.5\topsep}
\begin{enumerate}
  \setlength\itemsep{0em}
  \item $(skE, pkE) \leftarrow \mathrm{EKeygen}()$ 
  \item $(C_0, \dots, C_\ell) \leftarrow \mathcal{A}^{\oraSet{Forge}}(pkExchange)$
  \item Our adversary wins if they made at most $\ell$ withdrawals
    but $C_0, \dots, C_\ell$ are all distinct valid unspent coins.
\end{enumerate}
% TODO: We should clarify that refresh spends the coin


\subsection{Income Transparency}
Intuition: Adversary wins if money is in exclusive control of corrupted players but the exchange has no record of withdrawal or spending for it.

Let \oraSet{Income} stand for access to the oracles \ora{AddClient}, \ora{WithdrawAsExchange}, \ora{Spend},
\ora{RefreshAsExchange}, \ora{Share}, \ora{CorruptClient}

\bigskip
\noindent $\mathit{Exp}_{\prt{A}}^{income}(1^\lambda, \kappa)$:
\vspace{-0.5\topsep}
\begin{enumerate}
  \setlength\itemsep{0em}
  \item $(skE, pkE) \leftarrow \mathrm{EKeygen}()$ 
  \item $(C_1, \dots, C_\ell) \leftarrow \mathcal{A}^{\oraSet{Income}}(pkExchange)$
  \item Augment the wallets of all non-corrupted users with their
    transitive closure using the \algo{Link} protocol.
    Mark all coins in wallets of non-corrupted users as spent.
  \item Let $w$ denote the number of coins withdrawn by corrupted users.
    Also let $b$ denote the number of coins lost in refresh operations
    with false planchets.  Our adversary wins if both $\ell > w$ and 
    ${b \over \ell - w'} \le 1-{1\over\kappa}$ with $C_1, \dots, C_\ell$
     all being distinct valid unspent coins.
\end{enumerate}


Note that we want to show in the end that the probability of winning one Income Transparency game is at most $1/\kappa$.
This is why $\kappa$ does not appear directly in the proof.

\subsection{Others?}
Let adversary distinguish between freshly withdrawn coin and coin obtained via refresh protocol.  Why?

Camenisch-style fair exchange and endorsements.  Should not be too much work, games are already
given in literature.

\section{Instantiation}

Let $G \in \mathbb{E}$ be the generator of the Ed25519 curve (with Edwards coordinates).  

\begin{itemize}
  \item \algo{EKeygen}():  Generate an RSA key pair of length $k$ and return it.
  \item \algo{CKeygen}():  Generate an EdDSA key pair and return it.
  \item \algo{Withdraw}(\prt{E}(\V{skE}, \V{pkE}), \prt{U}(\V{skU}, \V{pkU})):
    \begin{enumerate}
      \item \prt{U} selects blinding factor $r \randsel \Z_N^*$, coin secret $\V{skC} \randsel \Z_{|\mathbb{E}|}$, computes
        $\V{pkC} = \V{skC} \cdot G$, $\overline{M} = r \cdot H(\V{pkC})$ and sends $\overline{M}$ to $\prt{E}$.
      \item \prt{E} receives $\overline{M}$ and sends back $\overline{M}^d \bmod N$ to \prt{U}.
    \end{enumerate}

    Thus the protocol transcript is $(\overline {M}, \overline{M}^d \bmod N)$.
  \item \algo{Spend}(contract, skCoin, pkReceiver):  TODO

    The deposit permission is computed as
    \begin{equation*}
      (\V{sig}, \V{pkCoin}) = (\algo{Sign}(skCoin, (contract, pkReceiver)), \V{skCoin} \cdot G)
    \end{equation*}

    
  \item \algo{Deposit}(\prt{E}(\V{skE}, \V{pkE}), \prt{M}(\V{skU}, \V{depositPermission})):
    TODO
  \item \algo{Refresh}(\prt{E}(\V{skE}, \V{pkE}), \prt{U}(\V{skU}, \V{pkU}, \V{skCoin})):
    The protocol transcript is 
    \begin{equation*}
      (\V{pkCoin}, sig, T_1, \dots, T_\kappa, \overline{M}_1, \dots, \overline{M}_\kappa, \gamma, \tilde{t}_1, \dots, \tilde{t}_\kappa, \overline{M}_\gamma^d \bmod N)
    \end{equation*}

    where $t_i \randsel U$, $T_i = t_i \cdot G$, $s_i = ECDH(t_i, pkCoin)$, $r_i = PRF_{pkCoin}(s_i)$, $M_i = PRF_{pkCoin+1}(s_i)$, $\overline{M}_i = r_i \cdot M_i $ 
  \item \algo{Link}(\prt{E}(\V{skE}, \V{pkE}), \prt{U}(\V{skU}, \V{pkU}, \V{linkSecret}, \V{skCoin})):
    TODO
\end{itemize}

\section{Proofs}

\subsection{Anonymity}



%We can describe a simple blinding game for an RSA key pair $(n,e,d)$ and
%generators $M(\cdot)$ and $B(\cdot)$ for elements of $\Z/n\Z$ whose
%parameters we need not specify: 
%We take $m_0,m_1$ from $M$ and $b_0,b_1$ from $B$ and give our adversary
%$\cal A$ the unordered pairs of withdrawals $\{ m_0^d b_0, m_1^d b_1 \}$
%and deposits $\{ m_0^d, m_1^d \}$.  $\cal A$ wins if it can correctly
%match the withdrawals and deposits.
%
%\begin{lemma}\label{RSA_blind_signatures}
%Assume adversary $\cal A$ with an advantage in this blinding game for
%some $M_0(\cdot)$ and $B_0(\cdot)$ whatever their parameters.  There is
%a machine $\cal A'$ that identifies $B_0$ as opposed to a uniform
%distribution $U(Z/nZ)$ on $Z/nZ$.
%\end{lemma}
%
%\begin{proof}
%$\cal A'$ plays the blinding game with $\cal A$ taking $M$ to be $M_0$
%and $B$ to be $X$.  $\cal A$ either guesses correctly or incorrectly.
%If $\cal A$ guesses correctly, then $\cal A'$ guesses that yes $X$ is
%$B_0$.
%
%If $X$ is $B_0$ then $\cal A$ guesses correctly with advantage $\epsilon$, meaning
%  $P[ \textrm{$\cal A$ correct} | X=B_0 ] = 1/2+\epsilon$
%and
%  $P[ \textrm{$\cal A$ correct} | X=U ] = 1/2$.
%We imagine A' is given uniform trials to guess X=F vs X=U, so that
%  $P[X=F] = 1/2$ too,
%and 
%  $P[\textrm{$\cal A$ correct}] = 1/2 + \epsilon/2$.
%Now $\cal A'$ has an advantage in guessing if $X$ is $B_0$ or uniform correctly by
%Bays rule
%  $P[ \textrm{$\cal A$ correct} | X=B_0 ] P[X=B_0] = P[ X=B_0 | \textrm{$\cal A$ correct} ] P[A correct]$
%so
%  $P[ X=F | \textrm{$\cal A$ correct} ]
%  = 1/2 (1/2+\epsilon) / (1/2 + \epsilon/2)
%  = (1/2+\epsilon) / (1+\epsilon)
%  = 1 - 1/2 / (1+\epsilon)$.
%\end{proof}
%
%\begin{lemma}\label{interleaved}
%Let $X$ and $Y$ denote generators for elements in $\Z/n\Z$, taking
%unspecified parameters.  Let $I$ denote an interleaved sequence from
%$X$ and $Y$ taking concatenated parameters.  If some adversary has
%a non-ngeligable advnatage in distinguishing $I$ from $U(Z/nZ)$
%then some adversary has a non-ngeligable advnatage in distinguishing
%$J$ from $U(Z/nZ)$ wher eitehr $J=X$ or $J=Y$.
%\end{lemma}
%
%\begin{proof}
%Exercise for the reader.
%\end{proof}
%
%\begin{lemma}\label{PRF_composed_wth_ECDH}
%...
%\end{lemma}
%
%\begin{proof}
%...
%\end{proof}
%
%\begin{theorem}
%
%... $\cal A$ ...
%\end{theorem}
%
%\newcommand\pkCoin{pkCoin}
%
%\begin{proof}[Proof-ish]
%We consider the coin $\pkCoin$ of $U_b$ selected and spent by the
%game/environment starting from line 5, as well as the coin of
%$U_{1-b}$ that was unspent unshared in line 5, denoted $\pkCoin'$.
%
%We cannot corrupt either $U_0$ or $U_1$ nor share either $\pkCoin$ or
%$\pkCoin'$.  We may however add a spend or refresh of $\pkCoin'$ if
%$\cal A$ does not do so.  It follows that an advantage for $\cal A$
%in guessing $b'$ for our anonymity game yields an advantage in the
%blinding game given by the creation of $\pkCoin$ and $\pkCoin'$ in
%line 2 together with spending them in line 6. % and their deposit in line 7 
%
%In creating each of $\pkCoin$ and $\pkCoin'$, $\cal A$ either
%(1) invokes the withdrawal oracle directly, or else (2) applies the
%refresh oracle to some previous withdrawn coin.  These invokations
%together provide the $B_0$ in Lemma \ref{RSA_blind_signatures}.
%It follows that a non-negligible advantage for $\cal A$ yields a
%non-negligible advantage for the adversary $\cal A'$ who distinguishes
%this $B_0$ from a uniform distribution $U(Z/nZ)$ on $Z/nZ$.
%We cannot know if $\cal A$ constructs $B_0$ with direct withdrawals,
%refresh operations, or both.
%
%In the direct withdrawal only case, any advantage yields an advantage
%in distinguishing the FD-PRNG used from a uniform distribution,
% in which case we are done. 
%In the refresh only case, any advantage yields an advantage
%in distinguishing from uniform the compostion of the FD-PRF and ECDH
% used, in which case we  conclude by Lemma \ref{PRF_composed_wth_ECDH}.
%In mixed cases, we obtian one of the same two conclusions,
% by Lemma \ref{interleaved}.
%\end{proof}





\paragraph{``Proof sketch''.}  Proof by looking at withdraw/deposit/refresh transcripts seen by the adversary.  Do game hopping, replace
everything that's not random by something random (with computationally indistinguishable distribution) until everything that the adversary
could see in a game has the same probability, and he must win with probability $1/2$.


\subsection{Fairness}

\begin{proof}[Proof-sketch]
We required that any refresh operations were run to conclusion, 
which makes sense with our adversary $\prt{A}$ being a merchant
unable to control either the customer or exchange.  It follows 
that $\prt{A}$ never called the refresh oracle on $C_n$.

As the refresh $R$ must fail, $\prt{A}$ must have the customer
spend $C_n$, and then either deposit $C_n$, refresh $C_n$, or
spend $C_n$ with another merchant.
In any case, $\prt{A}$ must not return the correct receipt to
the customer, doing so concludes the transaction honestly.  

If $\prt{A}$ deposits $C_n$, then the customer would also obtain
the correct receipt from exchange by doing a refresh, so the
adversary must distract them with signed message from the exchange
indicating double spending or previous refresh. In either subcase,
$\prt{A}$ provides signatures by both $C_n$ and $\V{pkE}$.

If $\prt{A}$ either refreshes or spends $C_n$, then they provide
a signature by $C_n$ too.

TODO: Anything more about signature reduction?
\end{proof}

We have stated the game and theorem with $\prt{A}$ controlling only
the merchant, but even if they control the exchange as well they
still cannot forge the signature by $C_n$.  An exchange has access
to more oracles however so they can take actions like dropping the
refresh connection.  Attacks like these can only be thwarted with
the aid of authorities who can witness the attack, like our auditor.


\subsection{Unforgeability} % Exculpability?

\begin{theorem}
In the random oracle model,
if the RSA known-target inversion problem (RSA-KTI) is hard, then
Taler is polynomially-secure against one-more forgery attacks.
% by probabilistic polynomially time adversaries.
\end{theorem}

\begin{proof}
We consider a probabilistic polynomially time adversary $\cal A$ with
a non-negligible advantage for winning the unforgeability game
 $\mathit{Exp}_{\prt{A}}^{forge}(1^\lambda, \kappa)$.
We describe an RSA Chosen-Target Inversion Problem (RSA-CTI)
 \cite[Definition 3]{RSA-FDH-KTIvCTI} % or \cite[DEfinition 6.1]{OneMoreInversion}.
won by $\cal A$. 

We let $C_{\ell+1}, \ldots, C_m$ denote all the spent coins arising
from the operation of $\cal A$. % Also let $C_{m+1}, ..., C_n$ denote
% the unsigned planchets used by refresh oracle call. 
% Now set $Y_i = FDA_N(C_i)$ for $0 \le i \le n$. 
% DISCUSS: We could exploit some of the power of RSA-CTI to dispose
% of these planchets.  I think this seems unnecessary, but maybe it
% might refines our usage of ROM or something.
We know $\cal A$ made at most $m$ withdrawal and refresh oracle
queries to obtain the $l+1$ RSA signatures %, aka inversions,
 on the $Y_i := FDA_N(C_i)$ with $0 \le i \le m$. 
%
It follows that $\cal A$ has produced one-more forgery in the sense
 of \cite[Definition 4 \& 5, pp. 369]{Pointcheval_n_Stern}, so
RSA-KTI cannot be hard by \cite[Theorem 12]{RSA-FDH-KTIvCTI}.
%
% So $\cal A$ wins this RSA-CTI game with its random sampling to produce
% $Y_i$ replaced by our PRF $FDA_N$, which requires nothing since we're
% already working in the stronger random oracle model anyways.
% We finally exploit the full random oracle model to apply 
% \cite[Theorem 6]{RSA-FDH-KTIvCTI} to produce an adversary who breaks
% RSA-KTI.
% DISCUSS CONTINUED: This argument directly from Theorem 6 seems wrong
% because the ROM in \cite[Lemma 13]{RSA-FDH-KTIvCTI} does not appear.
% We should figure out what's really going on.
\end{proof}


\subsection{Income Transparency}

\begin{proof}[Proof-sketch]
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
unforgeability.  We may transform our our adversary $\cal A$ into
any adversary for the protocol that commits to full planchets by
rewinding $\cal A$ to try each $\gamma \in 1,\ldots,\kappa$ during
each refresh operation to obtain all planchets.  We observe a hash 
collision if this fails to provide the correct coins. 

We consider the refresh operations in which $\cal A$ in which
$\cal A$ submits a false planchets for some choice of $\gamma$. 
In these, we may assume $\cal A$ submits a false planchet for at most
one choice of $\gamma$, as otherwise the refresh always fails.
We let $f$ denote the number of these in which a non-corrupted user
could obtain the coin consumed in the refresh via the linking protocol.
It follows from unforgeability that $\ell \le w + f$ because
any refresh without a false planchet results in that coin being
obtainable by a non-corrupted user and thus being marked as spent.

As our $\gamma$ are chosen randomly, any given refresh with a false
planchet has a $1-{1\over\kappa}$ chance of contributing to $b$,
so $E[{b \over f}] = 1-{1\over\kappa}$.  It follows that 
$P[{b \over \ell-w} \ge (1-{1\over\kappa})] = 1/2 > {1\over\kappa}$.
\end{proof}

% injectivity of the ECDH operation seems like a red herring???



To win the game, the adversary must produce enough coins that are not in the wallet of any non-corrupted user, but withdraw little
coins via corrupted users.

\begin{lemma}
  The signatures on $C_1, \dots, C_\ell$ must have been obtained by using either \ora{Withdraw}, \ora{RefreshReveal} or \ora{Link}.
\end{lemma}

\begin{lemma}
  \ora{Link} can not be used to get a coin from a non-corrupted peer.
\end{lemma}

\begin{lemma}
  To win the Income Transparency game, the adversary must call $\ora{RefreshReveal}$ at least $(\kappa V_r - V_w) > 0$ times
  in a way that causes the linking step to fail.  (This implies unforgeability.)
\end{lemma}

\begin{lemma}
  The probability to successfully use \ora{RefreshCommit} and \ora{RefreshReveal} in a way that causes \algo{Link} to return $\bot$ is at most $1/\kappa$.
\end{lemma}

\begin{theorem}
  The adversary wins the Income Transparency game with with probability at most $1 / \kappa$.
\end{theorem}

FIXME:  We should also include what the expected ``untaxed'' money for the adversary is for each won game, vs. the money wasted.

\section{Standard Definitions}
\begin{definition}[One-more forgery]
For any integer $\ell$, an $(\ell, \ell + 1)$-
forgery comes from a probabilistic polynomial time Turing machine $\mathcal{A}$ that can
compute, after $\ell$ interactions with the signer $\Sigma$, $\ell + 1$ signatures with nonnegligible
  probability. The ``one-more forgery'' is an $(\ell, \ell + 1)$-forgery for some
integer $\ell$. 
\end{definition}

Taken from \cite{pointcheval1996provably}.  This definition applies to blind signature schemes in general.
Intuition:  EUF-CMA is not strong enough for blind signatures,
since attacker can choose the message (without going through a hash function before signing).

\begin{definition}[RSA-KTI]
  Game (security parameter $k$, $m : \mathbb{N} \rightarrow \mathbb{N}$, $\mathcal{A}$ adversary with access to RSA inversion oracle \ora{Inv}):
  \begin{enumerate}
    \item $(N, e, d) \leftarrow \mathsf{KeyGen}(k)$
    \item $y_i \leftarrow_R \mathbb{Z}_N^*$ for $i \in 1, \dots, m(k) + 1$
    \item $(x_1, \dots, x_{m(k) + 1}) \leftarrow \mathcal{A}^{\ora{Inv}}(N, e, k, y_1, \dots, y_{m(k) + 1})$
    \item $\mathcal{A}$ wins if it made at most $m(k)$ oracle queries and $x_i^e \equiv y_i \pmod N$
  \end{enumerate}
\end{definition}

From \cite{bellare2003onemore}.  Assumption to prove security of RSA blind signatures.  Equivalent to RSA-CTI.

\section{Questions/Todo}
\begin{itemize}
  \item We trivially get endorsed e-cash, should we add the games / definitions?
\end{itemize}


\bibliography{lit}
\bibliographystyle{alpha}

\end{document}