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{enumitem}
% \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}[section]
\newtheorem{theorem}[lemma]{Theorem}
\newtheorem{corollary}[lemma]{Corollary}

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

\begin{document}


% uniform random selection from set
\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}}}

% probability with square brackets of the right size
\newcommand{\Prb}[1]{\ensuremath{\Pr\left [#1 \right ]}}

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

\maketitle


%%%%%%%%%
% TODOS
%%%%%%%%
% 
% * properly characterize what having "Anonymity", "(Weak/Strong) Income Transparency" etc means
%   in terms of winning the games
% * our theorems don't really mention the security parameters "in the output",
%   shouldn't we be able to talk about the bounds of the reduction?
% * fairness is not a reduction or game hop
% * the "tracking variables" should probably be part
%   of the oracles, not of the protocol syntax
% * the concept of "finishing operations" before the next step in a game
%   is unclear, what power does this give the adversary?
% * do we need the deposit oracle?  cutting down the tree does not have it ...
% * adding the link oracle means we must also account for it in fairness and
%   unforgeability
% * can we formulate games so they don't refer to "failed refresh" directly?
%   (since in some instantiations, refreshing can't fail)
% * at least for fairness, we have to think more about Deposit, and
%   whether there should be a separate oracle for it
%


% TODO:
% - note about double spending vs overspending

\section{Model and Syntax}

We consider a single exchange with many users.  The users can act as a
merchant, a customer or both, with no further distinction other than in naming.
We prefix public and secret keys with $pk$ and $sk$, following standard
convention.  For succinctness, the public key of a coin always implicitly has a
denomination (in form of the exchange's denomination public key) associated
with it.

Every denomination has an associated financial value; this mapping is not
chosen by the adversary but is a system parameter.  We mostly ignore the
denomination values here, including their impact on both bandwidth and
anonymity, in keeping with existing literature.  For anonymity, we believe this
amounts to assuming that all users have similar financial behavior.  
We note logarithmic bandwidth demands denominations distributed by at least 
powers of a fixed constant, like two.  

We do not include fees taken by the exchange in our model.  Reserves are also
omitted, conceptually every user has exactly one bank account that they
withdraw from, the bank account balance starts at zero and can go negative
without any limit.  
% TODO: Say roughly: In the real world Taler depends on account balances being only positive,
% but this model simplifies our games and security arguments.  ??? 

Coins can be partially spent by specifying a fraction $f \in \mathbb{Q}$. 
Our refresh protocol cannot then give change below the smallest denomination 
though. % so doing this either looses money or requires the exchange permit users to break their anonymity for small transactions.

The spending of multiple coins is modeled non-atomically: to spend multiple coins,
they must be spent one-by-one.  The individual spend/deposit operations are correlated
by a unique identifier for the transaction.  In practice this identifier is the hash
of a nonce and the contract terms that merchant and customer agreed upon.

Our model tracks the following data for users:
\begin{itemize}
\item $\V{valueWithdrawn}[\V{pkUser}]$ contains of the values
 withdrawn by each user $\V{pkUser}$,
\item $\V{wallet}[\V{pkUser}]$ contains sets of the users coins records,
 which individually consist of the coin private keys and denomination signatures.
\item $\V{acceptedContracts}[\V{pkUser}]$ contains the sets of contracts accepted by the user
  during spending operations, together with coins spent for it and their contribution.
\end{itemize}
The overspending database of the exchange is modeled by $\V{deposited}[\V{pkCoin}]$ and
$\V{refreshed}[\V{pkCoin}]$, which records the protocol transcript of deposit and refresh
operations respectively.

We say that a coin is \emph{fresh} if it appears in neither the $\V{deposited}$
or $\V{refreshed}$ lists nor in $\V{acceptedContracts}$.  We say that a coin is
being $\V{overspent}$ if adding a transcript to $\V{deposited}$ or
$\V{refreshed}$ would cause the total value of transcripts in both lists to
exceed the value of the denomination.


\subsection{Algorithms}

The Taler e-cash scheme is modely by the following probabilistic\footnote{Our
Taler instantiations are not necessarily probabilistic, but we do not want to
prohibit this for other instatiations} polynomial-time algorithms and
protocols.  The notation $\prt{E}(X_1,\dots,X_n)$ / $\prt{U}(X_1,\dots,X_n)$
stands for a party (Exchange or User) in an interactive protocol, with
$X_1,\dots,X_n$ being the private inputs contributed by the party to the
protocol.

\begin{itemize}
  \item $\algo{ExchangeKeygen}(1^{\lambda}, 1^{\kappa}, \V{M})$:  Algorithm executed by the exchange
    that outputs a key pair $(\V{skE}, \V{pkE})$, which contain both the
    signing key and the denomination keys for the exchange.  The financial
    value assigned to a denomination public key $d$ is determined by
    $\V{M}(d)$.  Both $\lambda$ and $\kappa$ are security parameters.

  \item $\algo{UserKeygen}(1^\lambda{})$:  Algorithm executed by merchants and customers
    that outputs a key pair $(\V{skU}, \V{pkU})$.  We refer to this key pair by $(\V{skM}, \V{skM})$ when
    the user acts as a merchant.
    \comment{pkDenom needs to appear here}

  \item \algo{Withdraw}(\prt{E}(\V{skE}, \V{pkU}), \prt{U}(\V{skU}, \V{pkE}, \V{pkDenom})):
    Interactive protocol between exchange and user to withdraw a single coin of
    a particular denomination.
    \comment{A planchet like pkCoin needs to be an argument here, no?  How do we handle the signature though?  Also skDenom.  }

    % pkDenom needs to appear in ExchangeKeygen

  \item \algo{Spend}(contract, \V{f}, \V{pkUser}, \V{skCoin}, pkReceiver):
    Algorithm to produce and sign a deposit permission \V{depositPermission}
    for a particular contract.  The fraction $0 < \V{f} \le 1$ determines the
    fraction of the coin's value that will be spent.

  \item \algo{Deposit}(\prt{E}(\V{skE}, \V{pkE}), \prt{M}(\V{skU}, \V{depositPermission})):
    Interactive protocol between the exchange and a user, who acts as a merchant.

    In the deposit permission, there are coin public keys $\V{pkCoin}$
    corresponding to $\V{skCoin}$.
    If $\V{pkCoin}$ is being overspent, we return the protocol transcript
    of the previous deposits and refreshes.  

    On success, we mark $\V{pkCoin}$ spent in $\V{deposited}[\V{pkCoin}]$ and
    return the exchange's signature over the request.

  \item \algo{Refresh}(\prt{E}(\V{skE}, \V{pkU}), \prt{U}(\V{skU}, \V{pkE}, \V{skCoin})):
    Interactive protocol between exchange and user.

    If $\V{pkCoin}$ (derived from \V{skCoin}) is being overspent, then
    we return the protocol transcript of the previous deposits and refreshes.

    Assuming otherwise, we mark $\V{pkCoin}$ as refreshed in $\V{refreshed}[\V{pkCoin}]$.

    If the user \prt{U} plays honestly, the unlinkable 
    change they obtain will be stored in their wallet $wallet[\V{pkU}]$.
    If \prt{U} is caught playing dishonestly, the coin's refresh transcript
    will be marked as spent without anything in return.
    
    Note that some instantiation (e.g. those using zero knowledge proofs) might
    not leave \prt{U} the possibility to play dishonestly.

  \item \algo{Link}(\prt{E}(\V{skE}), \prt{U}(\V{skU}, \V{pkE}, \V{skCoin})):
    Interactive protocol between exchange and user.
    If \V{skCoin} is the secret key of a coin that was refreshed, then 
    we recompute the refreshed coin and add it to to the user's wallet $wallet[\V{pkU}]$.

\end{itemize}

\subsection{Oracles}

We define the following oracles:

\begin{itemize}
  \item $\ora{AddUser}()$:
    Creates a new user, sets $valueWithdrawn$ for the user to $0$, sets $wallet[pkUser] := \{\}$.
    Returns the public key of the user,

  \item $\ora{Withdraw}(pkUser, pkDenom)$:  Do a withdraw.
    Effectively the adversary is an active man-in-the middle between the user and the ``real'' exchange.

    The adversary obtains the protocol transcript, but does not gain access to the exchange's database directly.

    % FIXME: talk about share

  \item $\ora{Refresh}()$:  Do a withdraw.
    Effectively the adversary is an active man-in-the middle between the user and the ``real'' exchange.

    The adversary obtains the protocol transcript, but does not gain access to the exchange's database directly.

  \item $\ora{Link}(pkUser)$:  Force the execution ot the link protocol.  The adversary is an
    Effectively the adversary is an active man-in-the middle between the user and the ``real'' exchange.

  \item $\ora{Spend}(contractHash, pkSpender, \mathcal{T}^C, pkReceiver)$:
    Make a customer sign a deposit permission over a coin identified by
    transcript $\mathcal{T}_C$, which is either a withdraw transcript, link
    transcript or refresh transcript with coin index.  Returns the deposit
    permission on success, or $\bot$ if the $skSpender$ does not have enough
    coins.

    Adds $\V{contract}$ to $\V{acceptedContracts}[pkUser]$ and
    initializes $\V{spent}[\V{pkCoin}]$.

  \item $\ora{Share}(\mathcal{T}^C, pkReceiver)$:

    Shares a coin (identified by withdraw/refresh/link transcript $\mathcal{T}^C$ with the user identified
    by $pkReceiver$.  Used by the adversary in attempts to violate income transparency.

    Note that this trivially violates anonymity (by sharing with corrupted user), thus the usage must
    be restricted most other games.
    \comment{ENGLISH to / from ?}

    % the share oracle is the reason why we don't need a second withdraw oracle

  \item $\ora{AddCorruptUser}(pkUser)$:
    Used by the adversary to add a corrupted user, giving
    it permanent access to the user's private key, wallet and accepted contracts.

  \item $\ora{Deposit}(depositPermission)$:
    Give a deposit permission to the exchange.  If the deposit permission is valid and the coin is not overspent,
    the exchange adds it to $spent[pkU]$ for the user $U$ identified in the deposit permission.

    This oracle does not give the adversary new information, but is used to
    model the situation where there might be multiple conflicting deposit
    permissions generated via $\algo{Spend}$, but only a limited number can be
    deposited (even though \ora{Spend} tracks spending, coin sharing can otherwise cause overspending).
\end{itemize}

% addcorruptuser and adduser+corrupt is the same,
% since corrupt would give the adversary all previous protocol
% transcripts, and we don't have any notion of forward security


The exchange does not need to be corrupted with an oracle. A corrupted exchange
is modelled by giving the adversary the appropriate oracles and the exchange
private key from the exchange key generation.

If the adversary determines the exchange's private key during the setup,
invoking \ora{Withdraw}, \ora{Refresh} or \ora{Link} can be seen as the
adversary plaing the exchange.  Since the adversary is an active
man-in-the-middle in these oracles, they can drop messages to the simulated
exchange and make up their own response.  If the adversary calls these oracles
with a corrupted user, the adversary plays as the user.

\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.


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}

\subsection{Remarks}
% I've moved these remarks here, since it does not make sense to talk about details
% without introducing the syntax of the model.

Anonymous e-cash schemes all require protections against network, etc. failures,
and hence require a refresh operations.  If this refresh operations also
provided partial spending, which seems logical, then refreshes can be run after
spends, which invalidates assumptions in anonymity games.

\section{Games}

We have two seperate security parameters in Taler
First, our primary security parameter $\lambda$ characterizes
the security of signatures and blind signatures.

% here we can't talk about the cut-and-choose parameter yet,
% we model taxable e-cash in general and don't want to refer
% to Taler-specific implementation details.

Our second security parameter $\kappa$ is used to characterize
the assurances of Income Transparency.

For some instantiations, e.g. ones based on zero knowledge proofs, $\kappa$
might be a security parameter in the traditional sense.  However to
be useful in practice, the adversary does not need to have neglegible
success probability to win the Income Transparency game.  It suffices
that the financial losses of the adversary in the game are a deterrent, 
afterall the purpose of the game is to characterize tax evasion.

Taler does not fulfill strong Income Transparency since for Taler $\kappa \ge 3$ is a small
cut-and-choose parameter.  Instead we show that Taler satisfies Weak Income Transparency,
which is a statement about the adversary's financial loss when winning the game instead
of the winning probability.

We still characterize Income Transparency as a game, since it might be useful
for other instantiations that provide more absolute guarantees.

\subsection{Anonymity}
Intuitively, an adversary $\prt{A}$ (controlling the exchange and merchants) wins the
anonymity game if they have a non-neglegible advantage in correlating spending operations
with the withdrawal or refresh operations that created a coin used in the
spending operation.

Let \oraSet{Anon} stand for access to the oracles
 \ora{AddUser}, \ora{Withdraw}, \ora{Spend},
 \ora{RefreshAsExchange}, \ora{LinkAsExchange}, \ora{AddCorruptUser}, \ora{Deposit}.  Let $b$ be the bit that will
 determine the mapping between users and spend operation, which the adversary must guess.

\bigskip
\noindent $\mathit{Exp}_{\prt{A}}^{anon}(1^\lambda, \kappa, b)$:
\vspace{-0.5\topsep}
\begin{enumerate}
  \setlength\itemsep{0em}
  \item $(\V{skE}, \V{pkE}, \V{skM}, \V{pkM}) \leftarrow {\prt{A}}()$ \\
    The adversary controls the exchange and a merchant.
    \footnote{We emphasize that our oracles give the adversary all data a real
    exchange learns (from the protocol transcripts returned by oracles), but we
    do not give our adversary access to our simulation's data structures
    because they include data only
    known by the customers.}
  \item $(\V{pkU}_0, \V{pkU}_1, \V{contract}_0, \V{contract}_1) \leftarrow {\prt{A}}^{\oraSet{Anon}}()$ \\
    The adversary creates two users and selects two contract identifiers.
  \item Return 0 if $\V{pkU}_0$ or $\V{pkU}_1$ are not uncorrupted registered users.
  \item Select distinct fresh coins $\V{pkC}_0$ and $\V{pkC}_1$
    from the wallets of $\V{pkU}_0$ and $\V{pkU}_1$, respectively.
    \footnote{In principle, we might anonymously refresh coins before
    or concurrently with spending them, but if our adversary directs a
    non-anonymous refresh then they can mark coins with it}
    Return 0 if either $\V{pkU}_0$ or $\V{pkU}_1$ has insufficient unspent unrefreshed coins.
  \item $\V{dp_0} \leftarrow \algo{Spend}(\V{contract}_0, \V{pkU}_b, \V{pkC}_b, \V{pkM})$, \\
      $\V{dp_1} \leftarrow \algo{Spend}(\V{contract}_1, \V{pkU}_{1-b}, \V{pkC}_{1-b}, \V{pkM})$ \\
      Spend these two coins without revealing the mapping between users and coins.
  \item $r_0 \leftarrow \algo{Deposit}(\prt{E}(\V{skE}, \V{pkE}), {\prt{A}}(dp_0))$, \\
    $r_1 \leftarrow \algo{Deposit}(\prt{E}(\V{skE}, \V{pkE}), {\prt{A}}(dp_1))$ \\
    Deposit these two coins with the adversary controlled exchange.  Return 0 if $r_0$ or $r_1$ indicate a failure.
  \item $b' \leftarrow {\cal A}^{\oraSet{Anon}}()$ \\
    The adversary makes one guess $b' \in \{0,1\}$ for $b$, which determines the mapping between users and contracts.
  \item if $b = b'$ return 1, otherwise return 0
\end{enumerate}

We do not assume distinct users because ... FIXME

\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 spent 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 / does not give them more power.
\end{mdframed}

\subsection{Fairness}
\begin{mdframed}
  Fairness is a very overloaded term in crypto, can we come up with something better?
  It's already used for (a) protocols where either none or all parties obtain a result and
  (b) as fair e-cash, which is e-cash with selective tracability/deanonymization for e.g. law enforcement.

  Christian prefers Exculpability and both of us like Fair Exchange.  Exchange fairness has issues.
\end{mdframed}

Intuitively, the adversary wins if a non-corrupted user is unable to obtain a
proof-of-spending or unlinkable change for a coin.  This can happen, for
example, when the merchant is able to spend a coin in a way not anticipated by
the customer, keep the coin in a state that neither gives the customer a
receipt nor allows the customer to refresh it.

In practice, this property is necessary to guarantee that aborted or partially completed
payments do not result in the customer losing money or their anonymity.

The game also covers the case where a malicious exchange pretends the customer
did a dishonest refresh (in instantiations that allow dishonest refreshes).

Let \oraSet{Fair} stand for access to the oracles
 \ora{AddUser}, \ora{Withdraw}, \ora{Spend},
 \ora{RefreshAsExchange}, \ora{Share}, \ora{AddCorruptUser}, \ora{Deposit}.

\bigskip
\noindent $\mathit{Exp}_{\cal A}^{fair}(1^\lambda, 1^\kappa)$:
\vspace{-0.5\topsep}
\begin{enumerate}
  \setlength\itemsep{0em}
  \item $(skE, pkE) \leftarrow \mathrm{ExchangeKeygen}(1^\lambda, 1^\kappa, M)$ 
  \item $C_0 \leftarrow {\cal A}^{\oraSet{Fair}}(pkExchange)$
  \item The simulator runs all refresh operations to conclusion by looking for
    partial refresh transcripts.  We assume additional state in the wallet of
    each user to finish refresh operations.
  \item If $C_0$ is not a coin public key, return 0.
        Also 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$.  
        We note the user obtains unlinkable change through refreshes, which merely extend this list.
  \item Return 0 if either $U$ was corrupted or \ora{Share} was called with any of $C_0, \dots, C_n$.
  \item For each $C \in \{C_0, \dots, C_n\}$, we check if the exchange's database records value transfers not present in the user's wallet's database:
    \begin{enumerate}[label*=\arabic*.]
      \item Return 1 if $\V{deposited}[C]$ contains a contract not appearing in the wallet's database $\V{acceptedContracts}[U]$.
      \item Return 1 if the total value $r_E$ of attempted refreshes in $\V{refreshed}[C]$ exceeds the total value $r_U$ of coins in $C_0, \dots, C_n$ directly reachable in one link from $C$.  We note $r_E$ includes refreshes that failed due to dishonesty, but not refreshes that failed to authenticate as $C$.
     \end{enumerate}
  \item Return 0 if this step is reached without an earlier return.
\end{enumerate}

\begin{mdframed}
  The game is written in a way that does not refer to failed refreshes explicitly.
\end{mdframed}


\subsection{Unforgability} % Exculpability?

Intuitively, adversarial customers win if they can forge more valid coins than
they withdraw.

Let \oraSet{Forge} stand for access to the oracles
 \ora{AddUser}, \ora{Withdraw}, \ora{Spend},
 \ora{RefreshAsExchange}, \ora{Share}, \ora{AddCorruptUser}.

\bigskip
\noindent $\mathit{Exp}_{\cal A}^{forge}(1^\lambda, \kappa)$:
\vspace{-0.5\topsep}
\begin{enumerate}
  \setlength\itemsep{0em}
  \item $(skE, pkE) \leftarrow \mathrm{ExchangeKeygen}()$ 
  \item $(C_0, \dots, C_\ell) \leftarrow \mathcal{A}^{\oraSet{Forge}}(pkExchange)$
  \item Our adversary wins if the sum of the unspend value of valid coins in $C_0 \dots, C_\ell$
    exceeds the amount withdrawn by corrupted peers.
  \comment{Return 0 or 1 vs adversary wins or looses}
\end{enumerate}


\subsection{Income Transparency}

Intuitively, the adversary wins if money is in exclusive control of corrupted
users, but the exchange has no record of withdrawal or spending for it.  This
of course presumes that the adversary cannot delete from non-corrupted
customer's wallets, even though they can use oracles to force protocol
interactions of non-corrupted customers.

For practical e-cash systems, Income Transparency disincentivizes the emergence
of ``black markets'' among mutually distrusting users, where currency
circulates without the transactions being visible.  The Link protocol
introduces the threat of losing exclusive control of coins (despite having the option to refresh them) that
were received without involvement of the exchange.

Let \oraSet{Income} stand for access to the oracles
 \ora{AddUser}, \ora{Withdraw}, \ora{Spend},
 \ora{RefreshAsExchange}, \ora{Share}, \ora{AddCorruptUser}.

\bigskip
\noindent $\mathit{Exp}_{\cal A}^{income}(1^\lambda, 1^\kappa)$:
\vspace{-0.5\topsep}
\begin{enumerate}
  \setlength\itemsep{0em}
  \item $(skE, pkE) \leftarrow \mathrm{ExchangeKeygen}()$ 
  \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.
    Spend all remaining value on coins in wallets of non-corrupted users with \algo{Deposit}.\footnote{If \algo{Deposit} can only be run once per coin, then run a similar alggorithm that ignores this check.} 
  \item Let $L$ be the sum of unspent value for valid coins in $C_1, \dots\, C_\ell$, after
    accounting for the previous spending step.
  \item Let $w$ be the sum of coins withdrawn by non-corrupted users,
    $w'$ be the sum of coins withdrawn by corruped users, and $s$ be the value marked as spent
    by non-corrupted users.
    Our adversary wins if $L - w' > 0$.
  \item Return $(L, w, w', s)$
  \comment{Big stile break so split into two games.  Return ratio.  Two expectations is wrong. }
\end{enumerate}

The adversary is said to win the Income Transparency game if $L - w' > 0$.
Intuitively, the expenses for getting untaxed money are less or equal to the gained
untaxed money.

For Taler (which only safisfies Weak Income Transparency) our proofs would only bound
adversaries' probability of winning one Income Transparency game by $1/\kappa$.
Instead, we shall prove that attacks cannot be profitable for the adversary
in the sense that the expected loss $E[w-s]$ for obtaining
untaxed coins of value $L$ is bounded by $E[w - s] \ge \kappa \cdot E[L - w']$,
independent from whether the adversary wins the game or not.

% In the proof, we look at fixed values of L and w'.
% The value of L-w' prime can't come from withdraw directly,
% it can't come from forging coins (or we could win the unforgeability game)
% It can't come from linking
% If it is to come from refresh, either we must find a hash collision
% or guess 

\begin{mdframed}
  Older formulations were talking about ``value lost during refresh'', but this concept does
  not necessarily exist for other instantiations (and the game was more complicated with it).
\end{mdframed}

\subsection{Others}

\subsubsection{Exculpability}
Exculpability is not necessary, since coins are spent on-line with the exchange.
In practice, even offline e-cash systems that provide exculpability are often undesireable, 
since hardware failures can result in unintentional overspending.

\subsubsection{Fair Exchange and Endorsements}
Camenisch and others \cite{camenisch2007endorsed} describes a version of (offline) e-cash where it is possible to
generate lightweight endorsement for coins.  These endorsements are unlinkable from
each other and from the coin.  An endorsement allows the implementation of fair exchange
(where either both goods are exchanged and a payment is made or neither) without giving up
anonymity.

Taler supports a similar concept of endorsements via the coin public key, deposit permissions and the
refresh protocol.  The deposit permission (augmented with some additional data) can be viewed as an endorsement
that enables fair exchange.  Unlinkability is guaranteed by the Refresh protocol.

\section{Security Definitions}

\begin{definition}[Anonymity]
We say that an e-cash scheme satisfies \emph{Anonymity} if
the success probability $\Prb{b \randsel \{0,1\}: \mathit{Exp}_{\cal A}^{anon}(1^\lambda, 1^\kappa, b) = 1}$
of the anonymity game is neglegible for any polynomial time adversary $\mathcal{A}$.
\end{definition}

\begin{definition}[Strong Income Transparency]
We say that an e-cash scheme satisfies \emph{Strong Income Transparency} if
the success probability $\Prb{(L, w, w', s) \leftarrow \mathit{Exp}_{\cal A}^{income}(1^\lambda, 1^\kappa); L - w' > 0}$
for the income transparency game is neglegible for any polynomial time adversary $\mathcal{A}$.
\end{definition}

\begin{definition}[Weak Income Transparency]
We say that an e-cash scheme satisfies \emph{Weak Income Transparency} if for any polynomial time adversary $\mathcal{A}$,
our random variables $(L, w, w', s) \leftarrow \mathit{Exp}_{\cal A}^{income}(1^\lambda, 1^\kappa)$ from the income transparency
game satisfy $E[w - s] \ge \kappa \cdot E[L - w']$.
\end{definition}

\begin{definition}[Unforgeability]
We say that an e-cash scheme satisfies \emph{Unforgeability} if
the success probability $\Prb{\mathit{Exp}_{\cal A}^{forge}(1^\lambda, 1^\kappa) = 1}$
of the unforgeability game is neglegible for any polynomial time adversary $\mathcal{A}$.
\end{definition}


\begin{definition}[Fairness]
We say that an e-cash scheme satisfies \emph{Fairness} if
the success probability $\Prb{\mathit{Exp}_{\cal A}^{fair}(1^\lambda, 1^\kappa) = 1}$
of the fairness game is neglegible for any polynomial time adversary $\mathcal{A}$.
\end{definition}

\section{Instantiation}
\begin{mdframed}
  This section is incomplete.  Questions:  How do we reconcile our security parameter $\lambda$
  with Ed25519?  Should we be independent of the curve, even in our more concrete instantiation?

  Protocol transcripts are a mess, currently mostly there to show which values the adversary sees,
  and to check that after our hops they are all independent uniform random.

  Christian agrees with Jeff on using an abstract key exchange.
\end{mdframed}

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

\begin{itemize}
  \item \algo{ExchangeKeygen}():  Generate an RSA key pair of length $\lambda$ and return it.
  \item \algo{UserKeygen}():  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})):
    Exchange checks signatures, adds contribution $f$ of each coin to database of spent coins.
  \item \algo{Refresh}(\prt{E}(\V{skE}, \V{pkE}), \prt{U}(\V{skU}, \V{pkU}, \V{\overrightarrow{skCoinList}})):
    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, \tilde{n}_1, \dots, \tilde{n}_i \overline{M}_\gamma)
    \end{equation*}

    with
    \begin{itemize}
      \item Refresh confirmation signature $sig = Sign(skCoin, "refresh", \V{pkCoin})$
      \item Verification nonce $n_i \randsel U$
      \item Transfer private key $t_i \randsel U$
      \item Transfer public key $T_i = t_i \cdot G$A
      \item Transfer secret $s_i = ECDH(t_i, pkCoin)$
      \item Blinding factor $r_i = PRF_{pkCoin}(s_i)$
      \item Coin private key $m_i = PRF_{pkCoin+1}(s_i \mathbin{\|} n_i)$
      \item Coin public key $M_i = m_i \cdot G$
      \item Planchet $\overline{M}_i = (r_i \cdot M_i)^d \bmod N$
      \item (tide denotes item at index $\gamma$ set to zero)
    \end{itemize}
  \item \algo{Link}(\prt{E}(\V{skE}, \V{pkE}), \prt{U}(\V{skU}, \V{pkU}, \V{linkSecret}, \V{skCoin})):
    The user obtains the protocol transcript for the Refresh with coin public key derived from \V{skCoin}.
    The refresh protocol is then used to withdraw the planchet $\overline{M}_\kappa$.
\end{itemize}

\section{Proofs}
\begin{mdframed}
  Currently the proofs don't have any explicit tightess bounds.
  Because we don't know where to ``inject'' the value that we get from the challenger when carrying out
  a reduction, we need to randomly guess in which coin/signature we should ``hijack'' our challenge value.
  Thus for the proofs to work fully formally, we need to bound the total number of oracle invocations,
  and our exact bound for the tightness of the reduction depends on this limit.
\end{mdframed}

\subsection{Anonymity}


\begin{theorem}
  Assuming the existence of a Pseudo-Random Function Family (PRF), DDH, and a collision-resistant hash function, Taler satisfies \emph{Anonymity}.
\end{theorem}

\begin{proof}
  We give a proof via a sequence of games $\mathbb{G}_0(b), \mathbb{G}_1(b),
  \mathbb{G}_2(b), \mathbb{G}_3(b)$, where $\mathbb{G}_0(b)$ is the original
  anonymity game $\mathit{Exp}_{\cal A}^{anon}(1^\lambda, \kappa, b)$.  Let
  $\epsilon_{PRF}$ and $\epsilon_{DDH}$ be the advantage of an adversary for
  the PRF game and DDH game respectively.

  In $\mathbb{G}_1$ the game is modified by replacing the link oracle \ora{LinkAsExchange}
  by another oracle that behaves the same as \ora{LinkAsExchange} only if the adversary
  responds to the customer with link data that has been observed in a previous refresh.
  If the link data is not recognized by the simulator, the customer is instead given
  a uniform random value as link data.

  Recall that a coin obtained via refresh is only added to the wallet if the link
  secret is constructed as $linkSecret = H(nonce, skOldCoin)$.  Link secrets that
  do not pass this verification are discarded.

  In order to distinguish $\mathbb{G}_0$ from $\mathbb{G}_1$, the adversary must
  find a link secret that results in different behavior by the customer with regards
  to accepting/rejecting it.  The behaviour with previously seen link secrets is identical.
  In order to forge a distinguishing link secret, the adversary must either find a hash collision
  or find the coin's private key. \comment{Should we fully carry out this reduction, including tightness bound, and if so where?}
  
  In $\mathbb{G}_2$, the refresh oracle is modified so that the user responds
  with value drawn from a uniform random distribution for the the $\gamma$-th
  commitment instead of using a Diffie-Hellman function.  Since $\gamma$ is
  chosen by the adversary after seeing the commitments, the simulator first
  makes a guess $\gamma^*$ and draws a uniform random value only for the
  $\gamma^*$-th commitment.  If the $\gamma$ chosen by the adversary does not
  match $\gamma^*$, the simulator rewinds \prt{A} to the point where the
  refresh oracle was called.  Note that this succeeds with probability
  $1/\kappa + \epsilon_{DDH}$.  Since $\kappa \ll \lambda$, the runtime
  complexity of the simulator still says polynomial in $\lambda$.  Note that we
  only replace the one commitment that will not be opened to the adversary
  later. \comment{Tighness bound also missing}

  We now show that $\left| \Prb{\mathbb{G}_1 = 1} - \Prb{\mathbb{G}_2 = 1}
  \right| \le \epsilon_{DDH}$ by defining a distinguishing game $\mathbb{G}_{1
  \sim 2}$ for $DDH$ as follows:

  \bigskip
  \noindent $\mathbb{G}_{1 \sim 2}(b)$:
  \vspace{-0.5\topsep}
  \begin{enumerate}
    \setlength\itemsep{0em}
    \item $D = C_{ddh}(b)$
      \comment{The DDH challenger gives us a distribution that is either $(g^a, g^b, g^{ab})$ or $(g^a, g^b, g^c)$}
    \item return $\mathit{Exp'}_{\cal A}^{anon}(b, D)$
      \comment{Modified anonymity game where the $\gamma$-th commitment in the
      refresh oracle is drawn from distribution $D$ (using rewinding).  Technically we need to
      draw from $D$ on withdraw for the coin private key, write it to a table, look it up on refresh and 
      use the matching tuple.}
  \end{enumerate}
  
  We observe that depending on the coin flip $b$, we either simulate $\mathbb{G}_1$ or $\mathbb{G}_2$ perfectly for
  adversary $\cal A$ against $\mathbb{G}_1$.  At the same time $b$ determines whether \prt{A} receives $(g^a, g^b, g^{ab})$ or $(g^a, g^b, g^c)$.
  Thus $\left| \Prb{\mathbb{G}_1 = 1} - \Prb{\mathbb{G}_2 = 1} \right| = \epsilon_{DDH}$ is exactly the DDH advantage of $\mathbb{G}_{1 \sim 2}$.

  In the hop between $\mathbb{G}_2$ and $\mathbb{G}_3$ we replace the PRFs with a random uniform function. \comment{Does this need a proof?
  Do we need to do this for the next step?  If so, we just use exactly the same technique as in the last hop with PRF instead of DDH.}

  The coins obtained from refresh and from withdraw have now the same distribution in $\mathbb{G}_3$.
  Since the blinding is perfect, the adversary has no information to associate a withdraw/refresh transcript
  with a spend transcript.  Thus the success probability for $\mathbb{G}_3$ is $1/2$.

  We conclude that that the success probability for $\mathit{Exp}_{\cal A}^{anon}(1^\lambda, \kappa, b)$ is at most $1/2 + \epsilon_{DDH} + \epsilon_{PRF}$.

  \comment{The DDH game we use here is non-standard (stream of values to decide on instead of one, so maybe we need to use the number of refresh oracle invocations
  as a factor in front of $\epsilon_{DDH}$?}

\end{proof}


\begin{mdframed}
  Note that the order of the hops does matter, since it's important that we feed the PRF
  real randomness.
\end{mdframed}


\subsection{Fairness}

\begin{theorem}
Assuming unforgeability of signatures (EUF-CMA), Taler
satisfies \emph{Fairness}.
\end{theorem}

\begin{proof}
We replace coin public keys with signing public keys from the EUF-CMA
challenger, unless the coins are withdrawn by corrupted users.
Signature operations with these public keys are replaces with calls to the signing \ora{Sign} oracle of the EUF-CMA challenger.

If the adversary wins in step 6.2, there must be a valid deposit permission over a contract not signed by the user,
and thus not send to \ora{Sign}.   If the adversary wins in step 6.3, there must be a refresh request not signed
by the user.  In either case, we can extract a forged signature and use \prt{A} to construct an adversary against EUF-CMA.
\end{proof}

\subsection{Unforgeability}
\begin{theorem}
In the random oracle model,
if the RSA known-target inversion problem (RSA-KTI) is hard, then
Taler satisfies \emph{Unforgeability}.
% 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}_{\cal 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{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{TODO: Find this in literature?  Is it related to contributory behavior?}
\end{definition}

\begin{theorem}
Assuming
\begin{enumerate}
\item Unforgeability
\item a collision-resistant hash function
\end{enumerate}
Taler satisfies \emph{Weak Income Transparency}.
\end{theorem}

\begin{proof}
Recall that the adversary must show that they have exclusive control over coins with value $L$. We must assume that either
\ora{Refresh}, \ora{Link}, \ora{Share} or \ora{Withdraw} was used to obtain these coins, otherwise the adversary could be used to win break unforgeability.  TOO FAST... $L - w'$

Since the adversary only wins if $L - w' > 0$, the adversary could not have
withdrawn this value with corrupted users.

Access to \ora{LinkAsUser} only gives the adversary access to coins that are already in wallets of (honest) users, and are thus lost in step 3 of the game.

The only remaining possibility to obtain coins is via \ora{RefreshAsExchange} and \ora{Share}.  Specifically the adversary must try to gain exclusive ``ownership''
of a coin whose private key was previously obtained via \ora{Share}, since sharing alone would result in the adversary losing the coin in step 3 of the game.
To do this, they must change the transfer private key, so that the Link protocol will fail to recover the refreshed coin for non-corrupted users.

An adversary that can find hash collisions could break the commitment, but this violates our assumption.  The only remaining possibility is
to inject a transfer public key that would fail verification, and hope that the exchange selects the commitment with this index
as the one of $\kappa$ indexes that won't be revealed.

This strategy has $1/\kappa$ chance of succeeding.  If such a malicious refresh is detected, the coin is unspendable, and contributes to the lost coins $w - s$.
Thus in order to gain exclusive control over coins with value $L - w'$, the expected number of lost coins is at least $\kappa * (w - s)$.  This proves
our bound of $\kappa E[w-s] \ge E[L-w']$.



\end{proof}


\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$. 
\comment{TODO: Turing machine?!?}
\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.

\bibliography{lit}
\bibliographystyle{alpha}

\end{document}