\chapter{Security of Income-Transparent Anonymous E-Cash}\label{chapter:security} \def\Z{\mathbb{Z}} \def\mathperiod{.} \def\mathcomma{,} \newcommand*\ST[5]% {\left#1\,#4\vphantom{#5} \;\right#2 \left. #5 \vphantom{#4}\,\right#3} % uniform random selection from set \newcommand{\randsel}[0]{\ensuremath{\xleftarrow{\text{\$}}}} \newcommand{\Exp}[1]{\ensuremath{E\left[#1\right]}} % 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 \let\V\relax % clashes with siunitx volt \newcommand{\V}[1]{\ensuremath{\mathsf{#1}}} % probability with square brackets of the right size \newcommand{\Prb}[1]{\ensuremath{\Pr\left [#1 \right ]}} \newcommand{\mycomment}[1]{~\\ {\small \textcolor{blue}{({#1})}}} \theoremstyle{definition} \newtheorem{definition}{Definition}[section] \theoremstyle{corollary} \newtheorem{corollary}{Corollary}[section] %%%%%%%%% % TODOS %%%%%%%% % % * 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? We so far discussed Taler's protocols and security properties only informally. In this chapter, we model a slightly simplified version of the system that we have implemented (see Chapter~\ref{chapter:implementation}), make our desired security properties more precise, and prove that our protocol instantiation satisfies those properties. \section{Introduction to Provable Security} Provable security \cite{goldwasser1982probabilistic,pointcheval2005provable,shoup2004sequences,coron2000exact} is a common approach for constructing formal arguments that support the security of a cryptographic protocol with respect to specific security properties and underlying assumptions on cryptographic primitives. The adversary we consider is computationally bounded, i.e., the run time is typically restricted to be polynomial in the security parameters (such as key length) of the protocol. Contrary to what the name might suggest, a protocol that is provably secure'' is not necessarily secure in practice \cite{koblitz2007another,damgaard2007proof}. Instead, provable security results are typically based on reductions of the form \emph{if there is an effective adversary~$\mathcal{A}$against my protocol$P$, then I can use$\mathcal{A}$to construct an effective adversary~$\mathcal{A}'$against$Q$''} where$Q$is a protocol or primitive that is assumed to be secure or a computational problem that is assumed to be hard. The practical value of a security proof depends on various factors: \begin{itemize} \item How well-studied is$Q$? Some branches of cryptography, for example, some pairing-based constructions, rely on rather complex and exotic underlying problems that are assumed to be hard (but might not be) \cite{koblitz2010brave}. \item How tight is the reduction of$Q$to$P$? A security proof may only show that if$P$can be solved in time$T$, the underlying problem$Q$can be solved (using the hypothetical$\mathcal{A}$) in time, e.g.,$f(T) = T^2$. In practice, this might mean that for$P$to be secure, it needs to be deployed with a much larger key size or security parameter than$Q$to be secure. \item What other assumptions are used in the reduction? A common and useful but somewhat controversial assumption is the Random Oracle Model (ROM) \cite{bellare1993random}, where the usage of hash functions in a protocol is replaced with queries to a black box (called the Random Oracle), which is effectively a trusted third party that returns a truly random value for each input. Subsequent queries to the Random Oracle with the same value return the same result. While many consider ROM a practical assumption \cite{koblitz2015random,bellare1993random}, it has been shown that there exist carefully constructed protocols that are secure under the ROM, but are insecure with any concrete hash function \cite{canetti2004random}. It is an open question whether this result carries over to practical protocols, or just certain classes of artificially constructed protocols of theoretical interest. \end{itemize} Furthermore, a provably secure protocol does not always lend itself easily to a secure implementation, since side channels and fault injection attacks \cite{hsueh1997fault,lomne2011side} are usually not modeled. Finally, the security properties stated might not be sufficient or complete for the application. For our purposes, we focus on game-based provable security \cite{bellare2006code,pointcheval2005provable,shoup2004sequences,guo2018introduction} as opposed to simulation-based provable security \cite{goldwasser1989knowledge,lindell2017simulate}, which is another approach to provable security typically used for zero-knowledge proofs and secure multiparty computation protocols. \subsection{Algorithms, Oracles and Games} In order to analyze the security of a protocol, the protocol and its desired security properties against an adversary with specific capabilities must first be modeled formally. This part is independent of a concrete instantiation of the protocol; the protocol is only described on a syntactic level. The possible operations of a protocol (i.e., the protocol syntax) are abstractly defined as the signatures of \emph{algorithms}. Later, the protocol will be instantiated by providing a concrete implementation (formally a program for a probabilistic Turing machine) of each algorithm. A typical public key signature scheme, for example, might consist of the following algorithms: \begin{itemize} \item$\algo{KeyGen}(1^\lambda) \mapsto (\V{sk}, \V{pk})$, a probabilistic algorithm which on input$1^\lambda$generates a fresh key pair consisting of secret key$\V{sk}$of length$\lambda$and and the corresponding public key$\V{pk}$. Note that$1^\lambda$is the unary representation of$\lambda$.\footnote{% This formality ensures that the size of the input of the Turing machine program implementing the algorithm will be as least as big as the security parameter. Otherwise the run-time complexity cannot be directly expressed in relation to the size of the input tape.} \item$\algo{Sign}(\V{sk}, m) \mapsto \sigma$, an algorithm that signs the bit string$m$with secret key$\V{sk}$to output the signature$\sigma$. \item$\algo{Verify}(\V{pk}, \sigma, m) \mapsto b$, an algorithm that determines whether$\sigma$is a valid signature on$m$made with the secret key corresponding to the public key$\V{pk}$. It outputs the flag$b \in \{0, 1\}$to indicate whether the signature was valid (return value$1$) or invalid (return value$0$). \end{itemize} The abstract syntax could be instantiated with various concrete signature protocols. In addition to the computational power given to the adversary, the capabilities of the adversary are defined via oracles. The oracles can be thought of as the API\footnote{In the modern sense of application programming interface (API), where some system exposes a service with well-defined semantics.} that is given to the adversary and allows the adversary to interact with the environment it is running in. Unlike the algorithms, which the adversary has free access to, the access to oracles is often restricted, and oracles can keep state that is not accessible directly to the adversary. Oracles typically allow the adversary to access information that it normally would not have direct access to, or to trigger operations in the environment running the protocol. Formally, oracles are an extension to the Turing machine that runs the adversary, which allow the adversary to submit queries to interact with the environment that is running the protocol. For a signature scheme, the adversary could be given access to an \ora{Sign} oracle, which the adversary uses to make the system produce signatures, with secret keys that the adversary does not have direct access to. Different definitions of \ora{Sign} lead to different capabilities of the adversary and thus to different security properties later on: \begin{itemize} \item If the signing oracle$\ora{Sign}(m)$is defined to take a message$m$and return a signature$\sigma$on that message, the adversary gains the power to do chosen message attacks. \item If$\ora{Sign}(\cdot)$was defined to return a pair$(\sigma, m)$of a signature$\sigma$on a random message$m$, the power of the adversary would be reduced to a known message attack. \end{itemize} While oracles are used to describe the possible interactions with a system, it is more convenient to describe complex, multi-round interactions involving multiple parties as a special form of an algorithm, called an \emph{interactive protocol}, that takes the identifiers of communicating parties and their (private) inputs as a parameter, and orchestrates the interaction between them. The adversary will then have an oracle to start an instance of that particular interactive protocol and (if desired by the security property being modeled) the ability to drop, modify or inject messages in the interaction. The typically more cumbersome alternative would be to introduce one algorithm and oracle for every individual interaction step. Security properties are defined via \emph{games}, which are experiments that challenge the adversary to act in a way that would break the desired security property. Games usually consist multiple phases, starting with the setup phase where the challenger generates the parameters (such as encryption keys) for the game. In the subsequent query/response phase, the adversary is given some of the parameters (typically including public keys but excluding secrets) from the setup phase, and runs with access to oracles. The challenger\footnote{ The challenger is conceptually the party or environment that runs the game/experiment.} answers oracle queries during that phase. After the adversary's program terminates, the challenger invokes the adversary again with a challenge. The adversary must now compute a final response to the challenger, sometimes with access to oracles. Depending on the answer, the challenger decides if the adversary wins the game or not, i.e., the game returns$0$if the adversary loses and$1$if the adversary wins. A game for the existential unforgeability of signatures could be formulated like this: \bigskip \noindent$\mathit{Exp}_{\prt{A}}^{EUF}(1^\lambda)$: \vspace{-0.5\topsep} \begin{enumerate} \setlength\itemsep{0em} \item$(\V{sk}, \V{pk}) \leftarrow \algo{KeyGen}(1^\lambda)$\item$(\sigma, m) \leftarrow \prt{A}^{\ora{Sign(\cdot)}}(\V{pk})$(Run the adversary with input$\V{pk}$and access to the$\ora{Sign}$oracle.) \item If the adversary has called$\ora{Sign}(\cdot)$with$m$as argument, return$0$. \item Return$\algo{Verify}(\V{pk}, \sigma, m)$. \end{enumerate} Here the adversary is run once, with access to the signing oracle. Depending on which definition of$\ora{Sign}$is chosen, the game models existential unforgeability under chosen message attack (EUF-CMA) or existential unforgeability under known message attack (EUF-KMA) The following modification to the game would model selective unforgeability (SUF-CMA / SUF-KMA): \bigskip \noindent$\mathit{Exp}_{\prt{A}}^{SUF}(1^\lambda)$: \vspace{-0.5\topsep} \begin{enumerate} \setlength\itemsep{0em} \item$m \leftarrow \prt{A}()$\item$(\V{sk}, \V{pk}) \leftarrow \algo{KeyGen}(1^\lambda)$\item$\sigma \leftarrow \prt{A}^{\ora{Sign(\cdot)}}(\V{pk}, m)$\item If the adversary has called$\ora{Sign}(\cdot)$with$m$as argument, return$0$. \item Return$\algo{Verify}(\V{pk}, \sigma, m)$. \end{enumerate} Here the adversary has to choose a message to forge a signature for before knowing the message verification key. After having defined the game, we can now define a security property based on the probability of the adversary winning the game: we say that a signature scheme is secure against existential unforgeability attacks if for every adversary~\prt{A} (i.e., a polynomial-time probabilistic Turing machine program), the success probability \begin{equation*} \Prb{\mathit{Exp}_{\prt{A}}^{EUF}(1^\lambda) = 1 } \end{equation*} of \prt{A} in the EUF game is \emph{negligible} (i.e., grows less fast with$\lambda$than the inverse of any polynomial in$\lambda$). Note that the EUF and SUF games are related in the following way: an adversary against the SUF game can be easily transformed into an adversary against the EUF game, while the converse does not necessarily hold. Often security properties are defined in terms of the \emph{advantage} of the adversary. The advantage is a measure of how likely the adversary is to win against the real cryptographic protocol, compared to a perfectly secure version of the protocol. For example, let$\mathit{Exp}_{\prt{A}}^{BIT}()$be a game where the adversary has to guess the next bit in the output of a pseudo-random number generator (PRNG). The idealized functionality would be a real random number generator, where the adversary's chance of a correct guess is$1/2$. Thus, the adversary's advantage is \begin{equation*} \left|\Prb{\mathit{Exp}_{\prt{A}}^{BIT}()} - 1/2\right|. \end{equation*} Note that the definition of advantage depends on the game. The above definition, for example, would not work if the adversary had a way to voluntarily'' lose the game by querying an oracle in a forbidden way \subsection{Assumptions, Reductions and Game Hopping} The goal of a security proof is to transform an attacker against the protocol under consideration into an attacker against the security of an underlying assumption. Typical examples for common assumptions might be: \begin{itemize} \item the difficulty of the decisional/computational Diffie--Hellman problem (nicely described by~\cite{boneh1998decision}) \item existential unforgeability under chosen message attack (EUF-CMA) of a signature scheme \cite{goldwasser1988digital} \item indistinguishability against chosen-plaintext attacks (IND-CPA) of a symmetric encryption algorithm \cite{bellare1998relations} \end{itemize} To construct a reduction from an adversary \prt{A} against$P$to an adversary against$Q$, it is necessary to specify a program$R$that both interacts as an adversary with the challenger for$Q$, but at the same time acts as a challenger for the adversary against$P$. Most importantly,$R$can chose how to respond to oracle queries from the adversary, as long as$R$faithfully simulates a challenger for$P$. The reduction must be efficient, i.e.,$R$must still be a polynomial-time algorithm. A well-known example for a non-trivial reduction proof is the security proof of FDH-RSA signatures \cite{coron2000exact}. % FIXME: I think there's better reference, pointcheval maybe? In practice, reduction proofs are often complex and hard to verify. Game hopping has become a popular technique to manage the complexity of security proofs. The idea behind game hopping proofs is to make a sequence of small modifications starting from initial game, until you arrive at a game where the success probability for the adversary becomes obvious, for example, because the winning state for the adversary becomes unreachable in the code that defines the final game, or because all values the adversary can observe to make a decision are drawn from a truly random and uniform distribution. Each hop modifies the game in a way such that the success probability of game$\mathbb{G}_n$and game$\mathbb{G}_{n+1}$is negligibly close. Useful techniques for hops are, for example: \begin{itemize} \item Bridging hops, where the game is syntactically changed but remains semantically equivalent, i.e.,$\Prb{\mathbb{G}_n = 1} = \Prb{\mathbb{G}_n = 1}$. \item Indistinguishability hops, where some distribution is changed in a way that an adversary that could distinguish between two adjacent games could be turned into an adversary that distinguishes the two distributions. If the success probability to distinguish between those two distributions is$\epsilon$, then$\left|\Prb{\mathbb{G}_n = 1} - \Prb{\mathbb{G}_n = 1}\right| \le \epsilon$\item Hops based on small failure events. Here adjacent games proceed identically, until in one of the games a detectable failure event$F$(such as an adversary visibly forging a signature) occurs. Both games most proceed the same if$F$does not occur. Then it is easy to show \cite{shoup2004sequences} that$\left|\Prb{\mathbb{G}_n = 1} - \Prb{\mathbb{G}_n = 1}\right| \le \Prb{F}$\end{itemize} A tutorial introduction to game hopping is given by Shoup \cite{shoup2004sequences}, while a more formal treatment with a focus on games as code'' can be found in \cite{bellare2006code}. A version of the FDH-RSA security proof based on game hopping was generated with an automated theorem prover by Blanchet and Pointcheval \cite{blanchet2006automated}. % restore-from-backup % TODO: % - note about double spending vs overspending \subsection{Notation} We prefix public and secret keys with$\V{pk}$and$\V{sk}$, and write$x \randsel S$to randomly select an element$x$from the set$S$with uniform probability. \section{Model and Syntax for Taler} 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 merchants and subsequently depositing them at the exchange, as well as obtaining unlinkable change for partially spent coins with an online 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 values here, including their impact on anonymity, in keeping with existing 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, withdrawals of different denominations are tracked, effectively assuming every customer has unlimited funds. 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 charged by the exchange. 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. In practice, this identifier is the hash$\V{transactionId} = H(\V{contractTerms})$of the contract terms\footnote{The contract terms are a digital representation of an individual offer for a certain product or service the merchant sells for a certain price.}. Contract terms include a nonce to make them unique, that merchant and customer agreed upon. Note that this transaction identifier and the correlation between multiple spend operations for one payment need not be disclosed to the exchange (it might, however, be necessary to reveal during a detailed tax audit of the merchant): When spending the$i$-th coin for the transaction with the identifier$\V{transactionId}$, messages to the exchange would only contain$H(i \Vert \V{transactionId})$. This is preferable for merchants that might not want to disclose to the exchange the individual prices of products they sell to customers, but only the total transaction volume over time. For simplicity, we do not include this extra feature in our model. Our system model tracks the total amount ($\equiv$financial value) of coins withdrawn by each customer. Customers are identified by their public key$\V{pkCustomer}$. Every customer's wallet keeps track of the following data: \begin{itemize} \item$\V{wallet}[\V{pkCustomer}]$contains sets of the customer's coin records, which individually consist of the coin key pair, denomination and exchange's signature. \item$\V{acceptedContracts}[\V{pkCustomer}]$contains the sets of transaction identifiers accepted by the customer during spending operations, together with coins spent for it and their contributions$0 < f \le 1$. \item$\V{withdrawIds}[\V{pkCustomer}]$contains the withdraw identifiers of all withdraw operations that were created for this customer. \item$\V{refreshIds}[\V{pkCustomer}]$contains the refresh identifiers of all refresh operations that were created for this customer. \end{itemize} The exchange in our model keeps track of the following data: \begin{itemize} \item$\V{withdrawn}[\V{pkCustomer}]$contains the total amount withdrawn by each customer, i.e., the sum of the financial value of the denominations for all coins that were withdrawn by$\V{pkCustomer}$. \item The overspending database of the exchange is modeled by$\V{deposited}[\V{pkCoin}]$and$\V{refreshed}[\V{pkCoin}]$, which record deposit and refresh operations respectively on each coin. Note that since partial deposits and multiple refreshes to smaller denominations are possible, one deposit and multiple refresh operations can be recorded for a single coin. \end{itemize} 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 recording an operation in$\V{deposited}$or$\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 interact with the system. We parameterize our system with two security parameters: The general security parameter$\lambda$, and the refresh security parameter$\kappa$. While$\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}\label{sec:security-taler-syntax} 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} 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$being the (possibly private) inputs contributed by the party to the protocol. Interactive protocols can access the state maintained by party$P$. While the adversary can freely execute the interactive protocols by creating their own parties, the adversary is not given direct access to the private data of parties maintained by the challenger in the security games we define later. \begin{itemize} \item$\algo{ExchangeKeygen}(1^{\lambda}, 1^{\kappa}, \mathfrak{D}) \mapsto (\V{sksE}, \V{pksE})$: Algorithm executed to generate keys for the exchange, with general security parameter$\lambda$and refresh security parameter$\kappa$, both given as unary numbers. The denomination specification$\mathfrak{D} = d_1,\dots,d_n$is a finite sequence of positive rational numbers that defines the financial value of each generated denomination key pair. We henceforth use$\mathfrak{D}$to refer to some appropriate denomination specification, but our analysis is independent of a particular choice of$\mathfrak{D}$. The algorithm generates the exchange's master signing key pair$(\V{skESig}, \V{pkESig})$and denomination secret and public keys$(\V{skD}_1, \dots, \V{skD}_n), (\V{pkD}_1, \dots, \V{pkD}_n)$. We write$D(\V{pkD}_i)$, where$D : \{\V{pkD}_i\} \rightarrow \mathfrak{D}$to look up the financial value of denomination$\V{pkD_i}$. We collectively refer to the exchange's secrets by$\V{sksE}$and to the exchange's public keys together with$\mathfrak{D}$by$\V{pksE}$. \item$\algo{CustomerKeygen}(1^\lambda,1^\kappa) \mapsto (\V{skCustomer}, \V{pkCustomer})$: Key generation algorithm for customers with security parameters$\lambda$and$\kappa$. \item$\algo{MerchantKeygen}(1^\lambda,1^\kappa) \mapsto (\V{skMerchant}, \V{pkMerchant})$: Key generation algorithm for merchants. Typically the same as \algo{CustomerKeygen}. \item$\algo{WithdrawRequest}(\prt{E}(\V{sksE}, \V{pkCustomer}), \prt{C}(\V{skCustomer}, \V{pksE}, \V{pkD})) \mapsto (\mathcal{T}_{WR}, \V{wid})$: Interactive protocol between the exchange and a customer that initiates withdrawing a single coin of a particular denomination. The customer obtains a withdraw identifier$\V{wid}$from the protocol execution and stores it in$\V{withdrawIds}[\V{pkCustomer}]$. The \algo{WithdrawRequest} protocol only initiates a withdrawal. The coin is only obtained and stored in the customer's wallet by executing the \algo{WithdrawPickup} protocol on the withdraw identifier \V{wid}. The customer and exchange persistently store additional state (if required by the instantiation) such that the customer can use$\algo{WithdrawPickup}$to complete withdrawal or to complete a previously interrupted or unfinished withdrawal. Returns a protocol transcript$\mathcal{T}_{WR}$of all messages exchanged between the exchange and customer, as well as the withdraw identifier \V{wid}. \item$\algo{WithdrawPickup}(\prt{E}(\V{sksE}, \V{pkCustomer}), \prt{C}(\V{skCustomer}, \V{pksE}, \V{wid})) \mapsto (\mathcal{T}_{WP}, \V{coin})$: Interactive protocol between the exchange and a customer to obtain the coin from a withdraw operation started with$\algo{WithdrawRequest}$, identified by the withdraw identifier$\V{wid}$. The first time$\algo{WithdrawPickup}$is run with a particular withdraw identifier$\V{wid}$, the exchange increments$\V{withdrawn}[\V{pkCustomer}]$by$D(\V{pkD})$, where$\V{pkD}$is the denomination requested in the corresponding$\algo{WithdrawRequest}$execution. How exactly$\V{pkD}$is restored depends on the particular instantiation. The resulting coin $\V{coin} = (\V{skCoin}, \V{pkCoin}, \V{pkD}, \V{coinCert}),$ consisting of secret key$\V{skCoin}$, public key$\V{pkCoin}$, denomination public key$\V{pkD}$and certificate$\V{coinCert}$from the exchange, is stored in the customers wallet$\V{wallet}[\V{pkCustomer}]$. 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. Returns a protocol transcript$\mathcal{T}_{WP}$of all messages exchanged between the exchange and customer. \item$\algo{Spend}(\V{transactionId}, f, \V{coin}, \V{pkMerchant}) \mapsto \V{depositPermission}$: Algorithm to produce and sign a deposit permission \V{depositPermission} for a coin under a particular transaction identifier. The fraction$0 < f \le 1$determines the fraction of the coin's initial value that will be spent. The contents of the deposit permission depend on the instantiation, but it must be possible to derive the public coin identifier$\V{pkCoin}$from them. \item$\algo{Deposit}(\prt{E}(\V{sksE}, \V{pkMerchant}), \prt{M}(\V{skMerchant}, \V{pksE}, \V{depositPermission})) \mapsto \mathcal{T}_D$: Interactive protocol between the exchange and a merchant. From the deposit permission we obtain the$\V{pkCoin}$of the coin to be deposited. If$\V{pkCoin}$is being overspent, the protocol is aborted with an error message to the merchant. On success, we add$\V{depositPermission}$to$\V{deposited}[\V{pkCoin}]$. Returns a protocol transcript$\mathcal{T}_D$of all messages exchanged between the exchange and merchant. \item$\algo{RefreshRequest}(\prt{E}(\V{sksE}), \prt{C}(\V{pkCustomer}, \V{pksE}, \V{coin}_0, \V{pkD}_u)) \rightarrow (\mathcal{T}_{RR}, \V{rid})$Interactive protocol between exchange and customer that initiates a refresh of$\V{coin}_0$. Together with$\algo{RefreshPickup}$, it allows the customer to convert$D(\V{pkD}_u)$of the remaining value on coin $\V{coin}_0 = (\V{skCoin}_0, \V{pkCoin}_0, \V{pkD}_0, \V{coinCert}_0)$ into a new, unlinkable coin$\V{coin}_u$of denomination$\V{pkD}_u$. Multiple refreshes on the same coin are allowed, but each run subtracts the respective financial value of$\V{coin}_u$from the remaining value of$\V{coin}_0$. The customer only records the refresh operation identifier$\V{rid}$in$\V{refreshIds}[\V{pkCustomer}]$, but does not yet obtain the new coin. To obtain the new coin, \algo{RefreshPickup} must be used. Returns the protocol transcript$\mathcal{T}_{RR}$and a refresh identifier$\V{rid}$. \item$\algo{RefreshPickup}(\prt{E}(\V{sksE}, \V{pkCustomer}), \prt{C}(\V{skCustomer}, \V{pksE}, \V{rid})) \rightarrow (\mathcal{T}_{RP}, \V{coin}_u)$: Interactive protocol between exchange and customer to obtain the new coin for a refresh operation previously started with \algo{RefreshRequest}, identified by the refresh identifier$\V{rid}$. The exchange learns the target denomination$\V{pkD}_u$and signed source coin$(\V{pkCoin}_0, \V{pkD}_0, \V{coinCert}_0)$. If the source coin is invalid, the exchange aborts the protocol. The first time \algo{RefreshPickup} is run for a particular refresh identifier, the exchange records a refresh operation of value$D(\V{pkD}_u)$in$\V{refreshed}[\V{pkCoin}_0]$. If$\V{pkCoin}_0$is being overspent, the refresh operation is not recorded in$\V{refreshed}[\V{pkCoin}_0]$, the exchange sends the customer the protocol transcript of the previous deposits and refreshes and aborts the protocol. If the customer \prt{C} plays honestly in \algo{RefreshRequest} and \V{RefreshPickup}, the unlinkable coin$\V{coin}_u$they obtain as change will be stored in their wallet$\V{wallet}[\V{pkCustomer}]$. If \prt{C} is caught playing dishonestly, the \algo{RefreshPickup} protocol aborts. An honest customer must be able to repeat a \algo{RefreshPickup} with the same$\V{rid}$multiple times and (re-)obtain the same coin, even if previous$\algo{RefreshPickup}$executions were aborted. Returns a protocol transcript$\mathcal{T}_{RP}$. \item$\algo{Link}(\prt{E}(\V{sksE}), \prt{C}(\V{skCustomer}, \V{pksE}, \V{coin}_0)) \rightarrow (\mathcal{T}, (\V{coin}_1, \dots, \V{coin}_n))$: Interactive protocol between exchange and customer. If$\V{coin}_0$is a coin that was refreshed, the customer can recompute all the coins obtained from previous refreshes on$\V{coin}_0$, with data obtained from the exchange during the protocol. These coins are added to the customer's wallet$\V{wallet}[\V{pkCustomer}]$and returned together with the protocol transcript. \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. We refer to customers in the parameters to an oracle query simply by their public key. 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 to the coins' public keys directly. Therefore we allow the adversary to use the (successful) transcripts of the withdraw, refresh and link protocols to indirectly refer to coins. We refer to this as a coin handle$\mathcal{H}$. Since the execution of a link protocol results in a transcript$\mathcal{T}$that can contain multiple coins, the adversary needs to select a particular coin from the transcript via the index$i$as$\mathcal{H} = (\mathcal{T}, i)$. The respective oracle tries to find the coin that resulted from the transcript given by the adversary. If the transcript has not been seen before in the 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 Section \ref{sec:security-taler-syntax}, 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 allows the adversary to leave the execution of an interactive protocol in an unfinished state, where one or more parties are still waiting for messages. We use$\mathcal{I}$to refer to a handle to interactive protocols where the adversary can send and receive messages. \begin{itemize} \item$\ora{AddCustomer}() \mapsto \V{pkCustomer}$: Generates a key pair$(\V{skCustomer}, \V{pkCustomer})using the \algo{CustomerKeygen} algorithm, and sets \begin{align*} \V{withdrawn}[\V{pkCustomer}] &:= 0\\ \V{acceptedContracts}[\V{pkCustomer}] &:= \{ \}\\ \V{wallet}[\V{pkCustomer}] &:= \{\} \\ \V{withdrawIds}[\V{pkCustomer}] &:= \{\} \\ \V{refreshIds}[\V{pkCustomer}] &:= \{\}. \end{align*} Returns the public key of the newly created customer. \item\ora{AddMerchant}() \mapsto \V{pkMerchant}$: Generate a key pair$(\V{skMerchant}, \V{pkMerchant})$using the \algo{MerchantKeygen} algorithm. Returns the public key of the newly created merchant. \item$\ora{SendMessage}(\mathcal{I}, P_1, P_2, m) \mapsto ()$: Send message$m$on the channel from party$P_1$to party$P_2$in the execution of interactive protocol$\mathcal{I}$. The oracle does not have a return value. \item$\ora{ReceiveMessage}(\mathcal{I}, P_1, P_2) \mapsto m$: Read message$m$in the channel from party$P_1$to party$P_2$in the execution of interactive protocol$\mathcal{I}$. If no message is queued in the channel, return$m = \bot$. \item$\ora{WithdrawRequest}(\V{pkCustomer}, \V{pkD}) \mapsto \mathcal{I}$: Triggers the execution of the \algo{WithdrawRequest} protocol. the adversary full control of the communication channels between customer and exchange. \item$\ora{WithdrawPickup}(\V{pkCustomer}, \V{pkD}, \mathcal{T}) \mapsto \mathcal{I}$: Triggers the execution of the \algo{WithdrawPickup} protocol, additionally giving the adversary full control of the communication channels between customer and exchange. The customer and withdraw identifier$\V{wid}$are obtained from the \algo{WithdrawRequest} transcript$\mathcal{T}$. \item$\ora{RefreshRequest}(\mathcal{H}, \V{pkD}) \mapsto \mathcal{I}$: Triggers the execution of the \algo{RefreshRequest} protocol with the coin identified by coin handle$\mathcal{H}$, additionally giving the adversary full control over the communication channels between customer and exchange. \item$\ora{RefreshPickup}(\mathcal{T}) \mapsto \mathcal{I}$: Triggers the execution of the \algo{RefreshPickup} protocol, where the customer and refresh identifier$\V{rid}$are obtained from the$\algo{RefreshRequest}$protocol transcript$\mathcal{T}$. Additionally gives the adversary full control over the communication channels between customer and exchange. \item$\ora{Link}(\mathcal{H}) \mapsto \mathcal{I}$: Triggers the execution of the \algo{Link} protocol for the coin referenced by handle$\mathcal{H}$, additionally giving the adversary full control over the communication channels between customer and exchange. \item$\ora{Spend}(\V{transactionId}, \V{pkCustomer}, \mathcal{H}, \V{pkMerchant}) \mapsto \V{depositPermission}$: Makes a customer sign a deposit permission over a coin identified by handle$\mathcal{H}$. Returns the deposit permission on success, or$\bot$if$\mathcal{H}$is not a coin handle that identifies a coin. Note that$\ora{Spend}$can be used to generate deposit permissions that, when deposited, would result in an error due to overspending Adds$(\V{transactionId}, \V{depositPermission})$to$\V{acceptedContracts}[\V{pkCustomer}]$. \item$\ora{Share}(\mathcal{H}, \V{pkCustomer}) \mapsto ()$: Shares a coin (identified by handle$\mathcal{H}$) with the customer identified by$\V{pkCustomer}$, i.e., puts the coin identified by$\mathcal{H}$into$\V{wallet}[\V{pkCustomer}]$. Intended to be used by the adversary in attempts to violate income transparency. Does not have a return value. Note that this trivially violates anonymity (by sharing with a corrupted customer), thus the usage must be restricted in some games. % the share oracle is the reason why we don't need a second withdraw oracle \item$\ora{CorruptCustomer}(\V{pkCustomer})\mapsto \newline{}\qquad (\V{skCustomer}, \V{wallet}[\V{pkCustomer}],\V{acceptedContracts}[\V{pkCustomer}], \newline{}\qquad \phantom{(}\V{refreshIds}[\V{pkCustomer}], \V{withdrawIds}[\V{pkCustomer}])$: Used by the adversary to corrupt a customer, giving the adversary access to the customer's secret key, wallet, withdraw/refresh identifiers and accepted contracts. Permanently marks the customer as corrupted. There is nothing special'' about corrupted customers, other than that the adversary has used \ora{CorruptCustomer} on them in the past. The adversary cannot modify corrupted customer's wallets directly, and must use the oracle again to obtain an updated view on the corrupted customer's private data. \item$\ora{Deposit}(\V{depositPermission}) \mapsto \mathcal{I}$: Triggers the execution of the \algo{Deposit} protocol, additionally giving the adversary full control over the communication channels between merchant and exchange. Returns an error if the deposit permission is addressed to a merchant that was not registered with$\ora{AddMerchant}$. 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. \end{itemize} We write \oraSet{Taler} for the set of all the oracles we just defined, and$\oraSet{NoShare} := \oraSet{Taler} - \ora{Share}$for all oracles except the share oracle. 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 secret key from the exchange key generation. If the adversary determines the exchange's secret key during the setup, invoking \ora{WithdrawRequest}, \ora{WithdrawPickup}, \ora{RefreshRequest}, \ora{RefreshPickup} or \ora{Link} can be seen as the adversary playing the exchange. Since the adversary is an active man-in-the-middle in these oracles, it can drop messages to the simulated exchange and make up its own response. If the adversary calls these oracles with a corrupted customer, the adversary plays as the customer. %\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} \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 terminate in finite time, and thus random choices made by the challenger and adversary can be taken from a finite sample space. All games except income transpacency return$1$to indicate that the adversary has won and$0$to indicate that the adversary has lost. The income transparency game returns$0$if the adversary has lost, and a positive laundering ratio'' if the adversary won. \subsection{Anonymity} Intuitively, an adversary~$\prt{A}$(controlling the exchange and merchants) wins the anonymity game if they have a non-negligible advantage in correlating spending operations with the withdrawal or refresh operations that created a coin used in the spending operation. Let$b$be the bit that will determine the mapping between customers and spend operations, which the adversary must guess. We define a helper procedure \begin{equation*} \algo{Refresh}(\prt{E}(\V{sksE}), \prt{C}(\V{pkCustomer}, \V{pksE}, \V{coin}_0)) \mapsto \mathfrak{R} \end{equation*} that refreshes the whole remaining amount on$\V{coin}_0$with repeated application of$\algo{RefreshRequest}$and$\algo{RefreshPickup}$using the smallest possible set of target denominations, and returns all protocol transcripts in$\mathfrak{R}$. \begin{mdframed} \small \noindent$\mathit{Exp}_{\prt{A}}^{anon}(1^\lambda, 1^\kappa, b)$: \vspace{-0.5\topsep} \begin{enumerate} \setlength\itemsep{0em} \item$(\V{sksE}, \V{pksE}, \V{skM}, \V{pkM}) \leftarrow {\prt{A}}()$\item$(\V{pkCustomer}_0, \V{pkCustomer}_1, \V{transactionId}_0, \V{transactionId}_1, f) \leftarrow {\prt{A}}^{\oraSet{NoShare}}()\item Select distinct fresh coins \begin{align*} \V{coin}_0 &\in \V{wallet}[\V{pkCustomer}_0]\\ \V{coin}_1 &\in \V{wallet}[\V{pkCustomer}_1] \end{align*} Return0$if either$\V{pkCustomer}_0$or$\V{pkCustomer}_1$are not registered customers with sufficient fresh coins. \item For$i \in \{0,1\}run \begin{align*} &\V{dp_i} \leftarrow \algo{Spend}(\V{transactionId}_i, f, \V{coin}_{i-b}, \V{pkM}) \\ &\algo{Deposit}(\prt{A}(), \prt{M}(\V{skM}, \V{pksE}, \V{dp}_i)) \\ &\mathfrak{R}_i \leftarrow \algo{Refresh}(\prt{A}(), \prt{C}(\V{pkCustomer}_i, \V{pksE}, \V{coin}_{i-b})) \end{align*} \itemb' \leftarrow {\cal A}^{\oraSet{NoShare}}(\mathfrak{R}_0, \mathfrak{R}_1)$\\ \item Return$0$if$\ora{Spend}$was used by the adversary on the coin handles for$\V{coin}_0$or$\V{coin}_1$or$\ora{CorruptCustomer}$was used on$\V{pkCustomer}_0$or$\V{pkCustomer}_1$. \item If$b = b'$return$1$, otherwise return$0$. \end{enumerate} \end{mdframed} Note that unlike some other anonymity games defined in the literature (such as \cite{pointcheval2017cut}), our anonymity game always lets both customers spend in order to avoid having to hide the missing coin in one customer's wallet from the adversary. \subsection{Conservation} The adversary wins the conservation game if it can bring an honest customer in a situation where the spendable financial value left in the user's wallet plus the value spent for transactions known to the customer is less than the value 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. \begin{mdframed} \small \noindent$\mathit{Exp}_{\cal A}^{conserv}(1^\lambda, 1^\kappa)$: \vspace{-0.5\topsep} \begin{enumerate} \setlength\itemsep{0em} \item$(\V{sksE}, \V{pksE}) \leftarrow \mathrm{ExchangeKeygen}(1^\lambda, 1^\kappa, M)$\item$\V{pkCustomer} \leftarrow {\cal A}^{\oraSet{NoShare}}(\V{pksE})$\item Return$0$if$\V{pkCustomer}$is a corrupted user. \item \label{game:conserv:run} Run$\algo{WithdrawPickup}$for each withdraw identifier$\V{wid}$and$\algo{RefreshPickup}$for each refresh identifier$\V{rid}$that the user has recorded in$\V{withdrawIds}$and$\V{refreshIds}$. Run$\algo{Deposit}$for all deposit permissions in$\V{acceptedContracts}$. \item Let$v_{C}$be the total financial value left on valid coins in$\V{wallet}[\V{pkCustomer}]$, i.e., the denominated values minus the spend/refresh operations recorded in the exchange's database. Let$v_{S}$be the total financial value of contracts in$\V{acceptedContracts}[\V{pkCustomer}]$. \item Return$1$if$\V{withdrawn}[\V{pkCustomer}] > v_{C} + v_{S}$. \end{enumerate} \end{mdframed} Hence we ensure that: \begin{itemize} \item if a coin was spent, it was spent for a contract that the customer knows about, i.e., in practice the customer could prove that they own'' what they paid for, \item if a coin was refreshed, the customer owns'' the resulting coins, even if the operation was aborted, and \item if the customer withdraws, they can always obtain a coin whenever the exchange accounted for a withdrawal, even when protocol executions are intermittently aborted. \end{itemize} Note that we do not give the adversary access to the \ora{Share} oracle, since that would trivially allow the adversary to win the conservation game. In practice, conservation only holds for customers that do not share coins with parties that they do not fully trust. \subsection{Unforgeability} Intuitively, adversarial customers win if they can obtain more valid coins than they legitimately withdraw. \begin{mdframed} \small \noindent$\mathit{Exp}_{\cal A}^{forge}(1^\lambda, 1^\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{All}}(pkExchange)$\item Return$0$if any$C_i$is not of the form$(\V{skCoin}, \V{pkCoin}, \V{pkD}, \V{coinCert})$or any$\V{coinCert}$is not a valid signature by$\V{pkD}$on the respective$\V{pkCoin}$. \item Return$1$if the sum of the unspent value of valid coins in$C_0 \dots, C_\ell$exceeds the amount withdrawn by corrupted customers, return$0$otherwise. \end{enumerate} \end{mdframed} \subsection{Income Transparency} Intuitively, the adversary wins if coins are in exclusive control of corrupted customers, but the exchange has no record of withdrawal or spending for them. This presumes that the adversary cannot delete from non-corrupted customer's wallets, even though it 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 customers, where currency circulates without the transactions being visible. This is in contrast to some other proposed e-cash systems and cryptocurrencies, where disintermediation is 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. \begin{mdframed} \small \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$(\V{coin}_1, \dots, \V{coin}_\ell) \leftarrow \mathcal{A}^{\oraSet{All}}(pkExchange)$(The$\V{coin}_i$must be coins, including secret key and signature by the denomination, for the adversary to win. However these coins need not be present in any honest or corrupted customer's wallet.) \item\label{game:income:spend} Augment the wallets of all non-corrupted customers with their transitive closure using the \algo{Link} protocol. Mark all remaining value on coins in wallets of non-corrupted customers as spent in the exchange's database. \item Let$L$denote the sum of unspent value on valid coins in$(\V{coin}_1, \dots\, \V{coin}_\ell)$, after accounting for the previous update of the exchange's database. Also let$w'$be the sum of coins withdrawn by corrupted customers. Then$p := L - w'$gives the adversary's untaxed income. \item Let$w$be the sum of coins withdrawn by non-corrupted customers, and$s$be the value marked as spent by non-corrupted customers, so that$b := w - s$gives the coins lost during refresh, that is the losses incurred attempting to hide income. \item If$b+p \ne 0$, return$\frac{p}{b + p}$, i.e., the laundering ratio for attempting to obtain untaxed income. Otherwise return$0$. \end{enumerate} \end{mdframed} \section{Security Definitions}\label{sec:security-properties} We now give security definitions based upon the games defined in the previous section. Recall that$\lambda$is the general security parameter, and$\kappa$is the security parameter for income transparency. A polynomial-time adversary is implied to be polynimial in$\lambda+\kappa$. \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 negligibly close to$1/2$for any polynomial-time adversary~$\mathcal{A}$. \end{definition} \begin{definition}[Conservation] We say that an e-cash scheme satisfies \emph{conservation} if the success probability$\Prb{\mathit{Exp}_{\cal A}^{conserv}(1^\lambda, 1^\kappa) = 1}$of the conservation game is negligible for any polynomial-time adversary~$\mathcal{A}$. \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 negligible 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{\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} if, for any polynomial-time adversary~$\mathcal{A}$, the return value of the income transparency game satisfies $$\label{eq:income-transparency-expectation} E\left[\mathit{Exp}_{\cal A}^{income}(1^\lambda, 1^\kappa)\right] \le {\frac{1}{\kappa}} \mathperiod$$ In (\ref{eq:income-transparency-expectation}), the expectation runs over any probability space used by the adversary and challenger. \end{definition} For some instantiations, e.g., ones based on zero-knowledge proofs,$\kappa$might be a security parameter in the traditional sense. However for an e-cash scheme to be useful in practice, the adversary does not need to have only 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 give an instantiation of our protocol syntax that is generic over a blind signature scheme, a signature scheme, a combined signature scheme / key exchange, a collision-resistant hash function and a pseudo-random function family (PRF). \subsection{Generic Instantiation}\label{sec:crypto: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} \item$\algo{KeyGen}_{BS}(1^\lambda) \mapsto (\V{sk}, \V{pk})$is the key generation algorithm for the signer of the blind signature protocol. \item$\algo{Blind}_{BS}(\mathcal{S}(\V{sk}), \mathcal{R}(\V{pk}, m)) \mapsto (\overline{m}, r)$is a possibly interactive protocol to blind a message$m$that is to be signed later. The result is a blinded message$\overline{m}$and a residual$r$that allows to unblind a blinded signature on$m$made by$\V{sk}$. \item$\algo{Sign}_{BS}(\mathcal{S}(\V{sk}), \mathcal{R}(\overline{m})) \mapsto \overline{\sigma}$is an algorithm to sign a blinded message$\overline{m}$. The result$\overline{\sigma}$is a blinded signature that must be unblinded using the$r$returned from the corresponding blinding operation before verification. \item$\algo{UnblindSig}_{BS}(r, m, \overline{\sigma}) \mapsto \sigma$is an algorithm to unblind a blinded signature. \item$\algo{Verify}_{BS}(\V{pk}, m, \sigma) \mapsto b$is an algorithm to check the validity of an unblinded blind signature. Returns$1$if the signature$\sigma$was valid for$m$and$0$otherwise. \end{itemize} Note that this syntax excludes some blind signature protocols, such as those with interactive/probabilistic verification or those without a blinding factor'', where the$\algo{Blind}_{BS}$and$\algo{Sign}_{BS}$and$\algo{UnblindSig}_{BS}$would be merged into one interactive signing protocol. Such blind signature protocols have already been used to construct e-cash \cite{camenisch2005compact}. We require the following two security properties for$\textsc{BlindSign}$: \begin{itemize} \item \emph{blindness}: It should be computationally infeasible for a malicious signer to decide which of two messages has been signed first in two executions with an honest user. The corresponding game can be defined as in Abe and Okamoto \cite{abe2000provably}, with the additional enhancement that the adversary generates the signing key \cite{schroder2017security}. \item \emph{unforgeability}: An adversary that requests$k$signatures with$\algo{Sign}_{BS}$is unable to produce$k+1$valid signatures with non-negligible probability. \end{itemize} For more generalized notions of the security of blind signatures see, e.g., \cite{fischlin2009security,schroder2017security}. Let$\textsc{CoinSignKx}$be combination of a signature scheme and key exchange protocol: \begin{itemize} \item$\algo{KeyGenSec}_{CSK}(1^\lambda) \mapsto \V{sk}$is a secret key generation algorithm. \item$\algo{KeyGenPub}_{CSK}(\V{sk}) \mapsto \V{pk}$produces the corresponding public key. \item$\algo{Sign}_{CSK}(\V{sk}, m) \mapsto \sigma$produces a signature$\sigma$over message$m$. \item$\algo{Verify}_{CSK}(\V{pk}, m, \sigma) \mapsto b$is a signature verification algorithm. Returns$1$if the signature$\sigma$is a valid signature on$m$by$\V{pk}$, and$0$otherwise. \item$\algo{Kx}_{CSK}(\V{sk}_1, \V{pk}_2) \mapsto x$is a key exchange algorithm that computes the shared secret$x$from secret key$\V{sk}_1$and public key$\V{pk}_2$. \end{itemize} We occasionally need these key generation algorithms separately, but we usually combine them into$\algo{KeyGen}_{CSK}(1^\lambda) \mapsto (\V{sk}, \V{pk})$. We require the following security properties to hold for$\textsc{CoinSignKx}$: \begin{itemize} \item \emph{unforgeability}: The signature scheme$(\algo{KeyGen}_{CSK}, \algo{Sign}_{CSK}, \algo{Verify}_{CSK})$must satisfy existential unforgeability under chosen message attacks (EUF-CMA). \item \emph{key exchange completeness}: Any probabilistic polynomial-time adversary has only negligible chance to find a degenerate key pair$(\V{sk}_A, \V{pk}_A)$such that for some honestly generated key pair$(\V{sk}_B, \V{pk}_B) \leftarrow \algo{KeyGen}_{CSK}(1^\lambda)$the key exchange fails, that is$\algo{Kex}_{CSK}(\V{sk}_A, \V{pk}_B) \neq \algo{Kex}_{CSK}(\V{sk}_B, \V{pk}_A)$, while the adversary can still produce a pair$(m, \sigma)$such that$\algo{Verify}_{BS}(\V{pk}_A, m, \sigma) = 1$. \item \emph{key exchange security}: The output of$\algo{Kx}_{CSK}$must be computationally indistinguishable from a random shared secret of the same length, for inputs that have been generated with$\algo{KeyGen}_{CSK}$. \end{itemize} Let$\textsc{Sign} = (\algo{KeyGen}_{S}, \algo{Sign}_{S}, \algo{Verify}_{S})$be a signature scheme that satisfies selective unforgeability under chosen message attacks (SUF-CMA). Let$\V{PRF}$be a pseudo-random function family and$H : \{0,1\}^* \rightarrow \{0,1\}^\lambda$a collision-resistant hash function. Using these primitives, we now instantiate the syntax of our income-transparent e-cash scheme: \begin{itemize} \item$\algo{ExchangeKeygen}(1^{\lambda}, 1^{\kappa}, \mathfrak{D})$: Generate the exchange's signing key pair$\V{skESig} \leftarrow \algo{KeyGen}_{S}(1^\lambda)$. For each element in the sequence$\mathfrak{D} = d_1,\dots,d_n$, generate denomination key pair$(\V{skD}_i, \V{pkD}_i) \leftarrow \algo{KeyGen}_{BS}(1^\lambda)$. \item$\algo{CustomerKeygen}(1^\lambda,1^\kappa)$: Return key pair$\algo{KeyGen}_S(1^\lambda)$. \item$\algo{MerchantKeygen}(1^\lambda,1^\kappa)$: Return key pair$\algo{KeyGen}_S(1^\lambda)$. \item$\algo{WithdrawRequest}(\prt{E}(\V{sksE}, \V{pkCustomer}), \prt{C}(\V{skCustomer}, \V{pksE}, \V{pkD}))$: Let$\V{skD}$be the exchange's denomination secret key corresponding to$\V{pkD}$. \begin{enumerate} \item \prt{C} generates coin key pair$(\V{skCoin}, \V{pkCoin}) \leftarrow \algo{KeyGen}_{CSK}(1^\lambda)$\item \prt{C} runs$(\overline{m}, r) \leftarrow \algo{Blind}_{CSK}(\mathcal{E}(\V{skCoin}), \mathcal{C}(m))$with the exchange \end{enumerate} The withdraw identifier is then \begin{equation*} \V{wid} := (\V{skCoin}, \V{pkCoin}, \overline{m}, r) \end{equation*} \item$\algo{WithdrawPickup}(\prt{E}(\V{sksE}, \V{pkCustomer}), \prt{C}(\V{skCustomer}, \V{pksE}, \V{wid}))$: The customer looks up$\V{skCoin}$,$\V{pkCoin}$, \V{pkD}$\overline{m}$and$r$via the withdraw identifier$\V{wid}$. \begin{enumerate} \item \prt{C} runs$\overline{\sigma} \leftarrow \algo{Sign}_{BS}(\mathcal{E}(\V{skD}), \mathcal{C}(\overline{m}))$with the exchange \item \prt{C} unblinds the signature$\sigma \leftarrow \algo{UnblindSig}_{BS}(\overline{\sigma}, r, \overline{m})$and stores the coin$(\V{skCoin}, \V{pkCoin}, \V{pkD}, \sigma)$in their wallet. \end{enumerate} \item$\algo{Spend}(\V{transactionId}, f, \V{coin}, \V{pkMerchant})$: Let$(\V{skCoin}, \V{pkCoin}, \V{pkD}, \sigma_C) := \V{coin}. The deposit permission is computed as \begin{equation*} \V{depositPermission} := (\V{pkCoin}, \sigma_D, m), \end{equation*} where \begin{align*} m &:= (\V{pkCoin}, \V{pkD}, \V{sigma}_C, \V{transactionId}, f, \V{pkMerchant}) \\ \sigma_D &\leftarrow \algo{Sign}_{CSK}(\V{skCoin}, m). \end{align*} \item\algo{Deposit}(\prt{E}(\V{sksE}, \V{pkMerchant}), \prt{M}(\V{skMerchant}, \V{pksE}, \V{depositPermission})): The merchant sends \V{depositPermission} to the exchange. The exchange checks that the deposit permission is well-formed and sets \begin{align*} (\V{pkCoin}, \V{pkD}, \sigma_C, \sigma_D, \V{transactionId}, f, \V{pkMerchant})) &:= \V{depositPermission} \end{align*} The exchange checks the signature on the deposit permission and the validity of the coin with \begin{align*} b_1 := \algo{Verify}_{CSK}(\V{pkCoin}, \sigma_D, m) \\ b_2 := \algo{Verify}_{BS}(\V{pkD}, \sigma_C, \V{pkCoin}) \end{align*} and aborts ofb_1 = 0$or$b_2=0$. The exchange aborts if spending$f$would result in overspending$\V{pkCoin}$based on existing deposit/refresh records, and otherwise marks$\V{pkCoin}$as spent for$D(\V{pkD})$. \item$\algo{RefreshRequest}(\prt{E}(\V{sksE}, \V{pkCustomer}), \prt{C}(\V{skCustomer}, \V{pksE}, \V{coin}_0, \V{pkD}_u))$: Let$\V{skD}_u$be the secret key corresponding to$\V{pkD}_u$. We write $\algo{Blind}^*_{BS}(\mathcal{S}(\V{sk}, \V{skESig}), \mathcal{R}(R, \V{skR}, \V{pk}, m)) \mapsto (\overline{m}, r, \mathcal{T}_{B*})$ for a modified version of$\algo{Blind}_{BS}$where the signature requester$\mathcal{R}$takes all randomness from the sequence$\left(\V{PRF}(R,\texttt{"blind"}\Vert n)\right)_{n>0}$, the messages from the exchange are recorded in transcript$\mathcal{T}_{B*}$, all messages sent by$\mathcal{R}$are signed with$\V{skR}$and all messages sent by$\mathcal{S}$are signed with$\V{skESig}$. Furthermore, we write $\algo{KeyGen}^*_{CSK}(R, 1^\lambda) \mapsto (\V{sk}, \V{pk})$ for a modified version of the key generation algorithm that takes randomness from the sequence$\left(\V{PRF}(R,\texttt{"key"}\Vert n)\right)_{n>0}$. For each$i\in \{1,\dots,\kappa \}$, the customer \begin{enumerate} \item generates seed$s_i \randsel \{1, \dots, 1^\lambda\}$\item generates transfer key pair$(t_i, T_i) \leftarrow \algo{KeyGen}^*_{CSK}(s_i, 1^\lambda)$\item computes transfer secret$x_i \leftarrow \algo{Kx}(t_i, \V{pkCoin}_0)$\item computes coin key pair$(\V{skCoin}_i, \V{pkCoin}_i) \leftarrow \algo{KeyGen}^*_{CSK}(x_i, 1^\lambda)$\item and executes the modified blinding protocol $(\overline{m}_i, r_i, \mathcal{T}_{(B*,i)}) \leftarrow \algo{Blind}^*_{BS}(\mathcal{E}(\V{skD_u}), \mathcal{C}(x_i, \V{skCoin}_0, \V{pkD}_u, \V{pkCoin}_i))$ with the exchange. \end{enumerate} The customer stores the refresh identifier $$\V{rid} := (\V{coin}_0, \V{pkD}_u, \{ s_i \}, \{ \overline{m}_i \}, \{r_i\}, \{\mathcal{T}_{(B*,i)}\} ).$$ \item$\algo{RefreshPickup}(\prt{E}(\V{sksE}, \V{pkCustomer}), \prt{C}(\V{skCustomer}, \V{pksE}, \V{rid})) \rightarrow \mathcal{T}$: The customer looks up the refresh identifier$\V{rid}$and recomputes the transfer key pairs, transfer secrets and new coin key pairs. Then customer sends the commitment$\pi_1 = (\V{pkCoin}_0, \V{pkD}_u, h_C)$together with signature$\V{sig}_1 \leftarrow \algo{Sign}_{CSK}(\V{skCoin}_0, \pi_1)to the exchange, where \begin{align*} h_T &:= H(T_1, \dots, T_\kappa)\\ h_{\overline{m}} &:= H(\overline{m}_1, \dots, \overline{m}_\kappa)\\ h_C &:= H(h_T \Vert h_{\overline{m}}) \end{align*} The exchange checks the signature\V{sig}_1$, and aborts if invalid. Otherwise, depending on the commitment: \begin{enumerate} \item If the exchange did not see$\pi_1$before, it marks$\V{pkCoin}_0$as spent for$D(\V{pkD}_u)$, chooses a uniform random$0 \le \gamma < \kappa$, stores it, and sends this choice in a signed message$(\gamma, \V{sig}_2)$to the customer, where$\V{sig}_2 \leftarrow \algo{Sign}_{S}(\V{skESig}, \gamma)$. \item Otherwise, the exchange sends back the same$\pi_2$as it sent for the last equivalent$\pi_1$. \end{enumerate} The customer checks if$\pi_2$differs from a previously received$\pi_2'$for the same request$\pi_1$, and aborts if such a conflicting response was found. Otherwise, the customer in response to$\pi_2$sends the reveal message \begin{equation*} \pi_3 = T_\gamma, \overline{m}_\gamma, (s_1, \dots, s_{\gamma-1}, s_{\gamma+1}, \dots, s_\kappa) \end{equation*} and signature \begin{equation*} \V{sig}_{3'} \leftarrow \algo{Sign}_{CSK}(\V{skCoin}_0, (\V{pkCoin}_0, \V{pkD}_u, \mathcal{T}_{(B*,\gamma)}, T_\gamma, \overline{m}_\gamma)) \end{equation*} to the exchange. Note that$\V{sig}_{3'}$is not a signature over the full reveal message, but is primarily used in the linking protocol for checks by the customer. The exchange checks the signature$\V{sig}_{3'}$and then computes for$i \ne \gamma: \begin{align*} (t_i', T_i') &\leftarrow \algo{KeyGen}^*_{CSK}(s_i, 1^\lambda)\\ x_i' &\leftarrow \algo{Kx}(t_i, \V{pkCoin}_0)\\ (\V{skCoin}_i', \V{pkCoin}_i') &\leftarrow \algo{KeyGen}^*_{CSK}(x_i', 1^\lambda) \\ h_T' &:= H(T'_1, \dots, T_{\gamma-1}', T_\gamma, T_{\gamma+1}', \dots, T_\kappa') \end{align*} and simulates the blinding protocol with recorded transcripts (without signing each message, as indicated by the dot (\cdot) instead of a signing secret key), obtaining \begin{align*} (\overline{m}_i', r_i', \mathcal{T}_i) &\leftarrow \algo{Blind}^*_{BS}(\mathcal{S}(\V{skD}_u), \mathcal{R}(x_i', \cdot, \V{pkD}_u, \V{skCoin}'_i))\\ \end{align*} and finally \begin{align*} h_{\overline{m}}' &:= H(\overline{m}_1', \dots, \overline{m}_{\gamma-1}', \overline{m}_\gamma, \overline{m}_{\gamma+1}',\dots, \overline{m}_\kappa')\\ h_C' &:= H(h_T' \Vert h_{\overline{m}}'). \end{align*} Now the exchange checks ifh_C = h_C'$, and aborts the protocol if the check fails. Otherwise, the exchange sends a message back to$\prt{C}$that the commitment verification succeeded and includes the signature \begin{equation*} \overline{\sigma}_\gamma := \algo{Sign}_{BS}(\mathcal{E}(\V{skD}_u), \mathcal{C}(\overline{m}_\gamma)). \end{equation*} As a last step, the customer obtains the signature$\sigma_\gamma$on the new coin's public key$\V{pkCoin}_u$with \begin{equation*} \sigma_\gamma := \algo{UnblindSig}(r_\gamma, \V{pkCoin}_\gamma, \overline{\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. For each completed refresh on$\V{pkCoin}_0$recorded in the exchange's database, the exchange sends the following data back to the customer: the signed commit message$(\V{sig}_1, \pi_1)$, the transfer public key$T_\gamma$, the signature$\V{sig}_{3'}$, the blinded signature$\overline{\sigma}_\gamma$, and the transcript$\mathcal{T}_{(B*,\gamma)}$of the customer's and exchange's messages during the$\algo{Blind}^*_{BS}$protocol execution. The following logic is repeated by the customer for each response: \begin{enumerate} \item Verify the signatures (both from$\V{pkESig}$and$\V{pkCoin}_0$) on the transcript$\mathcal{T}_{(B*,\gamma)}$, abort otherwise. \item Verify that$\V{sig}_1$is a valid signature on$\pi_1$by$\V{pkCoin}_0, abort otherwise. \item Re-compute the transfer secret and the new coin's key pair as \begin{align*} x_\gamma &\leftarrow \algo{Kx}_{CSK}(\V{skCoin}_0, T_\gamma)\\ (\V{skCoin}_\gamma, \V{pkCoin}_\gamma) &\leftarrow \algo{KeyGen}_{CSK}^*(x_\gamma, 1^\lambda). \end{align*} \item Simulate the blinding protocol with the message transcript received from the exchange to obtain(\overline{m}_\gamma, r_\gamma)$. \item Check that$\algo{Verify}_{CSK}(\V{pkCoin}_0, \V{pkD}_u, \V{skCoin}_0,(\mathcal{T}_{(B*,\gamma)}, \overline{m}_\gamma), \V{sig}_{3'})$indicates a valid signature, abort otherwise. \item Unblind the signature to obtain$\sigma_\gamma \leftarrow \algo{UnblindSig}(r_\gamma, \V{pkCoin}_\gamma, \overline{\sigma}_\gamma)$\item (Re-)add the coin$(\V{skCoin}_\gamma, \V{pkCoin}_\gamma, \V{pkD}_u, \sigma_\gamma)$to the customer's wallet. \end{enumerate} \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-FDH blind signatures \cite{chaum1983blind,bellare1996exact}. From the information-theoretic security of 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. For the collision-resistant hash function$H$we use SHA-512 \cite{rfc4634} and HKDF \cite{rfc5869} as a PRF. %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. %% https://safecurves.cr.yp.to/refs.html#2007/bernstein-newelliptic %% https://safecurves.cr.yp.to/complete.html %We warn however that Weierstrass curves have incomplete addition formulas %that permit an adversarial merchant to pick transfer keys that yields failures. %There are further implementation mistakes that might enable collaborative %key exchange failures, like if the exchange does not enforce the transfer %private key being a multiple of the cofactor. % %In this vein, almost all post-quantum key exchanges suffer from key exchange %failures that permit invalid key attacks against non-ephemeral keys. %All these schemes support only one ephemeral party by revealing the %ephemeral party's private key to the non-ephemeral party, % ala the Fujisaki-Okamoto transform~\cite{fujisaki-okamoto} or similar. %We cannot reveal the old coin's private key to the exchange when %verifying the transfer private keys though, which % complicates verifying honest key generation of the old coin's key. \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} We now give proofs for the security properties defined in Section \ref{sec:security-properties} with the generic instantiation of Taler. \subsection{Anonymity} \begin{theorem} Assuming \begin{itemize} \item the blindness of \textsc{BlindSign}, \item the unforgeability and key exchange security of \textsc{CoinSignKx}, and \item the collision resistance of$H$, \end{itemize} our instantiation satisfies 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)$, where$\mathbb{G}_0(b)$is the original anonymity game$\mathit{Exp}_{\cal A}^{anon}(1^\lambda, 1^\kappa, b)$. We show that the adversary can distinguish between subsequent games with only negligible probability. Let$\epsilon_{HC}$and$\epsilon_{KX}$be the advantage of an adversary for finding hash collisions and for breaking the security of the key exchange, respectively. We define$\mathbb{G}_1$by replacing the link oracle \ora{Link} with a modified version that behaves the same as \ora{Link}, unless the adversary responds with link data that did not occur in the transcript of a successful refresh operation, but despite of that still passes the customer's verification. In that case, the game is aborted instead. Observe that in case this failure event happens, the adversary must have forged a signature on$\V{sig}_{3}$on values not signed by the customer, yielding an existential forgery. Thus,$\left| \Prb{\mathbb{G}_0 = 1} - \Prb{\mathbb{G}_1 = 1} \right|$is negligible. In$\mathbb{G}_2$, the refresh oracle is modified so that the customer responds with value drawn from a uniform random distribution$D_1$for the$\gamma$-th commitment instead of using the key exchange function. We must handle the fact that$\gamma$is chosen by the adversary after seeing the commitments, so the challenger first makes a guess$\gamma^*$and replaces only the$\gamma^*$-th commitment with a uniform random value. If the$\gamma$chosen by the adversary does not match$\gamma^*$, then the challenger rewinds \prt{A} to the point where the refresh oracle was called. Note that we only replace the one commitment that will not be opened to the adversary later. Since$\kappa \ll \lambda$and the security property of$\algo{Kx}$guarantees that the adversary cannot distinguish the result of a key exchange from randomness, the runtime complexity of the challenger still stays polynomial in$\lambda$. An adversary that could with high probability choose a$\gamma$that would cause a rewind, could also distinguish randomness from the output of$\algo{Kx}$. %\mycomment{Tighness bound also missing} We now show that$\left| \Prb{\mathbb{G}_1 = 1} - \Prb{\mathbb{G}_2 = 1} \right| \le \epsilon_{KX}$by defining a distinguishing game$\mathbb{G}_{1 \sim 2}$for the key exchange as follows: \bigskip \noindent$\mathbb{G}_{1 \sim 2}(b)$: \vspace{-0.5\topsep} \begin{enumerate} \setlength\itemsep{0em} \item If$b=0$, set $D_0 := \{ (A, B, \V{Kex}(a, B)) \mid (a, A) \leftarrow \V{KeyGen}(1^\lambda),(b, B) \leftarrow \V{KeyGen}(1^\lambda) \}.$ Otherwise, set $D_1 := \{ (A, B, C) \mid (a, A) \leftarrow \V{KeyGen}(1^\lambda), (b, B) \leftarrow \V{KeyGen}(1^\lambda), C \randsel \{1,\dots,2^\lambda\} \}.$ \item Return$\mathit{Exp'}_{\cal A}^{anon}(b, D_b)$(Modified anonymity game where the$\gamma$-th commitment in the refresh oracle is drawn uniformly from$D_b$(using rewinding). Technically, we need to draw from$D_b$on withdraw for the coin secret key, write it to a table, look it up on refresh and use the matching tuple, so that with$b=0$we perfectly simulate$\mathbb{G}_1$.) \end{enumerate} Depending on the coin flip$b$, we either simulate$\mathbb{G}_1$or$\mathbb{G}_2$perfectly for our adversary~$\mathcal{A}$against$\mathbb{G}_1$. At the same time$b$determines whether \prt{A} receives the result of the key exchange or real randomness. Thus,$\left| \Prb{\mathbb{G}_1 = 1} - \Prb{\mathbb{G}_2 = 1} \right| = \epsilon_{KX}$is exactly the advantage of$\mathbb{G}_{1 \sim 2}$. We observe in$\mathbb{G}_2$that as$x_\gamma$is uniform random and not learned by the adversary, the generation of$(\V{skCoin}_\gamma, \V{pkCoin}_\gamma)$and the execution of the blinding protocol is equivalent (under the PRF assumption) to using the randomized algorithms$\algo{KeyGen}_{CSK}$and$\algo{Blind}_{BS}$. By the blindness of the$\textsc{BlindSign}$scheme, the adversary is not able to distinguish blinded values from randomness. Thus, the adversary is unable to correlate a$\algo{Sign}_{BS}$operation in refresh or withdraw with the unblinded value observed during$\algo{Deposit}$. We conclude the success probability for$\mathbb{G}_2$must be$1/2$and hence the success probability for$\mathit{Exp}_{\cal A}^{anon}(1^\lambda, \kappa, b)$is at most$1/2 + \epsilon(\lambda)$, where$\epsilon$is a negligible function. \end{proof} % RSA ratios vs CDH in BLS below \subsection{Conservation} \begin{theorem} Assuming existential unforgeability (EUF-CMA) of \textsc{CoinSignKx}, our instantiation satisfies conservation. \end{theorem} \begin{proof} % FIXME: argue that reduction is tight when you have malleability In honest executions, we have$\V{withdrawn}[\V{pkCustomer}] = v_C + v_S$, i.e., the coins withdrawn add up to the coins still available and the coins spent for known transactions. In order to win the conservation game, the adversary must increase$\V{withdrawn}[\V{pkCustomer}]$or decrease$v_C$or$v_S$. An adversary can abort withdraw operations, thus causing$\V{withdrawn}[\V{pkCustomer}]$to increase, while the customer does not obtain any coins. However, in step \ref{game:conserv:run}, the customer obtains coins from interrupted withdraw operations. Similarly, for the refresh protocol, aborted \algo{RefreshRequest} / \algo{RefreshPickup} operations that result in a coin's remaining value being reduced are completed in step \ref{game:conserv:run}. Thus, the only remaining option for the adversary is to decrease$v_C$or$v_S$with the$\ora{RefreshPickup}$and$\ora{Deposit}$oracles, respectively. Since the exchange verifies signatures made by the secret key of the coin that is being spent/refreshed, the adversary must forge this signature or have access to the coin's secret key. As we do not give the adversary access to the sharing oracle, it does not have direct access to any of the honest customer's coin secret keys. Thus, the adversary must either compute the coin's secret key from observing the coin's public key (e.g., during a partial deposit operation), or forge signatures directly. Both possibilities allow us to carry out a reduction against the unforgeability property of the$\textsc{CoinSignKx}$scheme, by injecting the challenger's public key into one of the coins. \end{proof} \subsection{Unforgeability} \begin{theorem} Assuming the unforgeability of \textsc{BlindSign}, our instantiation satisfies {unforgeability}. \end{theorem} \begin{proof} The adversary must have produced at least one coin that was not blindly signed by the exchange. In order to carry out a reduction from this adversary to a blind signature forgery, we inject the challenger's public key into one randomly chosen denomination. Since we do not have access to the corresponding secret key of the challenger, signing operations for this denomination are replaced with calls to the challenger's signing oracle in \ora{WithdrawPickup} and \ora{RefreshPickup}. For$n$denominations, an adversary against the unforgeability game would produce a blind signature forgery with probability$1/n$. \end{proof} %TODO: RSA-KTI \subsection{Income Transparency} \begin{theorem} Assuming \begin{itemize} \item the unforgeability of \textsc{BlindSign}, \item the key exchange completeness of \textsc{CoinSignKx}, \item the pseudo-random function property of \V{PRF}, and \item the collision resistance of$H$, \end{itemize} our instantiation satisfies {weak income transparency}. \end{theorem} \begin{proof} We consider the directed forest on coins induced by the refresh protocol. It follows from unforgeability that any coin must originate from some customer's withdraw in this graph. We may assume that all$\V{coin}_1, \dots, \V{coin}_l$originate from non-corrupted users, for some$l \leq \ell$. % So$\ell \leq w + |X|$. For any$i \leq l$, there is a final refresh operation$R_i$in which a non-corrupted user could obtain the coin$C'$consumed in the refresh via the linking protocol, but no non-corrupted user could obtain the coin provided by the refresh, as otherwise$\V{coin}_i$gets marked as spent in step step \ref{game:income:spend}. Set$F := \{ R_i \mid i \leq l \}$. During each$R_i \in F$, our adversary must have submitted a blinded coin and transfer public key for which the linking protocol fails to produce the resulting coin correctly, otherwise the coin would have been spent in step \ref{game:income:spend}. In this case, we consider several non-exclusive cases \begin{enumerate} \item the execution of the refresh protocol is incomplete, \item the commitment for the$\gamma$-th blinded coin and transfer public key is dishonest, \item a commitment for a blinded coin and transfer public key other than the$\gamma$-th is dishonest, \end{enumerate} We show these to be exhaustive by assuming their converses all hold: As the commitment is signed by$\V{skCoin}_0$, our key exchange completeness assumption of$\textsc{CoinSignKx}$applies to the coin public key. Any revealed values must match our honestly computed commitments, as otherwise a collision in$H$would have been found. We assumed the revealed$\gamma$-th transfer public key is honest. Hence our key exchange completeness assumption of$\textsc{CoinSignKx}$yields$\algo{Kex}_{CSK}(t,C') = \algo{Kex}_{CSK}(c',T)$where$T = \algo{KeyGenPub}_{CSK}(t)$is the transfer key, thus the customer obtains the correct transfer secret. We assumed the refresh concluded and all submissions besides the$\gamma$-th were honest, so the exchange correctly reveals the signed blinded coin. We assumed the$\gamma$-th blinded coin is correct too, so customer now re-compute the new coin correctly, violating$R_i \in F$. We shall prove $$\label{eq:income-transparency-proof} \Exp{{\frac{p}{b + p}} \middle| F \neq \emptyset} = {\frac{1}{\kappa}}$$ where the expectation runs over any probability space used by the adversary and challenger. We shall now consider executions of the income transparency game with an optimal adversary with respect to maximizing$\frac{p}{b + p}$. Note that this is permissible since we are not carring out a reduction, but are interested in the expectation of the game's return value. As a reminder, if a refresh operation is initiated using a false commitment that is detected by the exchange, then the new coin cannot be obtained, and contributes to the lost coins$b := w - s$instead of the winnings$p := L - w'$. We also note$b + p$gives the value of refreshes attempted with false commitments. As these are non-negative,$\frac{p}{b + p}$is undefined if and only if$p = 0$and$b = 0$, which happens if and only if the adversary does not use false commitments, i.e.,$F = \emptyset$. We may now assume for optimality that$\mathcal{A}$submits a false commitment for at most one choice of$\gamma$in any$R_i \in F$, as otherwise the refresh always fails. Furthermore, for an optimal adversary we can exclude refreshes in$F$that are incomplete, but that would be possible to complete successfully, as completing such a refresh would only increase the adversaries winnings. We emphasize that an adversary that loses an$R_i$loses the coin that would have resulted from it completely, while an optimal adversary who wins an$R_i$should not gamble again. Indeed, an adversary has no reason to touch its winnings from an$R_i$. % There is no way to influence$p$or$b$through withdrawals or spends % by corrupted users of course. In principle, one could decrease$b$by % sharing from a corrupted user to a non-corrupted users, % but we may assume this does not occur either, again by optimality. For any$R_i$, there are$\kappa$game runs identical up through the commitment phase of$R_i$and exhibiting different outcomes based on the challenger's random choice of$\gamma$. If$v_i$is the financial value of the coin resulting from refresh operation$R_i$then one of the possible runs adds$v_i$to$p$, while the remaining$\kappa-1$runs add$v_i$to$b$. We define$p_i$and$b_i$to be these contributions summed over the$\kappapossible runs, i.e., \begin{align*} p_i &:= v_i\\ b_i &= (\kappa - 1)v_i \end{align*} The adversary will succeed in1/\kappa$runs ($p_i=v$) and loses in$(\kappa-1)/\kappa$runs ($p_i=0). Hence: \begin{align*} \Exp{{\frac{p}{b + p}} \middle| F \neq \emptyset} &= \frac{1}{|F|} \sum_{R_i\in F} {p_i \over b_i + p_i} \\ &= \frac{1}{\kappa |F|} \sum_{R_i\in F} {\frac{v_i}{0 + v_i}} + \frac{\kappa-1}{\kappa |F|} \sum_{R_i \in F} {\frac{0}{v_i + 0}} \\ &= {\frac{1}{\kappa}}, \end{align*} which yields the equality (\ref{eq:income-transparency-proof}). As forF = \emptyset$, the return value of the game must be$0\$, we conclude \begin{equation*} E\left[\mathit{Exp}_{\cal A}^{income}(1^\lambda, 1^\kappa)\right] \le {\frac{1}{\kappa}}. \end{equation*} \end{proof} \section{Discussion} \subsection{Limitations} Not all features of our implementation are part of the security model and proofs. In particular, the following features are left out of the formal discussion: \begin{itemize} \item Reserves. In our formal model, we effectively assume that every customer has access to exactly one unlimited reserve. \item Offline and online keys. In our implementation, the exchange has one offline master signing key, and online signing keys with a shorter live span. \item Refunds allow merchants to effectively undo'' a deposit operation before the exchange settles the transaction with the merchant. This simple extension preserves unlinkability of payments through refresh. %\item Indian merchant scenario. In some markets (such as India), it is more % likely for the customer to have Internet access (via smart phones) than for % merchants, who in the case of street vendors often have simple phones % without Internet access or support for apps. To use Taler in this case, % it must be possible \item Timeouts. In practice, a merchant gives the customer a deadline until which the payment for a contract must have been completed, potentially by using multiple coins. If a customer is unable to complete a payment (e.g., because they notice that their coins are already spent after a restore from backup), a refund for this partial payment can be requested from the merchant. Should the merchant become unavailable after a partially completed payment, there are two possibilities: Either the customer can deposit the coins on behalf of the merchant to obtain proof of their on-time payment, which can be used in a later arbitration if necessary. Alternatively, the customer can ask the exchange to undo the partial payments, though this requires the exchange to know (or learn from the customer) the exact amount to be payed for the contract. %A complication in practice is that merchants may not want to reveal their %full bank account information to the customer, but this information is %necessary for the exchange to process the deposit, since we do not require %merchants to register beforehand the exchange (as the merchant might %support all exchanges audited by a specific auditor). We discuss a protocol %extension that allows customers to deposit coins on behalf of merchants %in~\ref{XXX}. \item The fees incurred for operations, the protocols for backup and synchronization as well as other possible extensions like tick payments are not formally modeled. %\item FIXME: auditor \end{itemize} We note that customer tipping (see \ref{taler:design:tipping}) basically amounts to an execution of the \algo{Withdraw} protocol where the party that generates the coin keys and blinding factors (in that case the merchant's customer) is different from the party that signs the withdraw request (the merchant with a customer'' key pair tied to the merchant's bank account). While this is desirable in some cases, we discussed in \ref{taler:design:fixing-withdraw-loophole} how this loophole'' for a one-hop untaxed payment could be avoided. \subsection{Other Properties} \subsubsection{Exculpability} Exculpability is a property of offline e-cash which guarantees that honest users cannot be falsely blamed for misbehavior such as double spending. For online e-cash it is not necessary, since coins are spent online with the exchange. In practice, even offline e-cash systems that provide exculpability are often undesirable, since hardware failures can result in unintentional overspending by honest users. If a device crashes after an offline coin has been sent to the merchant but before the write operation has been permanently recorded on the user's device (e.g., because it was not yet flushed from the cache to a hard drive), the next payment will cause a double spend, resulting in anonymity loss and a penalty for the customer. % FIXME: move this to design or implementation \subsubsection{Fair Exchange}\label{sec:security:atomic-swaps} % FIXME: we should mention "atomic swap" here The Endorsed E-Cash system by Camenisch et al. \cite{camenisch2007endorsed} allows for fair exchange---sometimes called atomic swap in the context of cryptocurrencies---of online or offline e-cash against digital goods. The online version of Camenisch's protocol 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.