author  paulson 
Fri, 13 Sep 1996 18:46:08 +0200  
changeset 1998  f8230821f1e8 
parent 1994  4ddfafdeefa4 
child 2011  d9af64c26be6 
permissions  rwrr 
1839  1 
(* Title: HOL/Auth/Message 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1996 University of Cambridge 

5 

6 
Datatypes of agents and messages; 

1913  7 
Inductive relations "parts", "analz" and "synth" 
1839  8 
*) 
9 

10 
open Message; 

11 

12 

13 
(** Inverse of keys **) 

14 

15 
goal thy "!!K K'. (invKey K = invKey K') = (K=K')"; 

16 
by (Step_tac 1); 

17 
br box_equals 1; 

18 
by (REPEAT (rtac invKey 2)); 

19 
by (Asm_simp_tac 1); 

20 
qed "invKey_eq"; 

21 

22 
Addsimps [invKey, invKey_eq]; 

23 

24 

25 
(**** keysFor operator ****) 

26 

27 
goalw thy [keysFor_def] "keysFor {} = {}"; 

28 
by (Fast_tac 1); 

29 
qed "keysFor_empty"; 

30 

31 
goalw thy [keysFor_def] "keysFor (H Un H') = keysFor H Un keysFor H'"; 

32 
by (Fast_tac 1); 

33 
qed "keysFor_Un"; 

34 

35 
goalw thy [keysFor_def] "keysFor (UN i. H i) = (UN i. keysFor (H i))"; 

36 
by (Fast_tac 1); 

37 
qed "keysFor_UN"; 

38 

39 
(*Monotonicity*) 

40 
goalw thy [keysFor_def] "!!G H. G<=H ==> keysFor(G) <= keysFor(H)"; 

41 
by (Fast_tac 1); 

42 
qed "keysFor_mono"; 

43 

44 
goalw thy [keysFor_def] "keysFor (insert (Agent A) H) = keysFor H"; 

45 
by (fast_tac (!claset addss (!simpset)) 1); 

46 
qed "keysFor_insert_Agent"; 

47 

48 
goalw thy [keysFor_def] "keysFor (insert (Nonce N) H) = keysFor H"; 

49 
by (fast_tac (!claset addss (!simpset)) 1); 

50 
qed "keysFor_insert_Nonce"; 

51 

52 
goalw thy [keysFor_def] "keysFor (insert (Key K) H) = keysFor H"; 

53 
by (fast_tac (!claset addss (!simpset)) 1); 

54 
qed "keysFor_insert_Key"; 

55 

56 
goalw thy [keysFor_def] "keysFor (insert {X,Y} H) = keysFor H"; 

57 
by (fast_tac (!claset addss (!simpset)) 1); 

58 
qed "keysFor_insert_MPair"; 

59 

60 
goalw thy [keysFor_def] 

61 
"keysFor (insert (Crypt X K) H) = insert (invKey K) (keysFor H)"; 

62 
by (Auto_tac()); 

1964  63 
by (Fast_tac 1); 
1839  64 
qed "keysFor_insert_Crypt"; 
65 

66 
Addsimps [keysFor_empty, keysFor_Un, keysFor_UN, 

67 
keysFor_insert_Agent, keysFor_insert_Nonce, 

68 
keysFor_insert_Key, keysFor_insert_MPair, 

69 
keysFor_insert_Crypt]; 

70 

71 

72 
(**** Inductive relation "parts" ****) 

73 

74 
val major::prems = 

75 
goal thy "[ {X,Y} : parts H; \ 

76 
\ [ X : parts H; Y : parts H ] ==> P \ 

77 
\ ] ==> P"; 

78 
by (cut_facts_tac [major] 1); 

79 
brs prems 1; 

80 
by (REPEAT (eresolve_tac [asm_rl, parts.Fst, parts.Snd] 1)); 

81 
qed "MPair_parts"; 

82 

83 
AddIs [parts.Inj]; 

1929
f0839bab4b00
Working version of NS, messages 13, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset

84 

f0839bab4b00
Working version of NS, messages 13, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset

85 
val partsEs = [MPair_parts, make_elim parts.Body]; 
f0839bab4b00
Working version of NS, messages 13, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset

86 

f0839bab4b00
Working version of NS, messages 13, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset

87 
AddSEs partsEs; 
f0839bab4b00
Working version of NS, messages 13, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset

88 
(*NB These two rules are UNSAFE in the formal sense, as they discard the 
f0839bab4b00
Working version of NS, messages 13, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset

89 
compound message. They work well on THIS FILE, perhaps because its 
f0839bab4b00
Working version of NS, messages 13, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset

90 
proofs concern only atomic messages.*) 
1839  91 

92 
goal thy "H <= parts(H)"; 

93 
by (Fast_tac 1); 

94 
qed "parts_increasing"; 

95 

96 
(*Monotonicity*) 

97 
goalw thy parts.defs "!!G H. G<=H ==> parts(G) <= parts(H)"; 

98 
by (rtac lfp_mono 1); 

99 
by (REPEAT (ares_tac basic_monos 1)); 

100 
qed "parts_mono"; 

101 

102 
goal thy "parts{} = {}"; 

103 
by (Step_tac 1); 

104 
be parts.induct 1; 

105 
by (ALLGOALS Fast_tac); 

106 
qed "parts_empty"; 

107 
Addsimps [parts_empty]; 

108 

109 
goal thy "!!X. X: parts{} ==> P"; 

110 
by (Asm_full_simp_tac 1); 

111 
qed "parts_emptyE"; 

112 
AddSEs [parts_emptyE]; 

113 

1893  114 
(*WARNING: loops if H = {Y}, therefore must not be repeated!*) 
115 
goal thy "!!H. X: parts H ==> EX Y:H. X: parts {Y}"; 

116 
be parts.induct 1; 

117 
by (ALLGOALS Fast_tac); 

118 
qed "parts_singleton"; 

119 

1839  120 

121 
(** Unions **) 

122 

123 
goal thy "parts(G) Un parts(H) <= parts(G Un H)"; 

124 
by (REPEAT (ares_tac [Un_least, parts_mono, Un_upper1, Un_upper2] 1)); 

125 
val parts_Un_subset1 = result(); 

126 

127 
goal thy "parts(G Un H) <= parts(G) Un parts(H)"; 

128 
br subsetI 1; 

129 
be parts.induct 1; 

130 
by (ALLGOALS Fast_tac); 

131 
val parts_Un_subset2 = result(); 

132 

133 
goal thy "parts(G Un H) = parts(G) Un parts(H)"; 

134 
by (REPEAT (ares_tac [equalityI, parts_Un_subset1, parts_Un_subset2] 1)); 

135 
qed "parts_Un"; 

136 

1852  137 
(*TWO inserts to avoid looping. This rewrite is better than nothing...*) 
138 
goal thy "parts (insert X (insert Y H)) = parts {X} Un parts {Y} Un parts H"; 

139 
by (stac (read_instantiate [("A","H")] insert_is_Un) 1); 

140 
by (stac (read_instantiate [("A","{Y} Un H")] insert_is_Un) 1); 

141 
by (simp_tac (HOL_ss addsimps [parts_Un, Un_assoc]) 1); 

142 
qed "parts_insert2"; 

143 

1839  144 
goal thy "(UN x:A. parts(H x)) <= parts(UN x:A. H x)"; 
145 
by (REPEAT (ares_tac [UN_least, parts_mono, UN_upper] 1)); 

146 
val parts_UN_subset1 = result(); 

147 

148 
goal thy "parts(UN x:A. H x) <= (UN x:A. parts(H x))"; 

149 
br subsetI 1; 

150 
be parts.induct 1; 

151 
by (ALLGOALS Fast_tac); 

152 
val parts_UN_subset2 = result(); 

153 

154 
goal thy "parts(UN x:A. H x) = (UN x:A. parts(H x))"; 

155 
by (REPEAT (ares_tac [equalityI, parts_UN_subset1, parts_UN_subset2] 1)); 

156 
qed "parts_UN"; 

157 

158 
goal thy "parts(UN x. H x) = (UN x. parts(H x))"; 

159 
by (simp_tac (!simpset addsimps [UNION1_def, parts_UN]) 1); 

160 
qed "parts_UN1"; 

161 

1913  162 
(*Added to simplify arguments to parts, analz and synth*) 
1839  163 
Addsimps [parts_Un, parts_UN, parts_UN1]; 
164 

165 
goal thy "insert X (parts H) <= parts(insert X H)"; 

1852  166 
by (fast_tac (!claset addEs [impOfSubs parts_mono]) 1); 
1839  167 
qed "parts_insert_subset"; 
168 

169 
(** Idempotence and transitivity **) 

170 

171 
goal thy "!!H. X: parts (parts H) ==> X: parts H"; 

172 
be parts.induct 1; 

173 
by (ALLGOALS Fast_tac); 

174 
qed "parts_partsE"; 

175 
AddSEs [parts_partsE]; 

176 

177 
goal thy "parts (parts H) = parts H"; 

178 
by (Fast_tac 1); 

179 
qed "parts_idem"; 

180 
Addsimps [parts_idem]; 

181 

182 
goal thy "!!H. [ X: parts G; G <= parts H ] ==> X: parts H"; 

183 
by (dtac parts_mono 1); 

184 
by (Fast_tac 1); 

185 
qed "parts_trans"; 

186 

187 
(*Cut*) 

1998
f8230821f1e8
Reordering of premises for cut theorems, and new law MPair_synth_analz
paulson
parents:
1994
diff
changeset

188 
goal thy "!!H. [ Y: parts (insert X H); X: parts H ] ==> Y: parts H"; 
1839  189 
be parts_trans 1; 
190 
by (Fast_tac 1); 

191 
qed "parts_cut"; 

192 

1929
f0839bab4b00
Working version of NS, messages 13, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset

193 
goal thy "!!H. X: parts H ==> parts (insert X H) = parts H"; 
f0839bab4b00
Working version of NS, messages 13, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset

194 
by (fast_tac (!claset addSEs [parts_cut] 
f0839bab4b00
Working version of NS, messages 13, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset

195 
addIs [impOfSubs (subset_insertI RS parts_mono)]) 1); 
f0839bab4b00
Working version of NS, messages 13, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset

196 
qed "parts_cut_eq"; 
f0839bab4b00
Working version of NS, messages 13, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset

197 

1839  198 

199 
(** Rewrite rules for pulling out atomic messages **) 

200 

201 
goal thy "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)"; 

202 
by (rtac (parts_insert_subset RSN (2, equalityI)) 1); 

203 
br subsetI 1; 

204 
be parts.induct 1; 

205 
(*Simplification breaks up equalities between messages; 

206 
how to make it work for fast_tac??*) 

207 
by (ALLGOALS (fast_tac (!claset addss (!simpset)))); 

208 
qed "parts_insert_Agent"; 

209 

210 
goal thy "parts (insert (Nonce N) H) = insert (Nonce N) (parts H)"; 

211 
by (rtac (parts_insert_subset RSN (2, equalityI)) 1); 

212 
br subsetI 1; 

213 
be parts.induct 1; 

214 
by (ALLGOALS (fast_tac (!claset addss (!simpset)))); 

215 
qed "parts_insert_Nonce"; 

216 

217 
goal thy "parts (insert (Key K) H) = insert (Key K) (parts H)"; 

218 
by (rtac (parts_insert_subset RSN (2, equalityI)) 1); 

219 
br subsetI 1; 

220 
be parts.induct 1; 

221 
by (ALLGOALS (fast_tac (!claset addss (!simpset)))); 

222 
qed "parts_insert_Key"; 

223 

224 
goal thy "parts (insert (Crypt X K) H) = \ 

225 
\ insert (Crypt X K) (parts (insert X H))"; 

226 
br equalityI 1; 

227 
br subsetI 1; 

228 
be parts.induct 1; 

229 
by (Auto_tac()); 

230 
be parts.induct 1; 

231 
by (ALLGOALS (best_tac (!claset addIs [parts.Body]))); 

232 
qed "parts_insert_Crypt"; 

233 

234 
goal thy "parts (insert {X,Y} H) = \ 

235 
\ insert {X,Y} (parts (insert X (insert Y H)))"; 

236 
br equalityI 1; 

237 
br subsetI 1; 

238 
be parts.induct 1; 

239 
by (Auto_tac()); 

240 
be parts.induct 1; 

241 
by (ALLGOALS (best_tac (!claset addIs [parts.Fst, parts.Snd]))); 

242 
qed "parts_insert_MPair"; 

243 

244 
Addsimps [parts_insert_Agent, parts_insert_Nonce, 

245 
parts_insert_Key, parts_insert_Crypt, parts_insert_MPair]; 

246 

247 

1913  248 
(**** Inductive relation "analz" ****) 
1839  249 

250 
val major::prems = 

1913  251 
goal thy "[ {X,Y} : analz H; \ 
252 
\ [ X : analz H; Y : analz H ] ==> P \ 

1839  253 
\ ] ==> P"; 
254 
by (cut_facts_tac [major] 1); 

255 
brs prems 1; 

1913  256 
by (REPEAT (eresolve_tac [asm_rl, analz.Fst, analz.Snd] 1)); 
257 
qed "MPair_analz"; 

1839  258 

1913  259 
AddIs [analz.Inj]; 
260 
AddSEs [MPair_analz]; 

261 
AddDs [analz.Decrypt]; 

1839  262 

1913  263 
Addsimps [analz.Inj]; 
1885  264 

1913  265 
goal thy "H <= analz(H)"; 
1839  266 
by (Fast_tac 1); 
1913  267 
qed "analz_increasing"; 
1839  268 

1913  269 
goal thy "analz H <= parts H"; 
1839  270 
by (rtac subsetI 1); 
1913  271 
be analz.induct 1; 
1839  272 
by (ALLGOALS Fast_tac); 
1913  273 
qed "analz_subset_parts"; 
1839  274 

1913  275 
bind_thm ("not_parts_not_analz", analz_subset_parts RS contra_subsetD); 
1839  276 

277 

1913  278 
goal thy "parts (analz H) = parts H"; 
1839  279 
br equalityI 1; 
1913  280 
br (analz_subset_parts RS parts_mono RS subset_trans) 1; 
1839  281 
by (Simp_tac 1); 
1913  282 
by (fast_tac (!claset addDs [analz_increasing RS parts_mono RS subsetD]) 1); 
283 
qed "parts_analz"; 

284 
Addsimps [parts_analz]; 

1839  285 

1913  286 
goal thy "analz (parts H) = parts H"; 
1885  287 
by (Auto_tac()); 
1913  288 
be analz.induct 1; 
1885  289 
by (Auto_tac()); 
1913  290 
qed "analz_parts"; 
291 
Addsimps [analz_parts]; 

1885  292 

1839  293 
(*Monotonicity; Lemma 1 of Lowe*) 
1913  294 
goalw thy analz.defs "!!G H. G<=H ==> analz(G) <= analz(H)"; 
1839  295 
by (rtac lfp_mono 1); 
296 
by (REPEAT (ares_tac basic_monos 1)); 

1913  297 
qed "analz_mono"; 
1839  298 

299 
(** General equational properties **) 

300 

1913  301 
goal thy "analz{} = {}"; 
1839  302 
by (Step_tac 1); 
1913  303 
be analz.induct 1; 
1839  304 
by (ALLGOALS Fast_tac); 
1913  305 
qed "analz_empty"; 
306 
Addsimps [analz_empty]; 

1839  307 

1913  308 
(*Converse fails: we can analz more from the union than from the 
1839  309 
separate parts, as a key in one might decrypt a message in the other*) 
1913  310 
goal thy "analz(G) Un analz(H) <= analz(G Un H)"; 
311 
by (REPEAT (ares_tac [Un_least, analz_mono, Un_upper1, Un_upper2] 1)); 

312 
qed "analz_Un"; 

1839  313 

1913  314 
goal thy "insert X (analz H) <= analz(insert X H)"; 
315 
by (fast_tac (!claset addEs [impOfSubs analz_mono]) 1); 

316 
qed "analz_insert"; 

1839  317 

318 
(** Rewrite rules for pulling out atomic messages **) 

319 

1913  320 
goal thy "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)"; 
321 
by (rtac (analz_insert RSN (2, equalityI)) 1); 

1839  322 
br subsetI 1; 
1913  323 
be analz.induct 1; 
1839  324 
(*Simplification breaks up equalities between messages; 
325 
how to make it work for fast_tac??*) 

326 
by (ALLGOALS (fast_tac (!claset addss (!simpset)))); 

1913  327 
qed "analz_insert_Agent"; 
1839  328 

1913  329 
goal thy "analz (insert (Nonce N) H) = insert (Nonce N) (analz H)"; 
330 
by (rtac (analz_insert RSN (2, equalityI)) 1); 

1839  331 
br subsetI 1; 
1913  332 
be analz.induct 1; 
1839  333 
by (ALLGOALS (fast_tac (!claset addss (!simpset)))); 
1913  334 
qed "analz_insert_Nonce"; 
1839  335 

336 
(*Can only pull out Keys if they are not needed to decrypt the rest*) 

337 
goalw thy [keysFor_def] 

1913  338 
"!!K. K ~: keysFor (analz H) ==> \ 
339 
\ analz (insert (Key K) H) = insert (Key K) (analz H)"; 

340 
by (rtac (analz_insert RSN (2, equalityI)) 1); 

1839  341 
br subsetI 1; 
1913  342 
be analz.induct 1; 
1839  343 
by (ALLGOALS (fast_tac (!claset addss (!simpset)))); 
1913  344 
qed "analz_insert_Key"; 
1839  345 

1913  346 
goal thy "analz (insert {X,Y} H) = \ 
347 
\ insert {X,Y} (analz (insert X (insert Y H)))"; 

1885  348 
br equalityI 1; 
349 
br subsetI 1; 

1913  350 
be analz.induct 1; 
1885  351 
by (Auto_tac()); 
1913  352 
be analz.induct 1; 
353 
by (ALLGOALS (deepen_tac (!claset addIs [analz.Fst, analz.Snd, analz.Decrypt]) 0)); 

354 
qed "analz_insert_MPair"; 

1885  355 

356 
(*Can pull out enCrypted message if the Key is not known*) 

1913  357 
goal thy "!!H. Key (invKey K) ~: analz H ==> \ 
358 
\ analz (insert (Crypt X K) H) = \ 

359 
\ insert (Crypt X K) (analz H)"; 

360 
by (rtac (analz_insert RSN (2, equalityI)) 1); 

1839  361 
br subsetI 1; 
1913  362 
be analz.induct 1; 
1839  363 
by (ALLGOALS (fast_tac (!claset addss (!simpset)))); 
1913  364 
qed "analz_insert_Crypt"; 
1839  365 

1913  366 
goal thy "!!H. Key (invKey K) : analz H ==> \ 
367 
\ analz (insert (Crypt X K) H) <= \ 

368 
\ insert (Crypt X K) (analz (insert X H))"; 

1839  369 
br subsetI 1; 
1913  370 
by (eres_inst_tac [("za","x")] analz.induct 1); 
1839  371 
by (ALLGOALS (fast_tac (!claset addss (!simpset)))); 
372 
val lemma1 = result(); 

373 

1913  374 
goal thy "!!H. Key (invKey K) : analz H ==> \ 
375 
\ insert (Crypt X K) (analz (insert X H)) <= \ 

376 
\ analz (insert (Crypt X K) H)"; 

1839  377 
by (Auto_tac()); 
1913  378 
by (eres_inst_tac [("za","x")] analz.induct 1); 
1839  379 
by (Auto_tac()); 
1913  380 
by (best_tac (!claset addIs [subset_insertI RS analz_mono RS subsetD, 
381 
analz.Decrypt]) 1); 

1839  382 
val lemma2 = result(); 
383 

1913  384 
goal thy "!!H. Key (invKey K) : analz H ==> \ 
385 
\ analz (insert (Crypt X K) H) = \ 

386 
\ insert (Crypt X K) (analz (insert X H))"; 

1839  387 
by (REPEAT (ares_tac [equalityI, lemma1, lemma2] 1)); 
1913  388 
qed "analz_insert_Decrypt"; 
1839  389 

1885  390 
(*Case analysis: either the message is secure, or it is not! 
1946  391 
Effective, but can cause subgoals to blow up! 
1885  392 
Use with expand_if; apparently split_tac does not cope with patterns 
1913  393 
such as "analz (insert (Crypt X' K) H)" *) 
394 
goal thy "analz (insert (Crypt X' K) H) = \ 

395 
\ (if (Key (invKey K) : analz H) then \ 

396 
\ insert (Crypt X' K) (analz (insert X' H)) \ 

397 
\ else insert (Crypt X' K) (analz H))"; 

398 
by (excluded_middle_tac "Key (invKey K) : analz H " 1); 

399 
by (ALLGOALS (asm_simp_tac (!simpset addsimps [analz_insert_Crypt, 

400 
analz_insert_Decrypt]))); 

401 
qed "analz_Crypt_if"; 

1885  402 

1913  403 
Addsimps [analz_insert_Agent, analz_insert_Nonce, 
404 
analz_insert_Key, analz_insert_MPair, 

405 
analz_Crypt_if]; 

1839  406 

407 
(*This rule supposes "for the sake of argument" that we have the key.*) 

1913  408 
goal thy "analz (insert (Crypt X K) H) <= \ 
409 
\ insert (Crypt X K) (analz (insert X H))"; 

1839  410 
br subsetI 1; 
1913  411 
be analz.induct 1; 
1839  412 
by (Auto_tac()); 
1913  413 
qed "analz_insert_Crypt_subset"; 
1839  414 

415 

416 
(** Idempotence and transitivity **) 

417 

1913  418 
goal thy "!!H. X: analz (analz H) ==> X: analz H"; 
419 
be analz.induct 1; 

1839  420 
by (ALLGOALS Fast_tac); 
1913  421 
qed "analz_analzE"; 
422 
AddSEs [analz_analzE]; 

1839  423 

1913  424 
goal thy "analz (analz H) = analz H"; 
1839  425 
by (Fast_tac 1); 
1913  426 
qed "analz_idem"; 
427 
Addsimps [analz_idem]; 

1839  428 

1913  429 
goal thy "!!H. [ X: analz G; G <= analz H ] ==> X: analz H"; 
430 
by (dtac analz_mono 1); 

1839  431 
by (Fast_tac 1); 
1913  432 
qed "analz_trans"; 
1839  433 

434 
(*Cut; Lemma 2 of Lowe*) 

1998
f8230821f1e8
Reordering of premises for cut theorems, and new law MPair_synth_analz
paulson
parents:
1994
diff
changeset

435 
goal thy "!!H. [ Y: analz (insert X H); X: analz H ] ==> Y: analz H"; 
1913  436 
be analz_trans 1; 
1839  437 
by (Fast_tac 1); 
1913  438 
qed "analz_cut"; 
1839  439 

440 
(*Cut can be proved easily by induction on 

1913  441 
"!!H. Y: analz (insert X H) ==> X: analz H > Y: analz H" 
1839  442 
*) 
443 

1885  444 

1913  445 
(** A congruence rule for "analz" **) 
1885  446 

1913  447 
goal thy "!!H. [ analz G <= analz G'; analz H <= analz H' \ 
448 
\ ] ==> analz (G Un H) <= analz (G' Un H')"; 

1885  449 
by (Step_tac 1); 
1913  450 
be analz.induct 1; 
451 
by (ALLGOALS (best_tac (!claset addIs [analz_mono RS subsetD]))); 

452 
qed "analz_subset_cong"; 

1885  453 

1913  454 
goal thy "!!H. [ analz G = analz G'; analz H = analz H' \ 
455 
\ ] ==> analz (G Un H) = analz (G' Un H')"; 

456 
by (REPEAT_FIRST (ares_tac [equalityI, analz_subset_cong] 

1885  457 
ORELSE' etac equalityE)); 
1913  458 
qed "analz_cong"; 
1885  459 

460 

1913  461 
goal thy "!!H. analz H = analz H' ==> analz(insert X H) = analz(insert X H')"; 
1885  462 
by (asm_simp_tac (!simpset addsimps [insert_def] 
1913  463 
setloop (rtac analz_cong)) 1); 
464 
qed "analz_insert_cong"; 

1885  465 

1913  466 
(*If there are no pairs or encryptions then analz does nothing*) 
1839  467 
goal thy "!!H. [ ALL X Y. {X,Y} ~: H; ALL X K. Crypt X K ~: H ] ==> \ 
1913  468 
\ analz H = H"; 
1839  469 
by (Step_tac 1); 
1913  470 
be analz.induct 1; 
1839  471 
by (ALLGOALS Fast_tac); 
1913  472 
qed "analz_trivial"; 
1839  473 

474 
(*Helps to prove Fake cases*) 

1913  475 
goal thy "!!X. X: analz (UN i. analz (H i)) ==> X: analz (UN i. H i)"; 
476 
be analz.induct 1; 

477 
by (ALLGOALS (fast_tac (!claset addEs [impOfSubs analz_mono]))); 

1839  478 
val lemma = result(); 
479 

1913  480 
goal thy "analz (UN i. analz (H i)) = analz (UN i. H i)"; 
1839  481 
by (fast_tac (!claset addIs [lemma] 
1913  482 
addEs [impOfSubs analz_mono]) 1); 
483 
qed "analz_UN_analz"; 

484 
Addsimps [analz_UN_analz]; 

1839  485 

486 

1913  487 
(**** Inductive relation "synth" ****) 
1839  488 

1913  489 
AddIs synth.intrs; 
1839  490 

1913  491 
goal thy "H <= synth(H)"; 
1839  492 
by (Fast_tac 1); 
1913  493 
qed "synth_increasing"; 
1839  494 

495 
(*Monotonicity*) 

1913  496 
goalw thy synth.defs "!!G H. G<=H ==> synth(G) <= synth(H)"; 
1839  497 
by (rtac lfp_mono 1); 
498 
by (REPEAT (ares_tac basic_monos 1)); 

1913  499 
qed "synth_mono"; 
1839  500 

501 
(** Unions **) 

502 

1913  503 
(*Converse fails: we can synth more from the union than from the 
1839  504 
separate parts, building a compound message using elements of each.*) 
1913  505 
goal thy "synth(G) Un synth(H) <= synth(G Un H)"; 
506 
by (REPEAT (ares_tac [Un_least, synth_mono, Un_upper1, Un_upper2] 1)); 

507 
qed "synth_Un"; 

1839  508 

1913  509 
goal thy "insert X (synth H) <= synth(insert X H)"; 
510 
by (fast_tac (!claset addEs [impOfSubs synth_mono]) 1); 

511 
qed "synth_insert"; 

1885  512 

1839  513 
(** Idempotence and transitivity **) 
514 

1913  515 
goal thy "!!H. X: synth (synth H) ==> X: synth H"; 
516 
be synth.induct 1; 

1839  517 
by (ALLGOALS Fast_tac); 
1913  518 
qed "synth_synthE"; 
519 
AddSEs [synth_synthE]; 

1839  520 

1913  521 
goal thy "synth (synth H) = synth H"; 
1839  522 
by (Fast_tac 1); 
1913  523 
qed "synth_idem"; 
1839  524 

1913  525 
goal thy "!!H. [ X: synth G; G <= synth H ] ==> X: synth H"; 
526 
by (dtac synth_mono 1); 

1839  527 
by (Fast_tac 1); 
1913  528 
qed "synth_trans"; 
1839  529 

530 
(*Cut; Lemma 2 of Lowe*) 

1998
f8230821f1e8
Reordering of premises for cut theorems, and new law MPair_synth_analz
paulson
parents:
1994
diff
changeset

531 
goal thy "!!H. [ Y: synth (insert X H); X: synth H ] ==> Y: synth H"; 
1913  532 
be synth_trans 1; 
1839  533 
by (Fast_tac 1); 
1913  534 
qed "synth_cut"; 
1839  535 

536 

537 
(*Can only produce a nonce or key if it is already known, 

1913  538 
but can synth a pair or encryption from its components...*) 
539 
val mk_cases = synth.mk_cases msg.simps; 

1839  540 

1913  541 
(*NO Agent_synth, as any Agent name can be synthd*) 
542 
val Nonce_synth = mk_cases "Nonce n : synth H"; 

543 
val Key_synth = mk_cases "Key K : synth H"; 

544 
val MPair_synth = mk_cases "{X,Y} : synth H"; 

545 
val Crypt_synth = mk_cases "Crypt X K : synth H"; 

1839  546 

1913  547 
AddSEs [Nonce_synth, Key_synth, MPair_synth, Crypt_synth]; 
1839  548 

1946  549 
goal thy "Agent A : synth H"; 
550 
by (Fast_tac 1); 

551 
qed "Agent_synth"; 

552 

1913  553 
goal thy "(Nonce N : synth H) = (Nonce N : H)"; 
1839  554 
by (Fast_tac 1); 
1913  555 
qed "Nonce_synth_eq"; 
1839  556 

1913  557 
goal thy "(Key K : synth H) = (Key K : H)"; 
1839  558 
by (Fast_tac 1); 
1913  559 
qed "Key_synth_eq"; 
1839  560 

1946  561 
Addsimps [Agent_synth, Nonce_synth_eq, Key_synth_eq]; 
1839  562 

563 

564 
goalw thy [keysFor_def] 

1913  565 
"keysFor (synth H) = keysFor H Un invKey``{K. Key K : H}"; 
1839  566 
by (Fast_tac 1); 
1913  567 
qed "keysFor_synth"; 
568 
Addsimps [keysFor_synth]; 

1839  569 

570 

1913  571 
(*** Combinations of parts, analz and synth ***) 
1839  572 

1913  573 
goal thy "parts (synth H) = parts H Un synth H"; 
1839  574 
br equalityI 1; 
575 
br subsetI 1; 

576 
be parts.induct 1; 

577 
by (ALLGOALS 

1913  578 
(best_tac (!claset addIs ((synth_increasing RS parts_mono RS subsetD) 
1839  579 
::parts.intrs)))); 
1913  580 
qed "parts_synth"; 
581 
Addsimps [parts_synth]; 

1839  582 

1913  583 
goal thy "analz (synth H) = analz H Un synth H"; 
1839  584 
br equalityI 1; 
585 
br subsetI 1; 

1913  586 
be analz.induct 1; 
1839  587 
by (best_tac 
1913  588 
(!claset addIs [synth_increasing RS analz_mono RS subsetD]) 5); 
1839  589 
(*Strange that best_tac just can't hack this one...*) 
1913  590 
by (ALLGOALS (deepen_tac (!claset addIs analz.intrs) 0)); 
591 
qed "analz_synth"; 

592 
Addsimps [analz_synth]; 

1839  593 

594 
(*Hard to prove; still needed now that there's only one Enemy?*) 

1913  595 
goal thy "analz (UN i. synth (H i)) = \ 
596 
\ analz (UN i. H i) Un (UN i. synth (H i))"; 

1839  597 
br equalityI 1; 
598 
br subsetI 1; 

1913  599 
be analz.induct 1; 
1839  600 
by (best_tac 
1913  601 
(!claset addEs [impOfSubs synth_increasing, 
602 
impOfSubs analz_mono]) 5); 

1839  603 
by (Best_tac 1); 
1913  604 
by (deepen_tac (!claset addIs [analz.Fst]) 0 1); 
605 
by (deepen_tac (!claset addIs [analz.Snd]) 0 1); 

606 
by (deepen_tac (!claset addSEs [analz.Decrypt] 

607 
addIs [analz.Decrypt]) 0 1); 

608 
qed "analz_UN1_synth"; 

609 
Addsimps [analz_UN1_synth]; 

1929
f0839bab4b00
Working version of NS, messages 13, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset

610 

1946  611 

612 
(** For reasoning about the Fake rule in traces **) 

613 

1929
f0839bab4b00
Working version of NS, messages 13, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset

614 
goal thy "!!Y. X: G ==> parts(insert X H) <= parts G Un parts H"; 
f0839bab4b00
Working version of NS, messages 13, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset

615 
br ([parts_mono, parts_Un_subset2] MRS subset_trans) 1; 
f0839bab4b00
Working version of NS, messages 13, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset

616 
by (Fast_tac 1); 
f0839bab4b00
Working version of NS, messages 13, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset

617 
qed "parts_insert_subset_Un"; 
f0839bab4b00
Working version of NS, messages 13, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset

618 

1946  619 
(*More specifically for Fake*) 
620 
goal thy "!!H. X: synth (analz G) ==> \ 

621 
\ parts (insert X H) <= synth (analz G) Un parts G Un parts H"; 

622 
bd parts_insert_subset_Un 1; 

623 
by (Full_simp_tac 1); 

624 
by (Deepen_tac 0 1); 

625 
qed "Fake_parts_insert"; 

626 

627 
goal thy "!!H. [ X: synth (analz G); G <= H ] ==> \ 

628 
\ analz (insert X H) <= synth (analz H) Un analz H"; 

629 
br subsetI 1; 

630 
by (subgoal_tac "x : analz (synth (analz H))" 1); 

631 
by (best_tac (!claset addIs [impOfSubs (analz_mono RS synth_mono)] 

632 
addSEs [impOfSubs analz_mono]) 2); 

633 
by (Full_simp_tac 1); 

634 
by (Fast_tac 1); 

635 
qed "Fake_analz_insert"; 

1929
f0839bab4b00
Working version of NS, messages 13, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset

636 

1998
f8230821f1e8
Reordering of premises for cut theorems, and new law MPair_synth_analz
paulson
parents:
1994
diff
changeset

637 
(*Without this equation, other rules for synth and analz would yield 
f8230821f1e8
Reordering of premises for cut theorems, and new law MPair_synth_analz
paulson
parents:
1994
diff
changeset

638 
redundant cases*) 
f8230821f1e8
Reordering of premises for cut theorems, and new law MPair_synth_analz
paulson
parents:
1994
diff
changeset

639 
goal thy "({X,Y} : synth (analz H)) = \ 
f8230821f1e8
Reordering of premises for cut theorems, and new law MPair_synth_analz
paulson
parents:
1994
diff
changeset

640 
\ (X : synth (analz H) & Y : synth (analz H))"; 
f8230821f1e8
Reordering of premises for cut theorems, and new law MPair_synth_analz
paulson
parents:
1994
diff
changeset

641 
by (Fast_tac 1); 
f8230821f1e8
Reordering of premises for cut theorems, and new law MPair_synth_analz
paulson
parents:
1994
diff
changeset

642 
qed "MPair_synth_analz"; 
f8230821f1e8
Reordering of premises for cut theorems, and new law MPair_synth_analz
paulson
parents:
1994
diff
changeset

643 

f8230821f1e8
Reordering of premises for cut theorems, and new law MPair_synth_analz
paulson
parents:
1994
diff
changeset

644 
AddIffs [MPair_synth_analz]; 
1929
f0839bab4b00
Working version of NS, messages 13, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset

645 

f0839bab4b00
Working version of NS, messages 13, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset

646 

f0839bab4b00
Working version of NS, messages 13, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset

647 
(*We do NOT want Crypt... messages broken up in protocols!!*) 
f0839bab4b00
Working version of NS, messages 13, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset

648 
Delrules partsEs; 
f0839bab4b00
Working version of NS, messages 13, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset

649 