author  paulson 
Tue, 16 Dec 1997 15:17:26 +0100  
changeset 4422  21238c9d363e 
parent 4331  34bb65b037dd 
child 4449  df30e75f670f 
permissions  rwrr 
1934  1 
(* Title: HOL/Auth/NS_Shared 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1996 University of Cambridge 

5 

6 
Inductive relation "ns_shared" for NeedhamSchroeder SharedKey protocol. 

7 

8 
From page 247 of 

9 
Burrows, Abadi and Needham. A Logic of Authentication. 

10 
Proc. Royal Soc. 426 (1989) 

11 
*) 

12 

13 
open NS_Shared; 

14 

1943  15 
proof_timing:=true; 
1997  16 
HOL_quantifiers := false; 
17 

18 

2323  19 
(*A "possibility property": there are traces that reach the end*) 
1997  20 
goal thy 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

21 
"!!A B. [ A ~= B; A ~= Server; B ~= Server ] \ 
4237
fb01353e363b
The dtac was discarding information, though apparently no proofs were hurt
paulson
parents:
4091
diff
changeset

22 
\ ==> EX N K. EX evs: ns_shared. \ 
3465  23 
\ Says A B (Crypt K {Nonce N, Nonce N}) : set evs"; 
1997  24 
by (REPEAT (resolve_tac [exI,bexI] 1)); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

25 
by (rtac (ns_shared.Nil RS ns_shared.NS1 RS ns_shared.NS2 RS 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

26 
ns_shared.NS3 RS ns_shared.NS4 RS ns_shared.NS5) 2); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

27 
by possibility_tac; 
2015  28 
result(); 
29 

3675
70dd312b70b2
Deleted the redundant simprule not_parts_not_analz
paulson
parents:
3651
diff
changeset

30 
goal thy 
70dd312b70b2
Deleted the redundant simprule not_parts_not_analz
paulson
parents:
3651
diff
changeset

31 
"!!A B. [ A ~= B; A ~= Server; B ~= Server ] \ 
70dd312b70b2
Deleted the redundant simprule not_parts_not_analz
paulson
parents:
3651
diff
changeset

32 
\ ==> EX evs: ns_shared. \ 
70dd312b70b2
Deleted the redundant simprule not_parts_not_analz
paulson
parents:
3651
diff
changeset

33 
\ Says A B (Crypt ?K {Nonce ?N, Nonce ?N}) : set evs"; 
70dd312b70b2
Deleted the redundant simprule not_parts_not_analz
paulson
parents:
3651
diff
changeset

34 
by (REPEAT (resolve_tac [exI,bexI] 1)); 
70dd312b70b2
Deleted the redundant simprule not_parts_not_analz
paulson
parents:
3651
diff
changeset

35 
by (rtac (ns_shared.Nil RS ns_shared.NS1 RS ns_shared.NS2 RS 
70dd312b70b2
Deleted the redundant simprule not_parts_not_analz
paulson
parents:
3651
diff
changeset

36 
ns_shared.NS3 RS ns_shared.NS4 RS ns_shared.NS5) 2); 
70dd312b70b2
Deleted the redundant simprule not_parts_not_analz
paulson
parents:
3651
diff
changeset

37 
by possibility_tac; 
1943  38 

1934  39 
(**** Inductive proofs about ns_shared ****) 
40 

41 
(*Nobody sends themselves messages*) 

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

42 
goal thy "!!evs. evs : ns_shared ==> ALL A X. Says A A X ~: set evs"; 
2032  43 
by (etac ns_shared.induct 1); 
1934  44 
by (Auto_tac()); 
45 
qed_spec_mp "not_Says_to_self"; 

46 
Addsimps [not_Says_to_self]; 

47 
AddSEs [not_Says_to_self RSN (2, rev_notE)]; 

48 

1943  49 
(*For reasoning about the encrypted portion of message NS3*) 
3465  50 
goal thy "!!evs. Says S A (Crypt KA {N, B, K, X}) : set evs \ 
3683  51 
\ ==> X : parts (spies evs)"; 
4091  52 
by (blast_tac (claset() addSEs spies_partsEs) 1); 
3683  53 
qed "NS3_msg_in_parts_spies"; 
2032  54 

2070  55 
goal thy 
3465  56 
"!!evs. Says Server A (Crypt (shrK A) {NA, B, K, X}) : set evs \ 
3683  57 
\ ==> K : parts (spies evs)"; 
4091  58 
by (blast_tac (claset() addSEs spies_partsEs) 1); 
3683  59 
qed "Oops_parts_spies"; 
2070  60 

3683  61 
(*For proving the easier theorems about X ~: parts (spies evs).*) 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

62 
fun parts_induct_tac i = 
4331  63 
EVERY [etac ns_shared.induct i, 
64 
REPEAT (FIRSTGOAL analz_mono_contra_tac), 

65 
forward_tac [Oops_parts_spies] (i+7), 

66 
forward_tac [NS3_msg_in_parts_spies] (i+4), 

67 
prove_simple_subgoals_tac i]; 

2070  68 

1934  69 

3683  70 
(** Theorems of the form X ~: parts (spies evs) imply that NOBODY 
2015  71 
sends messages containing X! **) 
1934  72 

3683  73 
(*Spy never sees another agent's shared key! (unless it's bad at start)*) 
1934  74 
goal thy 
3683  75 
"!!evs. evs : ns_shared ==> (Key (shrK A) : parts (spies evs)) = (A : bad)"; 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

76 
by (parts_induct_tac 1); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

77 
by (Fake_parts_insert_tac 1); 
3961  78 
by (ALLGOALS Blast_tac); 
2131  79 
qed "Spy_see_shrK"; 
80 
Addsimps [Spy_see_shrK]; 

1934  81 

2131  82 
goal thy 
3683  83 
"!!evs. evs : ns_shared ==> (Key (shrK A) : analz (spies evs)) = (A : bad)"; 
4091  84 
by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset())); 
2131  85 
qed "Spy_analz_shrK"; 
86 
Addsimps [Spy_analz_shrK]; 

1934  87 

3683  88 
goal thy "!!A. [ Key (shrK A) : parts (spies evs); \ 
89 
\ evs : ns_shared ] ==> A:bad"; 

4091  90 
by (blast_tac (claset() addDs [Spy_see_shrK]) 1); 
2131  91 
qed "Spy_see_shrK_D"; 
1934  92 

2131  93 
bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D); 
94 
AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D]; 

1934  95 

2070  96 

2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

97 
(*Nobody can have used nonexistent keys!*) 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

98 
goal thy "!!evs. evs : ns_shared ==> \ 
3683  99 
\ Key K ~: used evs > K ~: keysFor (parts (spies evs))"; 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

100 
by (parts_induct_tac 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

101 
(*Fake*) 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

102 
by (best_tac 
4091  103 
(claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)] 
4237
fb01353e363b
The dtac was discarding information, though apparently no proofs were hurt
paulson
parents:
4091
diff
changeset

104 
addIs [impOfSubs analz_subset_parts] 
fb01353e363b
The dtac was discarding information, though apparently no proofs were hurt
paulson
parents:
4091
diff
changeset

105 
addDs [impOfSubs (analz_subset_parts RS keysFor_mono)] 
fb01353e363b
The dtac was discarding information, though apparently no proofs were hurt
paulson
parents:
4091
diff
changeset

106 
addss (simpset())) 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

107 
(*NS2, NS4, NS5*) 
4091  108 
by (ALLGOALS (blast_tac (claset() addSEs spies_partsEs))); 
2160  109 
qed_spec_mp "new_keys_not_used"; 
1934  110 

111 
bind_thm ("new_keys_not_analzd", 

2032  112 
[analz_subset_parts RS keysFor_mono, 
113 
new_keys_not_used] MRS contra_subsetD); 

1934  114 

115 
Addsimps [new_keys_not_used, new_keys_not_analzd]; 

116 

117 

118 
(** Lemmas concerning the form of items passed in messages **) 

119 

2015  120 
(*Describes the form of K, X and K' when the Server sends this message.*) 
1934  121 
goal thy 
3683  122 
"!!evs. [ Says Server A (Crypt K' {N, Agent B, Key K, X}) : set evs; \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

123 
\ evs : ns_shared ] \ 
4267  124 
\ ==> K ~: range shrK & \ 
125 
\ X = (Crypt (shrK B) {Key K, Agent A}) & \ 

2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

126 
\ K' = shrK A"; 
2032  127 
by (etac rev_mp 1); 
128 
by (etac ns_shared.induct 1); 

2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

129 
by (Auto_tac()); 
1934  130 
qed "Says_Server_message_form"; 
131 

132 

2070  133 
(*If the encrypted message appears then it originated with the Server*) 
1934  134 
goal thy 
3683  135 
"!!evs. [ Crypt (shrK A) {NA, Agent B, Key K, X} : parts (spies evs); \ 
4267  136 
\ A ~: bad; evs : ns_shared ] \ 
137 
\ ==> Says Server A (Crypt (shrK A) {NA, Agent B, Key K, X}) \ 

3651  138 
\ : set evs"; 
2070  139 
by (etac rev_mp 1); 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

140 
by (parts_induct_tac 1); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

141 
by (Fake_parts_insert_tac 1); 
2323  142 
qed "A_trusts_NS2"; 
1934  143 

1965  144 

4331  145 
goal thy 
146 
"!!evs. [ Crypt (shrK A) {NA, Agent B, Key K, X} : parts (spies evs); \ 

147 
\ A ~: bad; evs : ns_shared ] \ 

148 
\ ==> K ~: range shrK & X = (Crypt (shrK B) {Key K, Agent A})"; 

149 
by (blast_tac (claset() addSDs [A_trusts_NS2, Says_Server_message_form]) 1); 

150 
qed "cert_A_form"; 

151 

152 

1965  153 
(*EITHER describes the form of X when the following message is sent, 
154 
OR reduces it to the Fake case. 

155 
Use Says_Server_message_form if applicable.*) 

1934  156 
goal thy 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

157 
"!!evs. [ Says S A (Crypt (shrK A) {Nonce NA, Agent B, Key K, X}) \ 
3651  158 
\ : set evs; \ 
159 
\ evs : ns_shared ] \ 

3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

160 
\ ==> (K ~: range shrK & X = (Crypt (shrK B) {Key K, Agent A})) \ 
3683  161 
\  X : analz (spies evs)"; 
162 
by (case_tac "A : bad" 1); 

4091  163 
by (fast_tac (claset() addSDs [Says_imp_spies RS analz.Inj] 
4237
fb01353e363b
The dtac was discarding information, though apparently no proofs were hurt
paulson
parents:
4091
diff
changeset

164 
addss (simpset())) 1); 
4331  165 
by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj, cert_A_form]) 1); 
1934  166 
qed "Says_S_message_form"; 
167 

168 

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

169 
(*For proofs involving analz.*) 
3683  170 
val analz_spies_tac = 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

171 
forward_tac [Says_Server_message_form] 8 THEN 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

172 
forward_tac [Says_S_message_form] 5 THEN 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

173 
REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE] ORELSE' hyp_subst_tac); 
2131  174 

1934  175 

176 
(**** 

177 
The following is to prove theorems of the form 

178 

3683  179 
Key K : analz (insert (Key KAB) (spies evs)) ==> 
180 
Key K : analz (spies evs) 

1934  181 

182 
A more general formula must be proved inductively. 

183 
****) 

184 

185 

186 
(*NOT useful in this form, but it says that session keys are not used 

187 
to encrypt messages containing other keys, in the actual protocol. 

188 
We require that agents should behave like this subsequently also.*) 

189 
goal thy 

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

190 
"!!evs. [ evs : ns_shared; Kab ~: range shrK ] ==> \ 
4237
fb01353e363b
The dtac was discarding information, though apparently no proofs were hurt
paulson
parents:
4091
diff
changeset

191 
\ (Crypt KAB X) : parts (spies evs) & \ 
3683  192 
\ Key K : parts {X} > Key K : parts (spies evs)"; 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

193 
by (parts_induct_tac 1); 
1934  194 
(*Deals with Faked messages*) 
4091  195 
by (blast_tac (claset() addSEs partsEs 
4237
fb01353e363b
The dtac was discarding information, though apparently no proofs were hurt
paulson
parents:
4091
diff
changeset

196 
addDs [impOfSubs parts_insert_subset_Un]) 1); 
1965  197 
(*Base, NS4 and NS5*) 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

198 
by (Auto_tac()); 
1934  199 
result(); 
200 

201 

202 
(** Session keys are not used to encrypt other session keys **) 

203 

2015  204 
(*The equality makes the induction hypothesis easier to apply*) 
1934  205 
goal thy 
4237
fb01353e363b
The dtac was discarding information, though apparently no proofs were hurt
paulson
parents:
4091
diff
changeset

206 
"!!evs. evs : ns_shared ==> \ 
fb01353e363b
The dtac was discarding information, though apparently no proofs were hurt
paulson
parents:
4091
diff
changeset

207 
\ ALL K KK. KK <= Compl (range shrK) > \ 
3683  208 
\ (Key K : analz (Key``KK Un (spies evs))) = \ 
209 
\ (K : KK  Key K : analz (spies evs))"; 

2032  210 
by (etac ns_shared.induct 1); 
3683  211 
by analz_spies_tac; 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

212 
by (REPEAT_FIRST (resolve_tac [allI, impI])); 
3961  213 
by (REPEAT_FIRST (rtac analz_image_freshK_lemma)); 
214 
(*Takes 9 secs*) 

2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

215 
by (ALLGOALS (asm_simp_tac analz_image_freshK_ss)); 
3451
d10f100676d8
Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents:
3441
diff
changeset

216 
(*Fake*) 
4422
21238c9d363e
Simplified proofs using rewrites for f``A where f is injective
paulson
parents:
4331
diff
changeset

217 
by (spy_analz_tac 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

218 
qed_spec_mp "analz_image_freshK"; 
1934  219 

220 

221 
goal thy 

4237
fb01353e363b
The dtac was discarding information, though apparently no proofs were hurt
paulson
parents:
4091
diff
changeset

222 
"!!evs. [ evs : ns_shared; KAB ~: range shrK ] ==> \ 
3683  223 
\ Key K : analz (insert (Key KAB) (spies evs)) = \ 
224 
\ (K = KAB  Key K : analz (spies evs))"; 

2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

225 
by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

226 
qed "analz_insert_freshK"; 
1934  227 

228 

2558  229 
(** The session key K uniquely identifies the message **) 
1965  230 

1934  231 
goal thy 
4267  232 
"!!evs. evs : ns_shared ==> \ 
4237
fb01353e363b
The dtac was discarding information, though apparently no proofs were hurt
paulson
parents:
4091
diff
changeset

233 
\ EX A' NA' B' X'. ALL A NA B X. \ 
3683  234 
\ Says Server A (Crypt (shrK A) {NA, Agent B, Key K, X}) : set evs \ 
235 
\ > A=A' & NA=NA' & B=B' & X=X'"; 

2032  236 
by (etac ns_shared.induct 1); 
4091  237 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); 
3730  238 
by Safe_tac; 
2070  239 
(*NS3*) 
240 
by (ex_strip_tac 2); 

3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

241 
by (Blast_tac 2); 
2070  242 
(*NS2: it can't be a new key*) 
243 
by (expand_case_tac "K = ?y" 1); 

244 
by (REPEAT (ares_tac [refl,exI,impI,conjI] 2)); 

4237
fb01353e363b
The dtac was discarding information, though apparently no proofs were hurt
paulson
parents:
4091
diff
changeset

245 
by (blast_tac (claset() delrules [conjI] (*prevent splitup into 4 subgoals*) 
fb01353e363b
The dtac was discarding information, though apparently no proofs were hurt
paulson
parents:
4091
diff
changeset

246 
addSEs spies_partsEs) 1); 
1934  247 
val lemma = result(); 
248 

249 
(*In messages of this form, the session key uniquely identifies the rest*) 

250 
goal thy 

4237
fb01353e363b
The dtac was discarding information, though apparently no proofs were hurt
paulson
parents:
4091
diff
changeset

251 
"!!evs. [ Says Server A \ 
fb01353e363b
The dtac was discarding information, though apparently no proofs were hurt
paulson
parents:
4091
diff
changeset

252 
\ (Crypt (shrK A) {NA, Agent B, Key K, X}) : set evs; \ 
fb01353e363b
The dtac was discarding information, though apparently no proofs were hurt
paulson
parents:
4091
diff
changeset

253 
\ Says Server A' \ 
3683  254 
\ (Crypt (shrK A') {NA', Agent B', Key K, X'}) : set evs; \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

255 
\ evs : ns_shared ] ==> A=A' & NA=NA' & B=B' & X = X'"; 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2374
diff
changeset

256 
by (prove_unique_tac lemma 1); 
1934  257 
qed "unique_session_keys"; 
258 

259 

2032  260 
(** Crucial secrecy property: Spy does not see the keys sent in msg NS2 **) 
2015  261 

1934  262 
goal thy 
3961  263 
"!!evs. [ A ~: bad; B ~: bad; evs : ns_shared ] \ 
2015  264 
\ ==> Says Server A \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

265 
\ (Crypt (shrK A) {NA, Agent B, Key K, \ 
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

266 
\ Crypt (shrK B) {Key K, Agent A}}) \ 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

267 
\ : set evs > \ 
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

268 
\ (ALL NB. Says A Spy {NA, NB, Key K} ~: set evs) > \ 
3683  269 
\ Key K ~: analz (spies evs)"; 
2032  270 
by (etac ns_shared.induct 1); 
3683  271 
by analz_spies_tac; 
1934  272 
by (ALLGOALS 
2015  273 
(asm_simp_tac 
4091  274 
(simpset() addsimps ([analz_insert_eq, analz_insert_freshK] @ 
4237
fb01353e363b
The dtac was discarding information, though apparently no proofs were hurt
paulson
parents:
4091
diff
changeset

275 
pushes @ expand_ifs)))); 
3451
d10f100676d8
Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents:
3441
diff
changeset

276 
(*Oops*) 
4091  277 
by (blast_tac (claset() addDs [unique_session_keys]) 5); 
3679  278 
(*NS3, replay subcase*) 
3451
d10f100676d8
Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents:
3441
diff
changeset

279 
by (Blast_tac 4); 
1934  280 
(*NS2*) 
4091  281 
by (blast_tac (claset() addSEs spies_partsEs 
4237
fb01353e363b
The dtac was discarding information, though apparently no proofs were hurt
paulson
parents:
4091
diff
changeset

282 
addIs [parts_insertI, 
fb01353e363b
The dtac was discarding information, though apparently no proofs were hurt
paulson
parents:
4091
diff
changeset

283 
impOfSubs analz_subset_parts]) 2); 
3451
d10f100676d8
Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents:
3441
diff
changeset

284 
(*Fake*) 
d10f100676d8
Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents:
3441
diff
changeset

285 
by (spy_analz_tac 1); 
3679  286 
(*NS3, Server subcase*) (**LEVEL 6 **) 
4091  287 
by (clarify_tac (claset() delrules [impCE]) 1); 
3683  288 
by (forward_tac [Says_imp_spies RS parts.Inj RS A_trusts_NS2] 1); 
2170  289 
by (assume_tac 2); 
4091  290 
by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj RS 
3683  291 
Crypt_Spy_analz_bad]) 1); 
4091  292 
by (blast_tac (claset() addDs [unique_session_keys]) 1); 
2070  293 
val lemma = result() RS mp RS mp RSN(2,rev_notE); 
2015  294 

295 

296 
(*Final version: Server's message in the most abstract form*) 

297 
goal thy 

4237
fb01353e363b
The dtac was discarding information, though apparently no proofs were hurt
paulson
parents:
4091
diff
changeset

298 
"!!evs. [ Says Server A \ 
4331  299 
\ (Crypt K' {NA, Agent B, Key K, X}) : set evs; \ 
300 
\ ALL NB. Says A Spy {NA, NB, Key K} ~: set evs; \ 

3683  301 
\ A ~: bad; B ~: bad; evs : ns_shared \ 
302 
\ ] ==> Key K ~: analz (spies evs)"; 

2015  303 
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); 
4091  304 
by (blast_tac (claset() addSDs [lemma]) 1); 
2032  305 
qed "Spy_not_see_encrypted_key"; 
306 

307 

2070  308 
(**** Guarantees available at various stages of protocol ***) 
309 

3651  310 
A_trusts_NS2 RS Spy_not_see_encrypted_key; 
2070  311 

312 

313 
(*If the encrypted message appears then it originated with the Server*) 

314 
goal thy 

4237
fb01353e363b
The dtac was discarding information, though apparently no proofs were hurt
paulson
parents:
4091
diff
changeset

315 
"!!evs. [ Crypt (shrK B) {Key K, Agent A} : parts (spies evs); \ 
fb01353e363b
The dtac was discarding information, though apparently no proofs were hurt
paulson
parents:
4091
diff
changeset

316 
\ B ~: bad; evs : ns_shared ] \ 
2070  317 
\ ==> EX NA. Says Server A \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

318 
\ (Crypt (shrK A) {NA, Agent B, Key K, \ 
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

319 
\ Crypt (shrK B) {Key K, Agent A}}) \ 
3465  320 
\ : set evs"; 
2070  321 
by (etac rev_mp 1); 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

322 
by (parts_induct_tac 1); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

323 
by (Fake_parts_insert_tac 1); 
2070  324 
(*Fake case*) 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

325 
by (ALLGOALS Blast_tac); 
2323  326 
qed "B_trusts_NS3"; 
2070  327 

328 

329 
goal thy 

4331  330 
"!!evs. [ Crypt K (Nonce NB) : parts (spies evs); \ 
331 
\ Says Server A (Crypt (shrK A) {NA, Agent B, Key K, X}) \ 

332 
\ : set evs; \ 

333 
\ Key K ~: analz (spies evs); \ 

334 
\ evs : ns_shared ] \ 

335 
\ ==> Says B A (Crypt K (Nonce NB)) : set evs"; 

336 
by (etac rev_mp 1); 

337 
by (etac rev_mp 1); 

338 
by (etac rev_mp 1); 

339 
by (parts_induct_tac 1); 

4267  340 
(*NS3*) 
341 
by (Blast_tac 3); 

342 
by (Fake_parts_insert_tac 1); 

343 
(*NS2: contradiction from the assumptions 

4331  344 
Key K ~: used evs2 and Crypt K (Nonce NB) : parts (spies evs2) *) 
345 
by (blast_tac (claset() addSEs [new_keys_not_used RSN (2,rev_notE)] 

346 
addSDs [Crypt_imp_keysFor]) 1); 

347 
(**LEVEL 7**) 

348 
(*NS4*) 

349 
by (Clarify_tac 1); 

350 
by (not_bad_tac "Ba" 1); 

4091  351 
by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS B_trusts_NS3, 
4331  352 
unique_session_keys]) 1); 
353 
qed "A_trusts_NS4_lemma"; 

2103  354 

4331  355 

356 
(*This version no longer assumes that K is secure*) 

2103  357 
goal thy 
4267  358 
"!!evs. [ Crypt K (Nonce NB) : parts (spies evs); \ 
4331  359 
\ Crypt (shrK A) {NA, Agent B, Key K, X} : parts (spies evs); \ 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

360 
\ ALL NB. Says A Spy {NA, NB, Key K} ~: set evs; \ 
4267  361 
\ A ~: bad; B ~: bad; evs : ns_shared ] \ 
3465  362 
\ ==> Says B A (Crypt K (Nonce NB)) : set evs"; 
4331  363 
by (blast_tac (claset() addSIs [A_trusts_NS2, A_trusts_NS4_lemma] 
4267  364 
addSEs [Spy_not_see_encrypted_key RSN (2,rev_notE)]) 1); 
2323  365 
qed "A_trusts_NS4"; 
4331  366 

367 

368 
(*If the session key has been used in NS4 then somebody has forwarded 

369 
component X in some instance of NS4. Perhaps an interesting property, 

370 
but not needed (after all) for the proofs below.*) 

371 
goal thy 

372 
"!!evs. [ Crypt K (Nonce NB) : parts (spies evs); \ 

373 
\ Says Server A (Crypt (shrK A) {NA, Agent B, Key K, X}) \ 

374 
\ : set evs; \ 

375 
\ Key K ~: analz (spies evs); \ 

376 
\ evs : ns_shared ] \ 

377 
\ ==> EX A'. Says A' B X : set evs"; 

378 
by (etac rev_mp 1); 

379 
by (etac rev_mp 1); 

380 
by (etac rev_mp 1); 

381 
by (parts_induct_tac 1); 

382 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib]))); 

383 
by (ALLGOALS Clarify_tac); 

384 
by (Fake_parts_insert_tac 1); 

385 
(**LEVEL 7**) 

386 
(*NS2*) 

387 
by (blast_tac (claset() addSEs [new_keys_not_used RSN (2,rev_notE)] 

388 
addSDs [Crypt_imp_keysFor]) 1); 

389 
(*NS4*) 

390 
by (not_bad_tac "Ba" 1); 

391 
by (Asm_full_simp_tac 1); 

392 
by (forward_tac [Says_imp_spies RS parts.Inj RS B_trusts_NS3] 1); 

393 
by (ALLGOALS Clarify_tac); 

394 
by (blast_tac (claset() addDs [unique_session_keys]) 1); 

395 
qed "NS4_implies_NS3"; 

396 

397 

398 
goal thy 

399 
"!!evs. [ B ~: bad; evs : ns_shared ] \ 

400 
\ ==> Key K ~: analz (spies evs) > \ 

401 
\ Says Server A \ 

402 
\ (Crypt (shrK A) {NA, Agent B, Key K, \ 

403 
\ Crypt (shrK B) {Key K, Agent A}}) \ 

404 
\ : set evs > \ 

405 
\ Says B A (Crypt K (Nonce NB)) : set evs > \ 

406 
\ Crypt K {Nonce NB, Nonce NB} : parts (spies evs) > \ 

407 
\ Says A B (Crypt K {Nonce NB, Nonce NB}) : set evs"; 

408 
by (parts_induct_tac 1); 

409 
(*NS4*) 

410 
by (blast_tac (claset() addSEs spies_partsEs) 4); 

411 
(*NS3*) 

412 
by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj, cert_A_form]) 3); 

413 
(*NS2*) 

414 
by (blast_tac (claset() addSEs [new_keys_not_used RSN (2,rev_notE)] 

415 
addSDs [Crypt_imp_keysFor]) 2); 

416 
by (Fake_parts_insert_tac 1); 

417 
(**LEVEL 5**) 

418 
(*NS5*) 

419 
by (Clarify_tac 1); 

420 
by (not_bad_tac "Aa" 1); 

421 
by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS A_trusts_NS2, 

422 
unique_session_keys]) 1); 

423 
val lemma = result(); 

424 

425 

426 
(*Very strong Oops condition reveals protocol's weakness*) 

427 
goal thy 

428 
"!!evs. [ Crypt K {Nonce NB, Nonce NB} : parts (spies evs); \ 

429 
\ Says B A (Crypt K (Nonce NB)) : set evs; \ 

430 
\ Crypt (shrK B) {Key K, Agent A} : parts (spies evs); \ 

431 
\ ALL NA NB. Says A Spy {NA, NB, Key K} ~: set evs; \ 

432 
\ A ~: bad; B ~: bad; evs : ns_shared ] \ 

433 
\ ==> Says A B (Crypt K {Nonce NB, Nonce NB}) : set evs"; 

434 
by (dtac B_trusts_NS3 1); 

435 
by (ALLGOALS Clarify_tac); 

436 
by (blast_tac (claset() addSIs [normalize_thm [RSspec, RSmp] lemma] 

437 
addSEs [Spy_not_see_encrypted_key RSN (2,rev_notE)]) 1); 

438 
qed "B_trusts_NS5"; 