author  paulson 
Fri, 17 Jan 1997 12:49:31 +0100  
changeset 2516  4d68fbe6378b 
parent 2451  ce85a2aafc7a 
child 2637  e9b203f854ae 
permissions  rwrr 
2320  1 
(* Title: HOL/Auth/Shared 
1934  2 
ID: $Id$ 
3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1996 University of Cambridge 

5 

6 
Theory of Shared Keys (common to all symmetrickey protocols) 

7 

8 
Server keys; initial states of agents; new nonces and keys; function "sees" 

2032  9 
*) 
10 

1934  11 

12 
open Shared; 

13 

1964  14 
(*Holds because Friend is injective: thus cannot prove for all f*) 
15 
goal thy "(Friend x : Friend``A) = (x:A)"; 

16 
by (Auto_tac()); 

17 
qed "Friend_image_eq"; 

18 
Addsimps [Friend_image_eq]; 

19 

1934  20 
Addsimps [Un_insert_left, Un_insert_right]; 
21 

22 
(*By default only o_apply is builtin. But in the presence of etaexpansion 

23 
this means that some terms displayed as (f o g) will be rewritten, and others 

24 
will not!*) 

25 
Addsimps [o_def]; 

26 

1943  27 
(*** Basic properties of shrK and newK ***) 
1934  28 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2376
diff
changeset

29 
(*Injectiveness and freshness of new keys and nonces*) 
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2376
diff
changeset

30 
AddIffs [inj_shrK RS inj_eq, inj_newN RS inj_eq, 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

31 
inj_newK RS inj_eq, inj_nPair RS inj_eq]; 
2376
f5c61fd9b9b6
Temporary additions (random) for the nested OtwayRees protocol
paulson
parents:
2320
diff
changeset

32 

1943  33 
(* invKey (shrK A) = shrK A *) 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

34 
bind_thm ("invKey_id", rewrite_rule [isSymKey_def] isSym_keys); 
1934  35 

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

36 
Addsimps [invKey_id]; 
2376
f5c61fd9b9b6
Temporary additions (random) for the nested OtwayRees protocol
paulson
parents:
2320
diff
changeset

37 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2376
diff
changeset

38 
goal thy "!!K. newK i = invKey K ==> newK i = K"; 
2376
f5c61fd9b9b6
Temporary additions (random) for the nested OtwayRees protocol
paulson
parents:
2320
diff
changeset

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

40 
by (Full_simp_tac 1); 
2376
f5c61fd9b9b6
Temporary additions (random) for the nested OtwayRees protocol
paulson
parents:
2320
diff
changeset

41 
val newK_invKey = result(); 
f5c61fd9b9b6
Temporary additions (random) for the nested OtwayRees protocol
paulson
parents:
2320
diff
changeset

42 

f5c61fd9b9b6
Temporary additions (random) for the nested OtwayRees protocol
paulson
parents:
2320
diff
changeset

43 
AddSDs [newK_invKey, sym RS newK_invKey]; 
1934  44 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2376
diff
changeset

45 
Addsimps [newK_neq_shrK, newK_neq_shrK RS not_sym]; 
2320  46 

1934  47 
(** Rewrites should not refer to initState(Friend i) 
48 
 not in normal form! **) 

49 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2376
diff
changeset

50 
goal thy "Key (newK i) ~: parts (initState lost B)"; 
2032  51 
by (agent.induct_tac "B" 1); 
1934  52 
by (Auto_tac ()); 
2032  53 
qed "newK_notin_initState"; 
1934  54 

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

55 
AddIffs [newK_notin_initState]; 
1934  56 

2032  57 
goalw thy [keysFor_def] "keysFor (parts (initState lost C)) = {}"; 
1934  58 
by (agent.induct_tac "C" 1); 
1993  59 
by (auto_tac (!claset addIs [range_eqI], !simpset)); 
1934  60 
qed "keysFor_parts_initState"; 
61 
Addsimps [keysFor_parts_initState]; 

62 

63 
goalw thy [keysFor_def] "keysFor (Key``E) = {}"; 

64 
by (Auto_tac ()); 

65 
qed "keysFor_image_Key"; 

66 
Addsimps [keysFor_image_Key]; 

67 

1943  68 
goal thy "shrK A ~: newK``E"; 
1934  69 
by (agent.induct_tac "A" 1); 
70 
by (Auto_tac ()); 

1943  71 
qed "shrK_notin_image_newK"; 
72 
Addsimps [shrK_notin_image_newK]; 

1934  73 

2032  74 

75 
(*** Function "sees" ***) 

76 

77 
goal thy 

78 
"!!evs. lost' <= lost ==> sees lost' A evs <= sees lost A evs"; 

79 
by (list.induct_tac "evs" 1); 

80 
by (agent.induct_tac "A" 1); 

81 
by (event.induct_tac "a" 2); 

82 
by (Auto_tac ()); 

83 
qed "sees_mono"; 

84 

1964  85 
(*Agents see their own shared keys!*) 
2032  86 
goal thy "A ~= Spy > Key (shrK A) : sees lost A evs"; 
1934  87 
by (list.induct_tac "evs" 1); 
88 
by (agent.induct_tac "A" 1); 

2032  89 
by (Auto_tac ()); 
90 
qed_spec_mp "sees_own_shrK"; 

1934  91 

2032  92 
(*Spy sees shared keys of lost agents!*) 
2045
ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

93 
goal thy "!!A. A: lost ==> Key (shrK A) : sees lost Spy evs"; 
2032  94 
by (list.induct_tac "evs" 1); 
95 
by (Auto_tac()); 

2045
ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

96 
qed "Spy_sees_lost"; 
1934  97 

2045
ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

98 
AddSIs [sees_own_shrK, Spy_sees_lost]; 
2032  99 

2124
9677fdf5fc23
New theorem Crypt_Spy_analz_lost; improvements to spy_analz_tac; ex_strip_tac
paulson
parents:
2109
diff
changeset

100 
(*Added for Yahalom/lost_tac*) 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

101 
goal thy "!!A. [ Crypt (shrK A) X : analz (sees lost Spy evs); A: lost ] \ 
2124
9677fdf5fc23
New theorem Crypt_Spy_analz_lost; improvements to spy_analz_tac; ex_strip_tac
paulson
parents:
2109
diff
changeset

102 
\ ==> X : analz (sees lost Spy evs)"; 
9677fdf5fc23
New theorem Crypt_Spy_analz_lost; improvements to spy_analz_tac; ex_strip_tac
paulson
parents:
2109
diff
changeset

103 
by (fast_tac (!claset addSDs [analz.Decrypt] addss (!simpset)) 1); 
9677fdf5fc23
New theorem Crypt_Spy_analz_lost; improvements to spy_analz_tac; ex_strip_tac
paulson
parents:
2109
diff
changeset

104 
qed "Crypt_Spy_analz_lost"; 
9677fdf5fc23
New theorem Crypt_Spy_analz_lost; improvements to spy_analz_tac; ex_strip_tac
paulson
parents:
2109
diff
changeset

105 

2032  106 
(** Specialized rewrite rules for (sees lost A (Says...#evs)) **) 
2026
0df5a96bf77e
Last working version prior to introduction of "lost"
paulson
parents:
2012
diff
changeset

107 

2078  108 
goal thy "sees lost B (Says A B X # evs) = insert X (sees lost B evs)"; 
1934  109 
by (Simp_tac 1); 
110 
qed "sees_own"; 

111 

2078  112 
goal thy "!!A. Server ~= B ==> \ 
113 
\ sees lost Server (Says A B X # evs) = sees lost Server evs"; 

1934  114 
by (Asm_simp_tac 1); 
115 
qed "sees_Server"; 

116 

2078  117 
goal thy "!!A. Friend i ~= B ==> \ 
118 
\ sees lost (Friend i) (Says A B X # evs) = sees lost (Friend i) evs"; 

1934  119 
by (Asm_simp_tac 1); 
120 
qed "sees_Friend"; 

121 

2032  122 
goal thy "sees lost Spy (Says A B X # evs) = insert X (sees lost Spy evs)"; 
1934  123 
by (Simp_tac 1); 
2032  124 
qed "sees_Spy"; 
1934  125 

2032  126 
goal thy "sees lost A (Says A' B X # evs) <= insert X (sees lost A evs)"; 
1934  127 
by (simp_tac (!simpset setloop split_tac [expand_if]) 1); 
128 
by (Fast_tac 1); 

129 
qed "sees_Says_subset_insert"; 

130 

2032  131 
goal thy "sees lost A evs <= sees lost A (Says A' B X # evs)"; 
1934  132 
by (simp_tac (!simpset setloop split_tac [expand_if]) 1); 
133 
by (Fast_tac 1); 

134 
qed "sees_subset_sees_Says"; 

135 

2132  136 
(*Pushing Unions into parts. One of the agents A is B, and thus sees Y. 
2160  137 
Once used to prove new_keys_not_seen; now obsolete.*) 
2032  138 
goal thy "(UN A. parts (sees lost A (Says B C Y # evs))) = \ 
139 
\ parts {Y} Un (UN A. parts (sees lost A evs))"; 

1934  140 
by (Step_tac 1); 
2132  141 
by (etac rev_mp 1); (*split_tac does not work on assumptions*) 
142 
by (ALLGOALS 

143 
(fast_tac (!claset addss (!simpset addsimps [parts_Un, sees_Cons] 

144 
setloop split_tac [expand_if])))); 

1934  145 
qed "UN_parts_sees_Says"; 
146 

2032  147 
goal thy "Says A B X : set_of_list evs > X : sees lost Spy evs"; 
1934  148 
by (list.induct_tac "evs" 1); 
149 
by (Auto_tac ()); 

2032  150 
qed_spec_mp "Says_imp_sees_Spy"; 
1934  151 

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

152 
(*Use with addSEs to derive contradictions from old Says events containing 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

153 
items known to be fresh*) 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

154 
val sees_Spy_partsEs = make_elim (Says_imp_sees_Spy RS parts.Inj):: partsEs; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

155 

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

157 
"!!evs. [ Says A B (Crypt (shrK C) X) : set_of_list evs; C : lost ] \ 
2064  158 
\ ==> X : analz (sees lost Spy evs)"; 
159 
by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj] 

160 
addss (!simpset)) 1); 

161 
qed "Says_Crypt_lost"; 

162 

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

164 
"!!evs. [ Says A B (Crypt (shrK C) X) : set_of_list evs; \ 
2072  165 
\ X ~: analz (sees lost Spy evs) ] \ 
166 
\ ==> C ~: lost"; 

167 
by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj] 

168 
addss (!simpset)) 1); 

169 
qed "Says_Crypt_not_lost"; 

170 

2320  171 
(*NEEDED??*) 
2032  172 
goal thy "initState lost C <= Key `` range shrK"; 
1934  173 
by (agent.induct_tac "C" 1); 
174 
by (Auto_tac ()); 

175 
qed "initState_subset"; 

176 

2320  177 
(*NEEDED??*) 
2032  178 
goal thy "X : sees lost C evs > \ 
2078  179 
\ (EX A B. Says A B X : set_of_list evs)  (EX A. X = Key (shrK A))"; 
1934  180 
by (list.induct_tac "evs" 1); 
181 
by (ALLGOALS Asm_simp_tac); 

182 
by (fast_tac (!claset addDs [impOfSubs initState_subset]) 1); 

2032  183 
by (rtac conjI 1); 
1934  184 
by (Fast_tac 2); 
185 
by (event.induct_tac "a" 1); 

186 
by (ALLGOALS (asm_simp_tac (!simpset addsimps [mem_if]))); 

187 
by (ALLGOALS Fast_tac); 

188 
qed_spec_mp "seesD"; 

189 

2160  190 
Addsimps [sees_own, sees_Server, sees_Friend, sees_Spy]; 
2032  191 
Delsimps [sees_Cons]; (**** NOTE REMOVAL  laws above are cleaner ****) 
1934  192 

193 

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

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

195 

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

196 
goal thy "Nonce N ~: parts (initState lost B)"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

197 
by (agent.induct_tac "B" 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

199 
qed "Nonce_notin_initState"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

200 

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

201 
AddIffs [Nonce_notin_initState]; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

202 

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

203 
goalw thy [used_def] "!!X. X: parts (sees lost B evs) ==> X: used evs"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

204 
by (etac (impOfSubs parts_mono) 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

206 
qed "usedI"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

207 

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

208 
AddIs [usedI]; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

209 

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

210 
(** Fresh keys never clash with longterm shared keys **) 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

211 

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

212 
goal thy "Key (shrK A) : used evs"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

214 
qed "shrK_in_used"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

215 
AddIffs [shrK_in_used]; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

216 

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

217 
(*Used in parts_Fake_tac and analz_Fake_tac to distinguish session keys 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

218 
from longterm shared keys*) 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

219 
goal thy "!!K. Key K ~: used evs ==> K ~: range shrK"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

221 
qed "Key_not_used"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

222 

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

223 
(*A session key cannot clash with a longterm shared key*) 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

224 
goal thy "!!K. K ~: range shrK ==> shrK B ~= K"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

226 
qed "shrK_neq"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

227 

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

228 
Addsimps [Key_not_used, shrK_neq, shrK_neq RS not_sym]; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

229 

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

230 

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

231 
goal thy "used (Says A B X # evs) = parts{X} Un used evs"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

232 
by (simp_tac (!simpset addsimps [used_def, UN_parts_sees_Says]) 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

233 
qed "used_Says"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

234 
Addsimps [used_Says]; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

235 

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

236 
goal thy "used [] <= used l"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

237 
by (list.induct_tac "l" 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

238 
by (event.induct_tac "a" 2); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

239 
by (ALLGOALS Asm_simp_tac); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

241 
qed "used_nil_subset"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

242 

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

243 
goal thy "used l <= used (l@l')"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

244 
by (list.induct_tac "l" 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

245 
by (simp_tac (!simpset addsimps [used_nil_subset]) 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

246 
by (event.induct_tac "a" 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

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

249 
qed "used_subset_append"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

250 

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

251 

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

252 
(*** Supply fresh nonces for possibility theorems. ***) 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

253 

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

254 
goalw thy [used_def] "EX N. ALL n. N<=n > Nonce n ~: used evs"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

255 
by (list.induct_tac "evs" 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

256 
by (res_inst_tac [("x","0")] exI 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

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

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

260 
by (event.induct_tac "a" 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

261 
by (full_simp_tac (!simpset addsimps [UN_parts_sees_Says]) 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

262 
by (msg.induct_tac "msg" 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

263 
by (ALLGOALS (asm_simp_tac (!simpset addsimps [exI, parts_insert2]))); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

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

266 
by (res_inst_tac [("x","Na+Nb")] exI 2); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

267 
by (fast_tac (!claset addSEs [add_leE]) 2); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

269 
by (res_inst_tac [("x","N + Suc nat")] exI 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

270 
by (fast_tac (!claset addSEs [add_leE] addafter (TRYALL trans_tac)) 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

271 
val lemma = result(); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

272 

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

273 
goal thy "EX N. Nonce N ~: used evs"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

274 
by (rtac (lemma RS exE) 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

276 
qed "Nonce_supply1"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

277 

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

278 
goal thy "EX N N'. Nonce N ~: used evs & Nonce N' ~: used evs' & N ~= N'"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

279 
by (cut_inst_tac [("evs","evs")] lemma 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

280 
by (cut_inst_tac [("evs","evs'")] lemma 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

282 
by (res_inst_tac [("x","N")] exI 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

283 
by (res_inst_tac [("x","Suc (N+Na)")] exI 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

284 
by (asm_simp_tac (!simpset addsimps [less_not_refl2 RS not_sym, 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

286 
le_eq_less_Suc RS sym]) 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

287 
qed "Nonce_supply2"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

288 

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

289 
goal thy "EX N N' N''. Nonce N ~: used evs & Nonce N' ~: used evs' & \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

290 
\ Nonce N'' ~: used evs'' & N ~= N' & N' ~= N'' & N ~= N''"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

291 
by (cut_inst_tac [("evs","evs")] lemma 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

292 
by (cut_inst_tac [("evs","evs'")] lemma 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

293 
by (cut_inst_tac [("evs","evs''")] lemma 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

295 
by (res_inst_tac [("x","N")] exI 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

296 
by (res_inst_tac [("x","Suc (N+Na)")] exI 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

297 
by (res_inst_tac [("x","Suc (Suc (N+Na+Nb))")] exI 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

298 
by (asm_simp_tac (!simpset addsimps [less_not_refl2 RS not_sym, 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

300 
le_eq_less_Suc RS sym]) 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

301 
by (rtac (less_trans RS less_not_refl2 RS not_sym) 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

302 
by (stac (le_eq_less_Suc RS sym) 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

303 
by (asm_simp_tac (!simpset addsimps [le_eq_less_Suc RS sym]) 2); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

304 
by (REPEAT (rtac le_add1 1)); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

305 
qed "Nonce_supply3"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

306 

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

307 
goal thy "Nonce (@ N. Nonce N ~: used evs) ~: used evs"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

308 
by (rtac (lemma RS exE) 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

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

311 
qed "Nonce_supply"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

312 

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

313 
(*** Supply fresh keys for possibility theorems. ***) 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

314 

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

315 
goal thy "EX K. Key K ~: used evs"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

316 
by (rtac (Fin.emptyI RS Key_supply_ax RS exE) 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

318 
qed "Key_supply1"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

319 

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

320 
val Fin_UNIV_insertI = UNIV_I RS Fin.insertI; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

321 

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

322 
goal thy "EX K K'. Key K ~: used evs & Key K' ~: used evs' & K ~= K'"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

323 
by (cut_inst_tac [("evs","evs")] (Fin.emptyI RS Key_supply_ax) 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

325 
by (cut_inst_tac [("evs","evs'")] 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

326 
(Fin.emptyI RS Fin_UNIV_insertI RS Key_supply_ax) 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

328 
qed "Key_supply2"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

329 

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

330 
goal thy "EX K K' K''. Key K ~: used evs & Key K' ~: used evs' & \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

331 
\ Key K'' ~: used evs'' & K ~= K' & K' ~= K'' & K ~= K''"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

332 
by (cut_inst_tac [("evs","evs")] (Fin.emptyI RS Key_supply_ax) 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

334 
by (cut_inst_tac [("evs","evs'")] 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

335 
(Fin.emptyI RS Fin_UNIV_insertI RS Key_supply_ax) 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

337 
by (cut_inst_tac [("evs","evs''")] 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

338 
(Fin.emptyI RS Fin_UNIV_insertI RS Fin_UNIV_insertI RS Key_supply_ax) 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

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

341 
by (fast_tac (!claset addSEs [allE]) 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

342 
qed "Key_supply3"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

343 

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

344 
goal thy "Key (@ K. Key K ~: used evs) ~: used evs"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

345 
by (rtac (Fin.emptyI RS Key_supply_ax RS exE) 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

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

348 
qed "Key_supply"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

349 

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

350 
(*** Tactics for possibility theorems ***) 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

351 

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

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

353 
REPEAT (*omit used_Says so that Nonces, Keys start from different traces!*) 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

355 
(!simpset delsimps [used_Says] setsolver safe_solver)) 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

357 
REPEAT_FIRST (eq_assume_tac ORELSE' 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

358 
resolve_tac [refl, conjI, Nonce_supply, Key_supply])); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

359 

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

360 
(*For harder protocols (such as Recur) where we have to set up some 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

361 
nonces and keys initially*) 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

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

364 
(ALLGOALS (asm_simp_tac (!simpset setsolver safe_solver)) 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

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

367 

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

368 

2049
d3b93e1765bc
Moved sees_lost_agent_subset_sees_Spy to common file
paulson
parents:
2045
diff
changeset

369 
(** Power of the Spy **) 
1934  370 

2049
d3b93e1765bc
Moved sees_lost_agent_subset_sees_Spy to common file
paulson
parents:
2045
diff
changeset

371 
(*The Spy can see more than anybody else, except for their initial state*) 
d3b93e1765bc
Moved sees_lost_agent_subset_sees_Spy to common file
paulson
parents:
2045
diff
changeset

372 
goal thy "sees lost A evs <= initState lost A Un sees lost Spy evs"; 
d3b93e1765bc
Moved sees_lost_agent_subset_sees_Spy to common file
paulson
parents:
2045
diff
changeset

373 
by (list.induct_tac "evs" 1); 
d3b93e1765bc
Moved sees_lost_agent_subset_sees_Spy to common file
paulson
parents:
2045
diff
changeset

374 
by (event.induct_tac "a" 2); 
d3b93e1765bc
Moved sees_lost_agent_subset_sees_Spy to common file
paulson
parents:
2045
diff
changeset

375 
by (ALLGOALS (fast_tac (!claset addDs [sees_Says_subset_insert RS subsetD] 
d3b93e1765bc
Moved sees_lost_agent_subset_sees_Spy to common file
paulson
parents:
2045
diff
changeset

376 
addss (!simpset)))); 
d3b93e1765bc
Moved sees_lost_agent_subset_sees_Spy to common file
paulson
parents:
2045
diff
changeset

377 
qed "sees_agent_subset_sees_Spy"; 
d3b93e1765bc
Moved sees_lost_agent_subset_sees_Spy to common file
paulson
parents:
2045
diff
changeset

378 

d3b93e1765bc
Moved sees_lost_agent_subset_sees_Spy to common file
paulson
parents:
2045
diff
changeset

379 
(*The Spy can see more than anybody else who's lost their key!*) 
d3b93e1765bc
Moved sees_lost_agent_subset_sees_Spy to common file
paulson
parents:
2045
diff
changeset

380 
goal thy "A: lost > A ~= Server > sees lost A evs <= sees lost Spy evs"; 
d3b93e1765bc
Moved sees_lost_agent_subset_sees_Spy to common file
paulson
parents:
2045
diff
changeset

381 
by (list.induct_tac "evs" 1); 
d3b93e1765bc
Moved sees_lost_agent_subset_sees_Spy to common file
paulson
parents:
2045
diff
changeset

382 
by (event.induct_tac "a" 2); 
d3b93e1765bc
Moved sees_lost_agent_subset_sees_Spy to common file
paulson
parents:
2045
diff
changeset

383 
by (agent.induct_tac "A" 1); 
d3b93e1765bc
Moved sees_lost_agent_subset_sees_Spy to common file
paulson
parents:
2045
diff
changeset

384 
by (auto_tac (!claset addDs [sees_Says_subset_insert RS subsetD], (!simpset))); 
d3b93e1765bc
Moved sees_lost_agent_subset_sees_Spy to common file
paulson
parents:
2045
diff
changeset

385 
qed_spec_mp "sees_lost_agent_subset_sees_Spy"; 
d3b93e1765bc
Moved sees_lost_agent_subset_sees_Spy to common file
paulson
parents:
2045
diff
changeset

386 

1934  387 

2032  388 
(** Simplifying parts (insert X (sees lost A evs)) 
2045
ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

389 
= parts {X} Un parts (sees lost A evs)  since general case loops*) 
2012  390 

391 
val parts_insert_sees = 

2045
ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

392 
parts_insert > read_instantiate_sg (sign_of thy) 
ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

393 
[("H", "sees lost A evs")] 
2012  394 
> standard; 
2045
ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

395 

ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

396 

2049
d3b93e1765bc
Moved sees_lost_agent_subset_sees_Spy to common file
paulson
parents:
2045
diff
changeset

397 
(*** Specialized rewriting for analz_insert_Key_newK ***) 
d3b93e1765bc
Moved sees_lost_agent_subset_sees_Spy to common file
paulson
parents:
2045
diff
changeset

398 

2320  399 
(*Push newK applications in, allowing other keys to be pulled out*) 
400 
val pushKey_newK = insComm thy "Key (newK ?evs)" "Key (shrK ?C)"; 

401 

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

402 
goal thy "!!A. A <= Compl (range shrK) ==> shrK x ~: A"; 
2045
ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

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

404 
qed "subset_Compl_range"; 
2045
ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

405 

ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

406 
goal thy "insert (Key (f x)) (Key``(f``E) Un C) = \ 
ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

407 
\ Key `` (f `` (insert x E)) Un C"; 
ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

408 
by (Fast_tac 1); 
ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

409 
qed "insert_Key_image"; 
ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

410 

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

411 
goal thy "insert (Key K) H = Key `` {K} Un H"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

413 
qed "insert_Key_singleton"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

414 

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

415 
goal thy "insert (Key K) (Key``KK Un C) = Key `` (insert K KK) Un C"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

417 
qed "insert_Key_image'"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

418 

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

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

420 
!simpset delsimps [image_insert, image_Un] 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

421 
addsimps ([image_insert RS sym, image_Un RS sym, 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

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

424 
insert_Key_image', Un_assoc RS sym] 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

426 
setloop split_tac [expand_if]; 
2045
ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

427 

ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

428 
(*Lemma for the trivial direction of the ifandonlyif*) 
ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

429 
goal thy 
ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

430 
"!!evs. (Key K : analz (Key``nE Un H)) > (K : nE  Key K : analz H) ==> \ 
ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

431 
\ (Key K : analz (Key``nE Un H)) = (K : nE  Key K : analz H)"; 
ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

432 
by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

433 
qed "analz_image_freshK_lemma"; 