author  paulson 
Fri, 11 Jul 1997 13:26:15 +0200  
changeset 3512  9dcb4daa15e8 
parent 3466  30791e5a69c4 
child 3516  470626799511 
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 

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

18 
(*Replacing the variable by a constant improves search speed by 50%!*) 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

19 
val Says_imp_sees_Spy' = read_instantiate [("lost","lost")] Says_imp_sees_Spy; 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

20 

1997  21 

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

24 
"!!A B. [ A ~= B; A ~= Server; B ~= Server ] \ 
2032  25 
\ ==> EX N K. EX evs: ns_shared lost. \ 
3465  26 
\ Says A B (Crypt K {Nonce N, Nonce N}) : set evs"; 
1997  27 
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

28 
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

29 
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

30 
by possibility_tac; 
2015  31 
result(); 
32 

1943  33 

1934  34 
(**** Inductive proofs about ns_shared ****) 
35 

2103  36 
(*Monotonicity*) 
2032  37 
goal thy "!!evs. lost' <= lost ==> ns_shared lost' <= ns_shared lost"; 
38 
by (rtac subsetI 1); 

39 
by (etac ns_shared.induct 1); 

40 
by (REPEAT_FIRST 

3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

41 
(blast_tac (!claset addIs (impOfSubs(sees_mono RS analz_mono RS synth_mono) 
2032  42 
:: ns_shared.intrs)))); 
43 
qed "ns_shared_mono"; 

44 

45 

1934  46 
(*Nobody sends themselves messages*) 
3465  47 
goal thy "!!evs. evs : ns_shared lost ==> ALL A X. Says A A X ~: set evs"; 
2032  48 
by (etac ns_shared.induct 1); 
1934  49 
by (Auto_tac()); 
50 
qed_spec_mp "not_Says_to_self"; 

51 
Addsimps [not_Says_to_self]; 

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

53 

1943  54 
(*For reasoning about the encrypted portion of message NS3*) 
3465  55 
goal thy "!!evs. Says S A (Crypt KA {N, B, K, X}) : set evs \ 
2131  56 
\ ==> X : parts (sees lost Spy evs)"; 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

57 
by (blast_tac (!claset addSEs sees_Spy_partsEs) 1); 
2032  58 
qed "NS3_msg_in_parts_sees_Spy"; 
59 

2070  60 
goal thy 
3465  61 
"!!evs. Says Server A (Crypt (shrK A) {NA, B, K, X}) : set evs \ 
2131  62 
\ ==> K : parts (sees lost Spy evs)"; 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

63 
by (blast_tac (!claset addSEs sees_Spy_partsEs) 1); 
2131  64 
qed "Oops_parts_sees_Spy"; 
2070  65 

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

66 
(*For proving the easier theorems about X ~: parts (sees lost Spy evs). 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

67 
We instantiate the variable to "lost" since leaving it as a Var would 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

68 
interfere with simplification.*) 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

69 
val parts_induct_tac = 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

70 
etac ns_shared.induct 1 THEN 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

71 
dres_inst_tac [("lost","lost")] NS3_msg_in_parts_sees_Spy 5 THEN 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

72 
forw_inst_tac [("lost","lost")] Oops_parts_sees_Spy 8 THEN 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

73 
prove_simple_subgoals_tac 1; 
2070  74 

1934  75 

2032  76 
(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY 
2015  77 
sends messages containing X! **) 
1934  78 

2131  79 
(*Spy never sees another agent's shared key! (unless it's lost at start)*) 
1934  80 
goal thy 
2131  81 
"!!evs. evs : ns_shared lost \ 
82 
\ ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)"; 

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

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

84 
by (Fake_parts_insert_tac 1); 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

85 
by (Blast_tac 1); 
2131  86 
qed "Spy_see_shrK"; 
87 
Addsimps [Spy_see_shrK]; 

1934  88 

2131  89 
goal thy 
90 
"!!evs. evs : ns_shared lost \ 

91 
\ ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)"; 

92 
by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset)); 

93 
qed "Spy_analz_shrK"; 

94 
Addsimps [Spy_analz_shrK]; 

1934  95 

2131  96 
goal thy "!!A. [ Key (shrK A) : parts (sees lost Spy evs); \ 
97 
\ evs : ns_shared lost ] ==> A:lost"; 

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

98 
by (blast_tac (!claset addDs [Spy_see_shrK]) 1); 
2131  99 
qed "Spy_see_shrK_D"; 
1934  100 

2131  101 
bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D); 
102 
AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D]; 

1934  103 

2070  104 

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

105 
(*Nobody can have used nonexistent keys!*) 
2160  106 
goal thy "!!evs. evs : ns_shared lost ==> \ 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

107 
\ Key K ~: used evs > K ~: keysFor (parts (sees lost Spy evs))"; 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

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

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

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

111 
(!claset addIs [impOfSubs analz_subset_parts] 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

112 
addDs [impOfSubs (analz_subset_parts RS keysFor_mono), 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

113 
impOfSubs (parts_insert_subset_Un RS keysFor_mono)] 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

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

115 
(*NS2, NS4, NS5*) 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

116 
by (ALLGOALS (blast_tac (!claset addSEs sees_Spy_partsEs))); 
2160  117 
qed_spec_mp "new_keys_not_used"; 
1934  118 

119 
bind_thm ("new_keys_not_analzd", 

2032  120 
[analz_subset_parts RS keysFor_mono, 
121 
new_keys_not_used] MRS contra_subsetD); 

1934  122 

123 
Addsimps [new_keys_not_used, new_keys_not_analzd]; 

124 

125 

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

127 

2015  128 
(*Describes the form of K, X and K' when the Server sends this message.*) 
1934  129 
goal thy 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

130 
"!!evs. [ Says Server A (Crypt K' {N, Agent B, Key K, X}) \ 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

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

132 
\ evs : ns_shared lost ] \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

133 
\ ==> K ~: range shrK & \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

134 
\ X = (Crypt (shrK B) {Key K, Agent A}) & \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

135 
\ K' = shrK A"; 
2032  136 
by (etac rev_mp 1); 
137 
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

138 
by (Auto_tac()); 
1934  139 
qed "Says_Server_message_form"; 
140 

141 

2070  142 
(*If the encrypted message appears then it originated with the Server*) 
1934  143 
goal thy 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

144 
"!!evs. [ Crypt (shrK A) {NA, Agent B, Key K, X} \ 
2070  145 
\ : parts (sees lost Spy evs); \ 
146 
\ A ~: lost; evs : ns_shared lost ] \ 

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

147 
\ ==> X = (Crypt (shrK B) {Key K, Agent A}) & \ 
2070  148 
\ Says Server A \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

149 
\ (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

150 
\ Crypt (shrK B) {Key K, Agent A}}) \ 
3465  151 
\ : set evs"; 
2070  152 
by (etac rev_mp 1); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

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

154 
by (Fake_parts_insert_tac 1); 
2015  155 
by (Auto_tac()); 
2323  156 
qed "A_trusts_NS2"; 
1934  157 

1965  158 

159 
(*EITHER describes the form of X when the following message is sent, 

160 
OR reduces it to the Fake case. 

161 
Use Says_Server_message_form if applicable.*) 

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

163 
"!!evs. [ Says S A (Crypt (shrK A) {Nonce NA, Agent B, Key K, X}) \ 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

164 
\ : set evs; evs : ns_shared lost ] \ 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

165 
\ ==> (K ~: range shrK & 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

166 
\  X : analz (sees lost Spy evs)"; 
2103  167 
by (case_tac "A : lost" 1); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

168 
by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj] 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

169 
addss (!simpset)) 1); 
2070  170 
by (forward_tac [Says_imp_sees_Spy RS parts.Inj] 1); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

171 
by (blast_tac (!claset addEs partsEs 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

172 
addSDs [A_trusts_NS2, Says_Server_message_form]) 1); 
1934  173 
qed "Says_S_message_form"; 
174 

175 

2131  176 
(*For proofs involving analz. We again instantiate the variable to "lost".*) 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

177 
val analz_sees_tac = 
2131  178 
forw_inst_tac [("lost","lost")] Says_Server_message_form 8 THEN 
179 
forw_inst_tac [("lost","lost")] 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

180 
REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE] ORELSE' hyp_subst_tac); 
2131  181 

1934  182 

183 
(**** 

184 
The following is to prove theorems of the form 

185 

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

186 
Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==> 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2374
diff
changeset

187 
Key K : analz (sees lost Spy evs) 
1934  188 

189 
A more general formula must be proved inductively. 

190 

191 
****) 

192 

193 

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

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

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

197 
goal thy 

3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

198 
"!!evs. [ evs : ns_shared lost; Kab ~: range shrK ] ==> \ 
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

199 
\ (Crypt KAB X) : parts (sees lost Spy evs) & \ 
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

200 
\ Key K : parts {X} > Key K : parts (sees lost Spy evs)"; 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

201 
by parts_induct_tac; 
1934  202 
(*Deals with Faked messages*) 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

203 
by (blast_tac (!claset addSEs partsEs 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

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

206 
by (Auto_tac()); 
1934  207 
result(); 
208 

209 

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

211 

2015  212 
(*The equality makes the induction hypothesis easier to apply*) 
1934  213 
goal thy 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

214 
"!!evs. evs : ns_shared lost ==> \ 
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

215 
\ ALL K KK. KK <= Compl (range shrK) > \ 
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

216 
\ (Key K : analz (Key``KK Un (sees lost Spy evs))) = \ 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

217 
\ (K : KK  Key K : analz (sees lost Spy evs))"; 
2032  218 
by (etac ns_shared.induct 1); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

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

220 
by (REPEAT_FIRST (resolve_tac [allI, impI])); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

221 
by (REPEAT_FIRST (rtac analz_image_freshK_lemma )); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

223 
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

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

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

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

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

228 
qed_spec_mp "analz_image_freshK"; 
1934  229 

230 

231 
goal thy 

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

232 
"!!evs. [ evs : ns_shared lost; KAB ~: range shrK ] ==> \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

233 
\ Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

234 
\ (K = KAB  Key K : analz (sees lost Spy evs))"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

235 
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

236 
qed "analz_insert_freshK"; 
1934  237 

238 

2558  239 
(** The session key K uniquely identifies the message **) 
1965  240 

1934  241 
goal thy 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2374
diff
changeset

242 
"!!evs. evs : ns_shared lost ==> \ 
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2374
diff
changeset

243 
\ EX A' NA' B' X'. ALL A NA B X. \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

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

245 
\ : set evs > A=A' & NA=NA' & B=B' & X=X'"; 
2032  246 
by (etac ns_shared.induct 1); 
2070  247 
by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib]))); 
2131  248 
by (Step_tac 1); 
2070  249 
(*NS3*) 
250 
by (ex_strip_tac 2); 

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

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

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

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

255 
by (blast_tac (!claset delrules [conjI] (*prevent splitup into 4 subgoals*) 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

256 
addSEs sees_Spy_partsEs) 1); 
1934  257 
val lemma = result(); 
258 

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

260 
goal thy 

2070  261 
"!!evs. [ Says Server A \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

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

263 
\ : set evs; \ 
2070  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, X'}) \ 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

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

268 
by (prove_unique_tac lemma 1); 
1934  269 
qed "unique_session_keys"; 
270 

271 

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

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

277 
\ (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

278 
\ 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

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

280 
\ (ALL NB. Says A Spy {NA, NB, Key K} ~: set evs) > \ 
2050
1b3343fa1278
Moved sees_lost_agent_subset_sees_Spy to common file, and simplified main thm
paulson
parents:
2045
diff
changeset

281 
\ Key K ~: analz (sees lost Spy evs)"; 
2032  282 
by (etac ns_shared.induct 1); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

283 
by analz_sees_tac; 
1934  284 
by (ALLGOALS 
2015  285 
(asm_simp_tac 
3451
d10f100676d8
Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents:
3441
diff
changeset

286 
(!simpset addsimps ([analz_insert_eq, not_parts_not_analz, 
d10f100676d8
Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents:
3441
diff
changeset

287 
analz_insert_freshK] @ pushes) 
1934  288 
setloop split_tac [expand_if]))); 
3451
d10f100676d8
Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents:
3441
diff
changeset

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

290 
by (blast_tac (!claset addDs [unique_session_keys]) 5); 
d10f100676d8
Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents:
3441
diff
changeset

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

292 
by (Blast_tac 4); 
1934  293 
(*NS2*) 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

294 
by (blast_tac (!claset addSEs sees_Spy_partsEs 
3451
d10f100676d8
Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents:
3441
diff
changeset

295 
addIs [parts_insertI, impOfSubs analz_subset_parts]) 2); 
d10f100676d8
Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents:
3441
diff
changeset

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

297 
by (spy_analz_tac 1); 
2529  298 
(*NS3*) (**LEVEL 6 **) 
2070  299 
by (step_tac (!claset delrules [impCE]) 1); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

300 
by (forward_tac [Says_imp_sees_Spy' RS parts.Inj RS A_trusts_NS2] 1); 
2170  301 
by (assume_tac 2); 
3441
6d2887123fa0
Adapted proofs to the removal of Says_Crypt_lost and Says_Crypt_not_lost
paulson
parents:
3121
diff
changeset

302 
by (blast_tac (!claset addDs [Says_imp_sees_Spy RS analz.Inj RS 
6d2887123fa0
Adapted proofs to the removal of Says_Crypt_lost and Says_Crypt_not_lost
paulson
parents:
3121
diff
changeset

303 
Crypt_Spy_analz_lost]) 1); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

304 
by (blast_tac (!claset addDs [unique_session_keys]) 1); 
2070  305 
val lemma = result() RS mp RS mp RSN(2,rev_notE); 
2015  306 

307 

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

309 
goal thy 

2070  310 
"!!evs. [ Says Server A \ 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

311 
\ (Crypt K' {NA, Agent B, Key K, X}) : set evs; \ 
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

312 
\ (ALL NB. Says A Spy {NA, NB, Key K} ~: set evs); \ 
2070  313 
\ A ~: lost; B ~: lost; evs : ns_shared lost \ 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

314 
\ ] ==> Key K ~: analz (sees lost Spy evs)"; 
2015  315 
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

316 
by (blast_tac (!claset addSDs [lemma]) 1); 
2032  317 
qed "Spy_not_see_encrypted_key"; 
318 

319 

320 
goal thy 

2070  321 
"!!evs. [ C ~: {A,B,Server}; \ 
322 
\ Says Server A \ 

3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

323 
\ (Crypt K' {NA, Agent B, Key K, X}) : set evs; \ 
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

324 
\ (ALL NB. Says A Spy {NA, NB, Key K} ~: set evs); \ 
2070  325 
\ A ~: lost; B ~: lost; evs : ns_shared lost ] \ 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

326 
\ ==> Key K ~: analz (sees lost C evs)"; 
2032  327 
by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1); 
328 
by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1); 

329 
by (FIRSTGOAL (rtac Spy_not_see_encrypted_key)); 

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

330 
by (REPEAT_FIRST (blast_tac (!claset addIs [ns_shared_mono RS subsetD]))); 
2032  331 
qed "Agent_not_see_encrypted_key"; 
2070  332 

333 

334 

335 
(**** Guarantees available at various stages of protocol ***) 

336 

2323  337 
A_trusts_NS2 RS conjunct2 RS Spy_not_see_encrypted_key; 
2070  338 

339 

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

341 
goal thy 

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

342 
"!!evs. [ Crypt (shrK B) {Key K, Agent A} : parts (sees lost Spy evs); \ 
2070  343 
\ B ~: lost; evs : ns_shared lost ] \ 
344 
\ ==> EX NA. Says Server A \ 

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

345 
\ (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

346 
\ Crypt (shrK B) {Key K, Agent A}}) \ 
3465  347 
\ : set evs"; 
2070  348 
by (etac rev_mp 1); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

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

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

352 
by (ALLGOALS Blast_tac); 
2323  353 
qed "B_trusts_NS3"; 
2070  354 

355 

356 
goal thy 

3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

357 
"!!evs. [ B ~: lost; evs : ns_shared lost ] \ 
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

358 
\ ==> Key K ~: analz (sees lost Spy evs) > \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

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

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

361 
\ Crypt K (Nonce NB) : parts (sees lost Spy evs) > \ 
3465  362 
\ Says B A (Crypt K (Nonce NB)) : set evs"; 
2070  363 
by (etac ns_shared.induct 1); 
364 
by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5); 

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

365 
by (dres_inst_tac [("lost","lost")] NS3_msg_in_parts_sees_Spy 5); 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

366 
by (forw_inst_tac [("lost","lost")] Oops_parts_sees_Spy 8); 
2103  367 
by (TRYALL (rtac impI)); 
368 
by (REPEAT_FIRST 

369 
(dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD))); 

370 
by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib]))); 

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

371 
(**LEVEL 7**) 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

372 
by (blast_tac (!claset addSDs [Crypt_Fake_parts_insert] 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

373 
addDs [impOfSubs analz_subset_parts]) 1); 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

374 
by (Blast_tac 2); 
2103  375 
by (REPEAT_FIRST (rtac impI ORELSE' etac conjE ORELSE' hyp_subst_tac)); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

376 
(*Subgoal 1: contradiction from the assumptions 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

377 
Key K ~: used evsa and Crypt K (Nonce NB) : parts (sees lost Spy evsa) *) 
2170  378 
by (dtac Crypt_imp_invKey_keysFor 1); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

379 
(**LEVEL 11**) 
2070  380 
by (Asm_full_simp_tac 1); 
2170  381 
by (rtac disjI1 1); 
2070  382 
by (thin_tac "?PP>?QQ" 1); 
383 
by (case_tac "Ba : lost" 1); 

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

384 
by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj RS B_trusts_NS3, 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

385 
unique_session_keys]) 2); 
3441
6d2887123fa0
Adapted proofs to the removal of Says_Crypt_lost and Says_Crypt_not_lost
paulson
parents:
3121
diff
changeset

386 
by (blast_tac (!claset addDs [Says_imp_sees_Spy RS analz.Inj RS 
6d2887123fa0
Adapted proofs to the removal of Says_Crypt_lost and Says_Crypt_not_lost
paulson
parents:
3121
diff
changeset

387 
Crypt_Spy_analz_lost]) 1); 
2103  388 
val lemma = result(); 
389 

390 
goal thy 

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

391 
"!!evs. [ Crypt K (Nonce NB) : parts (sees lost Spy evs); \ 
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

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

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

394 
\ ALL NB. Says A Spy {NA, NB, Key K} ~: set evs; \ 
2131  395 
\ A ~: lost; B ~: lost; evs : ns_shared lost ] \ 
3465  396 
\ ==> Says B A (Crypt K (Nonce NB)) : set evs"; 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

397 
by (blast_tac (!claset addSIs [lemma RS mp RS mp RS mp] 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

398 
addSEs [Spy_not_see_encrypted_key RSN (2,rev_notE)]) 1); 
2323  399 
qed "A_trusts_NS4"; 