author  huffman 
Wed, 10 Mar 2010 15:33:13 0800  
changeset 35702  fb7a386a15cb 
parent 35416  d8d7d1b785af 
child 37936  1e4c5015a72e 
permissions  rwrr 
3474  1 
(* Title: HOL/Auth/TLS 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1997 University of Cambridge 

5 

3759
3d1ac6b82b28
Fixed ServerResume to check for ServerHello instead of making a new NB
paulson
parents:
3757
diff
changeset

6 
Inductive relation "tls" for the TLS (Transport Layer Security) protocol. 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

7 
This protocol is essentially the same as SSL 3.0. 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

8 

56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

9 
Abstracted from "The TLS Protocol, Version 1.0" by Tim Dierks and Christopher 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

10 
Allen, Transport Layer Security Working Group, 21 May 1997, 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

11 
INTERNETDRAFT draftietftlsprotocol03.txt. Section numbers below refer 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

12 
to that memo. 
3474  13 

14 
An RSA cryptosystem is assumed, and X.509v3 certificates are abstracted down 

15 
to the trivial form {A, publicKey(A)}privateKey(Server), where Server is a 

16 
global signing authority. 

17 

18 
A is the client and B is the server, not to be confused with the constant 

19 
Server, who is in charge of all public keys. 

20 

3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

21 
The model assumes that no fraudulent certificates are present, but it does 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset

22 
assume that some private keys are to the spy. 
3474  23 

3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

24 
REMARK. The event "Notes A {Agent B, Nonce PMS}" appears in ClientKeyExch, 
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

25 
CertVerify, ClientFinished to record that A knows M. It is a note from A to 
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

26 
herself. Nobody else can see it. In ClientKeyExch, the Spy can substitute 
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

27 
his own certificate for A's, but he cannot replace A's note by one for himself. 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

28 

3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

29 
The Note event avoids a weakness in the publickey model. Each 
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

30 
agent's state is recorded as the trace of messages. When the true client (A) 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

31 
invents PMS, he encrypts PMS with B's public key before sending it. The model 
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

32 
does not distinguish the original occurrence of such a message from a replay. 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

33 
In the sharedkey model, the ability to encrypt implies the ability to 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

34 
decrypt, so the problem does not arise. 
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

35 

3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

36 
Proofs would be simpler if ClientKeyExch included A's name within 
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

37 
Crypt KB (Nonce PMS). As things stand, there is much overlap between proofs 
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

38 
about that message (which B receives) and the stronger event 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

39 
Notes A {Agent B, Nonce PMS}. 
3474  40 
*) 
41 

13956  42 
header{*The TLS Protocol: Transport Layer Security*} 
43 

35702  44 
theory TLS imports Public Nat_Bijection begin 
3474  45 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset

46 
definition certificate :: "[agent,key] => msg" where 
13922  47 
"certificate A KA == Crypt (priSK Server) {Agent A, Key KA}" 
48 

49 
text{*TLS apparently does not require separate keypairs for encryption and 

50 
signature. Therefore, we formalize signature as encryption using the 

51 
private encryption key.*} 

5653
204083e3f368
changed tags from 0, 1 to None, Some() to avoid special treatment of 0
paulson
parents:
5434
diff
changeset

52 

6284
147db42c1009
tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents:
5653
diff
changeset

53 
datatype role = ClientRole  ServerRole 
147db42c1009
tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents:
5653
diff
changeset

54 

3474  55 
consts 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

56 
(*Pseudorandom function of Section 5*) 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

57 
PRF :: "nat*nat*nat => nat" 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

58 

3704  59 
(*Client, server write keys are generated uniformly by function sessionK 
5653
204083e3f368
changed tags from 0, 1 to None, Some() to avoid special treatment of 0
paulson
parents:
5434
diff
changeset

60 
to avoid duplicating their properties. They are distinguished by a 
204083e3f368
changed tags from 0, 1 to None, Some() to avoid special treatment of 0
paulson
parents:
5434
diff
changeset

61 
tag (not a bool, to avoid the peculiarities of ifandonlyif). 
3704  62 
Session keys implicitly include MAC secrets.*) 
6284
147db42c1009
tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents:
5653
diff
changeset

63 
sessionK :: "(nat*nat*nat) * role => key" 
3474  64 

20768  65 
abbreviation 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset

66 
clientK :: "nat*nat*nat => key" where 
20768  67 
"clientK X == sessionK(X, ClientRole)" 
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

68 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset

69 
abbreviation 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset

70 
serverK :: "nat*nat*nat => key" where 
20768  71 
"serverK X == sessionK(X, ServerRole)" 
72 

3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

73 

14126
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset

74 
specification (PRF) 
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset

75 
inj_PRF: "inj PRF" 
13922  76 
{*the pseudorandom function is collisionfree*} 
35702  77 
apply (rule exI [of _ "%(x,y,z). prod_encode(x, prod_encode(y,z))"]) 
78 
apply (simp add: inj_on_def prod_encode_eq) 

14126
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset

79 
done 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

80 

14126
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset

81 
specification (sessionK) 
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset

82 
inj_sessionK: "inj sessionK" 
13922  83 
{*sessionK is collisionfree; also, no clientK clashes with any serverK.*} 
14126
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset

84 
apply (rule exI [of _ 
35702  85 
"%((x,y,z), r). prod_encode(role_case 0 1 r, 
86 
prod_encode(x, prod_encode(y,z)))"]) 

87 
apply (simp add: inj_on_def prod_encode_eq split: role.split) 

14126
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset

88 
done 
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

89 

14126
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset

90 
axioms 
13922  91 
{*sessionK makes symmetric keys*} 
11287  92 
isSym_sessionK: "sessionK nonces \<in> symKeys" 
3474  93 

13922  94 
{*sessionK never clashes with a longterm symmetric key 
95 
(they don't exist in TLS anyway)*} 

96 
sessionK_neq_shrK [iff]: "sessionK nonces \<noteq> shrK A" 

97 

3474  98 

23746  99 
inductive_set tls :: "event list set" 
100 
where 

13922  101 
Nil: {*The initial, empty trace*} 
11287  102 
"[] \<in> tls" 
3474  103 

23746  104 
 Fake: {*The Spy may say anything he can say. The sender field is correct, 
13922  105 
but agents don't use that information.*} 
11287  106 
"[ evsf \<in> tls; X \<in> synth (analz (spies evsf)) ] 
107 
==> Says Spy B X # evsf \<in> tls" 

3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset

108 

23746  109 
 SpyKeys: {*The spy may apply @{term PRF} and @{term sessionK} 
13956  110 
to available nonces*} 
11287  111 
"[ evsSK \<in> tls; 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

112 
{Nonce NA, Nonce NB, Nonce M} <= analz (spies evsSK) ] 
4421
88639289be39
Simplified SpyKeys and ClientKeyExch as suggested by James Margetson
paulson
parents:
4198
diff
changeset

113 
==> Notes Spy { Nonce (PRF(M,NA,NB)), 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

114 
Key (sessionK((NA,NB,M),role)) } # evsSK \<in> tls" 
3474  115 

23746  116 
 ClientHello: 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

117 
{*(7.4.1.2) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

118 
PA represents @{text CLIENT_VERSION}, @{text CIPHER_SUITES} and @{text COMPRESSION_METHODS}. 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

119 
It is uninterpreted but will be confirmed in the FINISHED messages. 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

120 
NA is CLIENT RANDOM, while SID is @{text SESSION_ID}. 
3676
cbaec955056b
Addition of SessionIDs to the Hello and Finished messages
paulson
parents:
3672
diff
changeset

121 
UNIX TIME is omitted because the protocol doesn't use it. 
13956  122 
May assume @{term "NA \<notin> range PRF"} because CLIENT RANDOM is 
123 
28 bytes while MASTER SECRET is 48 bytes*} 

11287  124 
"[ evsCH \<in> tls; Nonce NA \<notin> used evsCH; NA \<notin> range PRF ] 
3729
6be7cf5086ab
Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents:
3710
diff
changeset

125 
==> Says A B {Agent A, Nonce NA, Number SID, Number PA} 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

126 
# evsCH \<in> tls" 
3474  127 

23746  128 
 ServerHello: 
13922  129 
{*7.4.1.3 of the TLS InternetDraft 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

130 
PB represents @{text CLIENT_VERSION}, @{text CIPHER_SUITE} and @{text COMPRESSION_METHOD}. 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

131 
SERVER CERTIFICATE (7.4.2) is always present. 
13956  132 
@{text CERTIFICATE_REQUEST} (7.4.4) is implied.*} 
11287  133 
"[ evsSH \<in> tls; Nonce NB \<notin> used evsSH; NB \<notin> range PRF; 
3729
6be7cf5086ab
Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents:
3710
diff
changeset

134 
Says A' B {Agent A, Nonce NA, Number SID, Number PA} 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

135 
\<in> set evsSH ] 
11287  136 
==> Says B A {Nonce NB, Number SID, Number PB} # evsSH \<in> tls" 
3474  137 

23746  138 
 Certificate: 
13922  139 
{*SERVER (7.4.2) or CLIENT (7.4.6) CERTIFICATE.*} 
11287  140 
"evsC \<in> tls ==> Says B A (certificate B (pubK B)) # evsC \<in> tls" 
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

141 

23746  142 
 ClientKeyExch: 
13922  143 
{*CLIENT KEY EXCHANGE (7.4.7). 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

144 
The client, A, chooses PMS, the PREMASTER SECRET. 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

145 
She encrypts PMS using the supplied KB, which ought to be pubK B. 
13956  146 
We assume @{term "PMS \<notin> range PRF"} because a clash betweem the PMS 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

147 
and another MASTER SECRET is highly unlikely (even though 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

148 
both items have the same length, 48 bytes). 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

149 
The Note event records in the trace that she knows PMS 
13922  150 
(see REMARK at top). *} 
11287  151 
"[ evsCX \<in> tls; Nonce PMS \<notin> used evsCX; PMS \<notin> range PRF; 
152 
Says B' A (certificate B KB) \<in> set evsCX ] 

3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset

153 
==> Says A B (Crypt KB (Nonce PMS)) 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

154 
# Notes A {Agent B, Nonce PMS} 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

155 
# evsCX \<in> tls" 
3474  156 

23746  157 
 CertVerify: 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

158 
{*The optional Certificate Verify (7.4.8) message contains the 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

159 
specific components listed in the security analysis, F.1.1.2. 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

160 
It adds the premastersecret, which is also essential! 
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

161 
Checking the signature, which is the only use of A's certificate, 
13922  162 
assures B of A's presence*} 
11287  163 
"[ evsCV \<in> tls; 
164 
Says B' A {Nonce NB, Number SID, Number PB} \<in> set evsCV; 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

165 
Notes A {Agent B, Nonce PMS} \<in> set evsCV ] 
3729
6be7cf5086ab
Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents:
3710
diff
changeset

166 
==> Says A B (Crypt (priK A) (Hash{Nonce NB, Agent B, Nonce PMS})) 
11287  167 
# evsCV \<in> tls" 
3474  168 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

169 
{*Finally come the FINISHED messages (7.4.8), confirming PA and PB 
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset

170 
among other things. The mastersecret is PRF(PMS,NA,NB). 
13922  171 
Either party may send its message first.*} 
3474  172 

23746  173 
 ClientFinished: 
13922  174 
{*The occurrence of Notes A {Agent B, Nonce PMS} stops the 
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

175 
rule's applying when the Spy has satisfied the "Says A B" by 
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset

176 
repaying messages sent by the true client; in that case, the 
6284
147db42c1009
tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents:
5653
diff
changeset

177 
Spy does not know PMS and could not send ClientFinished. One 
13956  178 
could simply put @{term "A\<noteq>Spy"} into the rule, but one should not 
13922  179 
expect the spy to be wellbehaved.*} 
11287  180 
"[ evsCF \<in> tls; 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

181 
Says A B {Agent A, Nonce NA, Number SID, Number PA} 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

182 
\<in> set evsCF; 
11287  183 
Says B' A {Nonce NB, Number SID, Number PB} \<in> set evsCF; 
184 
Notes A {Agent B, Nonce PMS} \<in> set evsCF; 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

185 
M = PRF(PMS,NA,NB) ] 
3474  186 
==> Says A B (Crypt (clientK(NA,NB,M)) 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

187 
(Hash{Number SID, Nonce M, 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

188 
Nonce NA, Number PA, Agent A, 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

189 
Nonce NB, Number PB, Agent B})) 
11287  190 
# evsCF \<in> tls" 
3474  191 

23746  192 
 ServerFinished: 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

193 
{*Keeping A' and A'' distinct means B cannot even check that the 
13922  194 
two messages originate from the same source. *} 
11287  195 
"[ evsSF \<in> tls; 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

196 
Says A' B {Agent A, Nonce NA, Number SID, Number PA} 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

197 
\<in> set evsSF; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

198 
Says B A {Nonce NB, Number SID, Number PB} \<in> set evsSF; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

199 
Says A'' B (Crypt (pubK B) (Nonce PMS)) \<in> set evsSF; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

200 
M = PRF(PMS,NA,NB) ] 
3474  201 
==> Says B A (Crypt (serverK(NA,NB,M)) 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

202 
(Hash{Number SID, Nonce M, 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

203 
Nonce NA, Number PA, Agent A, 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

204 
Nonce NB, Number PB, Agent B})) 
11287  205 
# evsSF \<in> tls" 
3474  206 

23746  207 
 ClientAccepts: 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

208 
{*Having transmitted ClientFinished and received an identical 
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

209 
message encrypted with serverK, the client stores the parameters 
3687
fb7d096d7884
Simplified SpyKeys to use sessionK instead of clientK and serverK
paulson
parents:
3686
diff
changeset

210 
needed to resume this session. The "Notes A ..." premise is 
13956  211 
used to prove @{text Notes_master_imp_Crypt_PMS}.*} 
11287  212 
"[ evsCA \<in> tls; 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

213 
Notes A {Agent B, Nonce PMS} \<in> set evsCA; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

214 
M = PRF(PMS,NA,NB); 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

215 
X = Hash{Number SID, Nonce M, 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

216 
Nonce NA, Number PA, Agent A, 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

217 
Nonce NB, Number PB, Agent B}; 
11287  218 
Says A B (Crypt (clientK(NA,NB,M)) X) \<in> set evsCA; 
219 
Says B' A (Crypt (serverK(NA,NB,M)) X) \<in> set evsCA ] 

220 
==> 

221 
Notes A {Number SID, Agent A, Agent B, Nonce M} # evsCA \<in> tls" 

3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

222 

23746  223 
 ServerAccepts: 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

224 
{*Having transmitted ServerFinished and received an identical 
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

225 
message encrypted with clientK, the server stores the parameters 
3687
fb7d096d7884
Simplified SpyKeys to use sessionK instead of clientK and serverK
paulson
parents:
3686
diff
changeset

226 
needed to resume this session. The "Says A'' B ..." premise is 
13956  227 
used to prove @{text Notes_master_imp_Crypt_PMS}.*} 
11287  228 
"[ evsSA \<in> tls; 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

229 
A \<noteq> B; 
11287  230 
Says A'' B (Crypt (pubK B) (Nonce PMS)) \<in> set evsSA; 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

231 
M = PRF(PMS,NA,NB); 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

232 
X = Hash{Number SID, Nonce M, 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

233 
Nonce NA, Number PA, Agent A, 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

234 
Nonce NB, Number PB, Agent B}; 
11287  235 
Says B A (Crypt (serverK(NA,NB,M)) X) \<in> set evsSA; 
236 
Says A' B (Crypt (clientK(NA,NB,M)) X) \<in> set evsSA ] 

237 
==> 

238 
Notes B {Number SID, Agent A, Agent B, Nonce M} # evsSA \<in> tls" 

3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset

239 

23746  240 
 ClientResume: 
13956  241 
{*If A recalls the @{text SESSION_ID}, then she sends a FINISHED 
242 
message using the new nonces and stored MASTER SECRET.*} 

11287  243 
"[ evsCR \<in> tls; 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

244 
Says A B {Agent A, Nonce NA, Number SID, Number PA}: set evsCR; 
11287  245 
Says B' A {Nonce NB, Number SID, Number PB} \<in> set evsCR; 
246 
Notes A {Number SID, Agent A, Agent B, Nonce M} \<in> set evsCR ] 

3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

247 
==> Says A B (Crypt (clientK(NA,NB,M)) 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

248 
(Hash{Number SID, Nonce M, 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

249 
Nonce NA, Number PA, Agent A, 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

250 
Nonce NB, Number PB, Agent B})) 
11287  251 
# evsCR \<in> tls" 
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset

252 

23746  253 
 ServerResume: 
13956  254 
{*Resumption (7.3): If B finds the @{text SESSION_ID} then he can 
255 
send a FINISHED message using the recovered MASTER SECRET*} 

11287  256 
"[ evsSR \<in> tls; 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

257 
Says A' B {Agent A, Nonce NA, Number SID, Number PA}: set evsSR; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

258 
Says B A {Nonce NB, Number SID, Number PB} \<in> set evsSR; 
11287  259 
Notes B {Number SID, Agent A, Agent B, Nonce M} \<in> set evsSR ] 
3759
3d1ac6b82b28
Fixed ServerResume to check for ServerHello instead of making a new NB
paulson
parents:
3757
diff
changeset

260 
==> Says B A (Crypt (serverK(NA,NB,M)) 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

261 
(Hash{Number SID, Nonce M, 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

262 
Nonce NA, Number PA, Agent A, 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

263 
Nonce NB, Number PB, Agent B})) # evsSR 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

264 
\<in> tls" 
3759
3d1ac6b82b28
Fixed ServerResume to check for ServerHello instead of making a new NB
paulson
parents:
3757
diff
changeset

265 

23746  266 
 Oops: 
13922  267 
{*The most plausible compromise is of an old session key. Losing 
3686
4b484805b4c4
First working version with Oops event for session keys
paulson
parents:
3685
diff
changeset

268 
the MASTER SECRET or PREMASTER SECRET is more serious but 
13956  269 
rather unlikely. The assumption @{term "A\<noteq>Spy"} is essential: 
270 
otherwise the Spy could learn session keys merely by 

271 
replaying messages!*} 

11287  272 
"[ evso \<in> tls; A \<noteq> Spy; 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

273 
Says A B (Crypt (sessionK((NA,NB,M),role)) X) \<in> set evso ] 
11287  274 
==> Says A Spy (Key (sessionK((NA,NB,M),role))) # evso \<in> tls" 
275 

276 
(* 

277 
Protocol goals: 

278 
* M, serverK(NA,NB,M) and clientK(NA,NB,M) will be known only to the two 

279 
parties (though A is not necessarily authenticated). 

280 

281 
* B upon receiving CertVerify knows that A is present (But this 

282 
message is optional!) 

283 

284 
* A upon receiving ServerFinished knows that B is present 

285 

286 
* Each party who has received a FINISHED message can trust that the other 

287 
party agrees on all message components, including PA and PB (thus foiling 

288 
rollback attacks). 

289 
*) 

290 

291 
declare Says_imp_knows_Spy [THEN analz.Inj, dest] 

292 
declare parts.Body [dest] 

293 
declare analz_into_parts [dest] 

294 
declare Fake_parts_insert_in_Un [dest] 

295 

296 

13922  297 
text{*Automatically unfold the definition of "certificate"*} 
11287  298 
declare certificate_def [simp] 
299 

13922  300 
text{*Injectiveness of keygenerating functions*} 
11287  301 
declare inj_PRF [THEN inj_eq, iff] 
302 
declare inj_sessionK [THEN inj_eq, iff] 

303 
declare isSym_sessionK [simp] 

304 

305 

306 
(*** clientK and serverK make symmetric keys; no clashes with pubK or priK ***) 

307 

13922  308 
lemma pubK_neq_sessionK [iff]: "publicKey b A \<noteq> sessionK arg" 
11287  309 
by (simp add: symKeys_neq_imp_neq) 
310 

311 
declare pubK_neq_sessionK [THEN not_sym, iff] 

312 

13922  313 
lemma priK_neq_sessionK [iff]: "invKey (publicKey b A) \<noteq> sessionK arg" 
11287  314 
by (simp add: symKeys_neq_imp_neq) 
315 

316 
declare priK_neq_sessionK [THEN not_sym, iff] 

317 

318 
lemmas keys_distinct = pubK_neq_sessionK priK_neq_sessionK 

319 

320 

13922  321 
subsection{*Protocol Proofs*} 
11287  322 

13922  323 
text{*Possibility properties state that some traces run the protocol to the 
324 
end. Four paths and 12 rules are considered.*} 

11287  325 

326 

327 
(** These proofs assume that the Nonce_supply nonces 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

328 
(which have the form @ N. Nonce N \<notin> used evs) 
11287  329 
lie outside the range of PRF. It seems reasonable, but as it is needed 
330 
only for the possibility theorems, it is not taken as an axiom. 

331 
**) 

332 

333 

13922  334 
text{*Possibility property ending with ClientAccepts.*} 
11287  335 
lemma "[ \<forall>evs. (@ N. Nonce N \<notin> used evs) \<notin> range PRF; A \<noteq> B ] 
336 
==> \<exists>SID M. \<exists>evs \<in> tls. 

337 
Notes A {Number SID, Agent A, Agent B, Nonce M} \<in> set evs" 

338 
apply (intro exI bexI) 

339 
apply (rule_tac [2] tls.Nil 

340 
[THEN tls.ClientHello, THEN tls.ServerHello, 

341 
THEN tls.Certificate, THEN tls.ClientKeyExch, 

342 
THEN tls.ClientFinished, THEN tls.ServerFinished, 

13507  343 
THEN tls.ClientAccepts], possibility, blast+) 
11287  344 
done 
345 

346 

13922  347 
text{*And one for ServerAccepts. Either FINISHED message may come first.*} 
11287  348 
lemma "[ \<forall>evs. (@ N. Nonce N \<notin> used evs) \<notin> range PRF; A \<noteq> B ] 
349 
==> \<exists>SID NA PA NB PB M. \<exists>evs \<in> tls. 

350 
Notes B {Number SID, Agent A, Agent B, Nonce M} \<in> set evs" 

351 
apply (intro exI bexI) 

352 
apply (rule_tac [2] tls.Nil 

353 
[THEN tls.ClientHello, THEN tls.ServerHello, 

354 
THEN tls.Certificate, THEN tls.ClientKeyExch, 

355 
THEN tls.ServerFinished, THEN tls.ClientFinished, 

13507  356 
THEN tls.ServerAccepts], possibility, blast+) 
11287  357 
done 
358 

359 

13922  360 
text{*Another one, for CertVerify (which is optional)*} 
11287  361 
lemma "[ \<forall>evs. (@ N. Nonce N \<notin> used evs) \<notin> range PRF; A \<noteq> B ] 
362 
==> \<exists>NB PMS. \<exists>evs \<in> tls. 

363 
Says A B (Crypt (priK A) (Hash{Nonce NB, Agent B, Nonce PMS})) 

364 
\<in> set evs" 

365 
apply (intro exI bexI) 

366 
apply (rule_tac [2] tls.Nil 

367 
[THEN tls.ClientHello, THEN tls.ServerHello, 

368 
THEN tls.Certificate, THEN tls.ClientKeyExch, 

13507  369 
THEN tls.CertVerify], possibility, blast+) 
11287  370 
done 
371 

372 

13922  373 
text{*Another one, for session resumption (both ServerResume and ClientResume). 
374 
NO tls.Nil here: we refer to a previous session, not the empty trace.*} 

11287  375 
lemma "[ evs0 \<in> tls; 
376 
Notes A {Number SID, Agent A, Agent B, Nonce M} \<in> set evs0; 

377 
Notes B {Number SID, Agent A, Agent B, Nonce M} \<in> set evs0; 

378 
\<forall>evs. (@ N. Nonce N \<notin> used evs) \<notin> range PRF; 

379 
A \<noteq> B ] 

380 
==> \<exists>NA PA NB PB X. \<exists>evs \<in> tls. 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

381 
X = Hash{Number SID, Nonce M, 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

382 
Nonce NA, Number PA, Agent A, 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

383 
Nonce NB, Number PB, Agent B} & 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

384 
Says A B (Crypt (clientK(NA,NB,M)) X) \<in> set evs & 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

385 
Says B A (Crypt (serverK(NA,NB,M)) X) \<in> set evs" 
11287  386 
apply (intro exI bexI) 
387 
apply (rule_tac [2] tls.ClientHello 

388 
[THEN tls.ServerHello, 

13507  389 
THEN tls.ServerResume, THEN tls.ClientResume], possibility, blast+) 
11287  390 
done 
391 

392 

13922  393 
subsection{*Inductive proofs about tls*} 
11287  394 

395 

396 
(** Theorems of the form X \<notin> parts (spies evs) imply that NOBODY 

397 
sends messages containing X! **) 

398 

13922  399 
text{*Spy never sees a good agent's private key!*} 
11287  400 
lemma Spy_see_priK [simp]: 
13922  401 
"evs \<in> tls ==> (Key (privateKey b A) \<in> parts (spies evs)) = (A \<in> bad)" 
402 
by (erule tls.induct, force, simp_all, blast) 

11287  403 

404 
lemma Spy_analz_priK [simp]: 

13922  405 
"evs \<in> tls ==> (Key (privateKey b A) \<in> analz (spies evs)) = (A \<in> bad)" 
11287  406 
by auto 
407 

408 
lemma Spy_see_priK_D [dest!]: 

13922  409 
"[Key (privateKey b A) \<in> parts (knows Spy evs); evs \<in> tls] ==> A \<in> bad" 
11287  410 
by (blast dest: Spy_see_priK) 
411 

412 

13922  413 
text{*This lemma says that no false certificates exist. One might extend the 
11287  414 
model to include bogus certificates for the agents, but there seems 
415 
little point in doing so: the loss of their private keys is a worse 

13922  416 
breach of security.*} 
11287  417 
lemma certificate_valid: 
418 
"[ certificate B KB \<in> parts (spies evs); evs \<in> tls ] ==> KB = pubK B" 

419 
apply (erule rev_mp) 

13507  420 
apply (erule tls.induct, force, simp_all, blast) 
11287  421 
done 
422 

423 
lemmas CX_KB_is_pubKB = Says_imp_spies [THEN parts.Inj, THEN certificate_valid] 

424 

425 

13922  426 
subsubsection{*Properties of items found in Notes*} 
11287  427 

428 
lemma Notes_Crypt_parts_spies: 

429 
"[ Notes A {Agent B, X} \<in> set evs; evs \<in> tls ] 

430 
==> Crypt (pubK B) X \<in> parts (spies evs)" 

431 
apply (erule rev_mp) 

432 
apply (erule tls.induct, 

433 
frule_tac [7] CX_KB_is_pubKB, force, simp_all) 

434 
apply (blast intro: parts_insertI) 

435 
done 

436 

13922  437 
text{*C may be either A or B*} 
11287  438 
lemma Notes_master_imp_Crypt_PMS: 
439 
"[ Notes C {s, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))} \<in> set evs; 

440 
evs \<in> tls ] 

441 
==> Crypt (pubK B) (Nonce PMS) \<in> parts (spies evs)" 

442 
apply (erule rev_mp) 

443 
apply (erule tls.induct, force, simp_all) 

13922  444 
txt{*Fake*} 
11287  445 
apply (blast intro: parts_insertI) 
13922  446 
txt{*Client, Server Accept*} 
11287  447 
apply (blast dest!: Notes_Crypt_parts_spies)+ 
448 
done 

449 

13922  450 
text{*Compared with the theorem above, both premise and conclusion are stronger*} 
11287  451 
lemma Notes_master_imp_Notes_PMS: 
452 
"[ Notes A {s, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))} \<in> set evs; 

453 
evs \<in> tls ] 

454 
==> Notes A {Agent B, Nonce PMS} \<in> set evs" 

455 
apply (erule rev_mp) 

456 
apply (erule tls.induct, force, simp_all) 

13922  457 
txt{*ServerAccepts*} 
11287  458 
apply blast 
459 
done 

460 

461 

13922  462 
subsubsection{*Protocol goal: if B receives CertVerify, then A sent it*} 
11287  463 

13922  464 
text{*B can check A's signature if he has received A's certificate.*} 
11287  465 
lemma TrustCertVerify_lemma: 
466 
"[ X \<in> parts (spies evs); 

467 
X = Crypt (priK A) (Hash{nb, Agent B, pms}); 

468 
evs \<in> tls; A \<notin> bad ] 

469 
==> Says A B X \<in> set evs" 

470 
apply (erule rev_mp, erule ssubst) 

13507  471 
apply (erule tls.induct, force, simp_all, blast) 
11287  472 
done 
473 

13922  474 
text{*Final version: B checks X using the distributed KA instead of priK A*} 
11287  475 
lemma TrustCertVerify: 
476 
"[ X \<in> parts (spies evs); 

477 
X = Crypt (invKey KA) (Hash{nb, Agent B, pms}); 

478 
certificate A KA \<in> parts (spies evs); 

479 
evs \<in> tls; A \<notin> bad ] 

480 
==> Says A B X \<in> set evs" 

481 
by (blast dest!: certificate_valid intro!: TrustCertVerify_lemma) 

482 

483 

13922  484 
text{*If CertVerify is present then A has chosen PMS.*} 
11287  485 
lemma UseCertVerify_lemma: 
486 
"[ Crypt (priK A) (Hash{nb, Agent B, Nonce PMS}) \<in> parts (spies evs); 

487 
evs \<in> tls; A \<notin> bad ] 

488 
==> Notes A {Agent B, Nonce PMS} \<in> set evs" 

489 
apply (erule rev_mp) 

13507  490 
apply (erule tls.induct, force, simp_all, blast) 
11287  491 
done 
492 

13922  493 
text{*Final version using the distributed KA instead of priK A*} 
11287  494 
lemma UseCertVerify: 
495 
"[ Crypt (invKey KA) (Hash{nb, Agent B, Nonce PMS}) 

496 
\<in> parts (spies evs); 

497 
certificate A KA \<in> parts (spies evs); 

498 
evs \<in> tls; A \<notin> bad ] 

499 
==> Notes A {Agent B, Nonce PMS} \<in> set evs" 

500 
by (blast dest!: certificate_valid intro!: UseCertVerify_lemma) 

501 

502 

503 
lemma no_Notes_A_PRF [simp]: 

504 
"evs \<in> tls ==> Notes A {Agent B, Nonce (PRF x)} \<notin> set evs" 

505 
apply (erule tls.induct, force, simp_all) 

13922  506 
txt{*ClientKeyExch: PMS is assumed to differ from any PRF.*} 
11287  507 
apply blast 
508 
done 

509 

510 

511 
lemma MS_imp_PMS [dest!]: 

512 
"[ Nonce (PRF (PMS,NA,NB)) \<in> parts (spies evs); evs \<in> tls ] 

513 
==> Nonce PMS \<in> parts (spies evs)" 

514 
apply (erule rev_mp) 

515 
apply (erule tls.induct, force, simp_all) 

13922  516 
txt{*Fake*} 
11287  517 
apply (blast intro: parts_insertI) 
13922  518 
txt{*Easy, e.g. by freshness*} 
11287  519 
apply (blast dest: Notes_Crypt_parts_spies)+ 
520 
done 

521 

522 

523 

524 

13922  525 
subsubsection{*Unicity results for PMS, the premastersecret*} 
11287  526 

13922  527 
text{*PMS determines B.*} 
11287  528 
lemma Crypt_unique_PMS: 
529 
"[ Crypt(pubK B) (Nonce PMS) \<in> parts (spies evs); 

530 
Crypt(pubK B') (Nonce PMS) \<in> parts (spies evs); 

531 
Nonce PMS \<notin> analz (spies evs); 

532 
evs \<in> tls ] 

533 
==> B=B'" 

534 
apply (erule rev_mp, erule rev_mp, erule rev_mp) 

535 
apply (erule tls.induct, analz_mono_contra, force, simp_all (no_asm_simp)) 

13922  536 
txt{*Fake, ClientKeyExch*} 
11287  537 
apply blast+ 
538 
done 

539 

540 

541 
(** It is frustrating that we need two versions of the unicity results. 

542 
But Notes A {Agent B, Nonce PMS} determines both A and B. Sometimes 

543 
we have only the weaker assertion Crypt(pubK B) (Nonce PMS), which 

544 
determines B alone, and only if PMS is secret. 

545 
**) 

546 

13922  547 
text{*In A's internal Note, PMS determines A and B.*} 
11287  548 
lemma Notes_unique_PMS: 
549 
"[ Notes A {Agent B, Nonce PMS} \<in> set evs; 

550 
Notes A' {Agent B', Nonce PMS} \<in> set evs; 

551 
evs \<in> tls ] 

552 
==> A=A' & B=B'" 

553 
apply (erule rev_mp, erule rev_mp) 

554 
apply (erule tls.induct, force, simp_all) 

13922  555 
txt{*ClientKeyExch*} 
11287  556 
apply (blast dest!: Notes_Crypt_parts_spies) 
557 
done 

558 

559 

13922  560 
subsection{*Secrecy Theorems*} 
11287  561 

13956  562 
text{*Key compromise lemma needed to prove @{term analz_image_keys}. 
13922  563 
No collection of keys can help the spy get new private keys.*} 
11287  564 
lemma analz_image_priK [rule_format]: 
565 
"evs \<in> tls 

566 
==> \<forall>KK. (Key(priK B) \<in> analz (Key`KK Un (spies evs))) = 

567 
(priK B \<in> KK  B \<in> bad)" 

568 
apply (erule tls.induct) 

569 
apply (simp_all (no_asm_simp) 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

570 
del: image_insert 
11287  571 
add: image_Un [THEN sym] 
572 
insert_Key_image Un_assoc [THEN sym]) 

13922  573 
txt{*Fake*} 
11287  574 
apply spy_analz 
575 
done 

576 

577 

13922  578 
text{*slightly speeds up the big simplification below*} 
11287  579 
lemma range_sessionkeys_not_priK: 
580 
"KK <= range sessionK ==> priK B \<notin> KK" 

581 
by blast 

582 

583 

13922  584 
text{*Lemma for the trivial direction of the ifandonlyif*} 
11287  585 
lemma analz_image_keys_lemma: 
586 
"(X \<in> analz (G Un H)) > (X \<in> analz H) ==> 

587 
(X \<in> analz (G Un H)) = (X \<in> analz H)" 

588 
by (blast intro: analz_mono [THEN subsetD]) 

589 

590 
(** Strangely, the following version doesn't work: 

591 
\<forall>Z. (Nonce N \<in> analz (Key`(sessionK`Z) Un (spies evs))) = 

592 
(Nonce N \<in> analz (spies evs))" 

593 
**) 

594 

595 
lemma analz_image_keys [rule_format]: 

596 
"evs \<in> tls ==> 

597 
\<forall>KK. KK <= range sessionK > 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

598 
(Nonce N \<in> analz (Key`KK Un (spies evs))) = 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

599 
(Nonce N \<in> analz (spies evs))" 
11287  600 
apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB) 
601 
apply (safe del: iffI) 

602 
apply (safe del: impI iffI intro!: analz_image_keys_lemma) 

603 
apply (simp_all (no_asm_simp) (*faster*) 

604 
del: image_insert imp_disjL (*reduces blowup*) 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

605 
add: image_Un [THEN sym] Un_assoc [THEN sym] 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

606 
insert_Key_singleton 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

607 
range_sessionkeys_not_priK analz_image_priK) 
11287  608 
apply (simp_all add: insert_absorb) 
13922  609 
txt{*Fake*} 
11287  610 
apply spy_analz 
611 
done 

612 

13922  613 
text{*Knowing some session keys is no help in getting new nonces*} 
11287  614 
lemma analz_insert_key [simp]: 
615 
"evs \<in> tls ==> 

11655  616 
(Nonce N \<in> analz (insert (Key (sessionK z)) (spies evs))) = 
11287  617 
(Nonce N \<in> analz (spies evs))" 
618 
by (simp del: image_insert 

619 
add: insert_Key_singleton analz_image_keys) 

620 

621 

13922  622 
subsubsection{*Protocol goal: serverK(Na,Nb,M) and clientK(Na,Nb,M) remain secure*} 
11287  623 

624 
(** Some lemmas about session keys, comprising clientK and serverK **) 

625 

626 

13922  627 
text{*Lemma: session keys are never used if PMS is fresh. 
11287  628 
Nonces don't have to agree, allowing session resumption. 
629 
Converse doesn't hold; revealing PMS doesn't force the keys to be sent. 

13922  630 
THEY ARE NOT SUITABLE AS SAFE ELIM RULES.*} 
11287  631 
lemma PMS_lemma: 
632 
"[ Nonce PMS \<notin> parts (spies evs); 

633 
K = sessionK((Na, Nb, PRF(PMS,NA,NB)), role); 

634 
evs \<in> tls ] 

635 
==> Key K \<notin> parts (spies evs) & (\<forall>Y. Crypt K Y \<notin> parts (spies evs))" 

636 
apply (erule rev_mp, erule ssubst) 

13922  637 
apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB) 
11287  638 
apply (force, simp_all (no_asm_simp)) 
13922  639 
txt{*Fake*} 
11287  640 
apply (blast intro: parts_insertI) 
13922  641 
txt{*SpyKeys*} 
11287  642 
apply blast 
13922  643 
txt{*Many others*} 
11287  644 
apply (force dest!: Notes_Crypt_parts_spies Notes_master_imp_Crypt_PMS)+ 
645 
done 

646 

647 
lemma PMS_sessionK_not_spied: 

648 
"[ Key (sessionK((Na, Nb, PRF(PMS,NA,NB)), role)) \<in> parts (spies evs); 

649 
evs \<in> tls ] 

650 
==> Nonce PMS \<in> parts (spies evs)" 

651 
by (blast dest: PMS_lemma) 

652 

653 
lemma PMS_Crypt_sessionK_not_spied: 

654 
"[ Crypt (sessionK((Na, Nb, PRF(PMS,NA,NB)), role)) Y 

655 
\<in> parts (spies evs); evs \<in> tls ] 

656 
==> Nonce PMS \<in> parts (spies evs)" 

657 
by (blast dest: PMS_lemma) 

658 

13922  659 
text{*Write keys are never sent if M (MASTER SECRET) is secure. 
11287  660 
Converse fails; betraying M doesn't force the keys to be sent! 
661 
The strong Oops condition can be weakened later by unicity reasoning, 

662 
with some effort. 

13956  663 
NO LONGER USED: see @{text clientK_not_spied} and @{text serverK_not_spied}*} 
11287  664 
lemma sessionK_not_spied: 
665 
"[ \<forall>A. Says A Spy (Key (sessionK((NA,NB,M),role))) \<notin> set evs; 

666 
Nonce M \<notin> analz (spies evs); evs \<in> tls ] 

667 
==> Key (sessionK((NA,NB,M),role)) \<notin> parts (spies evs)" 

668 
apply (erule rev_mp, erule rev_mp) 

669 
apply (erule tls.induct, analz_mono_contra) 

670 
apply (force, simp_all (no_asm_simp)) 

13922  671 
txt{*Fake, SpyKeys*} 
11287  672 
apply blast+ 
673 
done 

674 

675 

13922  676 
text{*If A sends ClientKeyExch to an honest B, then the PMS will stay secret.*} 
11287  677 
lemma Spy_not_see_PMS: 
678 
"[ Notes A {Agent B, Nonce PMS} \<in> set evs; 

679 
evs \<in> tls; A \<notin> bad; B \<notin> bad ] 

680 
==> Nonce PMS \<notin> analz (spies evs)" 

681 
apply (erule rev_mp, erule tls.induct, frule_tac [7] CX_KB_is_pubKB) 

682 
apply (force, simp_all (no_asm_simp)) 

13922  683 
txt{*Fake*} 
11287  684 
apply spy_analz 
13922  685 
txt{*SpyKeys*} 
11287  686 
apply force 
687 
apply (simp_all add: insert_absorb) 

13922  688 
txt{*ClientHello, ServerHello, ClientKeyExch: mostly freshness reasoning*} 
11287  689 
apply (blast dest: Notes_Crypt_parts_spies) 
690 
apply (blast dest: Notes_Crypt_parts_spies) 

691 
apply (blast dest: Notes_Crypt_parts_spies) 

13956  692 
txt{*ClientAccepts and ServerAccepts: because @{term "PMS \<notin> range PRF"}*} 
11287  693 
apply force+ 
694 
done 

695 

696 

13922  697 
text{*If A sends ClientKeyExch to an honest B, then the MASTER SECRET 
698 
will stay secret.*} 

11287  699 
lemma Spy_not_see_MS: 
700 
"[ Notes A {Agent B, Nonce PMS} \<in> set evs; 

701 
evs \<in> tls; A \<notin> bad; B \<notin> bad ] 

702 
==> Nonce (PRF(PMS,NA,NB)) \<notin> analz (spies evs)" 

703 
apply (erule rev_mp, erule tls.induct, frule_tac [7] CX_KB_is_pubKB) 

704 
apply (force, simp_all (no_asm_simp)) 

13922  705 
txt{*Fake*} 
11287  706 
apply spy_analz 
13922  707 
txt{*SpyKeys: by secrecy of the PMS, Spy cannot make the MS*} 
11287  708 
apply (blast dest!: Spy_not_see_PMS) 
709 
apply (simp_all add: insert_absorb) 

13922  710 
txt{*ClientAccepts and ServerAccepts: because PMS was already visible; 
711 
others, freshness etc.*} 

11287  712 
apply (blast dest: Notes_Crypt_parts_spies Spy_not_see_PMS 
713 
Notes_imp_knows_Spy [THEN analz.Inj])+ 

714 
done 

715 

716 

717 

13922  718 
subsubsection{*Weakening the Oops conditions for leakage of clientK*} 
11287  719 

13922  720 
text{*If A created PMS then nobody else (except the Spy in replays) 
721 
would send a message using a clientK generated from that PMS.*} 

11287  722 
lemma Says_clientK_unique: 
723 
"[ Says A' B' (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) \<in> set evs; 

724 
Notes A {Agent B, Nonce PMS} \<in> set evs; 

725 
evs \<in> tls; A' \<noteq> Spy ] 

726 
==> A = A'" 

727 
apply (erule rev_mp, erule rev_mp) 

728 
apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB) 

729 
apply (force, simp_all) 

13922  730 
txt{*ClientKeyExch*} 
11287  731 
apply (blast dest!: PMS_Crypt_sessionK_not_spied) 
13922  732 
txt{*ClientFinished, ClientResume: by unicity of PMS*} 
11287  733 
apply (blast dest!: Notes_master_imp_Notes_PMS 
734 
intro: Notes_unique_PMS [THEN conjunct1])+ 

735 
done 

736 

737 

13922  738 
text{*If A created PMS and has not leaked her clientK to the Spy, 
739 
then it is completely secure: not even in parts!*} 

11287  740 
lemma clientK_not_spied: 
741 
"[ Notes A {Agent B, Nonce PMS} \<in> set evs; 

742 
Says A Spy (Key (clientK(Na,Nb,PRF(PMS,NA,NB)))) \<notin> set evs; 

743 
A \<notin> bad; B \<notin> bad; 

744 
evs \<in> tls ] 

745 
==> Key (clientK(Na,Nb,PRF(PMS,NA,NB))) \<notin> parts (spies evs)" 

746 
apply (erule rev_mp, erule rev_mp) 

747 
apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB) 

748 
apply (force, simp_all (no_asm_simp)) 

13922  749 
txt{*ClientKeyExch*} 
11287  750 
apply blast 
13922  751 
txt{*SpyKeys*} 
11287  752 
apply (blast dest!: Spy_not_see_MS) 
13922  753 
txt{*ClientKeyExch*} 
11287  754 
apply (blast dest!: PMS_sessionK_not_spied) 
13922  755 
txt{*Oops*} 
11287  756 
apply (blast intro: Says_clientK_unique) 
757 
done 

758 

759 

13922  760 
subsubsection{*Weakening the Oops conditions for leakage of serverK*} 
11287  761 

13922  762 
text{*If A created PMS for B, then nobody other than B or the Spy would 
763 
send a message using a serverK generated from that PMS.*} 

11287  764 
lemma Says_serverK_unique: 
765 
"[ Says B' A' (Crypt (serverK(Na,Nb,PRF(PMS,NA,NB))) Y) \<in> set evs; 

766 
Notes A {Agent B, Nonce PMS} \<in> set evs; 

767 
evs \<in> tls; A \<notin> bad; B \<notin> bad; B' \<noteq> Spy ] 

768 
==> B = B'" 

769 
apply (erule rev_mp, erule rev_mp) 

770 
apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB) 

771 
apply (force, simp_all) 

13922  772 
txt{*ClientKeyExch*} 
11287  773 
apply (blast dest!: PMS_Crypt_sessionK_not_spied) 
13922  774 
txt{*ServerResume, ServerFinished: by unicity of PMS*} 
11287  775 
apply (blast dest!: Notes_master_imp_Crypt_PMS 
776 
dest: Spy_not_see_PMS Notes_Crypt_parts_spies Crypt_unique_PMS)+ 

777 
done 

778 

779 

13922  780 
text{*If A created PMS for B, and B has not leaked his serverK to the Spy, 
781 
then it is completely secure: not even in parts!*} 

11287  782 
lemma serverK_not_spied: 
783 
"[ Notes A {Agent B, Nonce PMS} \<in> set evs; 

784 
Says B Spy (Key(serverK(Na,Nb,PRF(PMS,NA,NB)))) \<notin> set evs; 

785 
A \<notin> bad; B \<notin> bad; evs \<in> tls ] 

786 
==> Key (serverK(Na,Nb,PRF(PMS,NA,NB))) \<notin> parts (spies evs)" 

787 
apply (erule rev_mp, erule rev_mp) 

788 
apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB) 

789 
apply (force, simp_all (no_asm_simp)) 

13922  790 
txt{*Fake*} 
11287  791 
apply blast 
13922  792 
txt{*SpyKeys*} 
11287  793 
apply (blast dest!: Spy_not_see_MS) 
13922  794 
txt{*ClientKeyExch*} 
11287  795 
apply (blast dest!: PMS_sessionK_not_spied) 
13922  796 
txt{*Oops*} 
11287  797 
apply (blast intro: Says_serverK_unique) 
798 
done 

799 

800 

13922  801 
subsubsection{*Protocol goals: if A receives ServerFinished, then B is present 
11287  802 
and has used the quoted values PA, PB, etc. Note that it is up to A 
13956  803 
to compare PA with what she originally sent.*} 
11287  804 

13922  805 
text{*The mention of her name (A) in X assures A that B knows who she is.*} 
11287  806 
lemma TrustServerFinished [rule_format]: 
807 
"[ X = Crypt (serverK(Na,Nb,M)) 

808 
(Hash{Number SID, Nonce M, 

809 
Nonce Na, Number PA, Agent A, 

810 
Nonce Nb, Number PB, Agent B}); 

811 
M = PRF(PMS,NA,NB); 

812 
evs \<in> tls; A \<notin> bad; B \<notin> bad ] 

813 
==> Says B Spy (Key(serverK(Na,Nb,M))) \<notin> set evs > 

814 
Notes A {Agent B, Nonce PMS} \<in> set evs > 

815 
X \<in> parts (spies evs) > Says B A X \<in> set evs" 

816 
apply (erule ssubst)+ 

817 
apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB) 

818 
apply (force, simp_all (no_asm_simp)) 

13922  819 
txt{*Fake: the Spy doesn't have the critical session key!*} 
11287  820 
apply (blast dest: serverK_not_spied) 
13922  821 
txt{*ClientKeyExch*} 
11287  822 
apply (blast dest!: PMS_Crypt_sessionK_not_spied) 
823 
done 

824 

13922  825 
text{*This version refers not to ServerFinished but to any message from B. 
11287  826 
We don't assume B has received CertVerify, and an intruder could 
827 
have changed A's identity in all other messages, so we can't be sure 

828 
that B sends his message to A. If CLIENT KEY EXCHANGE were augmented 

13922  829 
to bind A's identity with PMS, then we could replace A' by A below.*} 
11287  830 
lemma TrustServerMsg [rule_format]: 
831 
"[ M = PRF(PMS,NA,NB); evs \<in> tls; A \<notin> bad; B \<notin> bad ] 

832 
==> Says B Spy (Key(serverK(Na,Nb,M))) \<notin> set evs > 

833 
Notes A {Agent B, Nonce PMS} \<in> set evs > 

834 
Crypt (serverK(Na,Nb,M)) Y \<in> parts (spies evs) > 

835 
(\<exists>A'. Says B A' (Crypt (serverK(Na,Nb,M)) Y) \<in> set evs)" 

836 
apply (erule ssubst) 

837 
apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB) 

838 
apply (force, simp_all (no_asm_simp) add: ex_disj_distrib) 

13922  839 
txt{*Fake: the Spy doesn't have the critical session key!*} 
11287  840 
apply (blast dest: serverK_not_spied) 
13922  841 
txt{*ClientKeyExch*} 
11287  842 
apply (clarify, blast dest!: PMS_Crypt_sessionK_not_spied) 
13922  843 
txt{*ServerResume, ServerFinished: by unicity of PMS*} 
11287  844 
apply (blast dest!: Notes_master_imp_Crypt_PMS 
845 
dest: Spy_not_see_PMS Notes_Crypt_parts_spies Crypt_unique_PMS)+ 

846 
done 

847 

848 

13922  849 
subsubsection{*Protocol goal: if B receives any message encrypted with clientK 
850 
then A has sent it*} 

851 

852 
text{*ASSUMING that A chose PMS. Authentication is 

11287  853 
assumed here; B cannot verify it. But if the message is 
13922  854 
ClientFinished, then B can then check the quoted values PA, PB, etc.*} 
11287  855 

856 
lemma TrustClientMsg [rule_format]: 

857 
"[ M = PRF(PMS,NA,NB); evs \<in> tls; A \<notin> bad; B \<notin> bad ] 

858 
==> Says A Spy (Key(clientK(Na,Nb,M))) \<notin> set evs > 

859 
Notes A {Agent B, Nonce PMS} \<in> set evs > 

860 
Crypt (clientK(Na,Nb,M)) Y \<in> parts (spies evs) > 

861 
Says A B (Crypt (clientK(Na,Nb,M)) Y) \<in> set evs" 

862 
apply (erule ssubst) 

863 
apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB) 

864 
apply (force, simp_all (no_asm_simp)) 

13922  865 
txt{*Fake: the Spy doesn't have the critical session key!*} 
11287  866 
apply (blast dest: clientK_not_spied) 
13922  867 
txt{*ClientKeyExch*} 
11287  868 
apply (blast dest!: PMS_Crypt_sessionK_not_spied) 
13922  869 
txt{*ClientFinished, ClientResume: by unicity of PMS*} 
11287  870 
apply (blast dest!: Notes_master_imp_Notes_PMS dest: Notes_unique_PMS)+ 
871 
done 

872 

873 

13922  874 
subsubsection{*Protocol goal: if B receives ClientFinished, and if B is able to 
11287  875 
check a CertVerify from A, then A has used the quoted 
13956  876 
values PA, PB, etc. Even this one requires A to be uncompromised.*} 
11287  877 
lemma AuthClientFinished: 
878 
"[ M = PRF(PMS,NA,NB); 

879 
Says A Spy (Key(clientK(Na,Nb,M))) \<notin> set evs; 

880 
Says A' B (Crypt (clientK(Na,Nb,M)) Y) \<in> set evs; 

881 
certificate A KA \<in> parts (spies evs); 

882 
Says A'' B (Crypt (invKey KA) (Hash{nb, Agent B, Nonce PMS})) 

883 
\<in> set evs; 

884 
evs \<in> tls; A \<notin> bad; B \<notin> bad ] 

885 
==> Says A B (Crypt (clientK(Na,Nb,M)) Y) \<in> set evs" 

886 
by (blast intro!: TrustClientMsg UseCertVerify) 

887 

888 
(*22/9/97: loads in 622s, which is 10 minutes 22 seconds*) 

889 
(*24/9/97: loads in 672s, which is 11 minutes 12 seconds [stronger theorems]*) 

890 
(*29/9/97: loads in 481s, after removing Certificate from ClientKeyExch*) 

891 
(*30/9/97: loads in 476s, after removing unused theorems*) 

892 
(*30/9/97: loads in 448s, after fixing ServerResume*) 

893 

894 
(*08/9/97: loads in 189s (pike), after much reorganization, 

895 
back to 621s on albatross?*) 

896 

897 
(*10/2/99: loads in 139s (pike) 

898 
down to 433s on albatross*) 

899 

900 
(*5/5/01: conversion to Isar script 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

901 
loads in 137s (perch) 
11287  902 
the last ML version loaded in 122s on perch, a 600MHz machine: 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

903 
twice as fast as pike. No idea why it's so much slower! 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

904 
The Isar script is slower still, perhaps because simp_all simplifies 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
29888
diff
changeset

905 
the assumptions be default. 
11287  906 
*) 
3474  907 

908 
end 