author  paulson 
Tue, 07 Jan 1997 16:28:43 +0100  
changeset 2484  596a5b5a68ff 
parent 2415  46de4b035f00 
child 2516  4d68fbe6378b 
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 

2327  10 
val prems = goal HOL.thy "[ P ==> Q(True); ~P ==> Q(False) ] ==> Q(P)"; 
11 
by (case_tac "P" 1); 

12 
by (ALLGOALS (asm_simp_tac (!simpset addsimps prems))); 

13 
val expand_case = result(); 

14 

15 
fun expand_case_tac P i = 

16 
res_inst_tac [("P",P)] expand_case i THEN 

17 
Simp_tac (i+1) THEN 

18 
Simp_tac i; 

19 

20 

21 

22 
(*GOALS.ML??*) 

23 
fun prlim n = (goals_limit:=n; pr()); 

24 

25 
(*FUN.ML?? WE NEED A NOTION OF INVERSE IMAGE, OR GRAPH!!*) 

26 
goal Set.thy "!!f. B <= range f = (B = f`` {x. f x: B})"; 

27 
by (fast_tac (!claset addEs [equalityE]) 1); 

28 
val subset_range_iff = result(); 

29 

30 

1839  31 
open Message; 
32 

2373  33 
AddIffs (msg.inject); 
1839  34 

35 
(** Inverse of keys **) 

36 

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

38 
by (Step_tac 1); 

2032  39 
by (rtac box_equals 1); 
1839  40 
by (REPEAT (rtac invKey 2)); 
41 
by (Asm_simp_tac 1); 

42 
qed "invKey_eq"; 

43 

44 
Addsimps [invKey, invKey_eq]; 

45 

46 

2484  47 
(**** Freeness laws for HPair ****) 
48 

49 
goalw thy [HPair_def] "Agent A ~= HPair X Y"; 

50 
by (Simp_tac 1); 

51 
qed "Agent_neq_HPair"; 

52 

53 
goalw thy [HPair_def] "Nonce N ~= HPair X Y"; 

54 
by (Simp_tac 1); 

55 
qed "Nonce_neq_HPair"; 

56 

57 
goalw thy [HPair_def] "Key K ~= HPair X Y"; 

58 
by (Simp_tac 1); 

59 
qed "Key_neq_HPair"; 

60 

61 
goalw thy [HPair_def] "Hash Z ~= HPair X Y"; 

62 
by (Simp_tac 1); 

63 
qed "Hash_neq_HPair"; 

64 

65 
goalw thy [HPair_def] "Crypt K X' ~= HPair X Y"; 

66 
by (Simp_tac 1); 

67 
qed "Crypt_neq_HPair"; 

68 

69 
val HPair_neqs = [Agent_neq_HPair, Nonce_neq_HPair, 

70 
Key_neq_HPair, Hash_neq_HPair, Crypt_neq_HPair]; 

71 

72 
AddIffs HPair_neqs; 

73 
AddIffs (HPair_neqs RL [not_sym]); 

74 

75 
goalw thy [HPair_def] "(HPair X' Y' = HPair X Y) = (X' = X & Y'=Y)"; 

76 
by (Simp_tac 1); 

77 
qed "HPair_eq"; 

78 

79 
goalw thy [HPair_def] "({X',Y'} = HPair X Y) = (X' = Hash{X,Y} & Y'=Y)"; 

80 
by (Simp_tac 1); 

81 
qed "MPair_eq_HPair"; 

82 

83 
goalw thy [HPair_def] "(HPair X Y = {X',Y'}) = (X' = Hash{X,Y} & Y'=Y)"; 

84 
by (Auto_tac()); 

85 
qed "HPair_eq_MPair"; 

86 

87 
AddIffs [HPair_eq, MPair_eq_HPair, HPair_eq_MPair]; 

88 

89 

1839  90 
(**** keysFor operator ****) 
91 

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

93 
by (Fast_tac 1); 

94 
qed "keysFor_empty"; 

95 

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

97 
by (Fast_tac 1); 

98 
qed "keysFor_Un"; 

99 

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

101 
by (Fast_tac 1); 

102 
qed "keysFor_UN"; 

103 

104 
(*Monotonicity*) 

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

106 
by (Fast_tac 1); 

107 
qed "keysFor_mono"; 

108 

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

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

111 
qed "keysFor_insert_Agent"; 

112 

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

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

115 
qed "keysFor_insert_Nonce"; 

116 

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

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

119 
qed "keysFor_insert_Key"; 

120 

2373  121 
goalw thy [keysFor_def] "keysFor (insert (Hash X) H) = keysFor H"; 
122 
by (fast_tac (!claset addss (!simpset)) 1); 

123 
qed "keysFor_insert_Hash"; 

124 

1839  125 
goalw thy [keysFor_def] "keysFor (insert {X,Y} H) = keysFor H"; 
126 
by (fast_tac (!claset addss (!simpset)) 1); 

127 
qed "keysFor_insert_MPair"; 

128 

129 
goalw thy [keysFor_def] 

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

130 
"keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)"; 
1839  131 
by (Auto_tac()); 
132 
qed "keysFor_insert_Crypt"; 

133 

134 
Addsimps [keysFor_empty, keysFor_Un, keysFor_UN, 

2373  135 
keysFor_insert_Agent, keysFor_insert_Nonce, keysFor_insert_Key, 
136 
keysFor_insert_Hash, keysFor_insert_MPair, keysFor_insert_Crypt]; 

1839  137 

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

138 
goalw thy [keysFor_def] "!!H. Crypt K X : H ==> invKey K : keysFor H"; 
2068  139 
by (Fast_tac 1); 
140 
qed "Crypt_imp_invKey_keysFor"; 

141 

1839  142 

143 
(**** Inductive relation "parts" ****) 

144 

145 
val major::prems = 

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

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

148 
\ ] ==> P"; 

149 
by (cut_facts_tac [major] 1); 

2032  150 
by (resolve_tac prems 1); 
1839  151 
by (REPEAT (eresolve_tac [asm_rl, parts.Fst, parts.Snd] 1)); 
152 
qed "MPair_parts"; 

153 

154 
AddIs [parts.Inj]; 

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

155 

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

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

157 

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

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

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

160 
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

161 
proofs concern only atomic messages.*) 
1839  162 

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

164 
by (Fast_tac 1); 

165 
qed "parts_increasing"; 

166 

167 
(*Monotonicity*) 

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

169 
by (rtac lfp_mono 1); 

170 
by (REPEAT (ares_tac basic_monos 1)); 

171 
qed "parts_mono"; 

172 

2373  173 
val parts_insertI = impOfSubs (subset_insertI RS parts_mono); 
174 

1839  175 
goal thy "parts{} = {}"; 
176 
by (Step_tac 1); 

2032  177 
by (etac parts.induct 1); 
1839  178 
by (ALLGOALS Fast_tac); 
179 
qed "parts_empty"; 

180 
Addsimps [parts_empty]; 

181 

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

183 
by (Asm_full_simp_tac 1); 

184 
qed "parts_emptyE"; 

185 
AddSEs [parts_emptyE]; 

186 

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

2032  189 
by (etac parts.induct 1); 
1893  190 
by (ALLGOALS Fast_tac); 
191 
qed "parts_singleton"; 

192 

1839  193 

194 
(** Unions **) 

195 

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

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

198 
val parts_Un_subset1 = result(); 

199 

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

2032  201 
by (rtac subsetI 1); 
202 
by (etac parts.induct 1); 

1839  203 
by (ALLGOALS Fast_tac); 
204 
val parts_Un_subset2 = result(); 

205 

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

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

208 
qed "parts_Un"; 

209 

2011  210 
goal thy "parts (insert X H) = parts {X} Un parts H"; 
1852  211 
by (stac (read_instantiate [("A","H")] insert_is_Un) 1); 
2011  212 
by (simp_tac (HOL_ss addsimps [parts_Un]) 1); 
213 
qed "parts_insert"; 

214 

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

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

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

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

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

1852  220 
qed "parts_insert2"; 
221 

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

224 
val parts_UN_subset1 = result(); 

225 

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

2032  227 
by (rtac subsetI 1); 
228 
by (etac parts.induct 1); 

1839  229 
by (ALLGOALS Fast_tac); 
230 
val parts_UN_subset2 = result(); 

231 

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

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

234 
qed "parts_UN"; 

235 

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

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

238 
qed "parts_UN1"; 

239 

1913  240 
(*Added to simplify arguments to parts, analz and synth*) 
1839  241 
Addsimps [parts_Un, parts_UN, parts_UN1]; 
242 

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

1852  244 
by (fast_tac (!claset addEs [impOfSubs parts_mono]) 1); 
1839  245 
qed "parts_insert_subset"; 
246 

247 
(** Idempotence and transitivity **) 

248 

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

2032  250 
by (etac parts.induct 1); 
1839  251 
by (ALLGOALS Fast_tac); 
252 
qed "parts_partsE"; 

253 
AddSEs [parts_partsE]; 

254 

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

256 
by (Fast_tac 1); 

257 
qed "parts_idem"; 

258 
Addsimps [parts_idem]; 

259 

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

261 
by (dtac parts_mono 1); 

262 
by (Fast_tac 1); 

263 
qed "parts_trans"; 

264 

265 
(*Cut*) 

2373  266 
goal thy "!!H. [ Y: parts (insert X G); X: parts H ] \ 
267 
\ ==> Y: parts (G Un H)"; 

2032  268 
by (etac parts_trans 1); 
2373  269 
by (Auto_tac()); 
1839  270 
qed "parts_cut"; 
271 

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

272 
goal thy "!!H. X: parts H ==> parts (insert X H) = parts H"; 
2373  273 
by (fast_tac (!claset addSDs [parts_cut] 
274 
addIs [parts_insertI] 

275 
addss (!simpset)) 1); 

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

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

277 

2028
738bb98d65ec
Last working version prior to addition of "lost" component
paulson
parents:
2026
diff
changeset

278 
Addsimps [parts_cut_eq]; 
738bb98d65ec
Last working version prior to addition of "lost" component
paulson
parents:
2026
diff
changeset

279 

1839  280 

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

282 

2373  283 
fun parts_tac i = 
284 
EVERY [rtac ([subsetI, parts_insert_subset] MRS equalityI) i, 

285 
etac parts.induct i, 

286 
REPEAT (fast_tac (!claset addss (!simpset)) i)]; 

287 

1839  288 
goal thy "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)"; 
2373  289 
by (parts_tac 1); 
1839  290 
qed "parts_insert_Agent"; 
291 

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

2373  293 
by (parts_tac 1); 
1839  294 
qed "parts_insert_Nonce"; 
295 

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

2373  297 
by (parts_tac 1); 
1839  298 
qed "parts_insert_Key"; 
299 

2373  300 
goal thy "parts (insert (Hash X) H) = insert (Hash X) (parts H)"; 
301 
by (parts_tac 1); 

302 
qed "parts_insert_Hash"; 

303 

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

304 
goal thy "parts (insert (Crypt K X) H) = \ 
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2170
diff
changeset

305 
\ insert (Crypt K X) (parts (insert X H))"; 
2032  306 
by (rtac equalityI 1); 
307 
by (rtac subsetI 1); 

308 
by (etac parts.induct 1); 

1839  309 
by (Auto_tac()); 
2032  310 
by (etac parts.induct 1); 
1839  311 
by (ALLGOALS (best_tac (!claset addIs [parts.Body]))); 
312 
qed "parts_insert_Crypt"; 

313 

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

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

2032  316 
by (rtac equalityI 1); 
317 
by (rtac subsetI 1); 

318 
by (etac parts.induct 1); 

1839  319 
by (Auto_tac()); 
2032  320 
by (etac parts.induct 1); 
1839  321 
by (ALLGOALS (best_tac (!claset addIs [parts.Fst, parts.Snd]))); 
322 
qed "parts_insert_MPair"; 

323 

2373  324 
Addsimps [parts_insert_Agent, parts_insert_Nonce, parts_insert_Key, 
325 
parts_insert_Hash, parts_insert_Crypt, parts_insert_MPair]; 

1839  326 

327 

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

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

329 
by (Auto_tac()); 
2032  330 
by (etac parts.induct 1); 
2026
0df5a96bf77e
Last working version prior to introduction of "lost"
paulson
parents:
2011
diff
changeset

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

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

333 

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

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

335 

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

336 

1913  337 
(**** Inductive relation "analz" ****) 
1839  338 

339 
val major::prems = 

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

1839  342 
\ ] ==> P"; 
343 
by (cut_facts_tac [major] 1); 

2032  344 
by (resolve_tac prems 1); 
1913  345 
by (REPEAT (eresolve_tac [asm_rl, analz.Fst, analz.Snd] 1)); 
346 
qed "MPair_analz"; 

1839  347 

1913  348 
AddIs [analz.Inj]; 
2011  349 
AddSEs [MPair_analz]; (*Perhaps it should NOT be deemed safe!*) 
1913  350 
AddDs [analz.Decrypt]; 
1839  351 

1913  352 
Addsimps [analz.Inj]; 
1885  353 

1913  354 
goal thy "H <= analz(H)"; 
1839  355 
by (Fast_tac 1); 
1913  356 
qed "analz_increasing"; 
1839  357 

1913  358 
goal thy "analz H <= parts H"; 
1839  359 
by (rtac subsetI 1); 
2032  360 
by (etac analz.induct 1); 
1839  361 
by (ALLGOALS Fast_tac); 
1913  362 
qed "analz_subset_parts"; 
1839  363 

1913  364 
bind_thm ("not_parts_not_analz", analz_subset_parts RS contra_subsetD); 
1839  365 

366 

1913  367 
goal thy "parts (analz H) = parts H"; 
2032  368 
by (rtac equalityI 1); 
369 
by (rtac (analz_subset_parts RS parts_mono RS subset_trans) 1); 

1839  370 
by (Simp_tac 1); 
1913  371 
by (fast_tac (!claset addDs [analz_increasing RS parts_mono RS subsetD]) 1); 
372 
qed "parts_analz"; 

373 
Addsimps [parts_analz]; 

1839  374 

1913  375 
goal thy "analz (parts H) = parts H"; 
1885  376 
by (Auto_tac()); 
2032  377 
by (etac analz.induct 1); 
1885  378 
by (Auto_tac()); 
1913  379 
qed "analz_parts"; 
380 
Addsimps [analz_parts]; 

1885  381 

1839  382 
(*Monotonicity; Lemma 1 of Lowe*) 
1913  383 
goalw thy analz.defs "!!G H. G<=H ==> analz(G) <= analz(H)"; 
1839  384 
by (rtac lfp_mono 1); 
385 
by (REPEAT (ares_tac basic_monos 1)); 

1913  386 
qed "analz_mono"; 
1839  387 

2373  388 
val analz_insertI = impOfSubs (subset_insertI RS analz_mono); 
389 

1839  390 
(** General equational properties **) 
391 

1913  392 
goal thy "analz{} = {}"; 
1839  393 
by (Step_tac 1); 
2032  394 
by (etac analz.induct 1); 
1839  395 
by (ALLGOALS Fast_tac); 
1913  396 
qed "analz_empty"; 
397 
Addsimps [analz_empty]; 

1839  398 

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

403 
qed "analz_Un"; 

1839  404 

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

407 
qed "analz_insert"; 

1839  408 

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

410 

2373  411 
fun analz_tac i = 
412 
EVERY [rtac ([subsetI, analz_insert] MRS equalityI) i, 

413 
etac analz.induct i, 

414 
REPEAT (fast_tac (!claset addss (!simpset)) i)]; 

415 

1913  416 
goal thy "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)"; 
2373  417 
by (analz_tac 1); 
1913  418 
qed "analz_insert_Agent"; 
1839  419 

1913  420 
goal thy "analz (insert (Nonce N) H) = insert (Nonce N) (analz H)"; 
2373  421 
by (analz_tac 1); 
1913  422 
qed "analz_insert_Nonce"; 
1839  423 

2373  424 
goal thy "analz (insert (Hash X) H) = insert (Hash X) (analz H)"; 
425 
by (analz_tac 1); 

426 
qed "analz_insert_Hash"; 

427 

1839  428 
(*Can only pull out Keys if they are not needed to decrypt the rest*) 
429 
goalw thy [keysFor_def] 

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

2373  432 
by (analz_tac 1); 
1913  433 
qed "analz_insert_Key"; 
1839  434 

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

2032  437 
by (rtac equalityI 1); 
438 
by (rtac subsetI 1); 

439 
by (etac analz.induct 1); 

1885  440 
by (Auto_tac()); 
2032  441 
by (etac analz.induct 1); 
2102  442 
by (ALLGOALS 
443 
(deepen_tac (!claset addIs [analz.Fst, analz.Snd, analz.Decrypt]) 0)); 

1913  444 
qed "analz_insert_MPair"; 
1885  445 

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

1913  447 
goal thy "!!H. Key (invKey K) ~: analz H ==> \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2170
diff
changeset

448 
\ analz (insert (Crypt K X) H) = \ 
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2170
diff
changeset

449 
\ insert (Crypt K X) (analz H)"; 
2373  450 
by (analz_tac 1); 
1913  451 
qed "analz_insert_Crypt"; 
1839  452 

1913  453 
goal thy "!!H. Key (invKey K) : analz H ==> \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2170
diff
changeset

454 
\ analz (insert (Crypt K X) H) <= \ 
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2170
diff
changeset

455 
\ insert (Crypt K X) (analz (insert X H))"; 
2032  456 
by (rtac subsetI 1); 
1913  457 
by (eres_inst_tac [("za","x")] analz.induct 1); 
1839  458 
by (ALLGOALS (fast_tac (!claset addss (!simpset)))); 
459 
val lemma1 = result(); 

460 

1913  461 
goal thy "!!H. Key (invKey K) : analz H ==> \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2170
diff
changeset

462 
\ insert (Crypt K X) (analz (insert X H)) <= \ 
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2170
diff
changeset

463 
\ analz (insert (Crypt K X) H)"; 
1839  464 
by (Auto_tac()); 
1913  465 
by (eres_inst_tac [("za","x")] analz.induct 1); 
1839  466 
by (Auto_tac()); 
1913  467 
by (best_tac (!claset addIs [subset_insertI RS analz_mono RS subsetD, 
2032  468 
analz.Decrypt]) 1); 
1839  469 
val lemma2 = result(); 
470 

1913  471 
goal thy "!!H. Key (invKey K) : analz H ==> \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2170
diff
changeset

472 
\ analz (insert (Crypt K X) H) = \ 
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2170
diff
changeset

473 
\ insert (Crypt K X) (analz (insert X H))"; 
1839  474 
by (REPEAT (ares_tac [equalityI, lemma1, lemma2] 1)); 
1913  475 
qed "analz_insert_Decrypt"; 
1839  476 

1885  477 
(*Case analysis: either the message is secure, or it is not! 
1946  478 
Effective, but can cause subgoals to blow up! 
1885  479 
Use with expand_if; apparently split_tac does not cope with patterns 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2170
diff
changeset

480 
such as "analz (insert (Crypt K X) H)" *) 
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2170
diff
changeset

481 
goal thy "analz (insert (Crypt K X) H) = \ 
2154  482 
\ (if (Key (invKey K) : analz H) \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2170
diff
changeset

483 
\ then insert (Crypt K X) (analz (insert X H)) \ 
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2170
diff
changeset

484 
\ else insert (Crypt K X) (analz H))"; 
2102  485 
by (case_tac "Key (invKey K) : analz H " 1); 
1913  486 
by (ALLGOALS (asm_simp_tac (!simpset addsimps [analz_insert_Crypt, 
2032  487 
analz_insert_Decrypt]))); 
1913  488 
qed "analz_Crypt_if"; 
1885  489 

2373  490 
Addsimps [analz_insert_Agent, analz_insert_Nonce, analz_insert_Key, 
491 
analz_insert_Hash, analz_insert_MPair, analz_Crypt_if]; 

1839  492 

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

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

494 
goal thy "analz (insert (Crypt K X) H) <= \ 
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2170
diff
changeset

495 
\ insert (Crypt K X) (analz (insert X H))"; 
2032  496 
by (rtac subsetI 1); 
497 
by (etac analz.induct 1); 

1839  498 
by (Auto_tac()); 
1913  499 
qed "analz_insert_Crypt_subset"; 
1839  500 

501 

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

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

503 
by (Auto_tac()); 
2032  504 
by (etac analz.induct 1); 
2026
0df5a96bf77e
Last working version prior to introduction of "lost"
paulson
parents:
2011
diff
changeset

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

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

507 

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

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

509 

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

510 

1839  511 
(** Idempotence and transitivity **) 
512 

1913  513 
goal thy "!!H. X: analz (analz H) ==> X: analz H"; 
2032  514 
by (etac analz.induct 1); 
1839  515 
by (ALLGOALS Fast_tac); 
1913  516 
qed "analz_analzE"; 
517 
AddSEs [analz_analzE]; 

1839  518 

1913  519 
goal thy "analz (analz H) = analz H"; 
1839  520 
by (Fast_tac 1); 
1913  521 
qed "analz_idem"; 
522 
Addsimps [analz_idem]; 

1839  523 

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

1839  526 
by (Fast_tac 1); 
1913  527 
qed "analz_trans"; 
1839  528 

529 
(*Cut; Lemma 2 of Lowe*) 

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

530 
goal thy "!!H. [ Y: analz (insert X H); X: analz H ] ==> Y: analz H"; 
2032  531 
by (etac analz_trans 1); 
1839  532 
by (Fast_tac 1); 
1913  533 
qed "analz_cut"; 
1839  534 

535 
(*Cut can be proved easily by induction on 

1913  536 
"!!H. Y: analz (insert X H) ==> X: analz H > Y: analz H" 
1839  537 
*) 
538 

1885  539 

1913  540 
(** A congruence rule for "analz" **) 
1885  541 

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

1885  544 
by (Step_tac 1); 
2032  545 
by (etac analz.induct 1); 
1913  546 
by (ALLGOALS (best_tac (!claset addIs [analz_mono RS subsetD]))); 
547 
qed "analz_subset_cong"; 

1885  548 

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

551 
by (REPEAT_FIRST (ares_tac [equalityI, analz_subset_cong] 

2032  552 
ORELSE' etac equalityE)); 
1913  553 
qed "analz_cong"; 
1885  554 

555 

1913  556 
goal thy "!!H. analz H = analz H' ==> analz(insert X H) = analz(insert X H')"; 
1885  557 
by (asm_simp_tac (!simpset addsimps [insert_def] 
2032  558 
setloop (rtac analz_cong)) 1); 
1913  559 
qed "analz_insert_cong"; 
1885  560 

1913  561 
(*If there are no pairs or encryptions then analz does nothing*) 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2170
diff
changeset

562 
goal thy "!!H. [ ALL X Y. {X,Y} ~: H; ALL X K. Crypt K X ~: H ] ==> \ 
1913  563 
\ analz H = H"; 
1839  564 
by (Step_tac 1); 
2032  565 
by (etac analz.induct 1); 
1839  566 
by (ALLGOALS Fast_tac); 
1913  567 
qed "analz_trivial"; 
1839  568 

569 
(*Helps to prove Fake cases*) 

1913  570 
goal thy "!!X. X: analz (UN i. analz (H i)) ==> X: analz (UN i. H i)"; 
2032  571 
by (etac analz.induct 1); 
1913  572 
by (ALLGOALS (fast_tac (!claset addEs [impOfSubs analz_mono]))); 
1839  573 
val lemma = result(); 
574 

1913  575 
goal thy "analz (UN i. analz (H i)) = analz (UN i. H i)"; 
1839  576 
by (fast_tac (!claset addIs [lemma] 
2032  577 
addEs [impOfSubs analz_mono]) 1); 
1913  578 
qed "analz_UN_analz"; 
579 
Addsimps [analz_UN_analz]; 

1839  580 

581 

1913  582 
(**** Inductive relation "synth" ****) 
1839  583 

1913  584 
AddIs synth.intrs; 
1839  585 

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

588 
val mk_cases = synth.mk_cases msg.simps; 

589 

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

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

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

2373  593 
val Hash_synth = mk_cases "Hash X : synth H"; 
2011  594 
val MPair_synth = mk_cases "{X,Y} : synth H"; 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2170
diff
changeset

595 
val Crypt_synth = mk_cases "Crypt K X : synth H"; 
2011  596 

2373  597 
AddSEs [Nonce_synth, Key_synth, Hash_synth, MPair_synth, Crypt_synth]; 
2011  598 

1913  599 
goal thy "H <= synth(H)"; 
1839  600 
by (Fast_tac 1); 
1913  601 
qed "synth_increasing"; 
1839  602 

603 
(*Monotonicity*) 

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

1913  607 
qed "synth_mono"; 
1839  608 

609 
(** Unions **) 

610 

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

615 
qed "synth_Un"; 

1839  616 

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

619 
qed "synth_insert"; 

1885  620 

1839  621 
(** Idempotence and transitivity **) 
622 

1913  623 
goal thy "!!H. X: synth (synth H) ==> X: synth H"; 
2032  624 
by (etac synth.induct 1); 
1839  625 
by (ALLGOALS Fast_tac); 
1913  626 
qed "synth_synthE"; 
627 
AddSEs [synth_synthE]; 

1839  628 

1913  629 
goal thy "synth (synth H) = synth H"; 
1839  630 
by (Fast_tac 1); 
1913  631 
qed "synth_idem"; 
1839  632 

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

1839  635 
by (Fast_tac 1); 
1913  636 
qed "synth_trans"; 
1839  637 

638 
(*Cut; Lemma 2 of Lowe*) 

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

639 
goal thy "!!H. [ Y: synth (insert X H); X: synth H ] ==> Y: synth H"; 
2032  640 
by (etac synth_trans 1); 
1839  641 
by (Fast_tac 1); 
1913  642 
qed "synth_cut"; 
1839  643 

1946  644 
goal thy "Agent A : synth H"; 
645 
by (Fast_tac 1); 

646 
qed "Agent_synth"; 

647 

1913  648 
goal thy "(Nonce N : synth H) = (Nonce N : H)"; 
1839  649 
by (Fast_tac 1); 
1913  650 
qed "Nonce_synth_eq"; 
1839  651 

1913  652 
goal thy "(Key K : synth H) = (Key K : H)"; 
1839  653 
by (Fast_tac 1); 
1913  654 
qed "Key_synth_eq"; 
1839  655 

2373  656 
goal thy "!!K. Key K ~: H ==> (Crypt K X : synth H) = (Crypt K X : H)"; 
2011  657 
by (Fast_tac 1); 
658 
qed "Crypt_synth_eq"; 

659 

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

1839  661 

662 

663 
goalw thy [keysFor_def] 

1913  664 
"keysFor (synth H) = keysFor H Un invKey``{K. Key K : H}"; 
1839  665 
by (Fast_tac 1); 
1913  666 
qed "keysFor_synth"; 
667 
Addsimps [keysFor_synth]; 

1839  668 

669 

1913  670 
(*** Combinations of parts, analz and synth ***) 
1839  671 

1913  672 
goal thy "parts (synth H) = parts H Un synth H"; 
2032  673 
by (rtac equalityI 1); 
674 
by (rtac subsetI 1); 

675 
by (etac parts.induct 1); 

1839  676 
by (ALLGOALS 
1913  677 
(best_tac (!claset addIs ((synth_increasing RS parts_mono RS subsetD) 
2032  678 
::parts.intrs)))); 
1913  679 
qed "parts_synth"; 
680 
Addsimps [parts_synth]; 

1839  681 

2373  682 
goal thy "analz (analz G Un H) = analz (G Un H)"; 
683 
by (REPEAT_FIRST (resolve_tac [equalityI, analz_subset_cong])); 

684 
by (ALLGOALS Simp_tac); 

685 
qed "analz_analz_Un"; 

686 

687 
goal thy "analz (synth G Un H) = analz (G Un H) Un synth G"; 

2032  688 
by (rtac equalityI 1); 
689 
by (rtac subsetI 1); 

690 
by (etac analz.induct 1); 

2373  691 
by (deepen_tac (!claset addIs [impOfSubs analz_mono]) 0 5); 
1839  692 
(*Strange that best_tac just can't hack this one...*) 
1913  693 
by (ALLGOALS (deepen_tac (!claset addIs analz.intrs) 0)); 
2373  694 
qed "analz_synth_Un"; 
695 

696 
goal thy "analz (synth H) = analz H Un synth H"; 

697 
by (cut_inst_tac [("H","{}")] analz_synth_Un 1); 

698 
by (Full_simp_tac 1); 

1913  699 
qed "analz_synth"; 
2373  700 
Addsimps [analz_analz_Un, analz_synth_Un, analz_synth]; 
1839  701 

2032  702 
(*Hard to prove; still needed now that there's only one Spy?*) 
1913  703 
goal thy "analz (UN i. synth (H i)) = \ 
704 
\ analz (UN i. H i) Un (UN i. synth (H i))"; 

2032  705 
by (rtac equalityI 1); 
706 
by (rtac subsetI 1); 

707 
by (etac analz.induct 1); 

1839  708 
by (best_tac 
1913  709 
(!claset addEs [impOfSubs synth_increasing, 
2032  710 
impOfSubs analz_mono]) 5); 
1839  711 
by (Best_tac 1); 
1913  712 
by (deepen_tac (!claset addIs [analz.Fst]) 0 1); 
713 
by (deepen_tac (!claset addIs [analz.Snd]) 0 1); 

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

2032  715 
addIs [analz.Decrypt]) 0 1); 
1913  716 
qed "analz_UN1_synth"; 
717 
Addsimps [analz_UN1_synth]; 

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

718 

1946  719 

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

721 

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

722 
goal thy "!!Y. X: G ==> parts(insert X H) <= parts G Un parts H"; 
2032  723 
by (rtac ([parts_mono, parts_Un_subset2] MRS subset_trans) 1); 
1929
f0839bab4b00
Working version of NS, messages 13, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset

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

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

726 

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

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

2032  730 
by (dtac parts_insert_subset_Un 1); 
1946  731 
by (Full_simp_tac 1); 
732 
by (Deepen_tac 0 1); 

733 
qed "Fake_parts_insert"; 

734 

2061  735 
goal thy 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2170
diff
changeset

736 
"!!H. [ Crypt K Y : parts (insert X H); X: synth (analz G); \ 
2061  737 
\ Key K ~: analz G ] \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2170
diff
changeset

738 
\ ==> Crypt K Y : parts G Un parts H"; 
2061  739 
by (dtac (impOfSubs Fake_parts_insert) 1); 
2170  740 
by (assume_tac 1); 
2061  741 
by (fast_tac (!claset addDs [impOfSubs analz_subset_parts] 
742 
addss (!simpset)) 1); 

743 
qed "Crypt_Fake_parts_insert"; 

744 

2373  745 
goal thy "!!H. X: synth (analz G) ==> \ 
746 
\ analz (insert X H) <= synth (analz G) Un analz (G Un H)"; 

747 
by (rtac subsetI 1); 

748 
by (subgoal_tac "x : analz (synth (analz G) Un H)" 1); 

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

750 
addSEs [impOfSubs analz_mono]) 2); 

751 
by (Full_simp_tac 1); 

752 
by (Fast_tac 1); 

753 
qed "Fake_analz_insert"; 

754 

755 
(*Needed????????????????*) 

1946  756 
goal thy "!!H. [ X: synth (analz G); G <= H ] ==> \ 
757 
\ analz (insert X H) <= synth (analz H) Un analz H"; 

2032  758 
by (rtac subsetI 1); 
1946  759 
by (subgoal_tac "x : analz (synth (analz H))" 1); 
760 
by (best_tac (!claset addIs [impOfSubs (analz_mono RS synth_mono)] 

761 
addSEs [impOfSubs analz_mono]) 2); 

762 
by (Full_simp_tac 1); 

763 
by (Fast_tac 1); 

2373  764 
qed "Fake_analz_insert_old"; 
1929
f0839bab4b00
Working version of NS, messages 13, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset

765 

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

768 
val analz_conj_parts = result(); 

769 

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

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

772 
val analz_disj_parts = result(); 

773 

774 
AddIffs [analz_conj_parts, analz_disj_parts]; 

775 

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

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

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

778 
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

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

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

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

782 

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

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

784 

2154  785 
goal thy "!!K. [ Key K : analz H; Key (invKey K) : analz H ] \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2170
diff
changeset

786 
\ ==> (Crypt K X : synth (analz H)) = (X : synth (analz H))"; 
2154  787 
by (Fast_tac 1); 
788 
qed "Crypt_synth_analz"; 

789 

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

790 

2373  791 
goal thy "!!K. Key K ~: analz H \ 
792 
\ ==> (Hash{Key K,X} : synth (analz H)) = (Hash{Key K,X} : analz H)"; 

793 
by (Fast_tac 1); 

794 
qed "Hash_synth_analz"; 

795 
Addsimps [Hash_synth_analz]; 

796 

797 

2484  798 
(**** HPair: a combination of Hash and MPair ****) 
799 

800 
(*** Freeness ***) 

801 

802 
goalw thy [HPair_def] "Agent A ~= HPair X Y"; 

803 
by (Simp_tac 1); 

804 
qed "Agent_neq_HPair"; 

805 

806 
goalw thy [HPair_def] "Nonce N ~= HPair X Y"; 

807 
by (Simp_tac 1); 

808 
qed "Nonce_neq_HPair"; 

809 

810 
goalw thy [HPair_def] "Key K ~= HPair X Y"; 

811 
by (Simp_tac 1); 

812 
qed "Key_neq_HPair"; 

813 

814 
goalw thy [HPair_def] "Hash Z ~= HPair X Y"; 

815 
by (Simp_tac 1); 

816 
qed "Hash_neq_HPair"; 

817 

818 
goalw thy [HPair_def] "Crypt K X' ~= HPair X Y"; 

819 
by (Simp_tac 1); 

820 
qed "Crypt_neq_HPair"; 

821 

822 
val HPair_neqs = [Agent_neq_HPair, Nonce_neq_HPair, 

823 
Key_neq_HPair, Hash_neq_HPair, Crypt_neq_HPair]; 

824 

825 
AddIffs HPair_neqs; 

826 
AddIffs (HPair_neqs RL [not_sym]); 

827 

828 
goalw thy [HPair_def] "(HPair X' Y' = HPair X Y) = (X' = X & Y'=Y)"; 

829 
by (Simp_tac 1); 

830 
qed "HPair_eq"; 

831 

832 
goalw thy [HPair_def] "({X',Y'} = HPair X Y) = (X' = Hash{X,Y} & Y'=Y)"; 

833 
by (Simp_tac 1); 

834 
qed "MPair_eq_HPair"; 

835 

836 
goalw thy [HPair_def] "(HPair X Y = {X',Y'}) = (X' = Hash{X,Y} & Y'=Y)"; 

837 
by (Auto_tac()); 

838 
qed "HPair_eq_MPair"; 

839 

840 
AddIffs [HPair_eq, MPair_eq_HPair, HPair_eq_MPair]; 

841 

842 

843 
(*** Specialized laws, proved in terms of those for Hash and MPair ***) 

844 

845 
goalw thy [HPair_def] "keysFor (insert (HPair X Y) H) = keysFor H"; 

846 
by (Simp_tac 1); 

847 
qed "keysFor_insert_HPair"; 

848 

849 
goalw thy [HPair_def] 

850 
"parts (insert (HPair X Y) H) = \ 

851 
\ insert (HPair X Y) (insert (Hash{X,Y}) (parts (insert Y H)))"; 

852 
by (Simp_tac 1); 

853 
qed "parts_insert_HPair"; 

854 

855 
goalw thy [HPair_def] 

856 
"analz (insert (HPair X Y) H) = \ 

857 
\ insert (HPair X Y) (insert (Hash{X,Y}) (analz (insert Y H)))"; 

858 
by (Simp_tac 1); 

859 
qed "analz_insert_HPair"; 

860 

861 
goalw thy [HPair_def] "!!H. X ~: synth (analz H) \ 

862 
\ ==> (HPair X Y : synth (analz H)) = \ 

863 
\ (Hash {X, Y} : analz H & Y : synth (analz H))"; 

864 
by (Simp_tac 1); 

865 
by (Fast_tac 1); 

866 
qed "HPair_synth_analz"; 

867 

868 
Addsimps [keysFor_insert_HPair, parts_insert_HPair, analz_insert_HPair, 

869 
HPair_synth_analz, HPair_synth_analz]; 

870 

871 

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

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

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

874 

2327  875 

876 
(** Rewrites to push in Key and Crypt messages, so that other messages can 

877 
be pulled out using the analz_insert rules **) 

878 

879 
fun insComm thy x y = read_instantiate_sg (sign_of thy) [("x",x), ("y",y)] 

880 
insert_commute; 

881 

882 
val pushKeys = map (insComm thy "Key ?K") 

2373  883 
["Agent ?C", "Nonce ?N", "Hash ?X", 
884 
"MPair ?X ?Y", "Crypt ?X ?K'"]; 

2327  885 

886 
val pushCrypts = map (insComm thy "Crypt ?X ?K") 

2373  887 
["Agent ?C", "Nonce ?N", "Hash ?X'", "MPair ?X' ?Y"]; 
2327  888 

889 
(*Cannot be added with Addsimps  we don't always want to reorder messages*) 

890 
val pushes = pushKeys@pushCrypts; 

891 

892 

2484  893 
(*No premature instantiation of variables during simplification. 
894 
For proving "possibility" properties.*) 

2327  895 
fun safe_solver prems = 
896 
match_tac (TrueI::refl::prems) ORELSE' eq_assume_tac 

897 
ORELSE' etac FalseE; 

898 

2373  899 
val Fake_insert_tac = 
900 
dresolve_tac [impOfSubs Fake_analz_insert, 

901 
impOfSubs Fake_parts_insert] THEN' 

902 
eresolve_tac [asm_rl, synth.Inj]; 

903 

904 
(*Analysis of Fake cases and of messages that forward unknown parts. 

2327  905 
Abstraction over i is ESSENTIAL: it delays the dereferencing of claset 
906 
DEPENDS UPON "X" REFERRING TO THE FRADULENT MESSAGE *) 

907 
fun spy_analz_tac i = 

2373  908 
DETERM 
909 
(SELECT_GOAL 

910 
(EVERY 

911 
[ (*push in occurrences of X...*) 

912 
(REPEAT o CHANGED) 

913 
(res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1), 

914 
(*...allowing further simplifications*) 

915 
simp_tac (!simpset setloop split_tac [expand_if]) 1, 

916 
REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI])), 

917 
DEPTH_SOLVE 

918 
(REPEAT (Fake_insert_tac 1) THEN Asm_full_simp_tac 1 

919 
THEN 

920 
IF_UNSOLVED (depth_tac (!claset addIs [impOfSubs analz_mono, 

921 
impOfSubs analz_subset_parts]) 2 1)) 

922 
]) i); 

2327  923 

2415  924 
(** Useful in many uniqueness proofs **) 
2327  925 
fun ex_strip_tac i = REPEAT (swap_res_tac [exI, conjI] i) THEN 
926 
assume_tac (i+1); 

927 

2415  928 
(*Apply the EXALL quantifification to prove uniqueness theorems in 
929 
their standard form*) 

930 
fun prove_unique_tac lemma = 

931 
EVERY' [dtac lemma, 

932 
REPEAT o (mp_tac ORELSE' eresolve_tac [asm_rl,exE]), 

933 
(*Duplicate the assumption*) 

934 
forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl, 

935 
fast_tac (!claset addSDs [spec])]; 

936 

2373  937 

938 
(*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*) 

939 
goal Set.thy "A Un (B Un A) = B Un A"; 

940 
by (Fast_tac 1); 

941 
val Un_absorb3 = result(); 

942 
Addsimps [Un_absorb3]; 