-
Notifications
You must be signed in to change notification settings - Fork 0
/
common.dhkem.ocvl
218 lines (179 loc) · 6.7 KB
/
common.dhkem.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
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
(* 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 *)
type G_t [bounded].
fun Serialize(G_t): bitstring [data].
type Z_t [bounded,nonuniform].
proba PCollKey.
expand DH_proba_collision_minimal(
G_t,
Z_t,
g,
exp,
mult,
PCollKey
).
ifdef(`square',`
proba Adv_sqGDH.
proba PDistRerandom.
expand square_GDH_RSR_minimal(
(* types *)
G_t, (* Group elements *)
Z_t, (* Exponents *)
(* variables *)
g, (* a generator of the group *)
exp, (* exponentiation function *)
mult, (* multiplication function for exponents *)
(* probabilities *)
Adv_sqGDH, (* probability of breaking the square GDH assumption *)
PDistRerandom (* probability of distinguishing a key that comes from
rerandomization from an honestly chosen key *)
).
',`
proba Adv_GDH.
proba PDistRerandom.
expand GDH_RSR_minimal(
(* types *)
G_t, (* Group elements *)
Z_t, (* Exponents *)
(* variables *)
g, (* a generator of the group *)
exp, (* exponentiation function *)
mult, (* multiplication function for exponents *)
(* probabilities *)
Adv_GDH, (* probability of breaking the GDH assumption *)
PDistRerandom (* probability of distinguishing a key that comes from
rerandomization from an honestly chosen key *)
).
')
(* For a group of prime order q:
PColl1Rand(Z_t) = PColl2Rand(Z_t) = 1/(q-1)
PCollKey1 = PCollKey2 = 1/(q-1)
PDistRerandom = 0
For Curve25519:
PColl1Rand(Z_t) = PColl2Rand(Z_t) = 2^{-251}
PCollKey1 = PCollKey2 = 2 PColl1Rand(Z_t) = 2^{-250}
PDistRerandom = 2^{-125}
For Curve448:
PColl1Rand(Z_t) = PColl2Rand(Z_t) = 2^{-445}
PCollKey1 = PCollKey2 = 2 PColl1Rand(Z_t) = 2^{-444}
PDistRerandom = 2^{-220}
*)
letfun DH(exponent: Z_t, group_element: G_t) =
exp(group_element, exponent).
letfun pkgen(exponent: Z_t) =
exp(g, exponent).
letfun skgen(exponent: Z_t) =
exponent.
letfun GenerateKeyPair() =
z <-R Z_t;
(skgen(z), pkgen(z)).
(* KDF *)
type hash_key_t [fixed]. (* RO key *)
type eae_input_t [fixed].
type eae_output_t [fixed,large].
type extract_salt_t [fixed]. (* We only use one constant salt value. *)
type extract_key_t [fixed].
type expand_info_t [fixed].
const lbytes_empty: extract_salt_t.
fun eae_input(extract_salt_t, extract_key_t, expand_info_t): eae_input_t [data].
(* The core of ExtractAndExpand, a.k.a. HKDF.
Usage of the RO assumption is for example justified in Lemma 6 of
Benjamin Lipp, Bruno Blanchet, Karthikeyan Bhargavan,
A Mechanised Cryptographic Proof of the WireGuard Virtual Private Network Protocol,
EuroSP2019 *)
expand ROM_hash_1(
(* types *)
hash_key_t,
eae_input_t,
eae_output_t,
(* functions *)
ExtractAndExpand_inner,
(* processes *)
ExtractAndExpand_inner_orcl,
(* parameters *)
Qh (* number of queries to the oracle by the adversary *)
).
type length_t [fixed].
type two_byte_t [fixed].
fun I2OSP2(length_t): two_byte_t [data].
const Nsecret: length_t.
type label_protocol_t [fixed].
const RFCXXXX: label_protocol_t.
type label_extract_t [fixed].
const label_eae_prk: label_extract_t.
type label_expand_t [fixed].
const label_shared_secret: label_expand_t.
type suite_id_t [fixed].
const suite_id: suite_id_t.
type GG_t [fixed].
type GGG_t [fixed].
fun concatDH(G_t, G_t): GG_t [data].
fun concatContext(G_t, G_t, G_t): GGG_t [data].
(* This can be data because we only use it with a few known constants
for the two first parameters, or with fixed-length parameters. *)
fun concatExtract(label_protocol_t, suite_id_t, label_extract_t, GG_t): extract_key_t [data].
(* concatExpand is only used in LabeledExpand, which is only used
in ExtractAndExpand in the KEM:
LabeledExpand(eae_prk, label_shared_secret, kem_context, Nsecret)
with the following call:
concatExpand(I2OSP2(L), RFCXXXX, suite_id, label, info).
I2OSP2 is fixed-length (two bytes),
RFCXXXX is fixed-length (7 bytes),
suite_id is fixed-length,
label_shared_secret is fixed-length;
info is fixed-length as concatenation of enc||pkR||pkS *)
fun concatExpand(two_byte_t, label_protocol_t, suite_id_t, label_expand_t, GGG_t): expand_info_t [data].
(* Detailed justification that the following usage of ExtractAndExpand
satisfies the assumptions of above-mentioned Lemma 6, given it is
implemented by HKDF:
- keyspace and info||i_0 do not collide, because info has two bytes and
then RFCXXXX, and RFCXXXX does not collide with itself when moved by
two bytes.
For long Nsecret, we also need to consider this:
- keyspace and hmac_output_space||info||i_j with j>0
Length(keyspace) - Length(hmac_output_space||info||i_j)
= -2 +Length(label_eae_prk) -Length(label_shared_secret) +Length(dh) -Length(kem_context) -Nh
= -2 +7 -13 +Ndh -Nenc -Npk -Npk -Nh
= -8 +Ndh -Nenc -Npk -Npk -Nh
Assuming that Ndh is pretty close to Npk, we can argue that
keyspace and hmac_output_space||info||i_j with j>0
have clearly different lengths, and thus, do not collide.
Therefore the following usage of ExtractAndExpand satisfies the
assumptions of Lemma 6.
*)
letfun ExtractAndExpand(key_extr: hash_key_t, dh: GG_t, kem_context: GGG_t) =
let key = concatExtract(RFCXXXX, suite_id, label_eae_prk, dh) in
let info = concatExpand(I2OSP2(Nsecret), RFCXXXX, suite_id, label_shared_secret, kem_context) in
ExtractAndExpand_inner(key_extr, eae_input(lbytes_empty, key, info)).
expand OptionType_2(AuthEncap_res_t, AuthEncap_tuple, AuthEncap_None, eae_output_t, bitstring).
letfun AuthEncap(key_extr: hash_key_t, pkR: G_t, skS: Z_t) =
let (skE: Z_t, pkE: G_t) = GenerateKeyPair() in
(
let dh: GG_t = concatDH(DH(skE, pkR), DH(skS, pkR)) in
let enc: bitstring = Serialize(pkE) in
let pkS = pkgen(skS) in
let kemContext: GGG_t = concatContext(pkE, pkR, pkS) in
let zz: eae_output_t = ExtractAndExpand(key_extr, dh, kemContext) in
AuthEncap_tuple(zz, enc)
) else (
AuthEncap_None
).
expand OptionType_1(AuthDecap_res_t, AuthDecap_Some, AuthDecap_None, eae_output_t).
letfun AuthDecap(key_extr: hash_key_t, enc: bitstring, skR: Z_t, pkS: G_t) =
let Serialize(pkE: G_t) = enc in
(
let dh: GG_t = concatDH(DH(skR, pkE), DH(skR, pkS)) in
let pkR = pkgen(skR) in
let kemContext: GGG_t = concatContext(pkE, pkR, pkS) in
let zz: eae_output_t = ExtractAndExpand(key_extr, dh, kemContext) in
AuthDecap_Some(zz)
) else (
AuthDecap_None
).