-
Notifications
You must be signed in to change notification settings - Fork 0
/
dhkem.auth.outsider-cca-lr.m4.ocv
166 lines (156 loc) · 5.78 KB
/
dhkem.auth.outsider-cca-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
(* 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 "l1.out.cv";
(* Let appear this case distinction in the Encap oracle,
that is present on the right side. *)
insert after "OAEncap(pk_R"
"find i1 <= N suchthat
defined(sk[i1])
&& pk_R = exp(g, sk[i1]) then";
(* Use unique names for the assignments of the following variables
that are currently not unique *)
SArename z;
SArename enc_1;
SArename zz_2;
SArename pkE_2;
SArename pkS;
SArename dh_2;
SArename kemContext_2;
SArename key;
SArename info;
(* Let appear this case distinction in the Decap oracle,
that is present on the right side *)
insert after "OADecap(pk_S"
"find ie1 <= Qeperuser, i1 <= N suchthat
defined(sk[i1], pk_R[ie1, i1], zz_10[ie1, i1], z_5[ie1, i1], enc_8[ie1, i1])
&& exp(g, sk) = pk_R[ie1, i1]
&& pk_S = exp(g, sk[i1])
&& enc_8[ie1, i1] = enc_2 then";
out_game "l2.out.cv";
out_game "l2occ.out.cv" occ;
(* Use correctness of the KEM: In the Decap oracle for honest
participants, return the key chosen in the Encap oracle.
This replacement is done at the 1st line that matches the regex,
at the 3rd term/occurrence number within the match (zz_3). *)
replace
at_nth 1 3 "return{[0-9]*}({[0-9]*}AuthDecap_Some({[0-9]*}zz_3))"
"zz_10[ie1, i1_4]";
all_simplify;
(* Make it possible to reason about the composition of the
random oracle inputs, specifically the group elements,
which is needed for the usage of the GDH assumption. *)
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";
out_game "l3.out.cv";
crypto rom(ExtractAndExpand_inner);
out_game "l4.out.cv";
(* Apply the GDH assumption, where the longterm static key sk, and
the ephemeral key z_5 (generated in the Encaps oracle in the case
of honest participants), are considered uncompromised. *)
crypto gdh(exp) [variables: sk -> a, z_5 -> b];
out_game "l5.out.cv";
(* go to the right side *)
start_from_other_end;
out_game "r1.out.cv";
(* Make it possible to reason about the composition of the
random oracle inputs, specifically the group elements,
which is needed for the usage of the GDH assumption. *)
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);
remove_assign binder E_1;
out_game "r2.out.cv";
success
}
include(`common.dhkem.ocvl')
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) :=
find i1 <= N suchthat defined(sk[i1]) && pk_R = pkgen(sk[i1]) then (
let AuthEncap_tuple(k: eae_output_t, ce: bitstring) = AuthEncap(key_extr, pk_R, skgen(sk)) in (
k' <-R eae_output_t;
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)
)
) else (
return(AuthEncap(key_extr, pk_R, skgen(sk)))
)) |
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 (
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-cca-lr.m4.ocv TAG: 1
All queries proved.
0.496s (user 0.492s + system 0.004s), max rss 26796K
END *)