1730 lines
90 KiB
TeX
1730 lines
90 KiB
TeX
\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 transparency 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*}
|
|
Return $0$ 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*}
|
|
\item $b' \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
|
|
\begin{equation}\label{eq:income-transparency-expectation}
|
|
E\left[\mathit{Exp}_{\cal A}^{income}(1^\lambda, 1^\kappa)\right] \le {\frac{1}{\kappa}} \mathperiod
|
|
\end{equation}
|
|
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 of $b_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
|
|
\begin{equation}
|
|
\V{rid} := (\V{coin}_0, \V{pkD}_u, \{ s_i \}, \{ \overline{m}_i \}, \{r_i\}, \{\mathcal{T}_{(B*,i)}\} ).
|
|
\end{equation}
|
|
|
|
\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 if $h_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
|
|
\begin{equation}\label{eq:income-transparency-proof}
|
|
\Exp{{\frac{p}{b + p}} \middle| F \neq \emptyset} = {\frac{1}{\kappa}}
|
|
\end{equation}
|
|
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 $\kappa$ possible
|
|
runs, i.e.,
|
|
\begin{align*}
|
|
p_i &:= v_i\\
|
|
b_i &= (\kappa - 1)v_i
|
|
\end{align*}
|
|
The adversary will succeed in $1/\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 for $F = \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 paid
|
|
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.
|
|
|