-
Notifications
You must be signed in to change notification settings - Fork 16
/
KeySchedule2.cv
executable file
·120 lines (86 loc) · 3.58 KB
/
KeySchedule2.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
(* This file proves that, when the handshake secret hs is a fresh random value,
log_1 -> derive-secret(hs, client_hts, log_1)
|| derive-secret(hs, server_hts, log_1)
is indistinguishable from a random function and
\hkdfextract(hs, 0) is indistinguishable from a fresh random value
independent from this random function. *)
(* Proof indications *)
proof {
auto;
SArename r2_77;
auto
}
type extracted [large, fixed].
type key [large, fixed].
type two_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)).
letfun HKDF_extract(Salt: extracted, Ikm: bitstring) =
HMAC(Salt, Ikm).
fun concat(key, key): two_keys [compos].
equiv concat
!N new r1: key; new r2: key; O() := concat(r1, r2)
<=(0)=>
!N new r: two_keys; O() := r.
(* Labels *)
const client_hts : label. (* hts = handshake traffic secret *)
const server_hts : label.
(* Concatenation of client_handshake_traffic_secret and server_handshake_traffic_secret *)
letfun Derive_Secret_cs_hts(hk: hashkey, HandshakeSecret: extracted, log: bitstring) =
concat(Derive_secret(hk, HandshakeSecret, client_hts, log),
Derive_secret(hk, HandshakeSecret, server_hts, log)).
(* Master Secret *)
const zero: bitstring.
letfun HKDF_extract_zero(HandshakeSecret: extracted) =
HKDF_extract(HandshakeSecret, zero).
forall l: label, h: hash; build_arg(l, h) <> zero.
(* Prove equivalence between processLeft and processRight *)
query secret b.
channel start, c1, c2, c3.
let processLeft =
!N3 in(c1, ()); new hs: extracted; out(c1, ());
((!N in(c2, log0: bitstring); out(c2, Derive_Secret_cs_hts(hk, hs, log0))) |
in(c3, ()); out(c3, HKDF_extract_zero(hs))).
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: two_keys; out(c2, r)) |
(in(c3, ()); 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.028s (user 0.024s + system 0.004s), max rss 33808K
END *)