summaryrefslogtreecommitdiff
path: root/games/games.tex
blob: abf57f93bc9237c60e21c6935daf9b4ddb5ac735 (plain)
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
\documentclass[a4paper]{scrartcl}

\usepackage[utf8]{inputenc}
\usepackage{amsmath,amssymb,amsthm}
\usepackage{pifont}
\usepackage{url}
\usepackage[left=20mm,top=20mm]{geometry}
\usepackage{booktabs}
\usepackage{hyperref}
\usepackage{subcaption}
\usepackage{mathpazo}
\usepackage{mathtools}
\usepackage{mdframed}
\usepackage{enumitem}
% \usepackage[amsmath,thmmarks]{ntheorem}
\usepackage[usenames,dvipsnames,svgnames,table]{xcolor}

\def\Z{\mathbb{Z}}

% not amsthm
% \theoremseparator{.} % normal theorem

\title{Taler Security Proofs}
\date{\today}

\newtheorem{lemma}{Lemma}[section]
\newtheorem{theorem}[lemma]{Theorem}
\newtheorem{corollary}[lemma]{Corollary}

\theoremstyle{definition}
\newtheorem{definition}{Definition}[section]

\def\mathperiod{.}
\def\mathcomma{,}

\newcommand*\ST[5]%
{\left#1\,#4\vphantom{#5} \;\right#2 \left. #5 \vphantom{#4}\,\right#3}


\begin{document}

% uniform random selection from set
\newcommand{\randsel}[0]{\ensuremath{\xleftarrow{\text{\$}}}}

% oracles
\newcommand{\ora}[1]{\ensuremath{\mathcal{O}\mathsf{#1}}}
% oracle set
\newcommand{\oraSet}[1]{\ensuremath{\mathcal{O}\textsc{#1}}}
% algorithm
\newcommand{\algo}[1]{\ensuremath{\mathsf{#1}}}
% party
\newcommand{\prt}[1]{\ensuremath{\mathcal{#1}}}
% long-form variable
\newcommand{\V}[1]{\ensuremath{\mathit{#1}}}

% probability with square brackets of the right size
\newcommand{\Prb}[1]{\ensuremath{\Pr\left [#1 \right ]}}

\newcommand{\comment}[1]{~\\ {\small \textcolor{blue}{({#1})}}}

\maketitle


%%%%%%%%%
% TODOS
%%%%%%%%
% 
% * properly characterize what having "Anonymity", "(Weak/Strong) Income Transparency" etc means
%   in terms of winning the games
% * our theorems don't really mention the security parameters "in the output",
%   shouldn't we be able to talk about the bounds of the reduction?
% * fairness is not a reduction or game hop
% * the "tracking variables" should probably be part
%   of the oracles, not of the protocol syntax
% * the concept of "finishing operations" before the next step in a game
%   is unclear, what power does this give the adversary?
% * do we need the deposit oracle?  cutting down the tree does not have it ...
% * adding the link oracle means we must also account for it in fairness and
%   unforgeability
% * can we formulate games so they don't refer to "failed refresh" directly?
%   (since in some instantiations, refreshing can't fail)
% * at least for fairness, we have to think more about Deposit, and
%   whether there should be a separate oracle for it
%


% TODO:
% - note about double spending vs overspending

\section{Model and Syntax}

We consider a single exchange with many users.  The users can act as a
merchant, a customer or both, with no further distinction other than in naming.
We prefix public and secret keys with $pk$ and $sk$, following standard
convention.  For succinctness, the public key of a coin always implicitly has a
denomination (in form of the exchange's denomination public key) associated
with it.

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 both bandwidth and
anonymity, in keeping with existing literature.  For anonymity, we believe this
amounts to assuming that all users have similar financial behavior.  
We note logarithmic bandwidth demands denominations distributed by at least 
powers of a fixed constant, like two.  

We do not include fees taken by the exchange in our model.  Reserves are also
omitted, conceptually every user has exactly one bank account that they
withdraw from, the bank account balance starts at zero and can go negative
without any limit.  
% TODO: Say roughly: In the real world Taler depends on account balances being only positive,
% but this model simplifies our games and security arguments.  ??? 

Coins can be partially spent by specifying a fraction $f \in \mathbb{Q}$. 
Our refresh protocol cannot then give change below the smallest denomination 
though. % so doing this either looses money or requires the exchange permit users to break their anonymity for small transactions.

The spending of multiple coins is modeled non-atomically: to spend multiple coins,
they must be spent one-by-one.  The individual spend/deposit operations are correlated
by a unique identifier for the transaction.  In practice this identifier is the hash
of a nonce and the contract terms that merchant and customer agreed upon.

Our model tracks the following data for users:
\begin{itemize}
\item $\V{valueWithdrawn}[\V{pkUser}]$ contains of the values
 withdrawn by each user $\V{pkUser}$,
\item $\V{wallet}[\V{pkUser}]$ contains sets of the users coins records,
 which individually consist of the coin private keys and denomination signatures.
\item $\V{acceptedContracts}[\V{pkUser}]$ contains the sets of contracts accepted by the user
  during spending operations, together with coins spent for it and their contribution.
\end{itemize}
The overspending database of the exchange is modeled by $\V{deposited}[\V{pkCoin}]$ and
$\V{refreshed}[\V{pkCoin}]$, which records the protocol transcript of deposit and refresh
operations respectively.

We say that a coin is \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 adding a transcript to $\V{deposited}$ or
$\V{refreshed}$ would cause the total value of transcripts in both lists to
exceed the value of the denomination.


\subsection{Algorithms}

The Taler e-cash scheme is modely by the following probabilistic\footnote{Our
Taler instantiations are not necessarily probabilistic, but we do not want to
prohibit this for other instatiations} polynomial-time algorithms and
protocols.  The notation $\prt{E}(X_1,\dots,X_n)$ / $\prt{U}(X_1,\dots,X_n)$
stands for a party (Exchange or User) in an interactive protocol, with
$X_1,\dots,X_n$ being the private inputs contributed by the party to the
protocol.

\begin{itemize}
  \item $\algo{ExchangeKeygen}(1^{\lambda}, 1^{\kappa}, \V{M})$:  Algorithm executed by the exchange
    that outputs a key pair $(\V{skE}, \V{pkE})$, which contain both the
    signing key and the denomination keys for the exchange.  The financial
    value assigned to a denomination public key $d$ is determined by
    $\V{M}(d)$.  Both $\lambda$ and $\kappa$ are security parameters.

  \item $\algo{UserKeygen}(1^\lambda{})$:  Algorithm executed by merchants and customers
    that outputs a key pair $(\V{skU}, \V{pkU})$.  We refer to this key pair by $(\V{skM}, \V{skM})$ when
    the user acts as a merchant.
    \comment{pkDenom needs to appear here}

  \item \algo{Withdraw}(\prt{E}(\V{skE}, \V{pkU}), \prt{U}(\V{skU}, \V{pkE}, \V{pkDenom})):
    Interactive protocol between exchange and user to withdraw a single coin of
    a particular denomination.
    \comment{A planchet like pkCoin needs to be an argument here, no?  How do we handle the signature though?  Also skDenom.  }

    % pkDenom needs to appear in ExchangeKeygen

  \item \algo{Spend}(contract, \V{f}, \V{pkUser}, \V{skCoin}, \V{pkReceiver}):
    Algorithm to produce and sign a deposit permission \V{depositPermission}
    for a particular contract.  The fraction $0 < \V{f} \le 1$ determines the
    fraction of the coin's value that will be spent.

  \item \algo{Deposit}(\prt{E}(\V{skE}, \V{pkE}), \prt{M}(\V{skU}, \V{depositPermission})):
    Interactive protocol between the exchange and a user, who acts as a merchant.

    In the deposit permission, there are coin public keys $\V{pkCoin}$
    corresponding to $\V{skCoin}$.
    If $\V{pkCoin}$ is being overspent, we return the protocol transcript
    of the previous deposits and refreshes.  

    On success, we mark $\V{pkCoin}$ spent in $\V{deposited}[\V{pkCoin}]$ and
    return the exchange's signature over the request.

  \item \algo{Refresh}(\prt{E}(\V{skE}, \V{pkU}), \prt{U}(\V{skU}, \V{pkE}, \V{skCoin}, \V{pkDenom})):
    Interactive protocol between exchange and user.

    If $\V{pkCoin}$ (derived from \V{skCoin}) is being overspent, then
    we return the protocol transcript of the previous deposits and refreshes.

    Assuming otherwise, we mark $\V{pkCoin}$ as refreshed in $\V{refreshed}[\V{pkCoin}]$.

    If the user \prt{U} plays honestly, the unlinkable 
    change they obtain will be stored in their wallet $wallet[\V{pkU}]$.
    If \prt{U} is caught playing dishonestly, the coin's refresh transcript
    will be marked as spent without anything in return.
    
    Note that some instantiation (e.g. those using zero knowledge proofs) might
    not leave \prt{U} the possibility to play dishonestly.

  \item \algo{Link}(\prt{E}(\V{skE}), \prt{U}(\V{skU}, \V{pkE}, \V{skCoin})):
    Interactive protocol between exchange and user.
    If \V{skCoin} is the secret key of a coin that was refreshed, then 
    we recompute the refreshed coin and add it to to the user's wallet $wallet[\V{pkU}]$.

\end{itemize}

\subsection{Oracles}

We define the following oracles:

\begin{itemize}
  \item $\ora{AddUser}()$:
    Creates a new user, sets $valueWithdrawn$ for the user to $0$, sets $wallet[pkUser] := \{\}$.
    Returns the public key of the user,

  \item $\ora{Withdraw}(pkUser, pkDenom)$:  Do a withdraw.
    Effectively the adversary is an active man-in-the middle between the user and the ``real'' exchange.

    The adversary obtains the protocol transcript, but does not gain access to the exchange's database directly.

    % FIXME: talk about share

  \item $\ora{Refresh}()$:  Do a withdraw.
    Effectively the adversary is an active man-in-the middle between the user and the ``real'' exchange.

    The adversary obtains the protocol transcript, but does not gain access to the exchange's database directly.

  \item $\ora{Link}(pkUser)$:  Force the execution ot the link protocol.  The adversary is an
    Effectively the adversary is an active man-in-the middle between the user and the ``real'' exchange.

  \item $\ora{Spend}(contractHash, pkSpender, \mathcal{T}^C, pkReceiver)$:
    Make a customer sign a deposit permission over a coin identified by
    transcript $\mathcal{T}_C$, which is either a withdraw transcript, link
    transcript or refresh transcript with coin index.  Returns the deposit
    permission on success, or $\bot$ if the $skSpender$ does not have enough
    coins.

    Adds $\V{contract}$ to $\V{acceptedContracts}[pkUser]$ and
    initializes $\V{spent}[\V{pkCoin}]$.

  \item $\ora{Share}(\mathcal{T}^C, pkReceiver)$:

    Shares a coin (identified by withdraw/refresh/link transcript $\mathcal{T}^C$ with the user identified
    by $pkReceiver$.  Used by the adversary in attempts to violate income transparency.

    Note that this trivially violates anonymity (by sharing with corrupted user), thus the usage must
    be restricted most other games.
    \comment{ENGLISH to / from ?}

    % the share oracle is the reason why we don't need a second withdraw oracle

  \item $\ora{AddCorruptUser}(pkUser)$:
    Used by the adversary to add a corrupted user, giving
    it permanent access to the user's private key, wallet and accepted contracts.

  \item $\ora{Deposit}(depositPermission)$:
    Give a deposit permission to the exchange.  If the deposit permission is valid and the coin is not overspent,
    the exchange adds it to $spent[pkU]$ for the user $U$ identified in the deposit permission.

    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 (even though \ora{Spend} tracks spending, coin sharing can otherwise cause overspending).
\end{itemize}

% addcorruptuser and adduser+corrupt is the same,
% since corrupt would give the adversary all previous protocol
% transcripts, and we don't have any notion of forward security


The exchange does not need to be corrupted with an oracle. A corrupted exchange
is modelled by giving the adversary the appropriate oracles and the exchange
private key from the exchange key generation.

If the adversary determines the exchange's private key during the setup,
invoking \ora{Withdraw}, \ora{Refresh} or \ora{Link} can be seen as the
adversary plaing the exchange.  Since the adversary is an active
man-in-the-middle in these oracles, they can drop messages to the simulated
exchange and make up their own response.  If the adversary calls these oracles
with a corrupted user, the adversary plays as the user.

\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}

\subsection{Remarks}
% I've moved these remarks here, since it does not make sense to talk about details
% without introducing the syntax of the model.

Anonymous e-cash schemes all require protections against network, etc. failures,
and hence require a refresh operations.  If this refresh operations also
provided partial spending, which seems logical, then refreshes can be run after
spends, which invalidates assumptions in anonymity games.

\section{Games}

We have two seperate security parameters in Taler
First, our primary security parameter $\lambda$ characterizes
the security of signatures and blind signatures.

% here we can't talk about the cut-and-choose parameter yet,
% we model taxable e-cash in general and don't want to refer
% to Taler-specific implementation details.

Our second security parameter $\kappa$ is used to characterize
the assurances of Income Transparency.

For some instantiations, e.g. ones based on zero knowledge proofs, $\kappa$
might be a security parameter in the traditional sense.  However to
be useful in practice, the adversary does not need to have negligible
success probability to win the Income Transparency game.  It suffices
that the financial losses of the adversary in the game are a deterrent, 
afterall the purpose of the game is to characterize tax evasion.

Taler does not fulfill strong Income Transparency since for Taler $\kappa \ge 3$ is a small
cut-and-choose parameter.  Instead we show that Taler satisfies Weak Income Transparency,
which is a statement about the adversary's financial loss when winning the game instead
of the winning probability.

We still characterize Income Transparency as a game, since it might be useful
for other instantiations that provide more absolute guarantees.

\subsection{Anonymity}
Intuitively, an adversary $\prt{A}$ (controlling the exchange and merchants) wins the
anonymity game if they have a non-negligible advantage in correlating spending operations
with the withdrawal or refresh operations that created a coin used in the
spending operation.

Let \oraSet{Anon} stand for access to the oracles
 \ora{AddUser}, \ora{Withdraw}, \ora{Spend},
 \ora{RefreshAsExchange}, \ora{LinkAsExchange}, \ora{AddCorruptUser}, \ora{Deposit}.  Let $b$ be the bit that will
 determine the mapping between users and spend operation, which the adversary must guess.

\bigskip
\noindent $\mathit{Exp}_{\prt{A}}^{anon}(1^\lambda, \kappa, b)$:
\vspace{-0.5\topsep}
\begin{enumerate}
  \setlength\itemsep{0em}
  \item $(\V{skE}, \V{pkE}, \V{skM}, \V{pkM}) \leftarrow {\prt{A}}()$ \\
    The adversary controls the exchange and a merchant.
    \footnote{We emphasize that our oracles give the adversary all data a real
    exchange learns (from the protocol transcripts returned by oracles), but we
    do not give our adversary access to our simulation's data structures
    because they include data only
    known by the customers.}
  \item $(\V{pkU}_0, \V{pkU}_1, \V{contract}_0, \V{contract}_1) \leftarrow {\prt{A}}^{\oraSet{Anon}}()$ \\
    The adversary creates two users and selects two contract identifiers.
  \item Return 0 if $\V{pkU}_0$ or $\V{pkU}_1$ are not uncorrupted registered users.
  \item Select distinct fresh coins $\V{pkCoin}_0$ and $\V{pkCoin}_1$
    from the wallets of $\V{pkU}_0$ and $\V{pkU}_1$ respectively.%
    \footnote{In principle, we might anonymously refresh coins before
    or concurrently with spending them, but if our adversary directs a
    non-anonymous refresh then they can mark coins with it}
    Return 0 if either $\V{pkU}_0$ or $\V{pkU}_1$ has insufficient unspent unrefreshed coins.
  \item $\V{dp_0} \leftarrow \algo{Spend}(\V{contract}_0, \V{pkU}_b, \V{pkCoin}_b, \V{pkM})$, \\
      $\V{dp_1} \leftarrow \algo{Spend}(\V{contract}_1, \V{pkU}_{1-b}, \V{pkCoin}_{1-b}, \V{pkM})$ \\
      Spend these two coins without revealing the mapping between users and coins.
  \item $r_0 \leftarrow \algo{Deposit}(\prt{E}(\V{skE}, \V{pkE}), {\prt{A}}(dp_0))$, \\
    $r_1 \leftarrow \algo{Deposit}(\prt{E}(\V{skE}, \V{pkE}), {\prt{A}}(dp_1))$ \\
    Deposit these two coins with the adversary controlled exchange.  Return 0 if $r_0$ or $r_1$ indicate a failure.
  \item $b' \leftarrow {\cal A}^{\oraSet{Anon}}()$ \\
    The adversary makes one guess $b' \in \{0,1\}$ for $b$, which determines the mapping between users and contracts.
  \item if $b = b'$ return 1, otherwise return 0
\end{enumerate}

We do not assume distinct users because ... FIXME

\begin{mdframed}
There are two kinds of games found for anonymity in the
literature, one is based in indistinguishability (between two users or coins) and
the other one on simulation.  The latter is claimed to be more powerful in \cite{izabachene2013divisible}.

Note that our game lets both users spend, which means we don't need to ``magically'' come up for
a fresh coin for the only user who just spent one.  If only one coin is spent and we don't replace it,
the adversary can exhaust wallets to see who spent.  We can avoid this, since we have contract identifiers
and can rely on those.

The ``\dots AsUser'' oracles are not given to the adversary, since they play as the exchange and thus
allowing them to talk to themselves does not make sense / does not give them more power.
\end{mdframed}

\subsection{Fairness} % Fair contract signing
\begin{mdframed}
  Fairness is a very overloaded term in crypto, can we come up with something better?
  It's already used for (a) protocols where either none or all parties obtain a result and
  (b) as fair e-cash, which is e-cash with selective tracability/deanonymization for e.g. law enforcement.

  Christian prefers Exculpability and both of us like Fair Exchange.  Exchange fairness has issues.
\end{mdframed}

Intuitively, the adversary wins if a non-corrupted user is unable to obtain a
proof-of-spending or unlinkable change for a coin.  This can happen, for
example, when the merchant is able to spend a coin in a way not anticipated by
the customer, keep the coin in a state that neither gives the customer a
receipt nor allows the customer to refresh it.

In practice, this property is necessary to guarantee that aborted or partially completed
payments do not result in the customer losing money or their anonymity.

The game also covers the case where a malicious exchange pretends the customer
did a dishonest refresh (in instantiations that allow dishonest refreshes).

Let \oraSet{Fair} stand for access to the oracles
 \ora{AddUser}, \ora{Withdraw}, \ora{Spend},
 \ora{RefreshAsExchange}, \ora{Share}, \ora{AddCorruptUser}, \ora{Deposit}.

\bigskip
\noindent $\mathit{Exp}_{\cal A}^{fair}(1^\lambda, 1^\kappa)$:
\vspace{-0.5\topsep}
\begin{enumerate}
  \setlength\itemsep{0em}
  \item $(skE, pkE) \leftarrow \mathrm{ExchangeKeygen}(1^\lambda, 1^\kappa, M)$ 
  \item $C_0 \leftarrow {\cal A}^{\oraSet{Fair}}(pkExchange)$
  \item The simulator runs all refresh operations to conclusion by looking for
    partial refresh transcripts.  We assume additional state in the wallet of
    each user to finish refresh operations.
  \item If $C_0$ is not a coin public key, return 0.
        Also let $U$ be the user that has $C_0$ in their wallet.  If no such $U$ exists, return 0.
  \item Let $C_0, \dots, C_n$ be the coins reachable via \algo{Link} from $C_0$.  
        We note the user obtains unlinkable change through refreshes, which merely extend this list.
  \item Return 0 if either $U$ was corrupted or \ora{Share} was called with any of $C_0, \dots, C_n$.
  \item For each $C \in \{C_0, \dots, C_n\}$, we check if the exchange's database records value transfers not present in the user's wallet's database:
    \begin{enumerate}[label*=\arabic*.]
      \item Return 1 if $\V{deposited}[C]$ contains a contract not appearing in the wallet's database $\V{acceptedContracts}[U]$.
      \item Return 1 if the total value $r_E$ of attempted refreshes in $\V{refreshed}[C]$ exceeds the total value $r_U$ of coins in $C_0, \dots, C_n$ directly reachable in one link from $C$.  We note $r_E$ includes refreshes that failed due to dishonesty, but not refreshes that failed to authenticate as $C$.
     \end{enumerate}
  \item Return 0 if this step is reached without an earlier return.
\end{enumerate}

\begin{mdframed}
  The game is written in a way that does not refer to failed refreshes explicitly.
\end{mdframed}


\subsection{Unforgability} % Exculpability?

Intuitively, adversarial customers win if they can forge more valid coins than
they withdraw.

Let \oraSet{Forge} stand for access to the oracles
 \ora{AddUser}, \ora{Withdraw}, \ora{Spend},
 \ora{RefreshAsExchange}, \ora{Share}, \ora{AddCorruptUser}.

\bigskip
\noindent $\mathit{Exp}_{\cal A}^{forge}(1^\lambda, \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{Forge}}(pkExchange)$
  \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 peers.
  \comment{TODO: Should we define unspent value anywhere?}
\end{enumerate}


\subsection{Income Transparency}

Intuitively, the adversary wins if money is in exclusive control of corrupted
users, but the exchange has no record of withdrawal or spending for it.  This
of course presumes that the adversary cannot delete from non-corrupted
customer's wallets, even though they can use oracles to force protocol
interactions of non-corrupted customers.

For practical e-cash systems, Income Transparency disincentivizes the emergence
of ``black markets'' among mutually distrusting users, where currency
circulates without the transactions being visible.  The Link protocol
introduces the threat of losing exclusive control of coins (despite having the option to refresh them) that
were received without involvement of the exchange.

Let \oraSet{Income} stand for access to the oracles
 \ora{AddUser}, \ora{Withdraw}, \ora{Spend},
 \ora{RefreshAsExchange}, \ora{Share}, \ora{AddCorruptUser}.

\bigskip
\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 $(C_1, \dots, C_\ell) \leftarrow \mathcal{A}^{\oraSet{Income}}(pkExchange)$
  \item Augment the wallets of all non-corrupted users with their
    transitive closure using the \algo{Link} protocol.
    Spend all remaining value on coins in wallets of non-corrupted users
    with \algo{Deposit}.\footnote{If \algo{Deposit} can only be run once per coin, then run a similar algorithm that ignores this check.} 
  \item Let $L$ denote the sum of unspent value on valid coins in $C_1, \dots\, C_\ell$,
    after accounting for the previous spending step.
    Also let $w'$ be the sum of coins withdrawn by corrupted users.
    So $p := L - w'$ gives the adversary's winnings.
  \item Let $w$ be the sum of coins withdrawn by non-corrupted users, and
    $s$ be the value marked as spent by non-corrupted users, so that
    $b := w - s$ gives the coins lost during refresh.
  \item If defined, return $p \over b + p$.  
    Also, we note our adversary wins the strong income transparency game if $L - w' > 0$.
  \comment{$(L, w, w', s)$  Big stile break so split into two games.  Return ratio.  Two expectations is wrong. }
\end{enumerate}

The adversary is said to win the Income Transparency game if $L - w' > 0$.
Intuitively, the expenses for getting untaxed money are less or equal to the gained
untaxed money.

For Taler (which only safisfies Weak Income Transparency) our proofs would only bound
adversaries' probability of winning one Income Transparency game by $1/\kappa$.
Instead, we shall prove that attacks cannot be profitable for the adversary
in the sense that the expected loss $E[w-s]$ for obtaining
untaxed coins of value $L$ is bounded by $E[w - s] \ge \kappa \cdot E[L - w']$,
independent from whether the adversary wins the game or not.

% In the proof, we look at fixed values of L and w'.
% The value of L-w' prime can't come from withdraw directly,
% it can't come from forging coins (or we could win the unforgeability game)
% It can't come from linking
% If it is to come from refresh, either we must find a hash collision
% or guess 

\begin{mdframed}
  Older formulations were talking about ``value lost during refresh'', but this concept does
  not necessarily exist for other instantiations (and the game was more complicated with it).
\end{mdframed}

\subsection{Others}

\subsubsection{Exculpability}
Exculpability is not necessary, since coins are spent on-line with the exchange.
In practice, even offline e-cash systems that provide exculpability are often undesireable, 
since hardware failures can result in unintentional overspending.

\subsubsection{Fair Exchange and Endorsements}
Camenisch and others \cite{camenisch2007endorsed} describes a version of (offline) e-cash where it is possible to
generate lightweight endorsement for coins.  These endorsements are unlinkable from
each other and from the coin.  An endorsement allows the implementation of fair exchange
(where either both goods are exchanged and a payment is made or neither) without giving up
anonymity.

Taler supports a similar concept of endorsements via the coin public key, deposit permissions and the
refresh protocol.  The deposit permission (augmented with some additional data) can be viewed as an endorsement
that enables fair exchange.  Unlinkability is guaranteed by the Refresh protocol.


\section{Security Definitions}

\begin{definition}[Anonymity]
We say that an e-cash scheme satisfies \emph{Anonymity} if
the success probability $\Prb{b \randsel \{0,1\}: \mathit{Exp}_{\cal A}^{anon}(1^\lambda, 1^\kappa, b) = 1}$
of the anonymity game is negligible for any polynomial time adversary $\mathcal{A}$.
\end{definition}

\begin{definition}[Fairness]
We say that an e-cash scheme satisfies \emph{Fairness} if
the success probability $\Prb{\mathit{Exp}_{\cal A}^{fair}(1^\lambda, 1^\kappa) = 1}$
of the fairness game is negligible for any polynomial time adversary $\mathcal{A}$.
\end{definition}

\begin{definition}[Unforgeability]
We say that an e-cash scheme satisfies \emph{Unforgeability} if
the success probability $\Prb{\mathit{Exp}_{\cal A}^{forge}(1^\lambda, 1^\kappa) = 1}$
of the unforgeability game is negligible for any polynomial time adversary $\mathcal{A}$.
\end{definition}

\begin{definition}[Strong Income Transparency]
We say that an e-cash scheme satisfies \emph{Strong Income Transparency} if
the success probability $\Prb{(L, w, w', s) \leftarrow \mathit{Exp}_{\cal A}^{income}(1^\lambda, 1^\kappa); L - w' > 0}$
for the income transparency game is negligible for any polynomial time adversary $\mathcal{A}$.
\end{definition}

\begin{definition}[Weak Income Transparency]
We say that an e-cash scheme satisfies \emph{Weak Income Transparency}
if, for any polynomial time adversary $\mathcal{A}$, our random variable
  $$ {p \over p + b} \leftarrow \mathit{Exp}_{\cal A}^{income}(1^\lambda, 1^\kappa) $$
optionally returned by the income transparency game satisfies
  $$ E\ST[|]{p \over b + p}{\textrm{$p \neq 0$ or $b \neq 0$}} \le {1\over\kappa} \mathperiod \eqno{(\textrm{\dag})}  $$
In (\dag), the expectation runs over 
 any probability space used by the adversary,
 times the uniform distribution on exchange keys $\V{skE}$,
 times the space of $\gamma$ choices by the exchange,
i.e. the uniform distribution on $\kappa^X$,
but the condition restricts it to games in which $p \over b + p$ is defined.
\end{definition}


\section{Instantiation}
\begin{mdframed}
  This section is incomplete.  Questions:  How do we reconcile our security parameter $\lambda$
  with Ed25519?  Should we be independent of the curve, even in our more concrete instantiation?

  Protocol transcripts are a mess, currently mostly there to show which values the adversary sees,
  and to check that after our hops they are all independent uniform random.

  Christian agrees with Jeff on using an abstract key exchange.
\end{mdframed}

Let $G \in \mathbb{E}$ be the generator of an Edwards curve in which the DDH problem yields $\lambda$ bits of security, like Ed25519 if $\lambda = 128$.

\begin{itemize}
  \item \algo{ExchangeKeygen}():  Generate and return denomination RSA key pair of a length that yields $\lambda$ bits of security, as well as the exchange signing key.
  \item \algo{UserKeygen}():  Generate and return merchant EdDSA key pair, which doubles as a reserve key for our purposes.
  \item \algo{Withdraw}(\prt{E}(\V{skE}, \V{pkU}), \prt{U}(\V{skU}, \V{pkE}, \V{pkDenom})):
    \begin{enumerate}
      \item \prt{U} selects blinding factor $r \randsel \Z_N^*$, coin secret $\V{skCoin} \randsel \Z_{|\mathbb{E}|}$, computes
        $\V{pkCoin} = \V{skCoin} \cdot G$, $\overline{M} = r \cdot \textrm{FDH}_{\V{pkDenom}}(\V{pkCoin})$ and sends $\overline{M}$ to $\prt{E}$.
      \item \prt{E} receives $\overline{M}$ and sends back $\overline{M}^d \bmod N$ to \prt{U}.
    \end{enumerate}

    Thus the protocol transcript is $(\overline {M}, \overline{M}^d \bmod N)$.
  \item \algo{Spend}(contract, \V{f}, \V{pkUser}, \V{skCoin}, \V{pkReceiver}):
  
    The deposit permission is computed as $(\V{sig}, \V{pkCoin})$ where $\V{pkCoin} = \V{skCoin} \cdot G$ and
    \begin{equation*}
      \V{sig} = \algo{Sign}(skCoin, (contract, pkReceiver))
    \end{equation*}

  \item \algo{Deposit}(\prt{E}(\V{skE}, \V{pkE}), \prt{M}(\V{skU}, \V{depositPermission})):
   
    Exchange checks signatures, records contribution $f$ of each coin to database of spent coins.

  \item \algo{Refresh}(\prt{E}(\V{skE}, \V{pkU}), \prt{U}(\V{skU}, \V{pkE}, \V{skCoin}, \V{pkDenom})):

	First the user samples a verification nonce $\V{nonce} \randsel U$ and, for each $i<\kappa$, computes the $i$th commitment data:
    \begin{itemize}
	\item Transfer private key $t_i \randsel U$
	\item Transfer public key $T_i = t_i \cdot G$A
	\item $\V{linkSecret}_i = H(\V{nonce} \mathbin{\|} \V{skCoin} \mathbin{\|} i)$
	\item Transfer secret $s_i = ECDH(t_i, pkCoin) \mathbin{\|} \V{linkSecret}_i$
	\item Blinding factor $r_i = \textrm{FD-PRF}_{pkDenom}(s_i)$
	\item Coin private key $m_i = \textrm{PRF}_{\V{pkCoin}}(s_i)$
	\item Coin public key $M_i = m_i \cdot G$
	\item Planchet $\overline{M}_i = r_i^e \cdot \textrm{FDH}_{\V{pkDenom}}(M_i) \bmod \V{pkDenom}$
	\end{itemize}
	The user aggregates this commitment data
    \begin{itemize}
	\item $h_M = H(\overline{M}_1, \dots, \overline{M}_\kappa)$,
	\item $h_T = H(T_1, \dots, T_\kappa)$,
	\end{itemize}
	and send the commitment $(\pi_1, \V{sig})$ where $\pi_1 = (\V{pkCoin}, \V{nonce}, h_T, h_M)$ and $\V{sig} = Sign_{\V{skCoin}}(\pi_1)$.
	
	Second, the exchange chooses a $0 \le \gamma < \kappa$ and signs this choice along with ???

	Third, the user reveals $T_\gamma$ and $\overline{M}_\gamma$ along with 
	$$ t_1, \dots, t_{\gamma-1}, t_{\gamma+1}, \dots, t_\kappa \quad\textrm{and}\quad
	     \V{linkSecret}_1, \dots, \V{linkSecret}_{\gamma-1}, \V{linkSecret}_{\gamma+1}, \dots, \V{linkSecret}_i \mathcomma $$
	 again signing this message with $\V{skCoin}$.

    Finally the exchange returns the signed planchet $\overline{M}_\gamma^d \bmod \V{pkDenom}$, which the user unblinds and verifies.

  \item \algo{Link}(\prt{E}(\V{skE}), \prt{U}(\V{skU}, \V{pkE}, \V{skCoin})):
  
    For each completed refresh of $\V{skCoin}$:
    The user obtains the verification nonce $\V{nonce}$, the new denomination $\V{pkDenom}$, the transfer public key $T_\gamma$, and the signed planchet $\overline{M}_\gamma^d \bmod \V{pkDenom}$ from the protocol transcript for the Refresh with coin public key derived from \V{skCoin}.  The user computes the $\V{linkSecret}_\gamma$ using $\V{nonce}$, computes both the blinding factor $r_i$ and the coin private key $m_i$ using $T_\gamma$, unblinds the signed planchet and verifies the result is the RSA signature for the new coin.

\end{itemize}

\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}


\subsection{Anonymity}

\begin{theorem}
If Taler's refresh is instantiated with PRFs, a key exchange satisfying DDH,
  and a collision-resistant hash function,
then Taler 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), \mathbb{G}_3(b)$, where $\mathbb{G}_0(b)$ is the original
  anonymity game $\mathit{Exp}_{\cal A}^{anon}(1^\lambda, \kappa, b)$.  We show 
  the adversary can distinguish between subsequent games with only negligible probability.
  Let $\epsilon_{PRF}$ and $\epsilon_{DDH}$ be the advantage of an adversary
  for the PRF game and DDH game respectively.

  We define $\mathbb{G}_1$ by replacing the link oracle \ora{Link} with
  another oracle that behaves the same as \ora{Link} only if the adversary
  responds to the customer with link data that has been observed in a previous refresh.
  If the link data is not recognized by the simulator, the customer is instead given
  a uniform random value as link data.

  In order to distinguish $\mathbb{G}_0$ from $\mathbb{G}_1$, our adversary
  must fake a link secret that causes the oracle to return random data leading
  to incorrect behavior by the customer.  We recall however that link secrets
  were constructed as $(\V{nonce}, \V{linkSecret})$ where
    $\V{linkSecret} = H(\V{nonce} \mathbin{\|} \V{skOldCoin})$,
  with the customer rejecting link secrets that fail this test.
  So our adversary must either find a hash collision or find the coin's private key. 
  
  In $\mathbb{G}_2$, the refresh oracle is modified so that the user responds
  with value drawn from a uniform random distribution for the the $\gamma$-th
  commitment instead of using a Diffie-Hellman function.  We must handle the
  fact that $\gamma$ is chosen by the adversary after seeing the commitments,
  so the simulator 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 simulator rewinds \prt{A} to the point where the refresh oracle was called.  
  We see this succeeds with probability $1/\kappa + \epsilon_{DDH}$.
  Since $\kappa \ll \lambda$, the runtime complexity of the simulator still says
  polynomial in $\lambda$.
  Note that we only replace the one commitment that will not be opened to the adversary later. \comment{Tighness bound also missing}

  We now show that $\left| \Prb{\mathbb{G}_1 = 1} - \Prb{\mathbb{G}_2 = 1}
  \right| \le \epsilon_{DDH}$ by defining a distinguishing game $\mathbb{G}_{1
  \sim 2}$ for $DDH$ as follows:

  \bigskip
  \noindent $\mathbb{G}_{1 \sim 2}(b)$:
  \vspace{-0.5\topsep}
  \begin{enumerate}
    \setlength\itemsep{0em}
    \item $D = C_{ddh}(b)$
      \comment{The DDH challenger gives us a distribution that is either $(g^a, g^b, g^{ab})$ or $(g^a, g^b, g^c)$}
    \item return $\mathit{Exp'}_{\cal A}^{anon}(b, D)$
      \comment{Modified anonymity game where the $\gamma$-th commitment in the
      refresh oracle is drawn from distribution $D$ (using rewinding).  Technically we need to
      draw from $D$ on withdraw for the coin private key, write it to a table, look it up on refresh and 
      use the matching tuple.}
  \end{enumerate}
  
  We observe that depending on the coin flip $b$,
  we either simulate $\mathbb{G}_1$ or $\mathbb{G}_2$ perfectly for
  our adversary $\cal A$ against $\mathbb{G}_1$.  At the same time $b$
  determines whether \prt{A} receives $(g^a, g^b, g^{ab})$ or $(g^a, g^b, g^c)$.
  Thus $\left| \Prb{\mathbb{G}_1 = 1} - \Prb{\mathbb{G}_2 = 1} \right| = \epsilon_{DDH}$
  is exactly the DDH advantage of $\mathbb{G}_{1 \sim 2}$.  
  At this point, the planchets used in refresh and withdraw differ only
  in the source of their blinding factor.

  In the hop between $\mathbb{G}_2$ and $\mathbb{G}_3$
  we replace the FD-PRF that produces the blinding factor with
  a uniformly random function, also on the full domain of the RSA modulus.
  At this point, any advantage of our adversary amounts to an advantage in
  distinguishing a random blinding factor from a random blinding factor
  multiplied by $\textrm{FDH}_N(C_1) / \textrm{FDH}(C_2) \mod N$,
  which violates the randomness of the blinding factor.
  
  We conclude the success probability for $\mathbb{G}_3$ is $1/2$ and hence .
  the success probability for $\mathit{Exp}_{\cal A}^{anon}(1^\lambda, \kappa, b)$
    is at most $1/2 + \epsilon_{DDH} + \epsilon_{PRF}$, as desired.
  \comment{The DDH game we use here is non-standard (stream of values to decide on instead of one, so maybe we need to use the number of refresh oracle invocations
  as a factor in front of $\epsilon_{DDH}$?}
\end{proof}

We observe that if Taler were instantiated with blind BLS signatures,
 instead of blind RSA signatures, then
our adversary must violate the computational Diffie-Hellman assumption
as well as the PRF assumption to compromise $\mathbb{G}_2$. 


\begin{mdframed}
  Note that the order of the hops does matter, since it's important that we feed the PRF
  real randomness.
\end{mdframed}


\subsection{Fairness}

\begin{theorem}
Assuming unforgeability of signatures (EUF-CMA), Taler satisfies Fairness.
\end{theorem}

\begin{proof}

% FIXME: argue that reduction is tight when you have malleability

We construct an adversary against EUF-CMA from an adversary $\mathcal{A}$
against Fairness.

Let $q$ be a bound (perhaps polynomial in the security parameter) on the
number of coins created by the adversary (via \ora{Withdraw} or
\ora{Refresh}).

Our goal is to embed the EUF-CMA challenge into one of the coins obtained via
\ora{Withdraw} or \ora{Refresh} from uncorrupted users.  We adjust \ora{Withdraw} and \ora{Refresh}
so that the challenge is used as public key for the coin with probability
$1/q$, but only if the user is uncorrupted and until the challenge has been embedded once.

The oracles \ora{Spend} and \ora{Refresh} are adjusted so that the signing oracle \ora{Sign} of the EUF-CMA challenger
is used for the coin with the embedded challenge.

If the adversary wins in step 6.1, there must be a valid deposit permission over a contract not signed by the user,
and thus not send to \ora{Sign}.   If the adversary wins in step 6.2, there must be a refresh request not signed
by the user.  In either case, we can extract a forged signature and use \prt{A} to construct an adversary against EUF-CMA.
\end{proof}

\subsection{Unforgeability}

\begin{theorem}
In the random oracle model,
if the RSA known-target inversion problem (RSA-KTI) is hard, then
Taler satisfies {unforgeability}.
% by probabilistic polynomially time adversaries.
\end{theorem}

\begin{proof}
We consider a probabilistic polynomially time adversary $\cal A$ with
a non-negligible advantage for winning the unforgeability game
 $\mathit{Exp}_{\cal A}^{forge}(1^\lambda, \kappa)$ against Taler
 instantiated with $d$ denominations.
%
% We describe an RSA Chosen-Target Inversion Problem (RSA-CTI)
%  \cite[Definition 3]{RSA-FDH-KTIvCTI} % or \cite[Definition 6.1]{OneMoreInversion}.
% won by $\cal A$. 

In other words, $\cal A$ made at most $l$ withdrawal and refresh oracle
queries to obtain the $l+1$ coins $C_1, \ldots, C_\ell$ in the game.
Also let $C_{\ell+1}, \ldots, C_m$ denote all the spent coins arising
from the operation of $\cal A$. % Also let $C_{m+1}, ..., C_n$ denote
% the unsigned planchets used by refresh oracle call. 
% Now set $Y_i = FDA_N(C_i)$ for $0 \le i \le n$. 
% DISCUSS: We could exploit some of the power of RSA-CTI to dispose
% of these planchets.  I think this seems unnecessary, but maybe it
% might refines our usage of ROM or something.
We now know $\cal A$ made at most $m$ withdrawal and refresh oracle
queries to obtain the $m+1$ RSA signatures %, aka inversions,
 on the $Y_i := \textrm{FDH}_{\V{pkDenom}_i}(C_i)$ with $0 \le i \le m$,
 where $\V{pkDenom}_i$ is the denomination key of $C_i$. 

It follows that $\cal A$ has produced one-more forgery in the sense
 of \cite[Definition 11]{RSA-FDH-KTIvCTI},
 also \cite[Definition 4 \& 5, pp. 369]{Pointcheval_n_Stern},
 for at least one $\V{pkDenom} \in \V{pkE}$.

We now create an adversary $\cal A^{\textrm{rsa-omf}}$ for the
 blind FDH-RSA signature one-more forgery game \cite[Definition 11]{RSA-FDH-KTIvCTI}
by assigning this challenger's target RSA key randomly to one of our $d$ denominations,
and inventing random new RSA keys for the remaining $d-1$ denominations.
As this assignment is random, $\cal A^{\textrm{rsa-omf}}$ wins the one-more forgery
game with $1/d$th the rate $\cal A$ wins the Taler unforgeability game.

We therefore conclude that RSA-KTI cannot be hard itself
 by \cite[Theorem 12]{RSA-FDH-KTIvCTI},
 and our random oracle assumption.
%
% So $\cal A$ wins this RSA-CTI game with its random sampling to produce
% $Y_i$ replaced by our PRF $FDA_N$, which requires nothing since we're
% already working in the stronger random oracle model anyways.
% We finally exploit the full random oracle model to apply 
% \cite[Theorem 6]{RSA-FDH-KTIvCTI} to produce an adversary who breaks
% RSA-KTI.
% DISCUSS CONTINUED: This argument directly from Theorem 6 seems wrong
% because the ROM in \cite[Lemma 13]{RSA-FDH-KTIvCTI} does not appear.
% We should figure out what's really going on.
\end{proof}


\subsection{Income Transparency}

Abstractly, a {\em key exchange} between parties Alice and Bob 
consists of two algorithms
 $(\V{sk}_i,\V{pk}_i) \leftarrow \V{gen}_i$ and $\V{kex}_i(\V{sk}_i,V{pk}_j)$
for each party, so $\{i,j\} = \{ \textrm{Alice}, \textrm{Bob} \}$, 
that, if run honestly, satisfies
$$ \V{kex}_\textrm{Alice}(\V{sk}_\textrm{Alice},V{pk}_\textrm{Bob})
  = \V{kex}_\textrm{Bob}(\V{sk}_\textrm{Bob},V{pk}_\textrm{Alice}) \mathperiod $$
In a normal key exchange, one considers when an adversary Eve can deduce
this shared secret, after having first played role $i$ multiple times while
$V{pk}_j$ remains fixed.  We took this view in the anonymity proof.

We invert this relationship in Taler's refresh, now viewing Alice and Bob
as an adversarial team who might deceive an observer Oscar about whether
they ran the key exchange honestly.

\begin{definition}
We say a key exchange is {\em secure against dishonest key generation by Alice}
if there is no probabilistic polynomial time adversary with non-negligible
advantage to provide Oscar a convincing transcript without actually running
$(\V{sk}_i,\V{pk}_i) \leftarrow \V{gen}_i$ honestly.
\end{definition}

In Taler's refresh, we prove honest key generation of the old coin $C$
by requiring a signature by $C$ on the initial commitment, which
 proves that either Alice or Bob knows $c$ where $C = c G$.
We emphasize that naively adding another non-signing key to $C$
 breaks honest key generation though.

In fact, we cannot know if the user produced $C$ themselves, and thus
knows the corresponding private key, or if merchant provided $C$
without telling the users the private key, the so called withdrawal loophole. 
In practice, our signature on $C$ with the exchange's denomination key
acts as a proxy for this.%
\footnote{A customer might still aid a merchant in tax evasion by making a
withdrawal with $C$ created by the merchant, but wait until actually making
a purchase to reveal the signature by the denomination key.
We could tighten this "future purchase" withdrawal loophole by using a
variant of the refresh during withdrawal, but we feel the user's commitment
to buy from a particular merchant would prove constraining enough to
limit applicability.}

Also, Ed25519 verification necessarily already checks that $C$ lies on
the Ed25519 curve, not some quadratic twist.  
% https://en.wikipedia.org/wiki/EdDSA
% https://safecurves.cr.yp.to/twist.html
If signature verification permitted using points on the twist, like
key exchanges frequently do, ala X25519, then the exchange might
compute a point on the twist while the customer would compute
a point on the original curve.

\begin{definition}
A {\em key exchange failure} consists of two honest key pairs
$(\V{sk}_i,V{pk}_i)$ with $i \in \{ \textrm{Alice}, \textrm{Bob} \}$
such that
$$ \V{kex}_\textrm{Alice}(\V{sk}_\textrm{Alice},V{pk}_\textrm{Bob})
\neq \V{kex}_\textrm{Bob}(\V{sk}_\textrm{Bob},V{pk}_\textrm{Alice}) \mathperiod $$
We say a key exchange is {\em secure against failures} if
there is no probabilistic polynomial time algorithm with non-negligible
advantage for producing a failure.
\end{definition}

In Taler's refresh, we avoid key exchange failures entirely because the
Edwards addition law is complete abelian group operation on the curve,
and the signature scheme verifies that the point lies on the curve.
% https://safecurves.cr.yp.to/refs.html#2007/bernstein-newelliptic
% https://safecurves.cr.yp.to/complete.html
We warn however that Weierstrass curves have incomplete addition formulas
that permit an adversarial merchant to pick transfer keys that yields failures.
There are further implementation mistakes that might enable collaborative
key exchange failures, like if the exchange does not enforce the transfer
private key being a multiple of the cofactor.

In this vein, almost all post-quantum key exchanges suffer from key exchange
failures that permit invalid key attacks against non-ephemeral keys.  
All these schemes support only one ephemeral party by revealing the
ephemeral party's private key to the non-ephemeral party,
 ala the Fujisaki-Okamoto transform~\cite{fujisaki-okamoto} or similar.
We cannot reveal the old coin's private key to the exchange when
verifying the transfer private keys though, which
 complicates verifying honest key generation of the old coin's key.

\begin{theorem}
Assume Taler both satisfies unforgeability and the refresh is instantiated with
\begin{enumerate}
\item a collision-resistant hash functions for planchet commitments, and
\item a key exchange secure against both
 dishonest generation of the old coin's public key, and key exchange failures.
\end{enumerate}
Then Taler satisfies {weak income transparency}.
\end{theorem}

\begin{proof}
In our actual refresh operation, our commitment phase sends only the
hash of the planchets to reduce bandwidth.  We therefore first convert
our adversary $\cal A$ into an adversary for a variant protocol in which
these commitments contain the full planchets:  We rewind $\cal A$ to
try two distinct $\gamma \in 1,\ldots,\kappa$ during each refresh operation,
so that we obtain all planchets.  We need only try two choices because
the adversary reveals all but one planchet in each run.  
We now witness a hash collision if transfer secrete the adversary reveals
does not yield the correct coins. 

If Taler satisfies unforgeability then this variant protocol does so too
because an adversary who reveals full planchets can trivially be replaced
 by an adversary who do hash commitments.

We next consider the directed forest on coins induced by the refresh protocol.
It follows from unforgeability that any coin must originate from
some user's withdraw in this graph.  
Let $X$ denote the coins from $\{C_1,\ldots,C_\ell\}$ that originate
from a non-corrupted user.  So $\ell \leq w + |X|$. 

For any $C \in X$, there is a final refresh operation $R_C$ in which
a non-corrupted user could obtain the coin $C'$ consumed in the refresh
via the linking protocol, but no non-corrupted user could obtain the
coin provided by the refresh, as otherwise $C$ gets marked as spend. 

In each $R_C$, we know $\cal A$ must submit a planchet for which the
linking protocol fails to produce $C$ correctly.  In this case, either
\begin{enumerate}
\item the planchet must be false outright, meaning either $C$ itself
      or the blinding factor does not arise form $t C'$, or else
\item the exchange would compute the planchet correctly, but not
      users employing the linking protocol, meaning
      $t C' \neq c' T$ where $T = t G$ is the transfer key.
\end{enumerate}

We may assume $C$ was generated honestly by our key exchange assumption. 
We may assume the first case that $\cal A$ provides a false planchet 
outright because we produce a key exchange failure in the second case,
 violating our key exchange assumptions.

We shall prove $E({p \over b + p} | X \neq \emptyset) \le {1\over\kappa}$ (\dag)
where the expectation runs over
 any probability space used by the adversary,
 times the uniform distribution on exchange keys $\V{skE}$,
 times the space of $\gamma$ choices by the exchange,
 i.e. the uniform distribution on $\kappa^X$,
but conditioned on games with false planchets.

We shall optimizes our adversary in ways that improve its $p \over b + p$.
We cannot actually produce this optimized adversary ourselves,
 but its existence suffices to prove the inequality (\dag).

As a reminder, 
if a refresh $R_C$ with $C\in X$ is observed using a false planchet,
then the coin $C$ becomes unspendable, and contributes to
the lost coins $b := w - s$ instead of the winnings $p := L - w'$ aka $|X|$.
We also note $b + p$ gives the value of refreshes attempted with
false planchets.  As these are positive,  $p \over b + p$ undefined 
if and only if $p = 0$ and $b = 0$, which happens if and only if
the adversary does not use false planchets, i.e. $X = \emptyset$.

We may now assume for optimality that $\cal A$ submits a false planchet
for at most one choice of $\gamma$ in $R_C$,
 as otherwise the refresh always fails.

% As our $\gamma$ are chosen randomly, any given refresh with one
% false planchet has only a $1\over\kappa$ chance of succeeding.
% % We recall ...  MAYBE COPY FROM REMOVED TEXT IN cf4086163362d68011d093bc683732bacac5aba1

We defined $R_C$ to be an anti-chain in the refresh forest, but
emphasize that an adversary who looses an $R_C$ looses $C$ completely,
while an optimal adversary who wins an $R_C$ should not gamble again. 
Indeed, an adversary has no reason to touch its winnings from an $R_C$.

% There is no way to influence $p$ or $b$ through withdrawals or spends
% by corrupted users of course.  In principle, one could decrease $b$ by
%  sharing from a corrupted user to a non-corrupted users,
% but we may assume this does not occur either, again by optimality.

An adversary may respond adaptively to $\gamma$ of course, but,
for any $R_C$, 
there are $\kappa$ game runs identical up through the commitment phase
of $R_C$ that diverge in simulator's random choice of $\gamma$.
% and suppress $C$'s decendents by optimality. 
If $v$ is the value of $R_C$ then one run adds $v$ to $p$, while
 the remaining $\kappa-1$ runs add $v$ to $b$. 

We define $p_C$ and $b_C$ to be these contributions summed
 over the $\kappa$ runs, so $\kappa p_C = b_C + p_C$. 
Now $p = {1\over\kappa |X|} \sum_{C \in X} p_C$
 and $b = {1\over\kappa |X|} \sum_{C \in X} b_C$
so $E({p \over b + p} | X \neq \emptyset) = {1\over\kappa}$,
 which yields the inequality (\dag).
\end{proof}
% https://math.stackexchange.com/questions/852890/expectation-of-random-variables-ratio
%%% $L - w' \over (L - w') + (w - s)$
% $E(b/p) + 1 = E(b/p + p/p) = E((b + p)/p) = \kappa$
% $E(b/p) = \kappa-1$
% $E(p/b) = {1 \over \kappa-1}$

\begin{corollary}
In the random oracle model,
if the RSA known-target inversion problem (RSA-KTI) is hard,
and refresh is instantiated with a key exchange secure against both failures
 and dishonest generation of the old coin's public key,
then Taler satisfies {weak income transparency}.
\end{corollary}

We could weaken our assumption that the adversary cannot find
any key exchange failures, primarily by requiring the customer
cannot produce the same failure with another algorithm.  
There is no immediate advantage to this extra generality because
integrating with post-quantum key exchange requires solving those
schemes key validation problems.

As it turns out, there is a simple hash-based solutions that provides
post-quantum anonymity without additional assumptions though: 
% because the coin holder is encrypting to themselves:  
We extend the coin private key $c$ by a secret $m$ and extend the
coin signing key $C$ to be a pair $(C,R)$ in which $R$ is the root
of a Merkle tree whose $i$th leave is $H(m,i)$.
In a refresh, the wallet first constructs the planchets from 
$H(t C', H(m,i))$ and commits to the index $i$ along with with each
transfer public key $T$, and later when revealing $t$ also reveals 
$H(m,i)$ and the proof that it lives in the Merkle tree.  
In this scheme, our Merkle tree should be large enough to accommodate
some fixed number of refreshes per coin, possibly just one, while
our wallet must avoid any fragility in committing its $i$ choices to disk. 


\section{Standard Definitions}
\begin{definition}[One-more forgery]
For any integer $\ell$, an $(\ell, \ell + 1)$-forgery comes from
a probabilistic polynomial time Turing machine $\mathcal{A}$ that can
compute, after $\ell$ interactions with the signer $\Sigma$, $\ell + 1$ signatures with nonnegligible
  probability. The ``one-more forgery'' is an $(\ell, \ell + 1)$-forgery for some
integer $\ell$. 
\comment{TODO: Turing machine?!?}
\end{definition}

Taken from \cite{pointcheval1996provably}.  This definition applies to blind signature schemes in general.
Intuition:  EUF-CMA is not strong enough for blind signatures,
since attacker can choose the message (without going through a hash function before signing).

\begin{definition}[RSA-KTI]
  Game (security parameter $k$, $m : \mathbb{N} \rightarrow \mathbb{N}$, $\mathcal{A}$ adversary with access to RSA inversion oracle \ora{Inv}):
  \begin{enumerate}
    \item $(N, e, d) \leftarrow \mathsf{KeyGen}(k)$
    \item $y_i \leftarrow_R \mathbb{Z}_N^*$ for $i \in 1, \dots, m(k) + 1$
    \item $(x_1, \dots, x_{m(k) + 1}) \leftarrow \mathcal{A}^{\ora{Inv}}(N, e, k, y_1, \dots, y_{m(k) + 1})$
    \item $\mathcal{A}$ wins if it made at most $m(k)$ oracle queries and $x_i^e \equiv y_i \pmod N$
  \end{enumerate}
\end{definition}

From \cite{bellare2003onemore}.  Assumption to prove security of RSA blind signatures.  Equivalent to RSA-CTI.

\bibliography{lit}
\bibliographystyle{alpha}

\end{document}