author  paulson 
Thu, 05 Dec 1996 19:03:38 +0100  
changeset 2327  00ac25b2791d 
parent 2284  80ebd1a213fd 
child 2373  490ffa16952e 
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 

33 

34 
(** Inverse of keys **) 

35 

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

37 
by (Step_tac 1); 

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

41 
qed "invKey_eq"; 

42 

43 
Addsimps [invKey, invKey_eq]; 

44 

45 

46 
(**** keysFor operator ****) 

47 

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

49 
by (Fast_tac 1); 

50 
qed "keysFor_empty"; 

51 

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

53 
by (Fast_tac 1); 

54 
qed "keysFor_Un"; 

55 

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

57 
by (Fast_tac 1); 

58 
qed "keysFor_UN"; 

59 

60 
(*Monotonicity*) 

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

62 
by (Fast_tac 1); 

63 
qed "keysFor_mono"; 

64 

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

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

67 
qed "keysFor_insert_Agent"; 

68 

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

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

71 
qed "keysFor_insert_Nonce"; 

72 

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

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

75 
qed "keysFor_insert_Key"; 

76 

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

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

79 
qed "keysFor_insert_MPair"; 

80 

81 
goalw thy [keysFor_def] 

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

82 
"keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)"; 
1839  83 
by (Auto_tac()); 
84 
qed "keysFor_insert_Crypt"; 

85 

86 
Addsimps [keysFor_empty, keysFor_Un, keysFor_UN, 

2032  87 
keysFor_insert_Agent, keysFor_insert_Nonce, 
88 
keysFor_insert_Key, keysFor_insert_MPair, 

89 
keysFor_insert_Crypt]; 

1839  90 

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

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

94 

1839  95 

96 
(**** Inductive relation "parts" ****) 

97 

98 
val major::prems = 

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

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

101 
\ ] ==> P"; 

102 
by (cut_facts_tac [major] 1); 

2032  103 
by (resolve_tac prems 1); 
1839  104 
by (REPEAT (eresolve_tac [asm_rl, parts.Fst, parts.Snd] 1)); 
105 
qed "MPair_parts"; 

106 

107 
AddIs [parts.Inj]; 

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

108 

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

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

110 

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

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

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

113 
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

114 
proofs concern only atomic messages.*) 
1839  115 

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

117 
by (Fast_tac 1); 

118 
qed "parts_increasing"; 

119 

120 
(*Monotonicity*) 

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

122 
by (rtac lfp_mono 1); 

123 
by (REPEAT (ares_tac basic_monos 1)); 

124 
qed "parts_mono"; 

125 

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

127 
by (Step_tac 1); 

2032  128 
by (etac parts.induct 1); 
1839  129 
by (ALLGOALS Fast_tac); 
130 
qed "parts_empty"; 

131 
Addsimps [parts_empty]; 

132 

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

134 
by (Asm_full_simp_tac 1); 

135 
qed "parts_emptyE"; 

136 
AddSEs [parts_emptyE]; 

137 

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

2032  140 
by (etac parts.induct 1); 
1893  141 
by (ALLGOALS Fast_tac); 
142 
qed "parts_singleton"; 

143 

1839  144 

145 
(** Unions **) 

146 

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

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

149 
val parts_Un_subset1 = result(); 

150 

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

2032  152 
by (rtac subsetI 1); 
153 
by (etac parts.induct 1); 

1839  154 
by (ALLGOALS Fast_tac); 
155 
val parts_Un_subset2 = result(); 

156 

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

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

159 
qed "parts_Un"; 

160 

2011  161 
goal thy "parts (insert X H) = parts {X} Un parts H"; 
1852  162 
by (stac (read_instantiate [("A","H")] insert_is_Un) 1); 
2011  163 
by (simp_tac (HOL_ss addsimps [parts_Un]) 1); 
164 
qed "parts_insert"; 

165 

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

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

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

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

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

1852  171 
qed "parts_insert2"; 
172 

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

175 
val parts_UN_subset1 = result(); 

176 

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

2032  178 
by (rtac subsetI 1); 
179 
by (etac parts.induct 1); 

1839  180 
by (ALLGOALS Fast_tac); 
181 
val parts_UN_subset2 = result(); 

182 

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

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

185 
qed "parts_UN"; 

186 

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

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

189 
qed "parts_UN1"; 

190 

1913  191 
(*Added to simplify arguments to parts, analz and synth*) 
1839  192 
Addsimps [parts_Un, parts_UN, parts_UN1]; 
193 

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

1852  195 
by (fast_tac (!claset addEs [impOfSubs parts_mono]) 1); 
1839  196 
qed "parts_insert_subset"; 
197 

198 
(** Idempotence and transitivity **) 

199 

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

2032  201 
by (etac parts.induct 1); 
1839  202 
by (ALLGOALS Fast_tac); 
203 
qed "parts_partsE"; 

204 
AddSEs [parts_partsE]; 

205 

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

207 
by (Fast_tac 1); 

208 
qed "parts_idem"; 

209 
Addsimps [parts_idem]; 

210 

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

212 
by (dtac parts_mono 1); 

213 
by (Fast_tac 1); 

214 
qed "parts_trans"; 

215 

216 
(*Cut*) 

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

217 
goal thy "!!H. [ Y: parts (insert X H); X: parts H ] ==> Y: parts H"; 
2032  218 
by (etac parts_trans 1); 
1839  219 
by (Fast_tac 1); 
220 
qed "parts_cut"; 

221 

2011  222 
val parts_insertI = impOfSubs (subset_insertI RS parts_mono); 
223 

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

224 
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

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

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

228 

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

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

230 

1839  231 

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

233 

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

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

2032  236 
by (rtac subsetI 1); 
237 
by (etac parts.induct 1); 

1839  238 
(*Simplification breaks up equalities between messages; 
239 
how to make it work for fast_tac??*) 

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

241 
qed "parts_insert_Agent"; 

242 

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

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

2032  245 
by (rtac subsetI 1); 
246 
by (etac parts.induct 1); 

1839  247 
by (ALLGOALS (fast_tac (!claset addss (!simpset)))); 
248 
qed "parts_insert_Nonce"; 

249 

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

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

2032  252 
by (rtac subsetI 1); 
253 
by (etac parts.induct 1); 

1839  254 
by (ALLGOALS (fast_tac (!claset addss (!simpset)))); 
255 
qed "parts_insert_Key"; 

256 

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

257 
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

258 
\ insert (Crypt K X) (parts (insert X H))"; 
2032  259 
by (rtac equalityI 1); 
260 
by (rtac subsetI 1); 

261 
by (etac parts.induct 1); 

1839  262 
by (Auto_tac()); 
2032  263 
by (etac parts.induct 1); 
1839  264 
by (ALLGOALS (best_tac (!claset addIs [parts.Body]))); 
265 
qed "parts_insert_Crypt"; 

266 

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

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

2032  269 
by (rtac equalityI 1); 
270 
by (rtac subsetI 1); 

271 
by (etac parts.induct 1); 

1839  272 
by (Auto_tac()); 
2032  273 
by (etac parts.induct 1); 
1839  274 
by (ALLGOALS (best_tac (!claset addIs [parts.Fst, parts.Snd]))); 
275 
qed "parts_insert_MPair"; 

276 

277 
Addsimps [parts_insert_Agent, parts_insert_Nonce, 

2032  278 
parts_insert_Key, parts_insert_Crypt, parts_insert_MPair]; 
1839  279 

280 

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

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

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

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

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

286 

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

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

288 

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

289 

1913  290 
(**** Inductive relation "analz" ****) 
1839  291 

292 
val major::prems = 

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

1839  295 
\ ] ==> P"; 
296 
by (cut_facts_tac [major] 1); 

2032  297 
by (resolve_tac prems 1); 
1913  298 
by (REPEAT (eresolve_tac [asm_rl, analz.Fst, analz.Snd] 1)); 
299 
qed "MPair_analz"; 

1839  300 

1913  301 
AddIs [analz.Inj]; 
2011  302 
AddSEs [MPair_analz]; (*Perhaps it should NOT be deemed safe!*) 
1913  303 
AddDs [analz.Decrypt]; 
1839  304 

1913  305 
Addsimps [analz.Inj]; 
1885  306 

1913  307 
goal thy "H <= analz(H)"; 
1839  308 
by (Fast_tac 1); 
1913  309 
qed "analz_increasing"; 
1839  310 

1913  311 
goal thy "analz H <= parts H"; 
1839  312 
by (rtac subsetI 1); 
2032  313 
by (etac analz.induct 1); 
1839  314 
by (ALLGOALS Fast_tac); 
1913  315 
qed "analz_subset_parts"; 
1839  316 

1913  317 
bind_thm ("not_parts_not_analz", analz_subset_parts RS contra_subsetD); 
1839  318 

319 

1913  320 
goal thy "parts (analz H) = parts H"; 
2032  321 
by (rtac equalityI 1); 
322 
by (rtac (analz_subset_parts RS parts_mono RS subset_trans) 1); 

1839  323 
by (Simp_tac 1); 
1913  324 
by (fast_tac (!claset addDs [analz_increasing RS parts_mono RS subsetD]) 1); 
325 
qed "parts_analz"; 

326 
Addsimps [parts_analz]; 

1839  327 

1913  328 
goal thy "analz (parts H) = parts H"; 
1885  329 
by (Auto_tac()); 
2032  330 
by (etac analz.induct 1); 
1885  331 
by (Auto_tac()); 
1913  332 
qed "analz_parts"; 
333 
Addsimps [analz_parts]; 

1885  334 

1839  335 
(*Monotonicity; Lemma 1 of Lowe*) 
1913  336 
goalw thy analz.defs "!!G H. G<=H ==> analz(G) <= analz(H)"; 
1839  337 
by (rtac lfp_mono 1); 
338 
by (REPEAT (ares_tac basic_monos 1)); 

1913  339 
qed "analz_mono"; 
1839  340 

341 
(** General equational properties **) 

342 

1913  343 
goal thy "analz{} = {}"; 
1839  344 
by (Step_tac 1); 
2032  345 
by (etac analz.induct 1); 
1839  346 
by (ALLGOALS Fast_tac); 
1913  347 
qed "analz_empty"; 
348 
Addsimps [analz_empty]; 

1839  349 

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

354 
qed "analz_Un"; 

1839  355 

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

358 
qed "analz_insert"; 

1839  359 

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

361 

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

2032  364 
by (rtac subsetI 1); 
365 
by (etac analz.induct 1); 

1839  366 
(*Simplification breaks up equalities between messages; 
367 
how to make it work for fast_tac??*) 

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

1913  369 
qed "analz_insert_Agent"; 
1839  370 

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

2032  373 
by (rtac subsetI 1); 
374 
by (etac analz.induct 1); 

1839  375 
by (ALLGOALS (fast_tac (!claset addss (!simpset)))); 
1913  376 
qed "analz_insert_Nonce"; 
1839  377 

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

379 
goalw thy [keysFor_def] 

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

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

2032  383 
by (rtac subsetI 1); 
384 
by (etac analz.induct 1); 

1839  385 
by (ALLGOALS (fast_tac (!claset addss (!simpset)))); 
1913  386 
qed "analz_insert_Key"; 
1839  387 

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

2032  390 
by (rtac equalityI 1); 
391 
by (rtac subsetI 1); 

392 
by (etac analz.induct 1); 

1885  393 
by (Auto_tac()); 
2032  394 
by (etac analz.induct 1); 
2102  395 
by (ALLGOALS 
396 
(deepen_tac (!claset addIs [analz.Fst, analz.Snd, analz.Decrypt]) 0)); 

1913  397 
qed "analz_insert_MPair"; 
1885  398 

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

1913  400 
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

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

402 
\ insert (Crypt K X) (analz H)"; 
1913  403 
by (rtac (analz_insert RSN (2, equalityI)) 1); 
2032  404 
by (rtac subsetI 1); 
405 
by (etac analz.induct 1); 

1839  406 
by (ALLGOALS (fast_tac (!claset addss (!simpset)))); 
1913  407 
qed "analz_insert_Crypt"; 
1839  408 

1913  409 
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

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

411 
\ insert (Crypt K X) (analz (insert X H))"; 
2032  412 
by (rtac subsetI 1); 
1913  413 
by (eres_inst_tac [("za","x")] analz.induct 1); 
1839  414 
by (ALLGOALS (fast_tac (!claset addss (!simpset)))); 
415 
val lemma1 = result(); 

416 

1913  417 
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

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

419 
\ analz (insert (Crypt K X) H)"; 
1839  420 
by (Auto_tac()); 
1913  421 
by (eres_inst_tac [("za","x")] analz.induct 1); 
1839  422 
by (Auto_tac()); 
1913  423 
by (best_tac (!claset addIs [subset_insertI RS analz_mono RS subsetD, 
2032  424 
analz.Decrypt]) 1); 
1839  425 
val lemma2 = result(); 
426 

1913  427 
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

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

429 
\ insert (Crypt K X) (analz (insert X H))"; 
1839  430 
by (REPEAT (ares_tac [equalityI, lemma1, lemma2] 1)); 
1913  431 
qed "analz_insert_Decrypt"; 
1839  432 

1885  433 
(*Case analysis: either the message is secure, or it is not! 
1946  434 
Effective, but can cause subgoals to blow up! 
1885  435 
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

436 
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

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

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

440 
\ else insert (Crypt K X) (analz H))"; 
2102  441 
by (case_tac "Key (invKey K) : analz H " 1); 
1913  442 
by (ALLGOALS (asm_simp_tac (!simpset addsimps [analz_insert_Crypt, 
2032  443 
analz_insert_Decrypt]))); 
1913  444 
qed "analz_Crypt_if"; 
1885  445 

1913  446 
Addsimps [analz_insert_Agent, analz_insert_Nonce, 
2032  447 
analz_insert_Key, analz_insert_MPair, 
448 
analz_Crypt_if]; 

1839  449 

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

451 
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

452 
\ insert (Crypt K X) (analz (insert X H))"; 
2032  453 
by (rtac subsetI 1); 
454 
by (etac analz.induct 1); 

1839  455 
by (Auto_tac()); 
1913  456 
qed "analz_insert_Crypt_subset"; 
1839  457 

458 

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

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

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

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

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

464 

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

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

466 

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

467 

1839  468 
(** Idempotence and transitivity **) 
469 

1913  470 
goal thy "!!H. X: analz (analz H) ==> X: analz H"; 
2032  471 
by (etac analz.induct 1); 
1839  472 
by (ALLGOALS Fast_tac); 
1913  473 
qed "analz_analzE"; 
474 
AddSEs [analz_analzE]; 

1839  475 

1913  476 
goal thy "analz (analz H) = analz H"; 
1839  477 
by (Fast_tac 1); 
1913  478 
qed "analz_idem"; 
479 
Addsimps [analz_idem]; 

1839  480 

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

1839  483 
by (Fast_tac 1); 
1913  484 
qed "analz_trans"; 
1839  485 

486 
(*Cut; Lemma 2 of Lowe*) 

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

487 
goal thy "!!H. [ Y: analz (insert X H); X: analz H ] ==> Y: analz H"; 
2032  488 
by (etac analz_trans 1); 
1839  489 
by (Fast_tac 1); 
1913  490 
qed "analz_cut"; 
1839  491 

492 
(*Cut can be proved easily by induction on 

1913  493 
"!!H. Y: analz (insert X H) ==> X: analz H > Y: analz H" 
1839  494 
*) 
495 

1885  496 

1913  497 
(** A congruence rule for "analz" **) 
1885  498 

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

1885  501 
by (Step_tac 1); 
2032  502 
by (etac analz.induct 1); 
1913  503 
by (ALLGOALS (best_tac (!claset addIs [analz_mono RS subsetD]))); 
504 
qed "analz_subset_cong"; 

1885  505 

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

508 
by (REPEAT_FIRST (ares_tac [equalityI, analz_subset_cong] 

2032  509 
ORELSE' etac equalityE)); 
1913  510 
qed "analz_cong"; 
1885  511 

512 

1913  513 
goal thy "!!H. analz H = analz H' ==> analz(insert X H) = analz(insert X H')"; 
1885  514 
by (asm_simp_tac (!simpset addsimps [insert_def] 
2032  515 
setloop (rtac analz_cong)) 1); 
1913  516 
qed "analz_insert_cong"; 
1885  517 

1913  518 
(*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

519 
goal thy "!!H. [ ALL X Y. {X,Y} ~: H; ALL X K. Crypt K X ~: H ] ==> \ 
1913  520 
\ analz H = H"; 
1839  521 
by (Step_tac 1); 
2032  522 
by (etac analz.induct 1); 
1839  523 
by (ALLGOALS Fast_tac); 
1913  524 
qed "analz_trivial"; 
1839  525 

526 
(*Helps to prove Fake cases*) 

1913  527 
goal thy "!!X. X: analz (UN i. analz (H i)) ==> X: analz (UN i. H i)"; 
2032  528 
by (etac analz.induct 1); 
1913  529 
by (ALLGOALS (fast_tac (!claset addEs [impOfSubs analz_mono]))); 
1839  530 
val lemma = result(); 
531 

1913  532 
goal thy "analz (UN i. analz (H i)) = analz (UN i. H i)"; 
1839  533 
by (fast_tac (!claset addIs [lemma] 
2032  534 
addEs [impOfSubs analz_mono]) 1); 
1913  535 
qed "analz_UN_analz"; 
536 
Addsimps [analz_UN_analz]; 

1839  537 

538 

1913  539 
(**** Inductive relation "synth" ****) 
1839  540 

1913  541 
AddIs synth.intrs; 
1839  542 

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

545 
val mk_cases = synth.mk_cases msg.simps; 

546 

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

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

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

550 
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

551 
val Crypt_synth = mk_cases "Crypt K X : synth H"; 
2011  552 

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

554 

1913  555 
goal thy "H <= synth(H)"; 
1839  556 
by (Fast_tac 1); 
1913  557 
qed "synth_increasing"; 
1839  558 

559 
(*Monotonicity*) 

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

1913  563 
qed "synth_mono"; 
1839  564 

565 
(** Unions **) 

566 

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

571 
qed "synth_Un"; 

1839  572 

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

575 
qed "synth_insert"; 

1885  576 

1839  577 
(** Idempotence and transitivity **) 
578 

1913  579 
goal thy "!!H. X: synth (synth H) ==> X: synth H"; 
2032  580 
by (etac synth.induct 1); 
1839  581 
by (ALLGOALS Fast_tac); 
1913  582 
qed "synth_synthE"; 
583 
AddSEs [synth_synthE]; 

1839  584 

1913  585 
goal thy "synth (synth H) = synth H"; 
1839  586 
by (Fast_tac 1); 
1913  587 
qed "synth_idem"; 
1839  588 

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

1839  591 
by (Fast_tac 1); 
1913  592 
qed "synth_trans"; 
1839  593 

594 
(*Cut; Lemma 2 of Lowe*) 

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

595 
goal thy "!!H. [ Y: synth (insert X H); X: synth H ] ==> Y: synth H"; 
2032  596 
by (etac synth_trans 1); 
1839  597 
by (Fast_tac 1); 
1913  598 
qed "synth_cut"; 
1839  599 

1946  600 
goal thy "Agent A : synth H"; 
601 
by (Fast_tac 1); 

602 
qed "Agent_synth"; 

603 

1913  604 
goal thy "(Nonce N : synth H) = (Nonce N : H)"; 
1839  605 
by (Fast_tac 1); 
1913  606 
qed "Nonce_synth_eq"; 
1839  607 

1913  608 
goal thy "(Key K : synth H) = (Key K : H)"; 
1839  609 
by (Fast_tac 1); 
1913  610 
qed "Key_synth_eq"; 
1839  611 

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

612 
goal thy "!!K. Key K ~: H ==> (Crypt K X : synth H) = (Crypt K X: H)"; 
2011  613 
by (Fast_tac 1); 
614 
qed "Crypt_synth_eq"; 

615 

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

1839  617 

618 

619 
goalw thy [keysFor_def] 

1913  620 
"keysFor (synth H) = keysFor H Un invKey``{K. Key K : H}"; 
1839  621 
by (Fast_tac 1); 
1913  622 
qed "keysFor_synth"; 
623 
Addsimps [keysFor_synth]; 

1839  624 

625 

1913  626 
(*** Combinations of parts, analz and synth ***) 
1839  627 

1913  628 
goal thy "parts (synth H) = parts H Un synth H"; 
2032  629 
by (rtac equalityI 1); 
630 
by (rtac subsetI 1); 

631 
by (etac parts.induct 1); 

1839  632 
by (ALLGOALS 
1913  633 
(best_tac (!claset addIs ((synth_increasing RS parts_mono RS subsetD) 
2032  634 
::parts.intrs)))); 
1913  635 
qed "parts_synth"; 
636 
Addsimps [parts_synth]; 

1839  637 

1913  638 
goal thy "analz (synth H) = analz H Un synth H"; 
2032  639 
by (rtac equalityI 1); 
640 
by (rtac subsetI 1); 

641 
by (etac analz.induct 1); 

1839  642 
by (best_tac 
1913  643 
(!claset addIs [synth_increasing RS analz_mono RS subsetD]) 5); 
1839  644 
(*Strange that best_tac just can't hack this one...*) 
1913  645 
by (ALLGOALS (deepen_tac (!claset addIs analz.intrs) 0)); 
646 
qed "analz_synth"; 

647 
Addsimps [analz_synth]; 

1839  648 

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

2032  652 
by (rtac equalityI 1); 
653 
by (rtac subsetI 1); 

654 
by (etac analz.induct 1); 

1839  655 
by (best_tac 
1913  656 
(!claset addEs [impOfSubs synth_increasing, 
2032  657 
impOfSubs analz_mono]) 5); 
1839  658 
by (Best_tac 1); 
1913  659 
by (deepen_tac (!claset addIs [analz.Fst]) 0 1); 
660 
by (deepen_tac (!claset addIs [analz.Snd]) 0 1); 

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

2032  662 
addIs [analz.Decrypt]) 0 1); 
1913  663 
qed "analz_UN1_synth"; 
664 
Addsimps [analz_UN1_synth]; 

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

665 

1946  666 

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

668 

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

669 
goal thy "!!Y. X: G ==> parts(insert X H) <= parts G Un parts H"; 
2032  670 
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

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

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

673 

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

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

2032  677 
by (dtac parts_insert_subset_Un 1); 
1946  678 
by (Full_simp_tac 1); 
679 
by (Deepen_tac 0 1); 

680 
qed "Fake_parts_insert"; 

681 

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

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

685 
\ ==> Crypt K Y : parts G Un parts H"; 
2061  686 
by (dtac (impOfSubs Fake_parts_insert) 1); 
2170  687 
by (assume_tac 1); 
2061  688 
by (fast_tac (!claset addDs [impOfSubs analz_subset_parts] 
689 
addss (!simpset)) 1); 

690 
qed "Crypt_Fake_parts_insert"; 

691 

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

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

697 
addSEs [impOfSubs analz_mono]) 2); 

698 
by (Full_simp_tac 1); 

699 
by (Fast_tac 1); 

700 
qed "Fake_analz_insert"; 

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

701 

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

704 
val analz_conj_parts = result(); 

705 

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

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

708 
val analz_disj_parts = result(); 

709 

710 
AddIffs [analz_conj_parts, analz_disj_parts]; 

711 

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

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

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

714 
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

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

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

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

718 

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

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

720 

2154  721 
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

722 
\ ==> (Crypt K X : synth (analz H)) = (X : synth (analz H))"; 
2154  723 
by (Fast_tac 1); 
724 
qed "Crypt_synth_analz"; 

725 

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

726 

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

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

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

729 

2327  730 

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

732 
be pulled out using the analz_insert rules **) 

733 

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

735 
insert_commute; 

736 

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

738 
["Agent ?C", "Nonce ?N", "MPair ?X ?Y", "Crypt ?X ?K'"]; 

739 

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

741 
["Agent ?C", "Nonce ?N", "MPair ?X' ?Y"]; 

742 

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

744 
val pushes = pushKeys@pushCrypts; 

745 

746 

747 
(*No premature instantiation of variables. For proving weak liveness.*) 

748 
fun safe_solver prems = 

749 
match_tac (TrueI::refl::prems) ORELSE' eq_assume_tac 

750 
ORELSE' etac FalseE; 

751 

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

753 
Abstraction over i is ESSENTIAL: it delays the dereferencing of claset 

754 
DEPENDS UPON "X" REFERRING TO THE FRADULENT MESSAGE *) 

755 
fun spy_analz_tac i = 

756 
SELECT_GOAL 

757 
(EVERY [ (*push in occurrences of X...*) 

758 
(REPEAT o CHANGED) 

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

760 
(*...allowing further simplifications*) 

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

762 
REPEAT (resolve_tac [allI,impI,notI] 1), 

763 
dtac (impOfSubs Fake_analz_insert) 1, 

764 
eresolve_tac [asm_rl, synth.Inj] 1, 

765 
Fast_tac 1, 

766 
Asm_full_simp_tac 1, 

767 
IF_UNSOLVED (depth_tac (!claset addIs [impOfSubs analz_mono]) 2 1) 

768 
]) i; 

769 

770 

771 
(*Useful in many uniqueness proofs*) 

772 
fun ex_strip_tac i = REPEAT (swap_res_tac [exI, conjI] i) THEN 

773 
assume_tac (i+1); 

774 