author  paulson 
Wed, 25 Sep 1996 17:15:18 +0200  
changeset 2026  0df5a96bf77e 
parent 2011  d9af64c26be6 
child 2028  738bb98d65ec 
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 

2011  137 
goal thy "parts (insert X H) = parts {X} Un parts H"; 
1852  138 
by (stac (read_instantiate [("A","H")] insert_is_Un) 1); 
2011  139 
by (simp_tac (HOL_ss addsimps [parts_Un]) 1); 
140 
qed "parts_insert"; 

141 

142 
(*TWO inserts to avoid looping. This rewrite is better than nothing. 

143 
Not suitable for Addsimps: its behaviour can be strange.*) 

144 
goal thy "parts (insert X (insert Y H)) = parts {X} Un parts {Y} Un parts H"; 

145 
by (simp_tac (!simpset addsimps [Un_assoc]) 1); 

146 
by (simp_tac (!simpset addsimps [parts_insert RS sym]) 1); 

1852  147 
qed "parts_insert2"; 
148 

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

151 
val parts_UN_subset1 = result(); 

152 

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

154 
br subsetI 1; 

155 
be parts.induct 1; 

156 
by (ALLGOALS Fast_tac); 

157 
val parts_UN_subset2 = result(); 

158 

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

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

161 
qed "parts_UN"; 

162 

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

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

165 
qed "parts_UN1"; 

166 

1913  167 
(*Added to simplify arguments to parts, analz and synth*) 
1839  168 
Addsimps [parts_Un, parts_UN, parts_UN1]; 
169 

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

1852  171 
by (fast_tac (!claset addEs [impOfSubs parts_mono]) 1); 
1839  172 
qed "parts_insert_subset"; 
173 

174 
(** Idempotence and transitivity **) 

175 

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

177 
be parts.induct 1; 

178 
by (ALLGOALS Fast_tac); 

179 
qed "parts_partsE"; 

180 
AddSEs [parts_partsE]; 

181 

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

183 
by (Fast_tac 1); 

184 
qed "parts_idem"; 

185 
Addsimps [parts_idem]; 

186 

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

188 
by (dtac parts_mono 1); 

189 
by (Fast_tac 1); 

190 
qed "parts_trans"; 

191 

192 
(*Cut*) 

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

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

196 
qed "parts_cut"; 

197 

2011  198 
val parts_insertI = impOfSubs (subset_insertI RS parts_mono); 
199 

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

200 
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

201 
by (fast_tac (!claset addSEs [parts_cut] 
2011  202 
addIs [parts_insertI]) 1); 
1929
f0839bab4b00
Working version of NS, messages 13, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset

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

204 

1839  205 

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

207 

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

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

210 
br subsetI 1; 

211 
be parts.induct 1; 

212 
(*Simplification breaks up equalities between messages; 

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

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

215 
qed "parts_insert_Agent"; 

216 

217 
goal thy "parts (insert (Nonce N) H) = insert (Nonce N) (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_Nonce"; 

223 

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

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

226 
br subsetI 1; 

227 
be parts.induct 1; 

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

229 
qed "parts_insert_Key"; 

230 

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

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

233 
br equalityI 1; 

234 
br subsetI 1; 

235 
be parts.induct 1; 

236 
by (Auto_tac()); 

237 
be parts.induct 1; 

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

239 
qed "parts_insert_Crypt"; 

240 

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

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

243 
br equalityI 1; 

244 
br subsetI 1; 

245 
be parts.induct 1; 

246 
by (Auto_tac()); 

247 
be parts.induct 1; 

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

249 
qed "parts_insert_MPair"; 

250 

251 
Addsimps [parts_insert_Agent, parts_insert_Nonce, 

252 
parts_insert_Key, parts_insert_Crypt, parts_insert_MPair]; 

253 

254 

2026
0df5a96bf77e
Last working version prior to introduction of "lost"
paulson
parents:
2011
diff
changeset

255 
goal thy "parts (Key``N) = Key``N"; 
0df5a96bf77e
Last working version prior to introduction of "lost"
paulson
parents:
2011
diff
changeset

256 
by (Auto_tac()); 
0df5a96bf77e
Last working version prior to introduction of "lost"
paulson
parents:
2011
diff
changeset

257 
be parts.induct 1; 
0df5a96bf77e
Last working version prior to introduction of "lost"
paulson
parents:
2011
diff
changeset

258 
by (Auto_tac()); 
0df5a96bf77e
Last working version prior to introduction of "lost"
paulson
parents:
2011
diff
changeset

259 
qed "parts_image_Key"; 
0df5a96bf77e
Last working version prior to introduction of "lost"
paulson
parents:
2011
diff
changeset

260 

0df5a96bf77e
Last working version prior to introduction of "lost"
paulson
parents:
2011
diff
changeset

261 
Addsimps [parts_image_Key]; 
0df5a96bf77e
Last working version prior to introduction of "lost"
paulson
parents:
2011
diff
changeset

262 

0df5a96bf77e
Last working version prior to introduction of "lost"
paulson
parents:
2011
diff
changeset

263 

1913  264 
(**** Inductive relation "analz" ****) 
1839  265 

266 
val major::prems = 

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

1839  269 
\ ] ==> P"; 
270 
by (cut_facts_tac [major] 1); 

271 
brs prems 1; 

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

1839  274 

1913  275 
AddIs [analz.Inj]; 
2011  276 
AddSEs [MPair_analz]; (*Perhaps it should NOT be deemed safe!*) 
1913  277 
AddDs [analz.Decrypt]; 
1839  278 

1913  279 
Addsimps [analz.Inj]; 
1885  280 

1913  281 
goal thy "H <= analz(H)"; 
1839  282 
by (Fast_tac 1); 
1913  283 
qed "analz_increasing"; 
1839  284 

1913  285 
goal thy "analz H <= parts H"; 
1839  286 
by (rtac subsetI 1); 
1913  287 
be analz.induct 1; 
1839  288 
by (ALLGOALS Fast_tac); 
1913  289 
qed "analz_subset_parts"; 
1839  290 

1913  291 
bind_thm ("not_parts_not_analz", analz_subset_parts RS contra_subsetD); 
1839  292 

293 

1913  294 
goal thy "parts (analz H) = parts H"; 
1839  295 
br equalityI 1; 
1913  296 
br (analz_subset_parts RS parts_mono RS subset_trans) 1; 
1839  297 
by (Simp_tac 1); 
1913  298 
by (fast_tac (!claset addDs [analz_increasing RS parts_mono RS subsetD]) 1); 
299 
qed "parts_analz"; 

300 
Addsimps [parts_analz]; 

1839  301 

1913  302 
goal thy "analz (parts H) = parts H"; 
1885  303 
by (Auto_tac()); 
1913  304 
be analz.induct 1; 
1885  305 
by (Auto_tac()); 
1913  306 
qed "analz_parts"; 
307 
Addsimps [analz_parts]; 

1885  308 

1839  309 
(*Monotonicity; Lemma 1 of Lowe*) 
1913  310 
goalw thy analz.defs "!!G H. G<=H ==> analz(G) <= analz(H)"; 
1839  311 
by (rtac lfp_mono 1); 
312 
by (REPEAT (ares_tac basic_monos 1)); 

1913  313 
qed "analz_mono"; 
1839  314 

315 
(** General equational properties **) 

316 

1913  317 
goal thy "analz{} = {}"; 
1839  318 
by (Step_tac 1); 
1913  319 
be analz.induct 1; 
1839  320 
by (ALLGOALS Fast_tac); 
1913  321 
qed "analz_empty"; 
322 
Addsimps [analz_empty]; 

1839  323 

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

328 
qed "analz_Un"; 

1839  329 

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

332 
qed "analz_insert"; 

1839  333 

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

335 

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

1839  338 
br subsetI 1; 
1913  339 
be analz.induct 1; 
1839  340 
(*Simplification breaks up equalities between messages; 
341 
how to make it work for fast_tac??*) 

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

1913  343 
qed "analz_insert_Agent"; 
1839  344 

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

1839  347 
br subsetI 1; 
1913  348 
be analz.induct 1; 
1839  349 
by (ALLGOALS (fast_tac (!claset addss (!simpset)))); 
1913  350 
qed "analz_insert_Nonce"; 
1839  351 

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

353 
goalw thy [keysFor_def] 

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

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

1839  357 
br subsetI 1; 
1913  358 
be analz.induct 1; 
1839  359 
by (ALLGOALS (fast_tac (!claset addss (!simpset)))); 
1913  360 
qed "analz_insert_Key"; 
1839  361 

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

1885  364 
br equalityI 1; 
365 
br subsetI 1; 

1913  366 
be analz.induct 1; 
1885  367 
by (Auto_tac()); 
1913  368 
be analz.induct 1; 
369 
by (ALLGOALS (deepen_tac (!claset addIs [analz.Fst, analz.Snd, analz.Decrypt]) 0)); 

370 
qed "analz_insert_MPair"; 

1885  371 

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

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

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

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

1839  377 
br subsetI 1; 
1913  378 
be analz.induct 1; 
1839  379 
by (ALLGOALS (fast_tac (!claset addss (!simpset)))); 
1913  380 
qed "analz_insert_Crypt"; 
1839  381 

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

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

1839  385 
br subsetI 1; 
1913  386 
by (eres_inst_tac [("za","x")] analz.induct 1); 
1839  387 
by (ALLGOALS (fast_tac (!claset addss (!simpset)))); 
388 
val lemma1 = result(); 

389 

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

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

1839  393 
by (Auto_tac()); 
1913  394 
by (eres_inst_tac [("za","x")] analz.induct 1); 
1839  395 
by (Auto_tac()); 
1913  396 
by (best_tac (!claset addIs [subset_insertI RS analz_mono RS subsetD, 
397 
analz.Decrypt]) 1); 

1839  398 
val lemma2 = result(); 
399 

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

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

1839  403 
by (REPEAT (ares_tac [equalityI, lemma1, lemma2] 1)); 
1913  404 
qed "analz_insert_Decrypt"; 
1839  405 

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

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

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

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

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

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

416 
analz_insert_Decrypt]))); 

417 
qed "analz_Crypt_if"; 

1885  418 

1913  419 
Addsimps [analz_insert_Agent, analz_insert_Nonce, 
420 
analz_insert_Key, analz_insert_MPair, 

421 
analz_Crypt_if]; 

1839  422 

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

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

1839  426 
br subsetI 1; 
1913  427 
be analz.induct 1; 
1839  428 
by (Auto_tac()); 
1913  429 
qed "analz_insert_Crypt_subset"; 
1839  430 

431 

2026
0df5a96bf77e
Last working version prior to introduction of "lost"
paulson
parents:
2011
diff
changeset

432 
goal thy "analz (Key``N) = Key``N"; 
0df5a96bf77e
Last working version prior to introduction of "lost"
paulson
parents:
2011
diff
changeset

433 
by (Auto_tac()); 
0df5a96bf77e
Last working version prior to introduction of "lost"
paulson
parents:
2011
diff
changeset

434 
be analz.induct 1; 
0df5a96bf77e
Last working version prior to introduction of "lost"
paulson
parents:
2011
diff
changeset

435 
by (Auto_tac()); 
0df5a96bf77e
Last working version prior to introduction of "lost"
paulson
parents:
2011
diff
changeset

436 
qed "analz_image_Key"; 
0df5a96bf77e
Last working version prior to introduction of "lost"
paulson
parents:
2011
diff
changeset

437 

0df5a96bf77e
Last working version prior to introduction of "lost"
paulson
parents:
2011
diff
changeset

438 
Addsimps [analz_image_Key]; 
0df5a96bf77e
Last working version prior to introduction of "lost"
paulson
parents:
2011
diff
changeset

439 

0df5a96bf77e
Last working version prior to introduction of "lost"
paulson
parents:
2011
diff
changeset

440 

1839  441 
(** Idempotence and transitivity **) 
442 

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

1839  445 
by (ALLGOALS Fast_tac); 
1913  446 
qed "analz_analzE"; 
447 
AddSEs [analz_analzE]; 

1839  448 

1913  449 
goal thy "analz (analz H) = analz H"; 
1839  450 
by (Fast_tac 1); 
1913  451 
qed "analz_idem"; 
452 
Addsimps [analz_idem]; 

1839  453 

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

1839  456 
by (Fast_tac 1); 
1913  457 
qed "analz_trans"; 
1839  458 

459 
(*Cut; Lemma 2 of Lowe*) 

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

460 
goal thy "!!H. [ Y: analz (insert X H); X: analz H ] ==> Y: analz H"; 
1913  461 
be analz_trans 1; 
1839  462 
by (Fast_tac 1); 
1913  463 
qed "analz_cut"; 
1839  464 

465 
(*Cut can be proved easily by induction on 

1913  466 
"!!H. Y: analz (insert X H) ==> X: analz H > Y: analz H" 
1839  467 
*) 
468 

1885  469 

1913  470 
(** A congruence rule for "analz" **) 
1885  471 

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

1885  474 
by (Step_tac 1); 
1913  475 
be analz.induct 1; 
476 
by (ALLGOALS (best_tac (!claset addIs [analz_mono RS subsetD]))); 

477 
qed "analz_subset_cong"; 

1885  478 

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

481 
by (REPEAT_FIRST (ares_tac [equalityI, analz_subset_cong] 

1885  482 
ORELSE' etac equalityE)); 
1913  483 
qed "analz_cong"; 
1885  484 

485 

1913  486 
goal thy "!!H. analz H = analz H' ==> analz(insert X H) = analz(insert X H')"; 
1885  487 
by (asm_simp_tac (!simpset addsimps [insert_def] 
1913  488 
setloop (rtac analz_cong)) 1); 
489 
qed "analz_insert_cong"; 

1885  490 

1913  491 
(*If there are no pairs or encryptions then analz does nothing*) 
1839  492 
goal thy "!!H. [ ALL X Y. {X,Y} ~: H; ALL X K. Crypt X K ~: H ] ==> \ 
1913  493 
\ analz H = H"; 
1839  494 
by (Step_tac 1); 
1913  495 
be analz.induct 1; 
1839  496 
by (ALLGOALS Fast_tac); 
1913  497 
qed "analz_trivial"; 
1839  498 

499 
(*Helps to prove Fake cases*) 

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

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

1839  503 
val lemma = result(); 
504 

1913  505 
goal thy "analz (UN i. analz (H i)) = analz (UN i. H i)"; 
1839  506 
by (fast_tac (!claset addIs [lemma] 
1913  507 
addEs [impOfSubs analz_mono]) 1); 
508 
qed "analz_UN_analz"; 

509 
Addsimps [analz_UN_analz]; 

1839  510 

511 

1913  512 
(**** Inductive relation "synth" ****) 
1839  513 

1913  514 
AddIs synth.intrs; 
1839  515 

2011  516 
(*Can only produce a nonce or key if it is already known, 
517 
but can synth a pair or encryption from its components...*) 

518 
val mk_cases = synth.mk_cases msg.simps; 

519 

520 
(*NO Agent_synth, as any Agent name can be synthd*) 

521 
val Nonce_synth = mk_cases "Nonce n : synth H"; 

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

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

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

525 

526 
AddSEs [Nonce_synth, Key_synth, MPair_synth, Crypt_synth]; 

527 

1913  528 
goal thy "H <= synth(H)"; 
1839  529 
by (Fast_tac 1); 
1913  530 
qed "synth_increasing"; 
1839  531 

532 
(*Monotonicity*) 

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

1913  536 
qed "synth_mono"; 
1839  537 

538 
(** Unions **) 

539 

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

544 
qed "synth_Un"; 

1839  545 

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

548 
qed "synth_insert"; 

1885  549 

1839  550 
(** Idempotence and transitivity **) 
551 

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

1839  554 
by (ALLGOALS Fast_tac); 
1913  555 
qed "synth_synthE"; 
556 
AddSEs [synth_synthE]; 

1839  557 

1913  558 
goal thy "synth (synth H) = synth H"; 
1839  559 
by (Fast_tac 1); 
1913  560 
qed "synth_idem"; 
1839  561 

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

1839  564 
by (Fast_tac 1); 
1913  565 
qed "synth_trans"; 
1839  566 

567 
(*Cut; Lemma 2 of Lowe*) 

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

568 
goal thy "!!H. [ Y: synth (insert X H); X: synth H ] ==> Y: synth H"; 
1913  569 
be synth_trans 1; 
1839  570 
by (Fast_tac 1); 
1913  571 
qed "synth_cut"; 
1839  572 

1946  573 
goal thy "Agent A : synth H"; 
574 
by (Fast_tac 1); 

575 
qed "Agent_synth"; 

576 

1913  577 
goal thy "(Nonce N : synth H) = (Nonce N : H)"; 
1839  578 
by (Fast_tac 1); 
1913  579 
qed "Nonce_synth_eq"; 
1839  580 

1913  581 
goal thy "(Key K : synth H) = (Key K : H)"; 
1839  582 
by (Fast_tac 1); 
1913  583 
qed "Key_synth_eq"; 
1839  584 

2011  585 
goal thy "!!K. Key K ~: H ==> (Crypt X K : synth H) = (Crypt X K: H)"; 
586 
by (Fast_tac 1); 

587 
qed "Crypt_synth_eq"; 

588 

589 
Addsimps [Agent_synth, Nonce_synth_eq, Key_synth_eq, Crypt_synth_eq]; 

1839  590 

591 

592 
goalw thy [keysFor_def] 

1913  593 
"keysFor (synth H) = keysFor H Un invKey``{K. Key K : H}"; 
1839  594 
by (Fast_tac 1); 
1913  595 
qed "keysFor_synth"; 
596 
Addsimps [keysFor_synth]; 

1839  597 

598 

1913  599 
(*** Combinations of parts, analz and synth ***) 
1839  600 

1913  601 
goal thy "parts (synth H) = parts H Un synth H"; 
1839  602 
br equalityI 1; 
603 
br subsetI 1; 

604 
be parts.induct 1; 

605 
by (ALLGOALS 

1913  606 
(best_tac (!claset addIs ((synth_increasing RS parts_mono RS subsetD) 
1839  607 
::parts.intrs)))); 
1913  608 
qed "parts_synth"; 
609 
Addsimps [parts_synth]; 

1839  610 

1913  611 
goal thy "analz (synth H) = analz H Un synth H"; 
1839  612 
br equalityI 1; 
613 
br subsetI 1; 

1913  614 
be analz.induct 1; 
1839  615 
by (best_tac 
1913  616 
(!claset addIs [synth_increasing RS analz_mono RS subsetD]) 5); 
1839  617 
(*Strange that best_tac just can't hack this one...*) 
1913  618 
by (ALLGOALS (deepen_tac (!claset addIs analz.intrs) 0)); 
619 
qed "analz_synth"; 

620 
Addsimps [analz_synth]; 

1839  621 

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

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

1839  625 
br equalityI 1; 
626 
br subsetI 1; 

1913  627 
be analz.induct 1; 
1839  628 
by (best_tac 
1913  629 
(!claset addEs [impOfSubs synth_increasing, 
630 
impOfSubs analz_mono]) 5); 

1839  631 
by (Best_tac 1); 
1913  632 
by (deepen_tac (!claset addIs [analz.Fst]) 0 1); 
633 
by (deepen_tac (!claset addIs [analz.Snd]) 0 1); 

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

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

636 
qed "analz_UN1_synth"; 

637 
Addsimps [analz_UN1_synth]; 

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

638 

1946  639 

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

641 

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

642 
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

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

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

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

646 

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

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

650 
bd parts_insert_subset_Un 1; 

651 
by (Full_simp_tac 1); 

652 
by (Deepen_tac 0 1); 

653 
qed "Fake_parts_insert"; 

654 

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

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

657 
br subsetI 1; 

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

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

660 
addSEs [impOfSubs analz_mono]) 2); 

661 
by (Full_simp_tac 1); 

662 
by (Fast_tac 1); 

663 
qed "Fake_analz_insert"; 

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

664 

2011  665 
goal thy "(X: analz H & X: parts H) = (X: analz H)"; 
666 
by (fast_tac (!claset addDs [impOfSubs analz_subset_parts]) 1); 

667 
val analz_conj_parts = result(); 

668 

669 
goal thy "(X: analz H  X: parts H) = (X: parts H)"; 

670 
by (fast_tac (!claset addDs [impOfSubs analz_subset_parts]) 1); 

671 
val analz_disj_parts = result(); 

672 

673 
AddIffs [analz_conj_parts, analz_disj_parts]; 

674 

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

675 
(*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

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

677 
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

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

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

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

681 

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

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

683 

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

684 

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

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

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

687 