-
Notifications
You must be signed in to change notification settings - Fork 0
/
dhkem.auth.outsider-auth-lr.m4.ocv
214 lines (201 loc) · 7.35 KB
/
dhkem.auth.outsider-auth-lr.m4.ocv
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
(* 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 *)
proof {
allowed_collisions default^4/large;
(* We allow eliminating collisions with probability in power 4 of
N, Qeperuser, Qdperuser, Qcperuser times PCollKey, to allow q^2 * PCollKey,
where q = N * (Qeperuser + Qdperuser + Qcperuser) *)
(* start on the left side *)
out_game "l.out.cv";
(* Preliminary work on the right-hand side. *)
start_from_other_end;
out_game "r.out.cv";
simplify;
(* We move the deserialization of the ciphertext earlier, so that the
whole computation in OADecap deals with a deserialized ciphertext *)
insert after "OADecap" "let Serialize(pkE_10) = cd in";
all_simplify;
out_game "r1.out.cv";
(* Now we work on the left-hand side *)
start_from_other_end;
(* We introduce in OADecap the structure we have on the right-hand side. *)
insert after "let Serialize(pkE_3"
"find ie1_1 = ie1 <= Qeperuser, i1_3 = i1_2 <= N suchthat
defined(zz_2[ie1, i1_2], enc_1[ie1, i1_2], sk[i1_2], pk_R[ie1, i1_2])
&& (exp(g, sk) = pk_R[ie1, i1_2])
&& (exp(g, sk[i1_2]) = pk_S)
&& (enc_1[ie1, i1_2] = enc_2) then
orfind id1_1 = id1 <= Qdperuser suchthat
defined(random_br[id1], zz_3[id1], enc_2[id1], pk_S[id1])
&& (pk_S[id1] = pk_S)
&& (enc_2[id1] = enc_2) then
else
find i1_1 = i1 <= N suchthat
defined(sk[i1])
&& (pk_S = exp(g, sk[i1])) then
random_br <- true";
simplify;
out_game "l1occ.out.cv" occ;
(* Use correctness of the KEM: Replace the result of OADecap with a
cleartext generated in OAEncap, in the first branch of the first
find introduced above. *)
replace
at_nth 1 3 "return{[0-9]*}({[0-9]*}AuthDecap_Some({[0-9]*}zz_3))"
"zz_2[ie1_1, i1_4]";
remove_assign useless;
out_game "l2occ.out.cv" occ;
(* Replace the result of OADecap with the result of a previous call to
OADecap, in the second branch of the first find introduced above *)
replace
at_nth 1 3 "return{[0-9]*}({[0-9]*}AuthDecap_Some({[0-9]*}zz_3))"
"zz_3[id1_1]";
(* Use unique names for the assignments of the following variables
that are currently not unique *)
SArename zz_3;
SArename dh_3;
SArename kemContext_3;
SArename key_1;
SArename info_1;
remove_assign useless;
(* In OAEncap, distinguish whether pk_R is an honest key or not *)
insert after "OAEncap(pk_R"
"find i1 <= N suchthat
defined(sk[i1])
&& pk_R = exp(g, sk[i1]) then";
out_game "l3.out.cv";
(* Use unique names for the assignments of the following variables
that are currently not unique *)
SArename z;
SArename enc_1;
SArename dh_2;
SArename zz_2;
SArename kemContext_2;
SArename key;
SArename info;
SArename pkR_1;
(* In OH, distinguish whether the argument is of the form used in the rest of the protocol *)
insert after "OH(x1"
"let eae_input(
salt: extract_salt_t,
concatExtract(
protocol1: label_protocol_t,
suite1: suite_id_t,
label1: label_extract_t,
concatDH(dh1: G_t, dh2: G_t)),
concatExpand(
l: two_byte_t,
protocol2: label_protocol_t,
suite2: suite_id_t,
label2: label_expand_t,
concatContext(pkE': G_t, pkR': G_t, pkS': G_t))) = x1 in";
crypto rom(ExtractAndExpand_inner);
crypto gdh(exp) sk z_2 . (*If we want to be more precise: sk z_2 . *);
all_simplify;
out_game "l4.out.cv" occ;
start_from_other_end;
(* Now we work on the right-hand side *)
remove_assign binder E_5;
(* In OAEncap, distinguish whether pk_R is an honest key or not *)
insert after "OAEncap(pk_R_1"
"find i1 <= N suchthat
defined(sk_1[i1])
&& pk_R_1 = exp(g, sk_1[i1]) then";
out_game "r1.out.cv";
(* Use unique names for the assignments of the following variables
that are currently not unique *)
SArename z_1;
SArename dh_7;
SArename enc_6;
SArename kemContext_7;
SArename key_2;
SArename info_2;
SArename zz_7;
(* In OH, distinguish whether the argument is of the form used in the rest of the protocol *)
insert after "OH(x1"
"let eae_input(
salt: extract_salt_t,
concatExtract(
protocol1: label_protocol_t,
suite1: suite_id_t,
label1: label_extract_t,
concatDH(dh1: G_t, dh2: G_t)),
concatExpand(l: two_byte_t,
protocol2: label_protocol_t,
suite2: suite_id_t,
label2: label_expand_t,
concatContext(pkE'': G_t, pkR'': G_t, pkS'': G_t))) = x1_1 in";
crypto rom(ExtractAndExpand_inner);
crypto gdh(exp) (* If we want to be more precise: sk_1 z_4 . *);
out_game "r2.out.cv" occ;
success
}
define(`square')
include(`common.dhkem.ocvl')
event AuthEncap_does_not_fail.
param N, Qeperuser, Qdperuser.
table E(G_t, G_t, bitstring, eae_output_t).
equivalence
Ostart() :=
key_extr <-R hash_key_t;
return();
((
foreach i <= N do Osetup() := sk <-R Z_t; return(); (
foreach ie <= Qeperuser do (
OAEncap(pk_R: G_t) :=
return(AuthEncap(key_extr, pk_R, skgen(sk)))) |
foreach id <= Qdperuser do (
OADecap(pk_S: G_t, enc: bitstring) :=
return(AuthDecap(key_extr, enc, skgen(sk), pk_S))) |
(* The next oracle gives the public key to the adversary *)
Opk() := return(pkgen(sk))
)) |
(* The random oracle ExtractAndExpand_inner *)
run ExtractAndExpand_inner_orcl(key_extr)
)
Ostart() :=
key_extr <-R hash_key_t;
return();
((
foreach i <= N do Osetup() := sk <-R Z_t; return(); (
foreach ie <= Qeperuser do (
OAEncap(pk_R: G_t) :=
let AuthEncap_tuple(k: eae_output_t, ce: bitstring) = AuthEncap(key_extr, pk_R, skgen(sk)) in (
insert E(pkgen(sk), pk_R, ce, k);
return(AuthEncap_tuple(k, ce))
) else (
(* Never happens because AuthEncap always returns AuthEncap_tuple(...) *)
return(AuthEncap_None)
)) |
foreach id <= Qdperuser do (
OADecap(pk_S: G_t, cd: bitstring) :=
get E(=pk_S, =pkgen(sk), =cd, k'') in (
return(AuthDecap_Some(k''))
) else (
(* This "find" checks whether pk_S is among the honest public keys pk_i *)
find i1 <= N suchthat defined(sk[i1]) && pk_S = pkgen(sk[i1]) then (
let AuthDecap_Some(k0) = AuthDecap(key_extr, cd, skgen(sk), pk_S) in (
k' <-R eae_output_t;
insert E(pk_S, pkgen(sk), cd, k');
return(AuthDecap_Some(k'))
) else (
return(AuthDecap_None)
)
) else (
return(AuthDecap(key_extr, cd, skgen(sk), pk_S))
)
)) |
Opk() := return(pkgen(sk))
)) |
run ExtractAndExpand_inner_orcl(key_extr)
)
(* EXPECTED FILENAME: examples/hpke/dhkem.auth.outsider-auth-lr.m4.ocv TAG: 1
All queries proved.
0.924s (user 0.916s + system 0.008s), max rss 30176K
END *)