explicit denoms, small changes / comments

1 files changed, 89 insertions, 63 deletions

diff --git a/games/games.tex b/games/games.tex
index 12dc31e..152d2a7 100644
--- a/games/games.tex
+++ b/games/games.tex
@@ -51,15 +51,27 @@
 
 \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
+%
+
 \section{Model and Syntax}
 
-We consider a single exchange with many clients,
- who can acts as a merchant, a customer or both
- with no further distinction other than naming in the role.  
+We consider a single exchange with many clients that 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.
+following standard convention.  For succinctness the public key
+of a coin always implicitly has a denomination associated with it.
 
-We track several data structures on behalf of clients : 
+Our model tracks the following data for clients:
 \begin{itemize}
 \item $\V{valueWithdrawn}[\V{pkClient}]$ contains of the values
  withdrawn by each client $\V{pkClient}$,
@@ -67,62 +79,27 @@ We track several data structures on behalf of clients :
  which individually consist of the coin private keys and denomination signatures.
 \item $\V{contractHashes}[\V{pkClient}]$ contains the sets of contracts created during deposits.
 \end{itemize}
-Also, our exchange implements an accounting scheme to prevent double
-spending by tracking coin public keys in $\V{spent}[\V{pkCoin}]$ and
-$\V{refreshed}[\V{pkCoin}]$, which record transcripts.  
+The double-spending 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 {\em unspent} or {\em unrefreshed} if it does
-not appear in the $\V{spent}$ or $\V{refreshed}$ lists respectively.
+We say that a coin is {\em unknown to the exchange} if it does
+not appear in the $\V{deposited}$ or $\V{refreshed}$ lists respectively.
 We say that a coin is being double spent if adding a transcript to
 either list would cause the total value of transcripts in both lists
 to exceed the value of the denomination.
 %
-We may say spent but undeposited for improperly spent coins the user can
-reclaim with the refresh protocol.
-
-
-As a rule, anonymous cash scheme consider only a single implicit
-denomination in their security proofs because explicit denominations
-complicate the financial games and proofs.  In fact, anonymous eCash
-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.
-
-As the same time, only financial games worry about the denomination
-value, so even multiple denomination can be left implicit in anonymity
-games.  We compromise by leaving denominations implicit but dropping
-down to a single denomination when this creates ambiguity.
-We design our oracles to be modular over the accounting scheme used too. 
-
-As refreshes consume only a single coin and return several,
-we define {\em refresh trees} with root given by a withdrawal operation
-and vertices given by refresh and spend operations, and with
-directed hyper-edges being coins that go from a the withdrawal or refresh
-that created them to all the spends or refreshes that consumed them.  
-In particular, our double spending protections ensure the value ascribed
-to each refresh or spend by a coin does not exceed the coin's denomination
-and that all coins's leaving a particular refresh have denominations that
-together do not exceed the refresh's value.
-
-As a result, this hyper-tree becomes simply a path when we only have one
-denomination, which simplifies both the games and proofs.  We views this
-simplification as instructive for financial games, so we only provide
-hints as to the value formulation.  Anonymity warrants our careful
-attention however, so we give a full proof there.
-
-We note that leaf edges might only have an origin operation with no
-destination operations in either formulation. 
 
 
 \subsection{Algorithms}
 
-The Taler e-cash system is defined by the following probabilistic polynomial-time algorithms and protocols.
+The Taler e-cash scheme is modely by the following probabilistic polynomial-time algorithms and protocols.
 
 \begin{itemize}
   \item \algo{EKeygen}():  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.
+    that outputs a key pair $(\V{skE}, \V{pkE}, \V{M})$, which contain both
+    the signing key and the denomination keys for the exchange.  The
+    value of a denomination key $d$ is given by $\V{M}(d)$.
 
   \item \algo{CKeygen}():  Algorithm executed by merchants and customers
     that outputs a key pair $(\V{skU}, \V{pkU})$.
@@ -133,28 +110,31 @@ The Taler e-cash system is defined by the following probabilistic polynomial-tim
     Increments $\V{valueWithdrawn}[\V{pkU}]$ appropriately,
     adds the resulting coin to the wallet $\V{wallet}[\V{pkU}]$.
 
-  \item \algo{Spend}(contract, \V{pkClient}, \V{skCoin}, pkReceiver):
+  \item \algo{Spend}(contract, \V{f}, \V{pkClient}, \V{skCoin}, pkReceiver):
     Algorithm to produce and sign a deposit permission for a particular contract.
     Adds $\V{contract}$ to $\V{contractHashes}[pkClient]$ and
     initializes $\V{spent}[\V{pkCoin}]$.
 
+    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 customer, who acts as a merchant.
+    Interactive protocol between the exchange and a client, 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 double spent, we return the protocol transcript
     of the previous deposits and refreshes.  
 
-    On success, we mark $\V{pkCoin}$ spent in $\V{spent}[\V{pkCoin}]$ and
+    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{pkE}), \prt{U}(\V{skU}, \V{pkU}, \V{skCoin})):
+  \item \algo{Refresh}(\prt{E}(\V{skE}, \V{pkE}), \prt{U}(\V{skU}, \V{pkU}, \V{\overrightarrow{skCoinList}})):
     Interactive protocol between exchange and user.
 
-    Again, there is a $\V{pkCoin}$ corresponding to $\V{skCoin}$ appearing.
-    If $\V{pkCoin}$ is being double spent, then we return the protocol
-    transcript of the previous deposits and refreshes. 
+    For each coin private key in \V{\overrightarrow{skCoinList}}, the client must
+    have a public key $\V{pkCoin}$.  If $\V{pkCoin}$ is being double spent, 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, they will store the unlinkable
@@ -225,6 +205,34 @@ While we do have a \algo{Deposit} protocol that's used in some of the games, hav
 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 eCash 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.
+
+As refreshes consume only a single coin and return several,
+we define {\em refresh trees} with root given by a withdrawal operation
+and vertices given by refresh and spend operations, and with
+directed hyper-edges being coins that go from a the withdrawal or refresh
+that created them to all the spends or refreshes that consumed them.  
+In particular, our double spending protections ensure the value ascribed
+to each refresh or spend by a coin does not exceed the coin's denomination
+and that all coins's leaving a particular refresh have denominations that
+together do not exceed the refresh's value.
+
+As a result, this hyper-tree becomes simply a path when we only have one
+denomination, which simplifies both the games and proofs.  We views this
+simplification as instructive for financial games, so we only provide
+hints as to the value formulation.  Anonymity warrants our careful
+attention however, so we give a full proof there.
+
+We note that leaf edges might only have an origin operation with no
+destination operations in either formulation. 
+
 
 
 \section{Games}
@@ -233,17 +241,35 @@ since it does not give the adversary any additional power.
 
 We have two seperate security paramaters in Taler:
 First, our primary security parameter $\lambda$ characterizes
- the security of all cryptographic operations.
+the security of all cryptographic operations.
 We employ information theoretically secure blinding, but
- $\lambda$ also characterizes the ECDH used in refresh.
-Second, our tiny cut-and-choose parameter $\kappa \ge 3$
- characterizes our income transperency assurances.
-We shall argue later that small $\kappa$ suffice
- since cheating results in lost funds.
+$\lambda$ also characterizes the ECDH used in refresh.
+
+% 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}$ including an exchange and merchant
-win the anonymity game if they have any advnatage in linking spending
+win the anonymity game if they have any advantage in linking spending
 operations with the withdrawal or refresh operations that created the coin.
 
 Let \oraSet{Anon} stand for access to the oracles