-
Notifications
You must be signed in to change notification settings - Fork 16
/
KeySchedule3.cv
executable file
·124 lines (91 loc) · 3.83 KB
/
KeySchedule3.cv
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
(* This file proves that, when the master secret ms is a fresh random value,
log_4 -> derive-secret(ms, client_ats, log_4)
|| derive-secret(ms, server_ats, log_4)
|| derive-secret(ms, exporter_ms, log_4)
and
log_7 -> derive-secret(ms, resumption_ms, log_7)
are indistinguishable from independent random functions. *)
(* Proof indications *)
proof {
auto;
SArename r2_84;
auto
}
type extracted [large, fixed].
type key [large, fixed].
type three_keys [large, fixed].
type label.
(* HMAC is a PRF *)
fun HMAC(extracted, bitstring):key.
proba Pprf.
param N, N3.
equiv prf(HMAC)
!N3 new r: extracted; !N O(x:bitstring) := HMAC(r,x)
<=(N3 * (2/|extracted| + Pprf(time + (N3-1)* N * time(HMAC, maxlength(x)), N, maxlength(x))))=>
!N3 !N O(x: bitstring) :=
find[unique] j<=N suchthat defined(x[j],r2[j]) && x = x[j] then r2[j]
else new r2: key; r2.
(* Hash is a collision resistant hash function *)
type hashkey [large,fixed].
type hash [fixed].
proba Phash.
expand CollisionResistant_hash(hashkey, bitstring, hash, Hash, Phash).
(* Derive_secret(Secret, Label, Messages) =
HKDF_expand_label(Secret, Label, Hash(Messages), Hash.length) =
HKDF_expand(Secret, [Hash.length, "TLS 1.3, " + Label, Hash(Messages)], Hash.length) =
HMAC(Secret, [Hash.length, "TLS 1.3, " + Label, Hash(Messages), 0x00])
We define build_arg(Label, Hash) = [Length, "TLS 1.3, " + Label, Hash, 0x00].
*)
fun build_arg(label, hash): bitstring [compos].
letfun HKDF_expand_label(Secret: extracted, Label: label, HashValue: hash) =
HMAC(Secret, build_arg(Label, HashValue)).
letfun Derive_secret(hk: hashkey, Secret: extracted, Label: label, Messages: bitstring) =
HKDF_expand_label(Secret, Label, Hash(hk, Messages)).
fun concat(key, key, key): three_keys [compos].
equiv concat
!N new r1: key; new r2: key; new r3: key; O() := concat(r1, r2, r3)
<=(0)=>
!N new r: three_keys; O() := r.
(* Labels *)
const client_ats : label. (* ats = application traffic secret *)
const server_ats : label.
const exporter_ms : label. (* ms = master secret *)
const resumption_ms : label.
(* Concatenation of client_traffic_secret_0, server_traffic_secret_0, and exporter_secret *)
letfun Derive_Secret_cs_ats_exp(hk: hashkey, MasterSecret: extracted, log: bitstring) =
concat(Derive_secret(hk, MasterSecret, client_ats, log),
Derive_secret(hk, MasterSecret, server_ats, log),
Derive_secret(hk, MasterSecret, exporter_ms, log)).
(* resumption_secret *)
letfun Derive_Secret_rms(hk: hashkey, MasterSecret: extracted, log: bitstring) =
Derive_secret(hk, MasterSecret, resumption_ms, log).
(* Prove equivalence between processLeft and processRight *)
query secret b.
channel start, c1, c2, c3.
param N'.
let processLeft =
!N3 in(c1, ()); new ms: extracted; out(c1, ());
((!N in(c2, log0: bitstring); out(c2, Derive_Secret_cs_ats_exp(hk, ms, log0))) |
(!N' in(c3, log0': bitstring); out(c3, Derive_Secret_rms(hk, ms, log0')))).
let processRight =
!N3 in(c1, ()); out(c1, ());
((!N in(c2, log: bitstring);
find[unique] j <= N suchthat defined(log[j], r[j]) && log = log[j] then
out(c2, r[j])
else
new r: three_keys; out(c2, r)) |
(!N' in(c3, log': bitstring);
find[unique] j' <= N' suchthat defined(log'[j'], r'[j']) && log' = log'[j'] then
out(c3, r'[j'])
else
new r': key; out(c3, r'))).
process
in(start, ());
new b: bool;
new hk: hashkey; (* This key models the choice of the collision resistant hash function *)
if b then out(start, hk); processLeft
else out(start, hk); processRight
(* EXPECTED
All queries proved.
0.480s (user 0.472s + system 0.008s), max rss 53424K
END *)