1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
1115
1116
1117
1118
1119
1120
1121
1122
1123
1124
1125
1126
1127
1128
1129
1130
1131
1132
1133
1134
1135
1136
1137
1138
1139
1140
1141
1142
1143
1144
1145
1146
1147
1148
1149
1150
1151
1152
1153
1154
1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
1170
1171
1172
1173
1174
1175
1176
1177
1178
1179
1180
1181
1182
1183
1184
1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
1198
1199
1200
1201
1202
1203
1204
1205
1206
1207
1208
1209
1210
1211
1212
1213
1214
1215
1216
1217
1218
1219
1220
1221
1222
1223
1224
1225
1226
1227
1228
1229
1230
1231
1232
1233
1234
1235
1236
1237
1238
1239
1240
1241
1242
1243
1244
1245
1246
1247
1248
1249
1250
1251
1252
1253
1254
1255
1256
1257
1258
1259
1260
1261
1262
1263
1264
1265
1266
1267
1268
1269
1270
1271
1272
1273
1274
1275
1276
1277
1278
1279
1280
1281
1282
1283
1284
1285
1286
1287
1288
1289
1290
1291
1292
1293
1294
1295
1296
1297
1298
1299
1300
1301
1302
1303
1304
1305
1306
1307
1308
1309
1310
1311
1312
1313
1314
1315
1316
1317
1318
1319
1320
1321
1322
1323
1324
1325
1326
1327
1328
1329
1330
1331
1332
1333
1334
1335
1336
1337
1338
1339
1340
1341
1342
1343
1344
1345
1346
1347
1348
1349
1350
1351
1352
1353
1354
1355
1356
1357
1358
1359
1360
1361
1362
1363
1364
1365
1366
1367
1368
1369
1370
1371
1372
1373
1374
1375
1376
1377
1378
1379
1380
1381
1382
1383
1384
1385
1386
1387
1388
1389
1390
1391
1392
1393
1394
1395
1396
1397
1398
1399
1400
1401
1402
1403
1404
1405
1406
1407
1408
1409
1410
1411
1412
1413
1414
1415
1416
1417
1418
1419
1420
1421
1422
1423
1424
1425
1426
1427
1428
1429
1430
1431
1432
1433
1434
1435
1436
1437
1438
1439
1440
1441
1442
1443
1444
1445
1446
1447
1448
1449
1450
1451
1452
1453
1454
1455
1456
1457
1458
1459
1460
1461
1462
1463
1464
1465
1466
1467
1468
1469
1470
1471
1472
1473
1474
1475
1476
1477
1478
1479
1480
1481
1482
1483
1484
1485
1486
1487
1488
1489
1490
1491
1492
1493
1494
1495
1496
1497
1498
1499
1500
1501
1502
1503
1504
1505
1506
1507
1508
1509
1510
1511
1512
1513
1514
1515
1516
1517
1518
1519
1520
1521
1522
1523
1524
1525
1526
1527
1528
1529
1530
1531
1532
1533
1534
1535
1536
1537
1538
1539
1540
1541
1542
1543
1544
1545
1546
1547
1548
1549
1550
1551
1552
1553
1554
1555
1556
1557
1558
1559
1560
1561
1562
1563
1564
1565
1566
1567
1568
1569
1570
1571
1572
1573
1574
1575
1576
1577
1578
1579
1580
1581
1582
1583
1584
1585
1586
1587
1588
1589
1590
1591
1592
1593
1594
1595
1596
1597
1598
1599
1600
1601
1602
1603
1604
1605
1606
1607
1608
1609
1610
1611
1612
1613
1614
1615
1616
1617
1618
1619
1620
1621
1622
1623
1624
1625
1626
1627
1628
1629
1630
1631
1632
1633
1634
1635
1636
1637
1638
1639
1640
1641
1642
1643
1644
1645
1646
1647
1648
1649
1650
1651
1652
1653
1654
1655
1656
1657
1658
1659
1660
1661
1662
1663
1664
1665
1666
1667
1668
1669
1670
1671
1672
1673
1674
1675
1676
1677
1678
1679
1680
1681
1682
1683
1684
1685
1686
1687
1688
1689
1690
1691
1692
1693
1694
1695
1696
1697
1698
1699
1700
1701
1702
1703
1704
1705
1706
1707
1708
1709
1710
1711
1712
1713
1714
1715
1716
1717
1718
1719
1720
1721
1722
1723
1724
1725
1726
1727
1728
1729

\chapter{Security of IncomeTransparent Anonymous ECash}\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}}}
% longform 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 wellstudied is $Q$? Some branches of cryptography, for example,
some pairingbased 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 gamebased provable security
\cite{bellare2006code,pointcheval2005provable,shoup2004sequences,guo2018introduction}
as opposed to simulationbased provable security \cite{goldwasser1989knowledge,lindell2017simulate},
which is another approach to provable security typically used for
zeroknowledge 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 runtime 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 welldefined 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, multiround 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 (EUFCMA) or existential
unforgeability under known message attack (EUFKMA)
The following modification to the game would model selective unforgeability
(SUFCMA / SUFKMA):
\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 polynomialtime 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 pseudorandom 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 DiffieHellman problem (nicely described by~\cite{boneh1998decision})
\item existential unforgeability under chosen message attack (EUFCMA) of a signature scheme \cite{goldwasser1988digital}
\item indistinguishability against chosenplaintext attacks (INDCPA) 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 polynomialtime algorithm.
A wellknown example for a nontrivial reduction proof is the security proof of
FDHRSA 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 FDHRSA security proof based on game hopping was generated with an
automated theorem prover by Blanchet and Pointcheval \cite{blanchet2006automated}.
% restorefrombackup
% 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 nonatomically: to spend (fractions
of) multiple coins, they must be spent onebyone. 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:securitytalersyntax}
The Taler ecash 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}
polynomialtime 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:securitytalersyntax}, 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 maninthemiddle in these oracles,
it can drop messages to the simulated exchange and make up its own response.
If the adversary calls these oracles with a corrupted customer, the adversary
plays as the customer.
%\begin{mdframed}
%The difference between algorithms and interactive protocols
%is that the ``pure'' algorithms only deal with data, while the interactive protocols
%take ``handles'' to parties that are communicating in the protocol. The adversary can
%always execute algorithms that don't depend on handles to communication partners.
%However the adversary can't run the interactive protocols directly, instead it must
%rely on the interaction oracles for it. Different interaction oracles might allow the
%adversary to play different roles in the same interactive protocol.
%
%While most algorithms in Taler are not probabilistic, we still say that they are, since
%somebody else might come up with an instantiation of Taler that uses probabilistic algorithms,
%and then the games should still apply.
%
%
%While we do have a \algo{Deposit} protocol that's used in some of the games, having a deposit oracle is not necessary
%since it does not give the adversary any additional power.
%\end{mdframed}
\section{Games}
We now define four security games (anonymity, conservation, unforgeability and
income transparency) that are later used to define the security properties for
Taler. Similar to \cite{bellare2006code} we assume that the game and adversary
terminate in finite time, and thus random choices made by the challenger and
adversary can be taken from a finite sample space.
All games except income transpacency return $1$ to indicate that the adversary
has won and $0$ to indicate that the adversary has lost. The income
transparency game returns $0$ if the adversary has lost, and a positive
``laundering ratio'' if the adversary won.
\subsection{Anonymity}
Intuitively, an adversary~$\prt{A}$ (controlling the exchange and merchants) wins the
anonymity game if they have a nonnegligible 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}_{ib}, \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}_{ib}))
\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 noncorrupted customer's
wallets, even though it can use oracles to force protocol interactions of
noncorrupted customers.
For practical ecash 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 ecash 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 noncorrupted customers with their
transitive closure using the \algo{Link} protocol.
Mark all remaining value on coins in wallets of noncorrupted 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 noncorrupted customers, and
$s$ be the value marked as spent by noncorrupted 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:securityproperties}
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 polynomialtime adversary is implied to
be polynimial in $\lambda+\kappa$.
\begin{definition}[Anonymity]
We say that an ecash 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
polynomialtime adversary~$\mathcal{A}$.
\end{definition}
\begin{definition}[Conservation]
We say that an ecash 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 polynomialtime adversary~$\mathcal{A}$.
\end{definition}
\begin{definition}[Unforgeability]
We say that an ecash 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 polynomialtime adversary
$\mathcal{A}$.
\end{definition}
\begin{definition}[Strong Income Transparency]
We say that an ecash 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 polynomialtime 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 nonzero, i.e., there was at least one
successful attempt to obtain untaxed income.
\begin{definition}[Weak Income Transparency]
We say that an ecash scheme satisfies \emph{weak income transparency}
if, for any polynomialtime adversary~$\mathcal{A}$,
the return value of the income transparency game satisfies
\begin{equation}\label{eq:incometransparencyexpectation}
E\left[\mathit{Exp}_{\cal A}^{income}(1^\lambda, 1^\kappa)\right] \le {\frac{1}{\kappa}} \mathperiod
\end{equation}
In (\ref{eq:incometransparencyexpectation}), the expectation runs over
any probability space used by the adversary and challenger.
\end{definition}
For some instantiations, e.g., ones based on zeroknowledge proofs, $\kappa$
might be a security parameter in the traditional sense. However for an ecash
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 cutandchoose parameter, as the complexity of our cutandchoose
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
returnoninvestment (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 collisionresistant hash function and a pseudorandom 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 ecash
\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 nonnegligible 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 (EUFCMA).
\item \emph{key exchange completeness}:
Any probabilistic polynomialtime 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 (SUFCMA).
Let $\V{PRF}$ be a pseudorandom function family and $H : \{0,1\}^* \rightarrow \{0,1\}^\lambda$
a collisionresistant hash function.
Using these primitives, we now instantiate the syntax of our incometransparent ecash 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 wellformed 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_{\gamma1}, 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_{\gamma1}', 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}_{\gamma1}', \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 Recompute 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 RSAFDH blind signatures
\cite{chaum1983blind,bellare1996exact}. From the informationtheoretic
security of blinding, the computational blindness property follows directly. For
the unforgeability property, we additionally rely on the RSAKTI assumption as
discussed in \cite{bellare2003onemore}. Note that since the blinding step in
RSA blind signatures is noninteractive, 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 DiffieHellman 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 ellipticcurve signatures, concretely Ed25519. For
the collisionresistant hash function $H$ we use SHA512 \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/bernsteinnewelliptic
%% 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 postquantum key exchanges suffer from key exchange
%failures that permit invalid key attacks against nonephemeral keys.
%All these schemes support only one ephemeral party by revealing the
%ephemeral party's private key to the nonephemeral party,
% ala the FujisakiOkamoto transform~\cite{fujisakiokamoto} 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:securityproperties}
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 (EUFCMA) 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: RSAKTI
\subsection{Income Transparency}
\begin{theorem}
Assuming
\begin{itemize}
\item the unforgeability of \textsc{BlindSign},
\item the key exchange completeness of \textsc{CoinSignKx},
\item the pseudorandom 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
noncorrupted 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 noncorrupted user could obtain the coin $C'$ consumed in the refresh
via the linking protocol, but no noncorrupted 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 nonexclusive 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 recompute the new coin correctly, violating
$R_i \in F$.
We shall prove
\begin{equation}\label{eq:incometransparencyproof}
\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 nonnegative,
$\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 noncorrupted 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
$\kappa1$ 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
$(\kappa1)/\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{\kappa1}{\kappa F} \sum_{R_i \in F} {\frac{0}{v_i + 0}} \\
&= {\frac{1}{\kappa}},
\end{align*}
which yields the equality (\ref{eq:incometransparencyproof}).
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 ontime payment, which can
be used in a later arbitration if necessary. Alternatively, the customer
can ask the exchange to undo the partial payments, though this requires the
exchange to know (or learn from the customer) the exact amount to be payed
for the contract.
%A complication in practice is that merchants may not want to reveal their
%full bank account information to the customer, but this information is
%necessary for the exchange to process the deposit, since we do not require
%merchants to register beforehand the exchange (as the merchant might
%support all exchanges audited by a specific auditor). We discuss a protocol
%extension that allows customers to deposit coins on behalf of merchants
%in~\ref{XXX}.
\item The fees incurred for operations, the protocols for backup and
synchronization as well as other possible extensions like tick payments are
not formally modeled.
%\item FIXME: auditor
\end{itemize}
We note that customer tipping (see \ref{taler:design:tipping}) basically amounts to an execution
of the \algo{Withdraw} protocol where the party that generates the coin keys
and blinding factors (in that case the merchant's customer) is different from
the party that signs the withdraw request (the merchant with a ``customer'' key
pair tied to the merchant's bank account). While this is desirable in some
cases, we discussed in \ref{taler:design:fixingwithdrawloophole} how this ``loophole'' for a onehop untaxed
payment could be avoided.
\subsection{Other Properties}
\subsubsection{Exculpability}
Exculpability is a property of offline ecash which guarantees that honest users
cannot be falsely blamed for misbehavior such as double spending. For online
ecash it is not necessary, since coins are spent online with the exchange. In
practice, even offline ecash 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:atomicswaps}
% FIXME: we should mention "atomic swap" here
The Endorsed ECash system by Camenisch et al. \cite{camenisch2007endorsed}
allows for fair exchangesometimes called atomic swap in the context of
cryptocurrenciesof online or offline ecash 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 ecash 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.
