-
Notifications
You must be signed in to change notification settings - Fork 15
/
Copy pathtls13-core-RecordProtocol-0RTT.cv
158 lines (121 loc) · 5.1 KB
/
tls13-core-RecordProtocol-0RTT.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
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
(* This file proves properties of the record protocol,
assuming the client and server initially share a random
traffic secret. *)
type key [fixed, large].
type seqn [fixed].
type nonce_t [fixed, large].
type nocolltype [fixed, large].
param N, Nk, Ne, Nd, Ns, NSr, Nr.
(* We use the lemma proved in HKDFexpand.cv *)
fun HKDF_expand_upd_label(key): key.
fun HKDF_expand_key_label(key): key.
fun HKDF_expand_iv_label(key): key.
proba Pprf_upd_key_iv.
equiv prf_upd_key_iv
!N new r: key; (O1() := HKDF_expand_upd_label(r),
O2() := HKDF_expand_key_label(r),
O3() := HKDF_expand_iv_label(r))
<=(N * Pprf_upd_key_iv(time + (N-1)*(time(HKDF_expand_upd_label) + time(HKDF_expand_key_label) + time(HKDF_expand_iv_label))))=>
!N (O1() := new r1: key; r1,
O2() := new r2: key; r2,
O3() := new r3: key; r3).
(* Injectivity of xor *)
fun xor(key, seqn): nonce_t.
forall k: key, n: seqn, n': seqn;
(xor(k, n) = xor(k,n')) = (n = n').
(* AEAD *)
fun AEAD_encrypt(key, nonce_t, bitstring): bitstring.
fun AEAD_decrypt(key, nonce_t, bitstring): bitstringbot.
(* encryption is IND-CPA and INT-CTXT provided the nonce is distinct
for each encryption *)
(* Z(x) is a bitstring of the same length as x, containing only zeroes *)
fun Z(bitstring): bitstring.
(* injbot is the natural injection from bitstring to bitstring union bottom *)
fun injbot(bitstring):bitstringbot [compos].
forall x:bitstring; injbot(x) <> bottom.
forall k: key, nonce: nonce_t, msg: bitstring;
AEAD_decrypt(k, nonce, AEAD_encrypt(k, nonce, msg)) = injbot(msg).
fun AEAD_encrypt'(key, nonce_t, bitstring): bitstring.
proba Penc.
event repeated_nonce.
equiv
!Nk new k: key; (!Ne Oenc(nonce_e: nonce_t, msg: bitstring) := AEAD_encrypt(k, nonce_e, msg),
!Nd Odec(nonce_d: nonce_t, cip: bitstring) := AEAD_decrypt(k, nonce_d, cip))
<=(Nk * Penc(time + (Nk-1)*(Ne*time(AEAD_encrypt, maxlength(msg)) + Ne*time(Z, maxlength(msg)) +
Nd*time(AEAD_decrypt, maxlength(cip))), Ne, Nd, maxlength(msg), maxlength(cip)))=>
!Nk new k: key;
(!Ne Oenc(nonce_e: nonce_t, msg: bitstring) :=
find i <= Ne suchthat defined(nonce_e[i],r[i]) && nonce_e = nonce_e[i] then
event_abort repeated_nonce
else
let r: bitstring = AEAD_encrypt'(k, nonce_e, Z(msg)) in
r,
!Nd Odec(nonce_d: nonce_t, cip: bitstring) :=
find j <= Ne suchthat defined(msg[j], nonce_e[j], r[j]) && nonce_d = nonce_e[j] && cip = r[j] then
injbot(msg[j])
else
bottom).
(* Test function *)
fun test(bool, bitstring, bitstring): bitstring.
forall x:bitstring,y:bitstring; test(true,x,y) = x.
forall x:bitstring,y:bitstring; test(false,x,y) = y.
forall b:bool,x:bitstring; test(b,x,x) = x.
forall b:bool,x:bitstring,y:bitstring;
Z(test(b, x, y)) = test(b, Z(x), Z(y)).
(* Tables used to record previously used sequence numbers,
to avoid reusing them *)
table table_count_send(seqn).
table table_count_recv(nocolltype, seqn).
(* Secrecy of plaintexts *)
query secret b public_vars traffic_secret_Nplus1.
(* Message authenticity *)
event sent(seqn, bitstring).
event received(seqn, bitstring).
query count: seqn, msg: bitstring;
event received(count, msg) ==> sent(count, msg).
(* The injective variant does not hold: messages
can be replayed in a different session *)
(* Secrecy of updated key *)
query secret traffic_secret_Nplus1 public_vars b.
channel io1, io2, io3, io4, io5, io6, io7, io8.
let send =
!Ns
in(io5, (clear1: bitstring, clear2: bitstring, count: seqn));
(* Make sure that count has not been used before *)
get table_count_send(=count) in yield else
insert table_count_send(count);
(* The two candidate plaintexts must have the same (padded) length *)
if Z(clear1) = Z(clear2) then
let clear = test(b, clear1, clear2) in
event sent(count, clear);
let nonce = xor(iv, count) in
let cipher = AEAD_encrypt(k, nonce, clear) in
out(io6, cipher).
let receive =
!isr <= NSr
in(io3, ());
new sessionid: nocolltype; (* used to make sure that for different sessions
of the receiver (that is, for different values of isr)
a different table is used *)
out(io4, ());
!Nr
in(io7, (cipher: bitstring, count: seqn));
(* Make sure that count has not been used before in this session *)
get table_count_recv(=sessionid, =count) in yield else
insert table_count_recv(sessionid, count);
let nonce = xor(iv, count) in
let injbot(clear) = AEAD_decrypt(k, nonce, cipher) in
event received(count, clear).
process
in(io1, ());
new b: bool;
new traffic_secret_N: key;
let traffic_secret_Nplus1: key = HKDF_expand_upd_label(traffic_secret_N) in
let k = HKDF_expand_key_label(traffic_secret_N) in
let iv = HKDF_expand_iv_label(traffic_secret_N) in
out(io2, ());
(send | receive)
(* EXPECTED
All queries proved.
0.044s (user 0.044s + system 0.000s), max rss 31408K
END *)