de-Talerize, move extras into appendix, cut down to 15 pages

1 files changed, 144 insertions, 136 deletions

diff --git a/taler-fc19/paper.tex b/taler-fc19/paper.tex
index 05e808e..d357749 100644
--- a/taler-fc19/paper.tex
+++ b/taler-fc19/paper.tex
@@ -21,25 +21,22 @@
 \maketitle

 

 \begin{abstract}

-  Traditional security definitions for anonymous e-cash omit properties that

-  are vital for practical deployments conducting real economic transactions.

-  First, they do not protect against economic losses when protocols are aborted.

-  Second, they do not require that customers have cryptographic evidence that they

-  spent e-cash on a particular business transaction.  We introduce \emph{conservation}

-  as an additional security property to anonymity and unforgeability.

-

-  Another omission of many existing e-cash schemes and their security

-  definitions is they do not provide anonymity when wallets are restored from

+  We present an anonymous e-cash protocol that protects against economic losses

+  when protocols are aborted.  Furthermore, we ensure that customers have

+  cryptographic evidence that they

+  spent e-cash on a particular business transaction and introduce \emph{conservation}

+  as an additional security property to anonymity and unforgeability, and

+  preserve anonymity when wallets are restored from

   backup or synchronized with other devices.  We argue from this position that

   a protocol for unlinkable change is necessary even in schemes that provide

-  divisibility. As a naive implementation of a change protocol opens up the

-  possibility of misusing it for tax evasion, we define an income transparency

+  divisibility. As a na\"ive implementation of a change protocol opens up the

+  possibility of abuse for tax evasion, we define an income transparency

   security property.

 

   We furthermore show that an e-cash protocol that fulfills these properties

   can be used to implement Camenisch-style fair exchange, tick payments, and

   can be used to provide anonymous refunds.

-\keywords{First keyword  \and Second keyword \and Another keyword.}

+\keywords{E-cash  \and blind signature \and key exchange}

 \end{abstract}

 

 \def\Z{\mathbb{Z}}

@@ -76,39 +73,36 @@
 %\theoremstyle{corollary}

 %\newtheorem{corollary}{Corollary}[section]

 

-\section{Model and Syntax for Taler}

+\section{Model and Syntax}

 

-We consider a payment system with a single, static exchange and multiple,

-dynamically created customers and merchants.  The subset of the full Taler

-protocol that we model includes withdrawing digital coins, spending them with

+We consider a Chaum-style~\cite{chaum1983blind}

+payment system with an exchange (Chaum: mint) and multiple,

+dynamically created customers and merchants.  

+We model withdrawing digital coins, spending them with

 merchants and subsequently depositing them at the exchange, as well as

-obtaining unlinkable change for partially spent coins with an online

+obtaining unlinkable change for partially spent coins with a

 ``refresh'' protocol.

 

-The exchange offers digital coins in multiple denominations, and 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

+The exchange offers digital coins in multiple denominations.  We mostly

+ignore the denomination

 values here, including their impact on anonymity, in keeping with existing

-literature \cite{camenisch2007endorsed,pointcheval2017cut}.  For anonymity, we

+literature~\cite{camenisch2007endorsed,pointcheval2017cut}.  For anonymity, we

 believe this amounts to assuming that all customers have similar financial

 behavior.  We note logarithmic storage, computation and bandwidth demands

-denominations distributed by powers of a fixed constant, like two.

-

-We do not model fees taken by the exchange.  Reserves\footnote{%

-  ``Reserve'' is Taler's terminology for funds submitted to the exchange that

-  can be converted to digital coins.

-}

-are also omitted.

-Instead of maintaining a reserve balance, we track the total amount of

-coins withdrawn by each customer.

+denominations distributed by powers of a fixed constant.

 

+%We do not model fees taken by the exchange.  Reserves\footnote{%

+%  ``Reserve'' is Taler's terminology for funds submitted to the exchange that

+%  can be converted to digital coins.

+%}

+%are also omitted.

 Coins can be partially spent by specifying a fraction $0 < f \le 1$ of the

 total value associated with the coin's denomination.  Unlinkable change below

 the smallest denomination cannot be given.  In

-practice the unspendable, residual value should be seen as an additional fee

+practice the unspendable, residual value should be seen as a fee

 charged by the exchange.

 

-The spending of multiple coins is modeled non-atomically: to spend (fractions

+Spending multiple coins is modeled non-atomically: to spend (fractions

 of) multiple coins, they must be spent one-by-one.  The individual

 spend/deposit operations are correlated by a unique identifier for the

 transaction.

@@ -127,6 +121,8 @@ transaction.
 %volume over time.  For simplicity, we do not include this extra feature in our

 %model.

 

+Our system model tracks the total amount of

+coins withdrawn by each customer.

 Customers are identified by their public key $\V{pkCustomer}$.  Every customer

 keeps track of the following data:

 \begin{itemize}

@@ -142,7 +138,7 @@ keeps track of the following data:
     all refresh operations that were created for this customer.

 \end{itemize}

 

-

+\noindent

 The exchange in our model keeps track of the following data:

 \begin{itemize}

   \item $\V{withdrawn}[\V{pkCustomer}]$ contains the total amount withdrawn by

@@ -163,7 +159,7 @@ $\V{refreshed}$ would cause the total spent value from both lists to exceed
 the value of the coin's denomination.

 

 Note that the adversary does not have direct read or write access to these

-values; instead the adversary needs to use the oracles (defined later) to

+values; instead the adversary needs to use the oracles (defined in Section~\ref{sec:oracles}) to

 interact with the system.

 

 We parameterize our system with two security parameters:  The general security

@@ -172,11 +168,11 @@ $\lambda$ determines the length of keys and thus the security level, using a
 larger $\kappa$ will only decrease the success chance of malicious merchants

 conspiring with customers to obtain unreported (and thus untaxable) income.

 

-\subsection{Algorithms}

+\subsection{Algorithms and Protocols} \label{sec:algorithms}

 

-The Taler e-cash scheme is modeled by the following probabilistic\footnote{Our

-Taler instantiations are not necessarily probabilistic (except e.g. key

-generation), but we do not want to prohibit this for other instantiations}

+Our e-cash scheme is modeled by the following probabilistic\footnote{Our

+instantiation is not probabilistic (except key

+generation), but we do not want to prohibit this for other instantiations.}

 polynomial-time algorithms and interactive protocols.  The notation $P(X_1,\dots,X_n)$

 stands for a party $P \in \{\prt{E}, \prt{C}, \prt{M}\}$ (Exchange, Customer

 and Merchant respectively) in an interactive protocol, with $X_1,\dots,X_n$

@@ -254,7 +250,7 @@ of parties maintained by the challenger in the security games we define later.
     Executing the $\algo{WithdrawPickup}$ protocol multiple times with the same

     customer and the same withdraw identifier does not result in any change of

     the customer's withdraw balance $\V{withdrawn}[\V{pkCustomer}]$,

-    and results in (re-)adding the same coin to the customer's wallet.

+    and results in \mbox{(re-)}adding the same coin to the customer's wallet.

 

     Returns a protocol transcript $\mathcal{T}_{WP}$ of all messages exchanged

     between the exchange and customer.

@@ -336,14 +332,15 @@ of parties maintained by the challenger in the security games we define later.
 

 \end{itemize}

 

-\subsection{Oracles}

-We now specify how the adversary can interact with the system by defining

-oracles.  Oracles are queried by the adversary, and upon a query the challenger

-will act according to the oracle's specification.  Note that the adversary for

-the different security games is run with specific oracles, and does not

-necessarily have access to all oracles simultaneously.

+\subsection{Oracles} \label{sec:oracles}

+

+%We now specify how the adversary can interact with the system by defining

+%oracles.  Oracles are queried by the adversary, and upon a query the challenger

+%will act according to the oracle's specification.  Note that the adversary for

+%the different security games is run with specific oracles, and does not

+%necessarily have access to all oracles simultaneously.

 

-We can refer to customers in the parameters to an oracle query simply by their

+We refer to customers in the parameters to an oracle query simply by their

 public key.  For coins, however, the situation is more complicated.  The

 adversary needs the ability to refer to coins to trigger operations such as

 spending and refresh, but to model anonymity we cannot give the adversary access

@@ -359,7 +356,7 @@ execution of a link, refresh or withdraw protocol; or the index for a link
 transcript is invalid, the oracle returns an error to the adversary.

 

 In oracles that trigger the execution of one of the interactive protocols

-defined in the last section, we give the adversary the ability to actively

+defined in Section~\ref{sec:algorithms}, we give the adversary the ability to actively

 control the communication channels between the exchange, customers and

 merchants; i.e. the adversary can effectively record, drop, modify and inject

 messages during the execution of the interactive protocol. Note that this

@@ -476,7 +473,7 @@ adversary can send and receive messages.
     deposited.

 \end{itemize}

 

-We write \oraSet{Taler} for the set of all the oracles we just defined.

+We write \oraSet{All} for the set of all the oracles we just defined.

 

 The exchange does not need to be corrupted with an oracle. A corrupted exchange

 is modeled by giving the adversary the appropriate oracles and the exchange

@@ -511,8 +508,8 @@ plays as the customer.
 \section{Games}

 

 We now define four security games (anonymity, conservation, unforgeability and

-income transparency) that are later used to define the security properties for

-Taler.  Similar to \cite{bellare2006code} we assume that the game and adversary

+income transparency) that are later used to define security properties for

+our protocol.  Similar to \cite{bellare2006code} we assume that the game and adversary

 terminate in finite time, and thus random choices made by the challenger and

 adversary can be taken from a finite sample space.

 

@@ -527,7 +524,7 @@ anonymity game if they have a non-negligible advantage in correlating spending o
 with the withdrawal or refresh operations that created a coin used in the

 spending operation.

 

-Let $\oraSet{Anon} := \oraSet{Taler} - \{ \ora{Share} \}$ stand for access to all Taler oracles

+Let $\oraSet{Anon} := \oraSet{All} - \{ \ora{Share} \}$ stand for access to all oracles

 except the share oracle.

 Let $b$ be the bit that will determine the mapping between customers and spend

 operations, which the adversary must guess.

@@ -584,10 +581,10 @@ withdrawn by the same customer through by the exchange.
 In practice, this property is necessary to guarantee that aborted or partially

 completed withdrawals, payments or refreshes, as well as other (transient)

 misbehavior from the exchange or merchant do not result in the customer losing

-money.

+money or privacy.

 

-Let $\oraSet{Conserv} := \oraSet{Taler} - \{\ora{Share}\}$ stand for access to the

-all Taler oracles except the sharing oracle.

+Let $\oraSet{Conserv} := \oraSet{All} - \{\ora{Share}\}$ stand for access to the

+all oracles except the sharing oracle.

 

 \begin{figure}

 \fbox{\begin{minipage}{\textwidth}

@@ -633,7 +630,7 @@ parties that they do not fully trust.
 Intuitively, adversarial customers win if they can obtain more valid coins than

 they legitimately withdraw.

 

-Let $\oraSet{Forge} := \oraSet{Taler}$ stand for access to the all Taler

+Let $\oraSet{Forge} := \oraSet{All}$ stand for access to the all 

 oracles.

 

 \begin{figure}

@@ -671,8 +668,8 @@ an explicit goal. The Link protocol introduces the threat of losing exclusive
 control of coins (despite having the option to refresh them) that were received

 without being visible as income to the exchange.

 

-Let $\oraSet{Income} := \oraSet{Taler}$ stand for access to the

-all Taler oracles.

+Let $\oraSet{Income} := \oraSet{All}$ stand for access to the

+all oracles.

 

 \begin{figure}

 \fbox{\begin{minipage}{\textwidth}

@@ -728,15 +725,6 @@ section.
   $\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{\mathit{Exp}_{\cal A}^{income}(1^\lambda, 1^\kappa) \ne 0}$

-  for the income transparency game is negligible for any polynomial time adversary~$\mathcal{A}$.

-\end{definition}

-The adversary is said to win one execution of the strong income transparency

-game if the game's return value is non-zero, i.e. there was at least one

-successful attempt to obtain untaxed income.

-

 

 \begin{definition}[Weak Income Transparency]

   We say that an e-cash scheme satisfies \emph{weak income transparency}

@@ -756,19 +744,10 @@ negligible success probability to win the income transparency game.  It
 suffices that the financial losses of the adversary in the game are a

 deterrent, after all our purpose of the game is to characterize tax evasion.

 

-Taler does not fulfill strong income transparency since for Taler $\kappa$ must

-be a small cut-and-choose parameter, as the complexity of our cut-and-choose

-protocol grows linearly with $\kappa$.  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.  The

-return-on-investment (represented by the game's return value) is bounded by

-$1/\kappa$.

-

-We still characterize strong income transparency, since it might be useful

-for other instantiations that provide more absolute guarantees.

 

 \section{Instantiation}

-We first give an instantiation of Taler's protocol syntax that is generic over

+

+We give an instantiation of our protocol syntax that is generic over

 a blind signature scheme, a signature scheme, a combined signature scheme / key

 exchange protocol.  Our instantiation is in the random oracle model (ROM), i.e. usage

 of the hash function $H : \{0,1\}^* \mapsto \{1,\dots,2^\lambda\}$ is modeled

@@ -777,7 +756,7 @@ $\{1,\dots,2^\lambda\}$ with uniform probability.  Subsequent oracle queries on
 the same bit string return the same value.

 

 

-\subsection{Generic Instantiation}

+%\subsection{Generic Instantiation}

 Let $\textsc{BlindSign}$ be a blind signature scheme with the following syntax, where the party $\mathcal{S}$

 is the signer and $\mathcal{R}$ is the signature requester:

 \begin{itemize}

@@ -846,7 +825,7 @@ We require the following security properties to hold for $\textsc{CoinSignKx}$:
 Let $\textsc{Sign} = (\algo{KeyGen}_{S}, \algo{Sign}_{S}, \algo{Verify}_{S})$ be a signature

 scheme that satisfies SUF-CMA.

 

-Using \textsc{Blind}, \textsc{CoinSignKx}, \textsc{Sign} and $H$ we now instantiate the Taler syntax:

+Using \textsc{Blind}, \textsc{CoinSignKx}, \textsc{Sign} and $H$ we now instantiate the syntax:

 

 \begin{itemize}

   \item $\algo{ExchangeKeygen}(1^{\lambda}, 1^{\kappa}, \mathfrak{D})$:

@@ -1004,10 +983,7 @@ Using \textsc{Blind}, \textsc{CoinSignKx}, \textsc{Sign} and $H$ we now instanti
       \sigma_\gamma &\leftarrow \algo{UnblindSig}(r_\gamma, \V{pkCoin}_\gamma, \overline{\sigma}_\gamma).

     \end{align*}

 

-    Thus the new, unlinkable coin is

-    \begin{equation*}

-      \V{coin}_u = (\V{skCoin}_\gamma, \V{pkCoin}_\gamma, \V{pkD}_u, \sigma_\gamma).

-    \end{equation*}

+    Thus the new, unlinkable coin is $\V{coin}_u = (\V{skCoin}_\gamma, \V{pkCoin}_\gamma, \V{pkD}_u, \sigma_\gamma)$.

 

   \item $\algo{Link}(\prt{E}(\V{sksE}), \prt{C}(\V{skCustomer}, \V{pksE}, \V{coin}_0))$:

     The customer sends the public key $\V{pkCoin}_0$ of $\V{coin}_0$ to the exchange.

@@ -1040,27 +1016,6 @@ Using \textsc{Blind}, \textsc{CoinSignKx}, \textsc{Sign} and $H$ we now instanti
 

 \end{itemize}

 

-\subsection{Concrete Instantiation}

-We now give a concrete instantiation that is used in the implementation

-of GNU Taler for the schemes \textsc{BlindSign}, \textsc{CoinSignKx} and \textsc{Sign}.

-

-For \textsc{BlindSign}, we use RSA blind signatures \cite{XXX}.  From

-the information theoretically secure blinding, the computational blindness property

-follows directly.  For the unforgeability property, we additionally rely on

-the RSA-KTI assumption as discussed in \cite{bellare2003onemore}.  Note

-that since the blinding step in RSA blind signatures is non-interactive,

-storage and verification of the transcript is omitted in refresh and link.

-

-We instantiate \textsc{CoinSignKx} with signatures and key exchange operations

-on elliptic curves in Edwards form, where the same key is used for signatures

-and the Diffie--Hellman key exchange operations.  In practice, we use Ed25519

-\cite{bernstein2012high} / Curve25519 \cite{bernstein2006curve25519} for

-$\lambda=256$.  We caution that some other elliptic curve key exchange

-implementation might not satisfy the completeness property that we require, due

-to the lack of complete addition laws.

-

-For \textsc{Sign}, we use elliptic-curve signatures, concretely Ed25519.

-

 %In Taler's refresh, we avoid key exchange failures entirely because the

 %Edwards addition law is complete abelian group operation on the curve,

 %and the signature scheme verifies that the point lies on the curve.

@@ -1082,37 +1037,11 @@ For \textsc{Sign}, we use elliptic-curve signatures, concretely Ed25519.
 % complicates verifying honest key generation of the old coin's key.

 

 

-\section{Discussion}

-

-\subsection{Other Properties}

-

-% FIXME: move this to design or implementation

-\subsubsection{Fair Exchange}

-

-% FIXME: we should mention "atomic swap" here

-

-The Endorsed E-Cash system by Camenisch et al. (described in Section

-\ref{sec:security-related-work}) allows for fair exchange of (online or

-offline) e-cash against digital goods.  The online version does not protect the

-customer against loss of anonymity from linkability of aborted fair exchanges.

-

-Taler's refresh protocol can be used for fair exchange of online e-cash against

-digital goods, without any loss of anonymity due to linkability of aborted

-transactions, with the following small extension: The customer asks the

-exchange to \emph{lock coins to a merchant} until a timeout.  Until the timeout

-occurs, the exchange provides the merchant with a guarantee that these coins can

-only be spent with this specific merchant, or not at all.  The

-fair exchange exchanges the merchant's digital goods against the customer's

-deposit permissions for the locked coins.  On aborted fair exchanges,

-the customer refreshes to obtain unlinkable coins.

-

-

 \bibliographystyle{splncs04}

 \bibliography{ref}

 

 

-\end{document}

-

+\appendix

 

 \section{Proofs}

 %\begin{mdframed}

@@ -1124,12 +1053,12 @@ the customer refreshes to obtain unlinkable coins.
 %\end{mdframed}

 

 We now give proofs for the security properties defined in Section \ref{sec:security-properties}

-with the generic instantiation of Taler.

+with the generic instantiation.

 

 \subsection{Anonymity}

 

 \begin{theorem}

-  In the random oracle model, Taler satisfies anonymity.

+  In the random oracle model, our instantiation satisfies anonymity.

 \end{theorem}

 

 \begin{proof}

@@ -1227,7 +1156,7 @@ with the generic instantiation of Taler.
 \subsection{Conservation}

 

 \begin{theorem}

-  Assuming existential unforgeability of signatures (EUF-CMA), Taler satisfies conservation.

+  Assuming existential unforgeability of signatures (EUF-CMA), our instantiation satisfies conservation.

 \end{theorem}

 

 \begin{proof}

@@ -1266,7 +1195,7 @@ with the generic instantiation of Taler.
 \subsection{Unforgeability}

 

 \begin{theorem}

-Taler satisfies {unforgeability}.

+Our instantiation satisfies {unforgeability}.

 % by probabilistic polynomially time adversaries.

 \end{theorem}

 

@@ -1285,7 +1214,7 @@ forgery with probability $1/n$.
 

 \subsection{Income Transparency}

 \begin{theorem}

-Taler satisfies {weak income transparency}.

+Our instantiation satisfies {weak income transparency}.

 \end{theorem}

 

 \begin{proof}

@@ -1438,3 +1367,82 @@ As for $F = \emptyset$, the return value of the game must be $0$, we conclude
 %From \cite{bellare2003onemore}.  Assumption to prove security of RSA blind signatures.  Equivalent to RSA-CTI.

 

 

+

+

+\section{Concrete Instantitation}

+

+We now give a concrete instantiation that is used in our implementation

+for the schemes \textsc{BlindSign}, \textsc{CoinSignKx} and \textsc{Sign}.

+

+For \textsc{BlindSign}, we use RSA blind signatures~\cite{chaum1983blind}.  From

+the information theoretically secure blinding, the computational blindness property

+follows directly.  For the unforgeability property, we additionally rely on

+the RSA-KTI assumption as discussed in \cite{bellare2003onemore}.  Note

+that since the blinding step in RSA blind signatures is non-interactive,

+storage and verification of the transcript is omitted in refresh and link.

+

+We instantiate \textsc{CoinSignKx} with signatures and key exchange operations

+on elliptic curves in Edwards form, where the same key is used for signatures

+and the Diffie--Hellman key exchange operations.  In practice, we use Ed25519

+\cite{bernstein2012high} / Curve25519 \cite{bernstein2006curve25519} for

+$\lambda=256$.  We caution that some other elliptic curve key exchange

+implementation might not satisfy the completeness property that we require, due

+to the lack of complete addition laws.

+

+For \textsc{Sign}, we use elliptic-curve signatures, concretely Ed25519.

+

+

+\section{Strong Income Transparency}

+

+We characterized {\em weak income transparency} in

+Section~\ref{sec:security-properties}.  We will now discuss the notion

+of {\em strong income transparency}, as it might be useful for other

+instantiations that provide more absolute guarantees.

+

+\begin{definition}[Strong Income Transparency]

+  We say that an e-cash scheme satisfies \emph{strong income transparency} if

+  the success probability $\Prb{\mathit{Exp}_{\cal A}^{income}(1^\lambda, 1^\kappa) \ne 0}$

+  for the income transparency game is negligible for any polynomial time adversary~$\mathcal{A}$.

+\end{definition}

+

+The adversary is said to win one execution of the strong income

+transparency game if the game's return value is non-zero, i.e. there

+was at least one successful attempt to obtain untaxed income.

+

+Our protocol does not fulfill strong income transparency since in

+practice $\kappa$ must be a small cut-and-choose parameter, as the

+complexity of our cut-and-choose protocol grows linearly with

+$\kappa$.  Instead we showed that our protocol satisfies weak income

+transparency, which is a statement about the adversary's financial

+loss when winning the game instead of the winning probability.  Here,

+the return-on-investment (represented by the game's return value) is

+bounded by $1/\kappa$.

+

+

+\section{Endorsed E-Cash and Fair Exchange}

+

+%\subsection{Other Properties}

+

+% FIXME: move this to design or implementation

+%\subsubsection{Fair Exchange}

+

+% FIXME: we should mention "atomic swap" here

+

+The Endorsed E-Cash system by Camenisch et al.~\cite{camenisch2007endorsed}

+allows for fair exchange of (online or

+offline) e-cash against digital goods.  The online version does not protect the

+customer against loss of anonymity from linkability of aborted fair exchanges.

+

+The refresh protocol can be used for fair exchange of online e-cash against

+digital goods, without any loss of anonymity due to linkability of aborted

+transactions, with the following small extension: The customer asks the

+exchange to \emph{lock coins to a merchant} until a timeout.  Until the timeout

+occurs, the exchange provides the merchant with a guarantee that these coins can

+only be spent with this specific merchant, or not at all.  The

+fair exchange exchanges the merchant's digital goods against the customer's

+deposit permissions for the locked coins.  On aborted fair exchanges,

+the customer refreshes to obtain unlinkable coins.

+

+

+

+\end{document}