-
Notifications
You must be signed in to change notification settings - Fork 2
Expand file tree
/
Copy pathCounterPRG_PRGSecurity.proof
More file actions
128 lines (108 loc) · 4.18 KB
/
CounterPRG_PRGSecurity.proof
File metadata and controls
128 lines (108 loc) · 4.18 KB
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
// Proof that the length-doubling Counter PRG G(s) = F(s, 0) || F(s, 1)
// is a secure PRG, assuming F is a secure PRF.
//
// High-level idea: hybrid argument over the q queries the adversary makes
// to the PRG oracle. Hybrid_i has the first i queries returning random
// strings and the remaining (q - i) queries returning real PRG outputs.
// Hybrid_0 is PRG.Real, Hybrid_q is PRG.Random.
//
// Within each hop Hybrid_{i-1} -> Hybrid_i we replace the i-th query's
// PRG output (a fresh-key F evaluation at inputs 0 and 1) with a single
// PRF challenger query at inputs 0 and 1, then invoke PRF security to
// turn those two F evaluations into two independent random strings, then
// fold the random pair back into a single fresh sample of length 2*lambda.
import '../../Primitives/PRF.primitive';
import '../../Schemes/PRG/CounterPRG.scheme';
import '../../Games/PRG/PRGSecurity.game';
import '../../Games/PRF/PRFSecurity.game';
// SecurityIntermediate2 = Hybrid_{i-1}: first (i-1) queries random,
// rest are CounterPRG real evaluations.
Game SecurityIntermediate2(PRF F, CounterPRG G, Int hybridNum) {
Int count;
Void Initialize() {
count = 0;
}
BitString<G.lambda + G.stretch> Query() {
count = count + 1;
if (count < hybridNum) {
BitString<G.lambda + G.stretch> r <- BitString<G.lambda + G.stretch>;
return r;
} else {
BitString<F.lambda> s <- BitString<F.lambda>;
BitString<G.lambda> x = F.evaluate(s, 0^1);
BitString<G.lambda> y = F.evaluate(s, 1^1);
return x || y;
}
}
}
// Reduction R1: routes the i-th query to the PRF challenger and runs the
// real PRG on the others.
Reduction R1(PRF F, CounterPRG G, Int hybridNum) compose PRFSecurity(F) against PRGSecurity(G).Adversary {
Int count;
Void Initialize() {
count = 0;
}
BitString<G.lambda + G.stretch> Query() {
count = count + 1;
if (count < hybridNum) {
BitString<G.lambda + G.stretch> r <- BitString<G.lambda + G.stretch>;
return r;
} else if (count == hybridNum) {
BitString<G.lambda> x = challenger.Lookup(0^1);
BitString<G.lambda> y = challenger.Lookup(1^1);
return x || y;
} else {
BitString<F.lambda> s <- BitString<F.lambda>;
BitString<G.lambda> x = F.evaluate(s, 0^1);
BitString<G.lambda> y = F.evaluate(s, 1^1);
return x || y;
}
}
}
// SecurityIntermediate5 = Hybrid_i: first i queries random, rest are real.
// After replacing F.evaluate with a random function (via PRF security),
// the engine's DistinctConstRFToUniform transform collapses RF(0^1)||RF(1^1)
// into a single fresh BitString<2*lambda> sample, which matches the count<=i
// random branch of this game.
Game SecurityIntermediate5(PRF F, CounterPRG G, Int hybridNum) {
Int count;
Void Initialize() {
count = 0;
}
BitString<G.lambda + G.stretch> Query() {
count = count + 1;
if (count <= hybridNum) {
BitString<G.lambda + G.stretch> r <- BitString<G.lambda + G.stretch>;
return r;
} else {
BitString<F.lambda> s <- BitString<F.lambda>;
BitString<G.lambda> x = F.evaluate(s, 0^1);
BitString<G.lambda> y = F.evaluate(s, 1^1);
return x || y;
}
}
}
proof:
let:
Int lambda;
Int q;
PRF F = PRF(lambda, 1, lambda);
CounterPRG G = CounterPRG(F);
assume:
PRFSecurity(F);
calls <= q;
theorem:
PRGSecurity(G);
games:
PRGSecurity(G).Real against PRGSecurity(G).Adversary;
assume SecurityIntermediate2(F, G, 1).count >= 1;
assume R1(F, G, 1).count >= 1;
induction(i from 1 to q) {
SecurityIntermediate2(F, G, i) against PRGSecurity(G).Adversary;
PRFSecurity(F).Real compose R1(F, G, i) against PRGSecurity(G).Adversary;
PRFSecurity(F).Random compose R1(F, G, i) against PRGSecurity(G).Adversary;
SecurityIntermediate5(F, G, i) against PRGSecurity(G).Adversary;
}
assume R1(F, G, q).count < q + 1;
assume SecurityIntermediate5(F, G, q).count < q + 1;
PRGSecurity(G).Random against PRGSecurity(G).Adversary;