author | paulson |
Thu, 29 Mar 2001 10:44:37 +0200 | |
changeset 11230 | 756c5034f08b |
parent 11185 | 1b737b4c2108 |
permissions | -rw-r--r-- |
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 |
||
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
6 |
Protocol goals: |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
7 |
* M, serverK(NA,NB,M) and clientK(NA,NB,M) will be known only to the two |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
8 |
parties (though A is not necessarily authenticated). |
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
9 |
|
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
10 |
* B upon receiving CertVerify knows that A is present (But this |
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
11 |
message is optional!) |
3474 | 12 |
|
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
13 |
* A upon receiving ServerFinished knows that B is present |
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
14 |
|
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
15 |
* Each party who has received a FINISHED message can trust that the other |
3729
6be7cf5086ab
Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents:
3711
diff
changeset
|
16 |
party agrees on all message components, including PA and PB (thus foiling |
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
17 |
rollback attacks). |
3474 | 18 |
*) |
19 |
||
11150 | 20 |
AddDs [Says_imp_knows_Spy RS parts.Inj, parts.Body]; |
21 |
AddDs [impOfSubs analz_subset_parts, impOfSubs Fake_parts_insert]; |
|
5433 | 22 |
|
3772 | 23 |
(*Automatically unfold the definition of "certificate"*) |
24 |
Addsimps [certificate_def]; |
|
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
25 |
|
3474 | 26 |
(*Injectiveness of key-generating functions*) |
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset
|
27 |
AddIffs [inj_PRF RS inj_eq, inj_sessionK RS inj_eq]; |
3474 | 28 |
|
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset
|
29 |
(* invKey(sessionK x) = sessionK x*) |
11230
756c5034f08b
misc tidying; changing the predicate isSymKey to the set symKeys
paulson
parents:
11185
diff
changeset
|
30 |
Addsimps [isSym_sessionK, rewrite_rule [symKeys_def] isSym_sessionK]; |
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
31 |
|
3474 | 32 |
|
33 |
(*** clientK and serverK make symmetric keys; no clashes with pubK or priK ***) |
|
34 |
||
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
35 |
Goal "pubK A \\<noteq> sessionK arg"; |
11230
756c5034f08b
misc tidying; changing the predicate isSymKey to the set symKeys
paulson
parents:
11185
diff
changeset
|
36 |
by (simp_tac (simpset() addsimps [symKeys_neq_imp_neq]) 1); |
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset
|
37 |
qed "pubK_neq_sessionK"; |
3474 | 38 |
|
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
39 |
Goal "priK A \\<noteq> sessionK arg"; |
11230
756c5034f08b
misc tidying; changing the predicate isSymKey to the set symKeys
paulson
parents:
11185
diff
changeset
|
40 |
by (simp_tac (simpset() addsimps [symKeys_neq_imp_neq]) 1); |
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset
|
41 |
qed "priK_neq_sessionK"; |
3474 | 42 |
|
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset
|
43 |
val keys_distinct = [pubK_neq_sessionK, priK_neq_sessionK]; |
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
44 |
AddIffs (keys_distinct @ (keys_distinct RL [not_sym])); |
3474 | 45 |
|
46 |
||
47 |
(**** Protocol Proofs ****) |
|
48 |
||
3772 | 49 |
(*Possibility properties state that some traces run the protocol to the end. |
50 |
Four paths and 12 rules are considered.*) |
|
3474 | 51 |
|
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
52 |
|
3772 | 53 |
(** These proofs assume that the Nonce_supply nonces |
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
54 |
(which have the form @ N. Nonce N \\<notin> used evs) |
3772 | 55 |
lie outside the range of PRF. It seems reasonable, but as it is needed |
56 |
only for the possibility theorems, it is not taken as an axiom. |
|
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
57 |
**) |
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
58 |
|
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
59 |
|
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
60 |
(*Possibility property ending with ClientAccepts.*) |
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
61 |
Goal "[| \\<forall>evs. (@ N. Nonce N \\<notin> used evs) \\<notin> range PRF; \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
62 |
\ A \\<noteq> B |] \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
63 |
\ ==> \\<exists>SID M. \\<exists>evs \\<in> tls. \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
64 |
\ Notes A {|Number SID, Agent A, Agent B, Nonce M|} \\<in> set evs"; |
3474 | 65 |
by (REPEAT (resolve_tac [exI,bexI] 1)); |
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
66 |
by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.Certificate RS |
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
67 |
tls.ClientKeyExch RS tls.ClientFinished RS tls.ServerFinished RS |
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
68 |
tls.ClientAccepts) 2); |
3474 | 69 |
by possibility_tac; |
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
70 |
by (REPEAT (Blast_tac 1)); |
3474 | 71 |
result(); |
72 |
||
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
73 |
(*And one for ServerAccepts. Either FINISHED message may come first.*) |
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
74 |
Goal "[| \\<forall>evs. (@ N. Nonce N \\<notin> used evs) \\<notin> range PRF; \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
75 |
\ A \\<noteq> B |] \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
76 |
\ ==> \\<exists>SID NA PA NB PB M. \\<exists>evs \\<in> tls. \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
77 |
\ Notes B {|Number SID, Agent A, Agent B, Nonce M|} \\<in> set evs"; |
3474 | 78 |
by (REPEAT (resolve_tac [exI,bexI] 1)); |
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
79 |
by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.Certificate RS |
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
80 |
tls.ClientKeyExch RS tls.ServerFinished RS tls.ClientFinished RS |
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
81 |
tls.ServerAccepts) 2); |
3474 | 82 |
by possibility_tac; |
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
83 |
by (REPEAT (Blast_tac 1)); |
3474 | 84 |
result(); |
85 |
||
86 |
(*Another one, for CertVerify (which is optional)*) |
|
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
87 |
Goal "[| \\<forall>evs. (@ N. Nonce N \\<notin> used evs) \\<notin> range PRF; \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
88 |
\ A \\<noteq> B |] \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
89 |
\ ==> \\<exists>NB PMS. \\<exists>evs \\<in> tls. \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
90 |
\ Says A B (Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|})) \\<in> set evs"; |
3474 | 91 |
by (REPEAT (resolve_tac [exI,bexI] 1)); |
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
92 |
by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.Certificate RS |
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
93 |
tls.ClientKeyExch RS tls.CertVerify) 2); |
3474 | 94 |
by possibility_tac; |
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
95 |
by (REPEAT (Blast_tac 1)); |
3474 | 96 |
result(); |
97 |
||
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
98 |
(*Another one, for session resumption (both ServerResume and ClientResume) *) |
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
99 |
Goal "[| evs0 \\<in> tls; \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
100 |
\ Notes A {|Number SID, Agent A, Agent B, Nonce M|} \\<in> set evs0; \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
101 |
\ Notes B {|Number SID, Agent A, Agent B, Nonce M|} \\<in> set evs0; \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
102 |
\ \\<forall>evs. (@ N. Nonce N \\<notin> used evs) \\<notin> range PRF; \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
103 |
\ A \\<noteq> B |] \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
104 |
\ ==> \\<exists>NA PA NB PB X. \\<exists>evs \\<in> tls. \ |
5433 | 105 |
\ X = Hash{|Number SID, Nonce M, \ |
106 |
\ Nonce NA, Number PA, Agent A, \ |
|
107 |
\ Nonce NB, Number PB, Agent B|} & \ |
|
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
108 |
\ Says A B (Crypt (clientK(NA,NB,M)) X) \\<in> set evs & \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
109 |
\ Says B A (Crypt (serverK(NA,NB,M)) X) \\<in> set evs"; |
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
110 |
by (REPEAT (resolve_tac [exI,bexI] 1)); |
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
111 |
by (etac (tls.ClientHello RS tls.ServerHello RS tls.ServerResume RS |
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
112 |
tls.ClientResume) 2); |
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
113 |
by possibility_tac; |
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
114 |
by (REPEAT (Blast_tac 1)); |
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
115 |
result(); |
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
116 |
|
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
117 |
|
3474 | 118 |
|
119 |
(**** Inductive proofs about tls ****) |
|
120 |
||
121 |
||
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset
|
122 |
(*Induction for regularity theorems. If induction formula has the form |
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
123 |
X \\<notin> analz (spies evs) --> ... then it shortens the proof by discarding |
3683 | 124 |
needless information about analz (insert X (spies evs)) *) |
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset
|
125 |
fun parts_induct_tac i = |
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset
|
126 |
etac tls.induct i |
11150 | 127 |
THEN REPEAT (FIRSTGOAL analz_mono_contra_tac) |
128 |
THEN Force_tac i THEN |
|
4686 | 129 |
ALLGOALS Asm_simp_tac; |
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset
|
130 |
|
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset
|
131 |
|
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
132 |
(** Theorems of the form X \\<notin> parts (spies evs) imply that NOBODY |
3474 | 133 |
sends messages containing X! **) |
134 |
||
3683 | 135 |
(*Spy never sees another agent's private key! (unless it's bad at start)*) |
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
136 |
Goal "evs \\<in> tls ==> (Key (priK A) \\<in> parts (spies evs)) = (A \\<in> bad)"; |
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset
|
137 |
by (parts_induct_tac 1); |
5433 | 138 |
by (Blast_tac 1); |
3474 | 139 |
qed "Spy_see_priK"; |
140 |
Addsimps [Spy_see_priK]; |
|
141 |
||
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
142 |
Goal "evs \\<in> tls ==> (Key (priK A) \\<in> analz (spies evs)) = (A \\<in> bad)"; |
5433 | 143 |
by Auto_tac; |
3474 | 144 |
qed "Spy_analz_priK"; |
145 |
Addsimps [Spy_analz_priK]; |
|
146 |
||
4472 | 147 |
AddSDs [Spy_see_priK RSN (2, rev_iffD1), |
148 |
Spy_analz_priK RSN (2, rev_iffD1)]; |
|
3474 | 149 |
|
150 |
||
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
151 |
(*This lemma says that no false certificates exist. One might extend the |
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset
|
152 |
model to include bogus certificates for the agents, but there seems |
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
153 |
little point in doing so: the loss of their private keys is a worse |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
154 |
breach of security.*) |
5076 | 155 |
Goalw [certificate_def] |
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
156 |
"[| certificate B KB \\<in> parts (spies evs); evs \\<in> tls |] ==> pubK B = KB"; |
3772 | 157 |
by (etac rev_mp 1); |
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset
|
158 |
by (parts_induct_tac 1); |
5433 | 159 |
by (Blast_tac 1); |
3772 | 160 |
qed "certificate_valid"; |
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
161 |
|
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
162 |
|
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
163 |
(*Replace key KB in ClientKeyExch by (pubK B) *) |
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
164 |
val ClientKeyExch_tac = |
3772 | 165 |
forward_tac [Says_imp_spies RS parts.Inj RS certificate_valid] |
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
166 |
THEN' assume_tac |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
167 |
THEN' hyp_subst_tac; |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
168 |
|
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
169 |
fun analz_induct_tac i = |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
170 |
etac tls.induct i THEN |
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
171 |
ClientKeyExch_tac (i+6) THEN (*ClientKeyExch*) |
6915 | 172 |
ALLGOALS (asm_simp_tac (simpset() addsimps split_ifs @ pushes)) THEN |
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
173 |
(*Remove instances of pubK B: the Spy already knows all public keys. |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
174 |
Combining the two simplifier calls makes them run extremely slowly.*) |
8054
2ce57ef2a4aa
used image_eq_UN to speed up slow proofs of base cases
paulson
parents:
7057
diff
changeset
|
175 |
ALLGOALS (asm_simp_tac (simpset() addsimps [image_eq_UN, insert_absorb])); |
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
176 |
|
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
177 |
|
3758
188a4fbfaf55
Exchanged the M and SID fields of the FINISHED messages to simplify proofs;
paulson
parents:
3745
diff
changeset
|
178 |
(*** Properties of items found in Notes ***) |
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
179 |
|
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
180 |
Goal "[| Notes A {|Agent B, X|} \\<in> set evs; evs \\<in> tls |] \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
181 |
\ ==> Crypt (pubK B) X \\<in> parts (spies evs)"; |
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
182 |
by (etac rev_mp 1); |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
183 |
by (analz_induct_tac 1); |
4091 | 184 |
by (blast_tac (claset() addIs [parts_insertI]) 1); |
3683 | 185 |
qed "Notes_Crypt_parts_spies"; |
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
186 |
|
3758
188a4fbfaf55
Exchanged the M and SID fields of the FINISHED messages to simplify proofs;
paulson
parents:
3745
diff
changeset
|
187 |
(*C may be either A or B*) |
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
188 |
Goal "[| Notes C {|s, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))|} \\<in> set evs; \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
189 |
\ evs \\<in> tls |] \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
190 |
\ ==> Crypt (pubK B) (Nonce PMS) \\<in> parts (spies evs)"; |
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
191 |
by (etac rev_mp 1); |
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
192 |
by (parts_induct_tac 1); |
3711 | 193 |
by (ALLGOALS Clarify_tac); |
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
194 |
(*Fake*) |
4091 | 195 |
by (blast_tac (claset() addIs [parts_insertI]) 1); |
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
196 |
(*Client, Server Accept*) |
5433 | 197 |
by (REPEAT (blast_tac (claset() addSDs [Notes_Crypt_parts_spies]) 1)); |
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
198 |
qed "Notes_master_imp_Crypt_PMS"; |
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
199 |
|
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
200 |
(*Compared with the theorem above, both premise and conclusion are stronger*) |
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
201 |
Goal "[| Notes A {|s, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))|} \\<in> set evs;\ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
202 |
\ evs \\<in> tls |] \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
203 |
\ ==> Notes A {|Agent B, Nonce PMS|} \\<in> set evs"; |
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
204 |
by (etac rev_mp 1); |
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
205 |
by (parts_induct_tac 1); |
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
206 |
(*ServerAccepts*) |
6284
147db42c1009
tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents:
5653
diff
changeset
|
207 |
by (Fast_tac 1); |
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
208 |
qed "Notes_master_imp_Notes_PMS"; |
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
209 |
|
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
210 |
|
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
211 |
(*** Protocol goal: if B receives CertVerify, then A sent it ***) |
3474 | 212 |
|
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
213 |
(*B can check A's signature if he has received A's certificate.*) |
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
214 |
Goal "[| X \\<in> parts (spies evs); \ |
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
215 |
\ X = Crypt (priK A) (Hash{|nb, Agent B, pms|}); \ |
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
216 |
\ evs \\<in> tls; A \\<notin> bad |] \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
217 |
\ ==> Says A B X \\<in> set evs"; |
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
218 |
by (etac rev_mp 1); |
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
219 |
by (hyp_subst_tac 1); |
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset
|
220 |
by (parts_induct_tac 1); |
5433 | 221 |
by (Blast_tac 1); |
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
222 |
val lemma = result(); |
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
223 |
|
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
224 |
(*Final version: B checks X using the distributed KA instead of priK A*) |
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
225 |
Goal "[| X \\<in> parts (spies evs); \ |
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
226 |
\ X = Crypt (invKey KA) (Hash{|nb, Agent B, pms|}); \ |
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
227 |
\ certificate A KA \\<in> parts (spies evs); \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
228 |
\ evs \\<in> tls; A \\<notin> bad |] \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
229 |
\ ==> Says A B X \\<in> set evs"; |
4091 | 230 |
by (blast_tac (claset() addSDs [certificate_valid] addSIs [lemma]) 1); |
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
231 |
qed "TrustCertVerify"; |
3474 | 232 |
|
233 |
||
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
234 |
(*If CertVerify is present then A has chosen PMS.*) |
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
235 |
Goal "[| Crypt (priK A) (Hash{|nb, Agent B, Nonce PMS|}) \ |
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
236 |
\ \\<in> parts (spies evs); \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
237 |
\ evs \\<in> tls; A \\<notin> bad |] \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
238 |
\ ==> Notes A {|Agent B, Nonce PMS|} \\<in> set evs"; |
4423 | 239 |
by (etac rev_mp 1); |
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset
|
240 |
by (parts_induct_tac 1); |
5433 | 241 |
by (Blast_tac 1); |
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
242 |
val lemma = result(); |
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
243 |
|
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
244 |
(*Final version using the distributed KA instead of priK A*) |
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
245 |
Goal "[| Crypt (invKey KA) (Hash{|nb, Agent B, Nonce PMS|}) \ |
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
246 |
\ \\<in> parts (spies evs); \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
247 |
\ certificate A KA \\<in> parts (spies evs); \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
248 |
\ evs \\<in> tls; A \\<notin> bad |] \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
249 |
\ ==> Notes A {|Agent B, Nonce PMS|} \\<in> set evs"; |
4091 | 250 |
by (blast_tac (claset() addSDs [certificate_valid] addSIs [lemma]) 1); |
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
251 |
qed "UseCertVerify"; |
3474 | 252 |
|
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
253 |
|
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
254 |
Goal "evs \\<in> tls ==> Notes A {|Agent B, Nonce (PRF x)|} \\<notin> set evs"; |
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
255 |
by (parts_induct_tac 1); |
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
256 |
(*ClientKeyExch: PMS is assumed to differ from any PRF.*) |
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
257 |
by (Blast_tac 1); |
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
258 |
qed "no_Notes_A_PRF"; |
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
259 |
Addsimps [no_Notes_A_PRF]; |
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
260 |
|
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
261 |
|
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
262 |
Goal "[| Nonce (PRF (PMS,NA,NB)) \\<in> parts (spies evs); evs \\<in> tls |] \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
263 |
\ ==> Nonce PMS \\<in> parts (spies evs)"; |
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
264 |
by (etac rev_mp 1); |
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
265 |
by (parts_induct_tac 1); |
5433 | 266 |
(*Easy, e.g. by freshness*) |
267 |
by (REPEAT (blast_tac (claset() addDs [Notes_Crypt_parts_spies]) 2)); |
|
268 |
(*Fake*) |
|
269 |
by (blast_tac (claset() addIs [parts_insertI]) 1); |
|
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
270 |
qed "MS_imp_PMS"; |
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
271 |
AddSDs [MS_imp_PMS]; |
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
272 |
|
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
273 |
|
3474 | 274 |
|
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
275 |
(*** Unicity results for PMS, the pre-master-secret ***) |
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
276 |
|
11104 | 277 |
(*PMS determines B.*) |
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
278 |
Goal "[| Crypt(pubK B) (Nonce PMS) \\<in> parts (spies evs); \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
279 |
\ Crypt(pubK B') (Nonce PMS) \\<in> parts (spies evs); \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
280 |
\ Nonce PMS \\<notin> analz (spies evs); \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
281 |
\ evs \\<in> tls |] \ |
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
282 |
\ ==> B=B'"; |
11104 | 283 |
by (etac rev_mp 1); |
284 |
by (etac rev_mp 1); |
|
285 |
by (etac rev_mp 1); |
|
286 |
by (parts_induct_tac 1); |
|
287 |
(*Fake, ClientKeyExch*) |
|
288 |
by (ALLGOALS Blast_tac); |
|
3704 | 289 |
qed "Crypt_unique_PMS"; |
290 |
||
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
291 |
|
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
292 |
(** It is frustrating that we need two versions of the unicity results. |
3704 | 293 |
But Notes A {|Agent B, Nonce PMS|} determines both A and B. Sometimes |
294 |
we have only the weaker assertion Crypt(pubK B) (Nonce PMS), which |
|
295 |
determines B alone, and only if PMS is secret. |
|
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
296 |
**) |
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
297 |
|
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset
|
298 |
(*In A's internal Note, PMS determines A and B.*) |
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
299 |
Goal "[| Notes A {|Agent B, Nonce PMS|} \\<in> set evs; \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
300 |
\ Notes A' {|Agent B', Nonce PMS|} \\<in> set evs; \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
301 |
\ evs \\<in> tls |] \ |
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
302 |
\ ==> A=A' & B=B'"; |
11104 | 303 |
by (etac rev_mp 1); |
304 |
by (etac rev_mp 1); |
|
305 |
by (parts_induct_tac 1); |
|
306 |
(*ClientKeyExch*) |
|
307 |
by (blast_tac (claset() addSDs [Notes_Crypt_parts_spies]) 1); |
|
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
308 |
qed "Notes_unique_PMS"; |
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
309 |
|
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
310 |
|
3772 | 311 |
(**** Secrecy Theorems ****) |
312 |
||
313 |
(*Key compromise lemma needed to prove analz_image_keys. |
|
314 |
No collection of keys can help the spy get new private keys.*) |
|
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
315 |
Goal "evs \\<in> tls \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
316 |
\ ==> \\<forall>KK. (Key(priK B) \\<in> analz (Key`KK Un (spies evs))) = \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
317 |
\ (priK B \\<in> KK | B \\<in> bad)"; |
3772 | 318 |
by (etac tls.induct 1); |
319 |
by (ALLGOALS |
|
320 |
(asm_simp_tac (analz_image_keys_ss |
|
5535 | 321 |
addsimps certificate_def::keys_distinct))); |
3772 | 322 |
(*Fake*) |
4422
21238c9d363e
Simplified proofs using rewrites for f``A where f is injective
paulson
parents:
4201
diff
changeset
|
323 |
by (spy_analz_tac 1); |
3772 | 324 |
qed_spec_mp "analz_image_priK"; |
325 |
||
326 |
||
327 |
(*slightly speeds up the big simplification below*) |
|
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
328 |
Goal "KK <= range sessionK ==> priK B \\<notin> KK"; |
3772 | 329 |
by (Blast_tac 1); |
330 |
val range_sessionkeys_not_priK = result(); |
|
331 |
||
332 |
(*Lemma for the trivial direction of the if-and-only-if*) |
|
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
333 |
Goal "(X \\<in> analz (G Un H)) --> (X \\<in> analz H) ==> \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
334 |
\ (X \\<in> analz (G Un H)) = (X \\<in> analz H)"; |
4091 | 335 |
by (blast_tac (claset() addIs [impOfSubs analz_mono]) 1); |
3961 | 336 |
val analz_image_keys_lemma = result(); |
3772 | 337 |
|
338 |
(** Strangely, the following version doesn't work: |
|
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
339 |
\ \\<forall>Z. (Nonce N \\<in> analz (Key`(sessionK`Z) Un (spies evs))) = \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
340 |
\ (Nonce N \\<in> analz (spies evs))"; |
3772 | 341 |
**) |
342 |
||
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
343 |
Goal "evs \\<in> tls ==> \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
344 |
\ \\<forall>KK. KK <= range sessionK --> \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
345 |
\ (Nonce N \\<in> analz (Key`KK Un (spies evs))) = \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
346 |
\ (Nonce N \\<in> analz (spies evs))"; |
3772 | 347 |
by (etac tls.induct 1); |
348 |
by (ClientKeyExch_tac 7); |
|
349 |
by (REPEAT_FIRST (resolve_tac [allI, impI])); |
|
3961 | 350 |
by (REPEAT_FIRST (rtac analz_image_keys_lemma)); |
5076 | 351 |
by (ALLGOALS (*4.5 seconds*) |
3772 | 352 |
(asm_simp_tac (analz_image_keys_ss |
5535 | 353 |
addsimps split_ifs @ pushes @ |
354 |
[range_sessionkeys_not_priK, |
|
355 |
analz_image_priK, certificate_def]))); |
|
4091 | 356 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [insert_absorb]))); |
3772 | 357 |
(*Fake*) |
4422
21238c9d363e
Simplified proofs using rewrites for f``A where f is injective
paulson
parents:
4201
diff
changeset
|
358 |
by (spy_analz_tac 1); |
3772 | 359 |
qed_spec_mp "analz_image_keys"; |
360 |
||
361 |
(*Knowing some session keys is no help in getting new nonces*) |
|
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
362 |
Goal "evs \\<in> tls ==> \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
363 |
\ Nonce N \\<in> analz (insert (Key (sessionK z)) (spies evs)) = \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
364 |
\ (Nonce N \\<in> analz (spies evs))"; |
3772 | 365 |
by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 1); |
366 |
qed "analz_insert_key"; |
|
367 |
Addsimps [analz_insert_key]; |
|
368 |
||
369 |
||
370 |
(*** Protocol goal: serverK(Na,Nb,M) and clientK(Na,Nb,M) remain secure ***) |
|
371 |
||
372 |
(** Some lemmas about session keys, comprising clientK and serverK **) |
|
373 |
||
374 |
||
375 |
(*Lemma: session keys are never used if PMS is fresh. |
|
376 |
Nonces don't have to agree, allowing session resumption. |
|
377 |
Converse doesn't hold; revealing PMS doesn't force the keys to be sent. |
|
378 |
THEY ARE NOT SUITABLE AS SAFE ELIM RULES.*) |
|
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
379 |
Goal "[| Nonce PMS \\<notin> parts (spies evs); \ |
6284
147db42c1009
tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents:
5653
diff
changeset
|
380 |
\ K = sessionK((Na, Nb, PRF(PMS,NA,NB)), role); \ |
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
381 |
\ evs \\<in> tls |] \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
382 |
\ ==> Key K \\<notin> parts (spies evs) & (\\<forall>Y. Crypt K Y \\<notin> parts (spies evs))"; |
3772 | 383 |
by (etac rev_mp 1); |
384 |
by (hyp_subst_tac 1); |
|
385 |
by (analz_induct_tac 1); |
|
386 |
(*SpyKeys*) |
|
8054
2ce57ef2a4aa
used image_eq_UN to speed up slow proofs of base cases
paulson
parents:
7057
diff
changeset
|
387 |
by (Blast_tac 2); |
3772 | 388 |
(*Fake*) |
8054
2ce57ef2a4aa
used image_eq_UN to speed up slow proofs of base cases
paulson
parents:
7057
diff
changeset
|
389 |
by (blast_tac (claset() addIs [parts_insertI]) 1); |
3772 | 390 |
(** LEVEL 6 **) |
391 |
(*Oops*) |
|
392 |
by (REPEAT |
|
7057
b9ddbb925939
tweaked proofs to handle new freeness reasoning for data c onstructors
paulson
parents:
6915
diff
changeset
|
393 |
(force_tac (claset() addSDs [Notes_Crypt_parts_spies, |
b9ddbb925939
tweaked proofs to handle new freeness reasoning for data c onstructors
paulson
parents:
6915
diff
changeset
|
394 |
Notes_master_imp_Crypt_PMS], |
b9ddbb925939
tweaked proofs to handle new freeness reasoning for data c onstructors
paulson
parents:
6915
diff
changeset
|
395 |
simpset()) 1)); |
3772 | 396 |
val lemma = result(); |
397 |
||
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
398 |
Goal "[| Key (sessionK((Na, Nb, PRF(PMS,NA,NB)), role)) \\<in> parts (spies evs); \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
399 |
\ evs \\<in> tls |] \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
400 |
\ ==> Nonce PMS \\<in> parts (spies evs)"; |
4091 | 401 |
by (blast_tac (claset() addDs [lemma]) 1); |
3772 | 402 |
qed "PMS_sessionK_not_spied"; |
403 |
||
6284
147db42c1009
tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents:
5653
diff
changeset
|
404 |
Goal "[| Crypt (sessionK((Na, Nb, PRF(PMS,NA,NB)), role)) Y \ |
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
405 |
\ \\<in> parts (spies evs); evs \\<in> tls |] \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
406 |
\ ==> Nonce PMS \\<in> parts (spies evs)"; |
4091 | 407 |
by (blast_tac (claset() addDs [lemma]) 1); |
3772 | 408 |
qed "PMS_Crypt_sessionK_not_spied"; |
409 |
||
5433 | 410 |
(*Write keys are never sent if M (MASTER SECRET) is secure. |
411 |
Converse fails; betraying M doesn't force the keys to be sent! |
|
3772 | 412 |
The strong Oops condition can be weakened later by unicity reasoning, |
5433 | 413 |
with some effort. |
414 |
NO LONGER USED: see clientK_not_spied and serverK_not_spied*) |
|
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
415 |
Goal "[| \\<forall>A. Says A Spy (Key (sessionK((NA,NB,M),role))) \\<notin> set evs; \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
416 |
\ Nonce M \\<notin> analz (spies evs); evs \\<in> tls |] \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
417 |
\ ==> Key (sessionK((NA,NB,M),role)) \\<notin> parts (spies evs)"; |
3772 | 418 |
by (etac rev_mp 1); |
419 |
by (etac rev_mp 1); |
|
6284
147db42c1009
tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents:
5653
diff
changeset
|
420 |
by (analz_induct_tac 1); (*5 seconds*) |
3772 | 421 |
(*SpyKeys*) |
8054
2ce57ef2a4aa
used image_eq_UN to speed up slow proofs of base cases
paulson
parents:
7057
diff
changeset
|
422 |
by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj]) 2); |
3772 | 423 |
(*Fake*) |
8054
2ce57ef2a4aa
used image_eq_UN to speed up slow proofs of base cases
paulson
parents:
7057
diff
changeset
|
424 |
by (spy_analz_tac 1); |
3772 | 425 |
qed "sessionK_not_spied"; |
426 |
||
427 |
||
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
428 |
(*If A sends ClientKeyExch to an honest B, then the PMS will stay secret.*) |
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
429 |
Goal "[| evs \\<in> tls; A \\<notin> bad; B \\<notin> bad |] \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
430 |
\ ==> Notes A {|Agent B, Nonce PMS|} \\<in> set evs --> \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
431 |
\ Nonce PMS \\<notin> analz (spies evs)"; |
6284
147db42c1009
tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents:
5653
diff
changeset
|
432 |
by (analz_induct_tac 1); (*4 seconds*) |
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
433 |
(*ClientAccepts and ServerAccepts: because PMS \\<notin> range PRF*) |
11150 | 434 |
by (REPEAT (Force_tac 6)); |
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
435 |
(*ClientHello, ServerHello, ClientKeyExch, ServerResume: |
3687
fb7d096d7884
Simplified SpyKeys to use sessionK instead of clientK and serverK
paulson
parents:
3686
diff
changeset
|
436 |
mostly freshness reasoning*) |
11150 | 437 |
by (REPEAT (blast_tac (claset() addSDs [parts.Body] |
4201 | 438 |
addDs [Notes_Crypt_parts_spies, |
439 |
Says_imp_spies RS analz.Inj]) 3)); |
|
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset
|
440 |
(*SpyKeys*) |
11150 | 441 |
by (Force_tac 2); |
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset
|
442 |
(*Fake*) |
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset
|
443 |
by (spy_analz_tac 1); |
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset
|
444 |
bind_thm ("Spy_not_see_PMS", result() RSN (2, rev_mp)); |
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset
|
445 |
|
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset
|
446 |
|
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
447 |
(*If A sends ClientKeyExch to an honest B, then the MASTER SECRET |
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset
|
448 |
will stay secret.*) |
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
449 |
Goal "[| evs \\<in> tls; A \\<notin> bad; B \\<notin> bad |] \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
450 |
\ ==> Notes A {|Agent B, Nonce PMS|} \\<in> set evs --> \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
451 |
\ Nonce (PRF(PMS,NA,NB)) \\<notin> analz (spies evs)"; |
6284
147db42c1009
tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents:
5653
diff
changeset
|
452 |
by (analz_induct_tac 1); (*4 seconds*) |
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset
|
453 |
(*ClientAccepts and ServerAccepts: because PMS was already visible*) |
4091 | 454 |
by (REPEAT (blast_tac (claset() addDs [Spy_not_see_PMS, |
4201 | 455 |
Says_imp_spies RS analz.Inj, |
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
6284
diff
changeset
|
456 |
Notes_imp_knows_Spy RS analz.Inj]) 6)); |
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset
|
457 |
(*ClientHello*) |
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset
|
458 |
by (Blast_tac 3); |
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset
|
459 |
(*SpyKeys: by secrecy of the PMS, Spy cannot make the MS*) |
4091 | 460 |
by (blast_tac (claset() addSDs [Spy_not_see_PMS, |
4422
21238c9d363e
Simplified proofs using rewrites for f``A where f is injective
paulson
parents:
4201
diff
changeset
|
461 |
Says_imp_spies RS analz.Inj]) 2); |
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset
|
462 |
(*Fake*) |
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset
|
463 |
by (spy_analz_tac 1); |
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
464 |
(*ServerHello and ClientKeyExch: mostly freshness reasoning*) |
11150 | 465 |
by (REPEAT (blast_tac (claset() addSDs [parts.Body] |
4201 | 466 |
addDs [Notes_Crypt_parts_spies, |
467 |
Says_imp_spies RS analz.Inj]) 1)); |
|
3677
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset
|
468 |
bind_thm ("Spy_not_see_MS", result() RSN (2, rev_mp)); |
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset
|
469 |
|
f2569416d18b
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
paulson
parents:
3676
diff
changeset
|
470 |
|
3704 | 471 |
(*** Weakening the Oops conditions for leakage of clientK ***) |
472 |
||
5433 | 473 |
(*If A created PMS then nobody else (except the Spy in replays) |
474 |
would send a message using a clientK generated from that PMS.*) |
|
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
475 |
Goal "[| Says A' B' (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) \\<in> set evs; \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
476 |
\ Notes A {|Agent B, Nonce PMS|} \\<in> set evs; \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
477 |
\ evs \\<in> tls; A' \\<noteq> Spy |] \ |
5433 | 478 |
\ ==> A = A'"; |
479 |
by (etac rev_mp 1); |
|
480 |
by (etac rev_mp 1); |
|
6284
147db42c1009
tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents:
5653
diff
changeset
|
481 |
by (analz_induct_tac 1); |
3711 | 482 |
by (ALLGOALS Clarify_tac); |
3704 | 483 |
(*ClientFinished, ClientResume: by unicity of PMS*) |
484 |
by (REPEAT |
|
4091 | 485 |
(blast_tac (claset() addSDs [Notes_master_imp_Notes_PMS] |
4201 | 486 |
addIs [Notes_unique_PMS RS conjunct1]) 2)); |
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
487 |
(*ClientKeyExch*) |
4472 | 488 |
by (blast_tac (claset() addSDs [PMS_Crypt_sessionK_not_spied, |
489 |
Says_imp_spies RS parts.Inj]) 1); |
|
5433 | 490 |
qed "Says_clientK_unique"; |
3704 | 491 |
|
492 |
||
493 |
(*If A created PMS and has not leaked her clientK to the Spy, |
|
5433 | 494 |
then it is completely secure: not even in parts!*) |
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
495 |
Goal "[| Notes A {|Agent B, Nonce PMS|} \\<in> set evs; \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
496 |
\ Says A Spy (Key (clientK(Na,Nb,PRF(PMS,NA,NB)))) \\<notin> set evs; \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
497 |
\ A \\<notin> bad; B \\<notin> bad; \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
498 |
\ evs \\<in> tls |] \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
499 |
\ ==> Key (clientK(Na,Nb,PRF(PMS,NA,NB))) \\<notin> parts (spies evs)"; |
5433 | 500 |
by (etac rev_mp 1); |
501 |
by (etac rev_mp 1); |
|
6284
147db42c1009
tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents:
5653
diff
changeset
|
502 |
by (analz_induct_tac 1); (*4 seconds*) |
3704 | 503 |
(*Oops*) |
5433 | 504 |
by (blast_tac (claset() addIs [Says_clientK_unique]) 4); |
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
505 |
(*ClientKeyExch*) |
5433 | 506 |
by (blast_tac (claset() addSDs [PMS_sessionK_not_spied]) 3); |
507 |
(*SpyKeys*) |
|
508 |
by (blast_tac (claset() addSEs [Spy_not_see_MS RSN (2,rev_notE)]) 2); |
|
509 |
(*Fake*) |
|
510 |
by (spy_analz_tac 1); |
|
511 |
qed "clientK_not_spied"; |
|
3704 | 512 |
|
513 |
||
514 |
(*** Weakening the Oops conditions for leakage of serverK ***) |
|
515 |
||
516 |
(*If A created PMS for B, then nobody other than B or the Spy would |
|
517 |
send a message using a serverK generated from that PMS.*) |
|
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
518 |
Goal "[| Says B' A' (Crypt (serverK(Na,Nb,PRF(PMS,NA,NB))) Y) \\<in> set evs; \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
519 |
\ Notes A {|Agent B, Nonce PMS|} \\<in> set evs; \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
520 |
\ evs \\<in> tls; A \\<notin> bad; B \\<notin> bad; B' \\<noteq> Spy |] \ |
5433 | 521 |
\ ==> B = B'"; |
522 |
by (etac rev_mp 1); |
|
523 |
by (etac rev_mp 1); |
|
6284
147db42c1009
tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents:
5653
diff
changeset
|
524 |
by (analz_induct_tac 1); |
3711 | 525 |
by (ALLGOALS Clarify_tac); |
3704 | 526 |
(*ServerResume, ServerFinished: by unicity of PMS*) |
527 |
by (REPEAT |
|
5433 | 528 |
(blast_tac (claset() addSDs [Notes_master_imp_Crypt_PMS] |
4201 | 529 |
addDs [Spy_not_see_PMS, |
530 |
Notes_Crypt_parts_spies, |
|
531 |
Crypt_unique_PMS]) 2)); |
|
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
532 |
(*ClientKeyExch*) |
4472 | 533 |
by (blast_tac (claset() addSDs [PMS_Crypt_sessionK_not_spied, |
534 |
Says_imp_spies RS parts.Inj]) 1); |
|
5433 | 535 |
qed "Says_serverK_unique"; |
3704 | 536 |
|
537 |
(*If A created PMS for B, and B has not leaked his serverK to the Spy, |
|
5433 | 538 |
then it is completely secure: not even in parts!*) |
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
539 |
Goal "[| Notes A {|Agent B, Nonce PMS|} \\<in> set evs; \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
540 |
\ Says B Spy (Key(serverK(Na,Nb,PRF(PMS,NA,NB)))) \\<notin> set evs; \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
541 |
\ A \\<notin> bad; B \\<notin> bad; evs \\<in> tls |] \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
542 |
\ ==> Key (serverK(Na,Nb,PRF(PMS,NA,NB))) \\<notin> parts (spies evs)"; |
5433 | 543 |
by (etac rev_mp 1); |
544 |
by (etac rev_mp 1); |
|
6284
147db42c1009
tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents:
5653
diff
changeset
|
545 |
by (analz_induct_tac 1); |
3704 | 546 |
(*Oops*) |
5433 | 547 |
by (blast_tac (claset() addIs [Says_serverK_unique]) 4); |
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
548 |
(*ClientKeyExch*) |
5433 | 549 |
by (blast_tac (claset() addSDs [PMS_sessionK_not_spied]) 3); |
550 |
(*SpyKeys*) |
|
551 |
by (blast_tac (claset() addSEs [Spy_not_see_MS RSN (2,rev_notE)]) 2); |
|
552 |
(*Fake*) |
|
553 |
by (spy_analz_tac 1); |
|
554 |
qed "serverK_not_spied"; |
|
3704 | 555 |
|
556 |
||
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
557 |
(*** Protocol goals: if A receives ServerFinished, then B is present |
3729
6be7cf5086ab
Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents:
3711
diff
changeset
|
558 |
and has used the quoted values PA, PB, etc. Note that it is up to A |
6be7cf5086ab
Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents:
3711
diff
changeset
|
559 |
to compare PA with what she originally sent. |
3474 | 560 |
***) |
561 |
||
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
562 |
(*The mention of her name (A) in X assures A that B knows who she is.*) |
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
563 |
Goal "[| X = Crypt (serverK(Na,Nb,M)) \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
564 |
\ (Hash{|Number SID, Nonce M, \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
565 |
\ Nonce Na, Number PA, Agent A, \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
566 |
\ Nonce Nb, Number PB, Agent B|}); \ |
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
567 |
\ M = PRF(PMS,NA,NB); \ |
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
568 |
\ evs \\<in> tls; A \\<notin> bad; B \\<notin> bad |] \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
569 |
\ ==> Says B Spy (Key(serverK(Na,Nb,M))) \\<notin> set evs --> \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
570 |
\ Notes A {|Agent B, Nonce PMS|} \\<in> set evs --> \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
571 |
\ X \\<in> parts (spies evs) --> Says B A X \\<in> set evs"; |
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
572 |
by (hyp_subst_tac 1); |
6284
147db42c1009
tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents:
5653
diff
changeset
|
573 |
by (analz_induct_tac 1); (*7 seconds*) |
3711 | 574 |
by (ALLGOALS Clarify_tac); |
4472 | 575 |
(*ClientKeyExch*) |
576 |
by (blast_tac (claset() addSDs [PMS_Crypt_sessionK_not_spied]) 2); |
|
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
577 |
(*Fake: the Spy doesn't have the critical session key!*) |
5433 | 578 |
by (blast_tac (claset() addEs [serverK_not_spied RSN (2,rev_notE)]) 1); |
3474 | 579 |
qed_spec_mp "TrustServerFinished"; |
580 |
||
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
581 |
(*This version refers not to ServerFinished but to any message from B. |
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
582 |
We don't assume B has received CertVerify, and an intruder could |
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
583 |
have changed A's identity in all other messages, so we can't be sure |
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3515
diff
changeset
|
584 |
that B sends his message to A. If CLIENT KEY EXCHANGE were augmented |
3704 | 585 |
to bind A's identity with PMS, then we could replace A' by A below.*) |
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
586 |
Goal "[| M = PRF(PMS,NA,NB); evs \\<in> tls; A \\<notin> bad; B \\<notin> bad |] \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
587 |
\ ==> Says B Spy (Key(serverK(Na,Nb,M))) \\<notin> set evs --> \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
588 |
\ Notes A {|Agent B, Nonce PMS|} \\<in> set evs --> \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
589 |
\ Crypt (serverK(Na,Nb,M)) Y \\<in> parts (spies evs) --> \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
590 |
\ (\\<exists>A'. Says B A' (Crypt (serverK(Na,Nb,M)) Y) \\<in> set evs)"; |
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
591 |
by (hyp_subst_tac 1); |
6284
147db42c1009
tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents:
5653
diff
changeset
|
592 |
by (analz_induct_tac 1); (*6 seconds*) |
4091 | 593 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib]))); |
3711 | 594 |
by (ALLGOALS Clarify_tac); |
3704 | 595 |
(*ServerResume, ServerFinished: by unicity of PMS*) |
596 |
by (REPEAT |
|
5433 | 597 |
(blast_tac (claset() addSDs [Notes_master_imp_Crypt_PMS] |
4201 | 598 |
addDs [Spy_not_see_PMS, |
599 |
Notes_Crypt_parts_spies, |
|
600 |
Crypt_unique_PMS]) 3)); |
|
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
601 |
(*ClientKeyExch*) |
4472 | 602 |
by (blast_tac (claset() addSDs [PMS_Crypt_sessionK_not_spied]) 2); |
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
603 |
(*Fake: the Spy doesn't have the critical session key!*) |
5433 | 604 |
by (blast_tac (claset() addEs [serverK_not_spied RSN (2,rev_notE)]) 1); |
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
605 |
qed_spec_mp "TrustServerMsg"; |
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
606 |
|
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
607 |
|
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
608 |
(*** Protocol goal: if B receives any message encrypted with clientK |
3672
56e4365a0c99
TLS now with a distinction between premaster secret and master secret
paulson
parents:
3519
diff
changeset
|
609 |
then A has sent it, ASSUMING that A chose PMS. Authentication is |
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
610 |
assumed here; B cannot verify it. But if the message is |
3729
6be7cf5086ab
Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents:
3711
diff
changeset
|
611 |
ClientFinished, then B can then check the quoted values PA, PB, etc. |
3506 | 612 |
***) |
3704 | 613 |
|
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
614 |
Goal "[| M = PRF(PMS,NA,NB); evs \\<in> tls; A \\<notin> bad; B \\<notin> bad |] \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
615 |
\ ==> Says A Spy (Key(clientK(Na,Nb,M))) \\<notin> set evs --> \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
616 |
\ Notes A {|Agent B, Nonce PMS|} \\<in> set evs --> \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
617 |
\ Crypt (clientK(Na,Nb,M)) Y \\<in> parts (spies evs) --> \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
618 |
\ Says A B (Crypt (clientK(Na,Nb,M)) Y) \\<in> set evs"; |
3772 | 619 |
by (hyp_subst_tac 1); |
6284
147db42c1009
tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents:
5653
diff
changeset
|
620 |
by (analz_induct_tac 1); (*6 seconds*) |
3711 | 621 |
by (ALLGOALS Clarify_tac); |
3704 | 622 |
(*ClientFinished, ClientResume: by unicity of PMS*) |
4091 | 623 |
by (REPEAT (blast_tac (claset() delrules [conjI] |
4201 | 624 |
addSDs [Notes_master_imp_Notes_PMS] |
625 |
addDs [Notes_unique_PMS]) 3)); |
|
4472 | 626 |
(*ClientKeyExch*) |
627 |
by (blast_tac (claset() addSDs [PMS_Crypt_sessionK_not_spied]) 2); |
|
3480
d59bbf053258
More realistic model: the Spy can compute clientK and serverK
paulson
parents:
3474
diff
changeset
|
628 |
(*Fake: the Spy doesn't have the critical session key!*) |
5433 | 629 |
by (blast_tac (claset() addEs [clientK_not_spied RSN (2,rev_notE)]) 1); |
630 |
qed_spec_mp "TrustClientMsg"; |
|
3506 | 631 |
|
632 |
||
3685
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
633 |
|
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
634 |
(*** Protocol goal: if B receives ClientFinished, and if B is able to |
5b8c0c8f576e
Full version of TLS including session resumption, but no Oops
paulson
parents:
3683
diff
changeset
|
635 |
check a CertVerify from A, then A has used the quoted |
3729
6be7cf5086ab
Renamed XA, XB to PA, PB and removed the certificate from Client Verify
paulson
parents:
3711
diff
changeset
|
636 |
values PA, PB, etc. Even this one requires A to be uncompromised. |
3506 | 637 |
***) |
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
638 |
Goal "[| M = PRF(PMS,NA,NB); \ |
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
639 |
\ Says A Spy (Key(clientK(Na,Nb,M))) \\<notin> set evs;\ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
640 |
\ Says A' B (Crypt (clientK(Na,Nb,M)) Y) \\<in> set evs; \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
641 |
\ certificate A KA \\<in> parts (spies evs); \ |
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
642 |
\ Says A'' B (Crypt (invKey KA) (Hash{|nb, Agent B, Nonce PMS|}))\ |
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
643 |
\ \\<in> set evs; \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
644 |
\ evs \\<in> tls; A \\<notin> bad; B \\<notin> bad |] \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
645 |
\ ==> Says A B (Crypt (clientK(Na,Nb,M)) Y) \\<in> set evs"; |
4091 | 646 |
by (blast_tac (claset() addSIs [TrustClientMsg, UseCertVerify] |
4201 | 647 |
addDs [Says_imp_spies RS parts.Inj]) 1); |
3515
d8a71f6eaf40
Now uses the Notes constructor to distinguish the Client (who has chosen M)
paulson
parents:
3506
diff
changeset
|
648 |
qed "AuthClientFinished"; |
3687
fb7d096d7884
Simplified SpyKeys to use sessionK instead of clientK and serverK
paulson
parents:
3686
diff
changeset
|
649 |
|
fb7d096d7884
Simplified SpyKeys to use sessionK instead of clientK and serverK
paulson
parents:
3686
diff
changeset
|
650 |
(*22/9/97: loads in 622s, which is 10 minutes 22 seconds*) |
3711 | 651 |
(*24/9/97: loads in 672s, which is 11 minutes 12 seconds [stronger theorems]*) |
3745
4c5d3b1ddc75
Client, Server certificates now sent using the separate Certificate rule,
paulson
parents:
3729
diff
changeset
|
652 |
(*29/9/97: loads in 481s, after removing Certificate from ClientKeyExch*) |
3758
188a4fbfaf55
Exchanged the M and SID fields of the FINISHED messages to simplify proofs;
paulson
parents:
3745
diff
changeset
|
653 |
(*30/9/97: loads in 476s, after removing unused theorems*) |
3760
77f71f650433
Strengthened the possibility property for resumption so that it could have
paulson
parents:
3758
diff
changeset
|
654 |
(*30/9/97: loads in 448s, after fixing ServerResume*) |
5433 | 655 |
|
656 |
(*08/9/97: loads in 189s (pike), after much reorganization, |
|
657 |
back to 621s on albatross?*) |
|
6284
147db42c1009
tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents:
5653
diff
changeset
|
658 |
|
147db42c1009
tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents:
5653
diff
changeset
|
659 |
(*10/2/99: loads in 139s (pike) |
147db42c1009
tidying in conjuntion with the TISSEC paper; replaced (unit option)
paulson
parents:
5653
diff
changeset
|
660 |
down to 433s on albatross*) |