-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathlib.gdh.ocvl
152 lines (128 loc) · 7.04 KB
/
lib.gdh.ocvl
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
(* Analysing the HPKE Standard - Supplementary Material
Joël Alwen; Bruno Blanchet; Eduard Hauck; Eike Kiltz; Benjamin Lipp;
Doreen Riepel
This is supplementary material accompanying the paper:
Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp,
and Doreen Riepel. Analysing the HPKE Standard. In Anne Canteaut and
Francois-Xavier Standaert, editors, Eurocrypt 2021, Lecture Notes in
Computer Science, pages 87-116, Zagreb, Croatia, October 2021. Springer.
Long version: https://eprint.iacr.org/2020/1499 *)
(* DH_proba_collision_minimal says that
the probability that exp(g, x) = Y for random x and Y independent of x
is at most PCollKey *)
def DH_proba_collision_minimal(G, Z, g, exp, mult, PCollKey) {
expand DH_basic(G, Z, g, exp, exp', mult).
(* In some game transformations, exp is rewritten into exp'
to avoid loops. We do not do that here, so exp' is not used. *)
collision x <-R Z; forall Y: G;
return(exp(g, x) = Y) <=(PCollKey)=> return(false) if Y independent-of x.
}
def GDH_RSR_minimal(G, Z, g, exp, mult, pGDH, pDistRerandom) {
(* the GDH assumption
This equivalence says that, when exp(g,a[i]) and exp(g,b[j]) are known to the
adversary, the adversary can compute exp(g, mult(a[i], b[j])) only with
negligible probability, even in the presence of a decision DH oracle
DH(A,B,C) tells whether A = g^a, C = B^a for some a. *)
param na, naeq, naDDH, naDDH1, naDDH2, naDDH3, naDDH4, naDDH5, naDDH6, naDDH7, naDDH8, naDH9,
nb, nbeq, nbDDH, nbDDH1, nbDDH2, nbDDH3, nbDDH4, nbDDH5, nbDDH6, nbDDH7, nbDDH8, nbDH9.
(* In the code below:
- oracles OA and OB give the public Diffie-Hellman keys to the adversary
- oracles ODHa9 and ODHb9 are particular cases of OA and OB, respectively:
exp(g, mult(a,x)) = exp(exp(g,a), x). They appear explicitly because
CryptoVerif would not detect that exp(g, mult(a,x)) can be computed
using exp(g,a), since exp(g,a) is not a subterm of exp(g, mult(a,x)).
- Oracles ODDHa1, ODDHa, ODDHa8, ODDHb1, ODDHb, ODDHb8 are instances
of the decision DH oracle.
ODDHa1[i](m,m') = DH_a(i, m', m)
ODDHa8[i](m,j) = DH_a(i, exp(g,a[j]), m)
ODDHb1[i](m,m') = DH_b(i, m', m)
ODDHb8[i](m,j) = DH_b(i, exp(g,b[j]), m)
where DH_a(i, m', m) = (m'^a[i] = m)
DH_b(i, m', m) = (m'^b[i] = m)
ODDHa[i](m,j) = DH_l(i, j, m)
and in this case we can apply the CDH assumption
and replace the result with "false" in the right-hand side
ODDHb[i](m,j) = DH_1(j, i, m)
and in this case we can apply the CDH assumption
and replace the result with "false" in the right-hand side
*)
equiv(gdh(exp))
foreach ia <= na do a <-R Z; (
OA() := return(exp(g,a)) |
foreach iaeq <= naeq do OAeq(m:G) := return(m = exp(g,a)) |
(* We put the oracle above before ODDHa1, so that ODDHa1 is not used when m' = g,
which would lead to additional calls to the DDH oracle when in fact
we can simply compare with the public key *)
foreach iaDDH1 <= naDDH1 do ODDHa1(m:G, m':G) := return(m = exp(m', a)) |
foreach iaDDH <= naDDH do ODDHa(m:G, j<=nb) [useful_change] := return(m = exp(g, mult(b[j], a))) |
foreach iaDDH8 <= naDDH8 do ODDHa8(m:G,j<=na) [3] := return(m = exp(g,mult(a[j], a))) |
foreach iaDH9 <= naDH9 do ODHa9(x:Z) [2] := return(exp(g, mult(a, x)))
) |
foreach ib <= nb do b <-R Z; (
OB() := return(exp(g,b)) |
foreach ibeq <= nbeq do OBeq(m:G) := return(m = exp(g,b)) |
foreach ibDDH1 <= nbDDH1 do ODDHb1(m:G, m':G) := return(m = exp(m', b)) |
foreach ibDDH <= nbDDH do ODDHb(m:G, j<=na) := return(m = exp(g, mult(a[j], b))) |
foreach ibDDH8 <= nbDDH8 do ODDHb8(m:G,j<=nb) [3] := return(m = exp(g,mult(b[j], b))) |
foreach ibDH9 <= nbDH9 do ODHb9(x:Z) [2] := return(exp(g, mult(b, x)))
)
<=(pGDH(time + (na + nb + 1 + #ODHa9 + #ODHb9) * time(exp),
#ODDHa + #ODDHa1 + #ODDHa8 +
#ODDHb + #ODDHb1 + #ODDHb8)
+ (na + nb) * pDistRerandom)=> [computational]
foreach ia <= na do a <-R Z [unchanged]; (
OA() := return(exp(g,a)) |
foreach iaeq <= naeq do OAeq(m:G) := return(m = exp(g,a)) |
foreach iaDDH1 <= naDDH1 do ODDHa1(m:G, m':G) := return(m = exp(m', a)) |
foreach iaDDH <= naDDH do ODDHa(m:G, j<=nb) := return(false) |
foreach iaDDH8 <= naDDH8 do ODDHa8(m:G,j<=na) [3] := return(m = exp(g,mult(a[j], a))) |
foreach iaDH9 <= naDH9 do ODHa9(x:Z) := return(exp(g, mult(a, x)))
) |
foreach ib <= nb do b <-R Z [unchanged]; (
OB() := return(exp(g,b)) |
foreach ibeq <= nbeq do OBeq(m:G) := return(m = exp(g,b)) |
foreach ibDDH1 <= nbDDH1 do ODDHb1(m:G, m':G) := return(m = exp(m', b)) |
foreach ibDDH <= nbDDH do ODDHb(m:G, j<=na) := return(false) |
foreach ibDDH8 <= nbDDH8 do ODDHb8(m:G,j<=nb) [3] := return(m = exp(g,mult(b[j], b))) |
foreach ibDH9 <= nbDH9 do ODHb9(x:Z) := return(exp(g, mult(b, x)))
).
}
def square_GDH_RSR_minimal(G, Z, g, exp, mult, pSQGDH, pDistRerandom) {
(* the square GDH assumption
This equivalence says that, when exp(g,a[i]) are known to the
adversary, the adversary can compute exp(g, mult(a[i], a[j])) only with
negligible probability, even in the presence of a decision DH oracle
DH(A,B,C) tells whether A = g^a, C = B^a for some a. *)
param na, naeq, naDDH, naDDH1, naDDH2, naDDH3, naDDH4, naDDH5, naDH9.
(* In the code below:
- oracle OA gives the public Diffie-Hellman keys to the adversary
- oracle ODHa9 is a particular case of OA:
exp(g, mult(a,x)) = exp(exp(g,a), x). It appears explicitly because
CryptoVerif would not detect that exp(g, mult(a,x)) can be computed
using exp(g,a), since exp(g,a) is not a subterm of exp(g, mult(a,x)).
- Oracles ODDHa1 and ODDHa are instances of the decision DH oracle.
ODDHa1[i](m,m') = DH_0(exp(g,a[i]), m', m)
ODDHa[i](m,j) = DH_l(i, j, m)
and in this case we can apply the CDH assumption
and replace the result with "false" in the right-hand side
*)
equiv(gdh(exp))
foreach ia <= na do a <-R Z; (
OA() := return(exp(g,a)) |
foreach iaeq <= naeq do OAeq(m:G) := return(m = exp(g,a)) |
(* We put the oracle above before ODDHa1, so that ODDHa1 is not used when m' = g,
which would lead to additional calls to the DDH oracle when in fact
we can simply compare with the public key *)
foreach iaDDH1 <= naDDH1 do ODDHa1(m:G, m':G) := return(m = exp(m', a)) |
foreach iaDDH <= naDDH do ODDHa(m:G, j<=na) [useful_change] := return(m = exp(g, mult(a[j], a))) |
foreach iaDH9 <= naDH9 do ODHa9(x:Z) [2] := return(exp(g, mult(a, x)))
)
<=(pSQGDH(time + (na+1 + #ODHa9) * time(exp), #ODDHa + #ODDHa1) + na * pDistRerandom)=> [computational]
foreach ia <= na do a <-R Z [unchanged]; (
OA() := return(exp(g,a)) |
foreach iaeq <= naeq do OAeq(m:G) := return(m = exp(g,a)) |
foreach iaDDH1 <= naDDH1 do ODDHa1(m:G, m':G) := return(m = exp(m', a)) |
foreach iaDDH <= naDDH do ODDHa(m:G, j<=na) := return(false) |
foreach iaDH9 <= naDH9 do ODHa9(x:Z) := return(exp(g, mult(a, x)))
).
}