author  paulson 
Fri, 11 Jul 1997 13:26:15 +0200  
changeset 3512  9dcb4daa15e8 
parent 3476  1be4fee7606b 
child 3514  eb16b8e8d872 
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 

2373  12 
AddIffs (msg.inject); 
1839  13 

14 
(** Inverse of keys **) 

15 

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

17 
by (Step_tac 1); 

2032  18 
by (rtac box_equals 1); 
1839  19 
by (REPEAT (rtac invKey 2)); 
20 
by (Asm_simp_tac 1); 

21 
qed "invKey_eq"; 

22 

23 
Addsimps [invKey, invKey_eq]; 

24 

25 

26 
(**** keysFor operator ****) 

27 

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

2891  29 
by (Blast_tac 1); 
1839  30 
qed "keysFor_empty"; 
31 

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

2891  33 
by (Blast_tac 1); 
1839  34 
qed "keysFor_Un"; 
35 

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

2891  37 
by (Blast_tac 1); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
3102
diff
changeset

38 
qed "keysFor_UN1"; 
1839  39 

40 
(*Monotonicity*) 

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

2891  42 
by (Blast_tac 1); 
1839  43 
qed "keysFor_mono"; 
44 

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

3102  46 
by (Blast_tac 1); 
1839  47 
qed "keysFor_insert_Agent"; 
48 

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

3102  50 
by (Blast_tac 1); 
1839  51 
qed "keysFor_insert_Nonce"; 
52 

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

3102  54 
by (Blast_tac 1); 
1839  55 
qed "keysFor_insert_Key"; 
56 

2373  57 
goalw thy [keysFor_def] "keysFor (insert (Hash X) H) = keysFor H"; 
3102  58 
by (Blast_tac 1); 
2373  59 
qed "keysFor_insert_Hash"; 
60 

1839  61 
goalw thy [keysFor_def] "keysFor (insert {X,Y} H) = keysFor H"; 
3102  62 
by (Blast_tac 1); 
1839  63 
qed "keysFor_insert_MPair"; 
64 

65 
goalw thy [keysFor_def] 

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

66 
"keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)"; 
1839  67 
by (Auto_tac()); 
68 
qed "keysFor_insert_Crypt"; 

69 

3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
3102
diff
changeset

70 
Addsimps [keysFor_empty, keysFor_Un, keysFor_UN1, 
2373  71 
keysFor_insert_Agent, keysFor_insert_Nonce, keysFor_insert_Key, 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2484
diff
changeset

72 
keysFor_insert_Hash, keysFor_insert_MPair, keysFor_insert_Crypt]; 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
3102
diff
changeset

73 
AddSEs [keysFor_Un RS equalityD1 RS subsetD RS UnE, 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
3102
diff
changeset

74 
keysFor_UN1 RS equalityD1 RS subsetD RS UN1_E]; 
1839  75 

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

76 
goalw thy [keysFor_def] "!!H. Crypt K X : H ==> invKey K : keysFor H"; 
2891  77 
by (Blast_tac 1); 
2068  78 
qed "Crypt_imp_invKey_keysFor"; 
79 

1839  80 

81 
(**** Inductive relation "parts" ****) 

82 

83 
val major::prems = 

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

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

86 
\ ] ==> P"; 

87 
by (cut_facts_tac [major] 1); 

2032  88 
by (resolve_tac prems 1); 
1839  89 
by (REPEAT (eresolve_tac [asm_rl, parts.Fst, parts.Snd] 1)); 
90 
qed "MPair_parts"; 

91 

92 
AddIs [parts.Inj]; 

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

93 

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

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

95 

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

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

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

98 
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

99 
proofs concern only atomic messages.*) 
1839  100 

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

2891  102 
by (Blast_tac 1); 
1839  103 
qed "parts_increasing"; 
104 

105 
(*Monotonicity*) 

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

107 
by (rtac lfp_mono 1); 

108 
by (REPEAT (ares_tac basic_monos 1)); 

109 
qed "parts_mono"; 

110 

2373  111 
val parts_insertI = impOfSubs (subset_insertI RS parts_mono); 
112 

1839  113 
goal thy "parts{} = {}"; 
114 
by (Step_tac 1); 

2032  115 
by (etac parts.induct 1); 
2891  116 
by (ALLGOALS Blast_tac); 
1839  117 
qed "parts_empty"; 
118 
Addsimps [parts_empty]; 

119 

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

121 
by (Asm_full_simp_tac 1); 

122 
qed "parts_emptyE"; 

123 
AddSEs [parts_emptyE]; 

124 

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

2032  127 
by (etac parts.induct 1); 
2891  128 
by (ALLGOALS Blast_tac); 
1893  129 
qed "parts_singleton"; 
130 

1839  131 

132 
(** Unions **) 

133 

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

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

136 
val parts_Un_subset1 = result(); 

137 

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

2032  139 
by (rtac subsetI 1); 
140 
by (etac parts.induct 1); 

2891  141 
by (ALLGOALS Blast_tac); 
1839  142 
val parts_Un_subset2 = result(); 
143 

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

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

146 
qed "parts_Un"; 

147 

2011  148 
goal thy "parts (insert X H) = parts {X} Un parts H"; 
1852  149 
by (stac (read_instantiate [("A","H")] insert_is_Un) 1); 
2011  150 
by (simp_tac (HOL_ss addsimps [parts_Un]) 1); 
151 
qed "parts_insert"; 

152 

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

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

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

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

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

1852  158 
qed "parts_insert2"; 
159 

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

162 
val parts_UN_subset1 = result(); 

163 

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

2032  165 
by (rtac subsetI 1); 
166 
by (etac parts.induct 1); 

2891  167 
by (ALLGOALS Blast_tac); 
1839  168 
val parts_UN_subset2 = result(); 
169 

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

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

172 
qed "parts_UN"; 

173 

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

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

176 
qed "parts_UN1"; 

177 

3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
3102
diff
changeset

178 
(*Added to simplify arguments to parts, analz and synth. 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
3102
diff
changeset

179 
NOTE: the UN versions are no longer used!*) 
1839  180 
Addsimps [parts_Un, parts_UN, parts_UN1]; 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
3102
diff
changeset

181 
AddSEs [parts_Un RS equalityD1 RS subsetD RS UnE, 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
3102
diff
changeset

182 
parts_UN RS equalityD1 RS subsetD RS UN_E, 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
3102
diff
changeset

183 
parts_UN1 RS equalityD1 RS subsetD RS UN1_E]; 
1839  184 

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

2922  186 
by (blast_tac (!claset addIs [impOfSubs parts_mono]) 1); 
1839  187 
qed "parts_insert_subset"; 
188 

189 
(** Idempotence and transitivity **) 

190 

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

2032  192 
by (etac parts.induct 1); 
2891  193 
by (ALLGOALS Blast_tac); 
2922  194 
qed "parts_partsD"; 
195 
AddSDs [parts_partsD]; 

1839  196 

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

2891  198 
by (Blast_tac 1); 
1839  199 
qed "parts_idem"; 
200 
Addsimps [parts_idem]; 

201 

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

203 
by (dtac parts_mono 1); 

2891  204 
by (Blast_tac 1); 
1839  205 
qed "parts_trans"; 
206 

207 
(*Cut*) 

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

2032  210 
by (etac parts_trans 1); 
2373  211 
by (Auto_tac()); 
1839  212 
qed "parts_cut"; 
213 

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

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

217 
addss (!simpset)) 1); 

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

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

219 

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

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

221 

1839  222 

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

224 

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

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

227 
etac parts.induct i, 
3102  228 
REPEAT (Blast_tac i)]; 
2373  229 

1839  230 
goal thy "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)"; 
2373  231 
by (parts_tac 1); 
1839  232 
qed "parts_insert_Agent"; 
233 

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

2373  235 
by (parts_tac 1); 
1839  236 
qed "parts_insert_Nonce"; 
237 

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

2373  239 
by (parts_tac 1); 
1839  240 
qed "parts_insert_Key"; 
241 

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

244 
qed "parts_insert_Hash"; 

245 

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

246 
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

247 
\ insert (Crypt K X) (parts (insert X H))"; 
2032  248 
by (rtac equalityI 1); 
249 
by (rtac subsetI 1); 

250 
by (etac parts.induct 1); 

1839  251 
by (Auto_tac()); 
2032  252 
by (etac parts.induct 1); 
2922  253 
by (ALLGOALS (blast_tac (!claset addIs [parts.Body]))); 
1839  254 
qed "parts_insert_Crypt"; 
255 

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

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

2032  258 
by (rtac equalityI 1); 
259 
by (rtac subsetI 1); 

260 
by (etac parts.induct 1); 

1839  261 
by (Auto_tac()); 
2032  262 
by (etac parts.induct 1); 
2922  263 
by (ALLGOALS (blast_tac (!claset addIs [parts.Fst, parts.Snd]))); 
1839  264 
qed "parts_insert_MPair"; 
265 

2373  266 
Addsimps [parts_insert_Agent, parts_insert_Nonce, parts_insert_Key, 
267 
parts_insert_Hash, parts_insert_Crypt, parts_insert_MPair]; 

1839  268 

269 

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

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

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

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

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

275 

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

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

277 

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

278 

1913  279 
(**** Inductive relation "analz" ****) 
1839  280 

281 
val major::prems = 

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

1839  284 
\ ] ==> P"; 
285 
by (cut_facts_tac [major] 1); 

2032  286 
by (resolve_tac prems 1); 
1913  287 
by (REPEAT (eresolve_tac [asm_rl, analz.Fst, analz.Snd] 1)); 
288 
qed "MPair_analz"; 

1839  289 

1913  290 
AddIs [analz.Inj]; 
2011  291 
AddSEs [MPair_analz]; (*Perhaps it should NOT be deemed safe!*) 
1913  292 
AddDs [analz.Decrypt]; 
1839  293 

1913  294 
Addsimps [analz.Inj]; 
1885  295 

1913  296 
goal thy "H <= analz(H)"; 
2891  297 
by (Blast_tac 1); 
1913  298 
qed "analz_increasing"; 
1839  299 

1913  300 
goal thy "analz H <= parts H"; 
1839  301 
by (rtac subsetI 1); 
2032  302 
by (etac analz.induct 1); 
2891  303 
by (ALLGOALS Blast_tac); 
1913  304 
qed "analz_subset_parts"; 
1839  305 

1913  306 
bind_thm ("not_parts_not_analz", analz_subset_parts RS contra_subsetD); 
1839  307 

308 

1913  309 
goal thy "parts (analz H) = parts H"; 
2032  310 
by (rtac equalityI 1); 
311 
by (rtac (analz_subset_parts RS parts_mono RS subset_trans) 1); 

1839  312 
by (Simp_tac 1); 
2891  313 
by (blast_tac (!claset addIs [analz_increasing RS parts_mono RS subsetD]) 1); 
1913  314 
qed "parts_analz"; 
315 
Addsimps [parts_analz]; 

1839  316 

1913  317 
goal thy "analz (parts H) = parts H"; 
1885  318 
by (Auto_tac()); 
2032  319 
by (etac analz.induct 1); 
1885  320 
by (Auto_tac()); 
1913  321 
qed "analz_parts"; 
322 
Addsimps [analz_parts]; 

1885  323 

1839  324 
(*Monotonicity; Lemma 1 of Lowe*) 
1913  325 
goalw thy analz.defs "!!G H. G<=H ==> analz(G) <= analz(H)"; 
1839  326 
by (rtac lfp_mono 1); 
327 
by (REPEAT (ares_tac basic_monos 1)); 

1913  328 
qed "analz_mono"; 
1839  329 

2373  330 
val analz_insertI = impOfSubs (subset_insertI RS analz_mono); 
331 

1839  332 
(** General equational properties **) 
333 

1913  334 
goal thy "analz{} = {}"; 
1839  335 
by (Step_tac 1); 
2032  336 
by (etac analz.induct 1); 
2891  337 
by (ALLGOALS Blast_tac); 
1913  338 
qed "analz_empty"; 
339 
Addsimps [analz_empty]; 

1839  340 

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

345 
qed "analz_Un"; 

1839  346 

1913  347 
goal thy "insert X (analz H) <= analz(insert X H)"; 
2922  348 
by (blast_tac (!claset addIs [impOfSubs analz_mono]) 1); 
1913  349 
qed "analz_insert"; 
1839  350 

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

352 

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

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

355 
etac analz.induct i, 
3102  356 
REPEAT (Blast_tac i)]; 
2373  357 

1913  358 
goal thy "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)"; 
2373  359 
by (analz_tac 1); 
1913  360 
qed "analz_insert_Agent"; 
1839  361 

1913  362 
goal thy "analz (insert (Nonce N) H) = insert (Nonce N) (analz H)"; 
2373  363 
by (analz_tac 1); 
1913  364 
qed "analz_insert_Nonce"; 
1839  365 

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

368 
qed "analz_insert_Hash"; 

369 

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

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

2373  374 
by (analz_tac 1); 
1913  375 
qed "analz_insert_Key"; 
1839  376 

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

2032  379 
by (rtac equalityI 1); 
380 
by (rtac subsetI 1); 

381 
by (etac analz.induct 1); 

1885  382 
by (Auto_tac()); 
2032  383 
by (etac analz.induct 1); 
2922  384 
by (ALLGOALS (blast_tac (!claset addIs [analz.Fst, analz.Snd]))); 
1913  385 
qed "analz_insert_MPair"; 
1885  386 

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

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

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

390 
\ insert (Crypt K X) (analz H)"; 
2373  391 
by (analz_tac 1); 
1913  392 
qed "analz_insert_Crypt"; 
1839  393 

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

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

396 
\ insert (Crypt K X) (analz (insert X H))"; 
2032  397 
by (rtac subsetI 1); 
1913  398 
by (eres_inst_tac [("za","x")] analz.induct 1); 
3102  399 
by (ALLGOALS (Blast_tac)); 
1839  400 
val lemma1 = result(); 
401 

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

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

404 
\ analz (insert (Crypt K X) H)"; 
1839  405 
by (Auto_tac()); 
1913  406 
by (eres_inst_tac [("za","x")] analz.induct 1); 
1839  407 
by (Auto_tac()); 
3449  408 
by (blast_tac (!claset addIs [analz_insertI, analz.Decrypt]) 1); 
1839  409 
val lemma2 = result(); 
410 

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

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

413 
\ insert (Crypt K X) (analz (insert X H))"; 
1839  414 
by (REPEAT (ares_tac [equalityI, lemma1, lemma2] 1)); 
1913  415 
qed "analz_insert_Decrypt"; 
1839  416 

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

420 
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

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

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

424 
\ else insert (Crypt K X) (analz H))"; 
2102  425 
by (case_tac "Key (invKey K) : analz H " 1); 
1913  426 
by (ALLGOALS (asm_simp_tac (!simpset addsimps [analz_insert_Crypt, 
2032  427 
analz_insert_Decrypt]))); 
1913  428 
qed "analz_Crypt_if"; 
1885  429 

2373  430 
Addsimps [analz_insert_Agent, analz_insert_Nonce, analz_insert_Key, 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2484
diff
changeset

431 
analz_insert_Hash, analz_insert_MPair, analz_Crypt_if]; 
1839  432 

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

434 
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

435 
\ insert (Crypt K X) (analz (insert X H))"; 
2032  436 
by (rtac subsetI 1); 
437 
by (etac analz.induct 1); 

1839  438 
by (Auto_tac()); 
1913  439 
qed "analz_insert_Crypt_subset"; 
1839  440 

441 

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

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

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

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

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

447 

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

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

449 

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

450 

1839  451 
(** Idempotence and transitivity **) 
452 

1913  453 
goal thy "!!H. X: analz (analz H) ==> X: analz H"; 
2032  454 
by (etac analz.induct 1); 
2891  455 
by (ALLGOALS Blast_tac); 
2922  456 
qed "analz_analzD"; 
457 
AddSDs [analz_analzD]; 

1839  458 

1913  459 
goal thy "analz (analz H) = analz H"; 
2891  460 
by (Blast_tac 1); 
1913  461 
qed "analz_idem"; 
462 
Addsimps [analz_idem]; 

1839  463 

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

2891  466 
by (Blast_tac 1); 
1913  467 
qed "analz_trans"; 
1839  468 

469 
(*Cut; Lemma 2 of Lowe*) 

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

470 
goal thy "!!H. [ Y: analz (insert X H); X: analz H ] ==> Y: analz H"; 
2032  471 
by (etac analz_trans 1); 
2891  472 
by (Blast_tac 1); 
1913  473 
qed "analz_cut"; 
1839  474 

475 
(*Cut can be proved easily by induction on 

1913  476 
"!!H. Y: analz (insert X H) ==> X: analz H > Y: analz H" 
1839  477 
*) 
478 

3449  479 
(*This rewrite rule helps in the simplification of messages that involve 
480 
the forwarding of unknown components (X). Without it, removing occurrences 

481 
of X can be very complicated. *) 

3431  482 
goal thy "!!H. X: analz H ==> analz (insert X H) = analz H"; 
483 
by (blast_tac (!claset addIs [analz_cut, analz_insertI]) 1); 

484 
qed "analz_insert_eq"; 

485 

1885  486 

1913  487 
(** A congruence rule for "analz" **) 
1885  488 

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

1885  491 
by (Step_tac 1); 
2032  492 
by (etac analz.induct 1); 
1913  493 
by (ALLGOALS (best_tac (!claset addIs [analz_mono RS subsetD]))); 
494 
qed "analz_subset_cong"; 

1885  495 

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

498 
by (REPEAT_FIRST (ares_tac [equalityI, analz_subset_cong] 

2032  499 
ORELSE' etac equalityE)); 
1913  500 
qed "analz_cong"; 
1885  501 

502 

1913  503 
goal thy "!!H. analz H = analz H' ==> analz(insert X H) = analz(insert X H')"; 
1885  504 
by (asm_simp_tac (!simpset addsimps [insert_def] 
2032  505 
setloop (rtac analz_cong)) 1); 
1913  506 
qed "analz_insert_cong"; 
1885  507 

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

509 
goal thy "!!H. [ ALL X Y. {X,Y} ~: H; ALL X K. Crypt K X ~: H ] ==> \ 
1913  510 
\ analz H = H"; 
1839  511 
by (Step_tac 1); 
2032  512 
by (etac analz.induct 1); 
2891  513 
by (ALLGOALS Blast_tac); 
1913  514 
qed "analz_trivial"; 
1839  515 

516 
(*Helps to prove Fake cases*) 

1913  517 
goal thy "!!X. X: analz (UN i. analz (H i)) ==> X: analz (UN i. H i)"; 
2032  518 
by (etac analz.induct 1); 
2922  519 
by (ALLGOALS (blast_tac (!claset addIs [impOfSubs analz_mono]))); 
1839  520 
val lemma = result(); 
521 

1913  522 
goal thy "analz (UN i. analz (H i)) = analz (UN i. H i)"; 
2922  523 
by (blast_tac (!claset addIs [lemma, impOfSubs analz_mono]) 1); 
1913  524 
qed "analz_UN_analz"; 
525 
Addsimps [analz_UN_analz]; 

1839  526 

527 

1913  528 
(**** Inductive relation "synth" ****) 
1839  529 

1913  530 
AddIs synth.intrs; 
1839  531 

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

534 
val mk_cases = synth.mk_cases msg.simps; 

535 

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

536 
(*NO Agent_synth, as any Agent name can be synthesized*) 
2011  537 
val Nonce_synth = mk_cases "Nonce n : synth H"; 
538 
val Key_synth = mk_cases "Key K : synth H"; 

2373  539 
val Hash_synth = mk_cases "Hash X : synth H"; 
2011  540 
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

541 
val Crypt_synth = mk_cases "Crypt K X : synth H"; 
2011  542 

2373  543 
AddSEs [Nonce_synth, Key_synth, Hash_synth, MPair_synth, Crypt_synth]; 
2011  544 

1913  545 
goal thy "H <= synth(H)"; 
2891  546 
by (Blast_tac 1); 
1913  547 
qed "synth_increasing"; 
1839  548 

549 
(*Monotonicity*) 

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

1913  553 
qed "synth_mono"; 
1839  554 

555 
(** Unions **) 

556 

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

561 
qed "synth_Un"; 

1839  562 

1913  563 
goal thy "insert X (synth H) <= synth(insert X H)"; 
2922  564 
by (blast_tac (!claset addIs [impOfSubs synth_mono]) 1); 
1913  565 
qed "synth_insert"; 
1885  566 

1839  567 
(** Idempotence and transitivity **) 
568 

1913  569 
goal thy "!!H. X: synth (synth H) ==> X: synth H"; 
2032  570 
by (etac synth.induct 1); 
2891  571 
by (ALLGOALS Blast_tac); 
2922  572 
qed "synth_synthD"; 
573 
AddSDs [synth_synthD]; 

1839  574 

1913  575 
goal thy "synth (synth H) = synth H"; 
2891  576 
by (Blast_tac 1); 
1913  577 
qed "synth_idem"; 
1839  578 

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

2891  581 
by (Blast_tac 1); 
1913  582 
qed "synth_trans"; 
1839  583 

584 
(*Cut; Lemma 2 of Lowe*) 

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

585 
goal thy "!!H. [ Y: synth (insert X H); X: synth H ] ==> Y: synth H"; 
2032  586 
by (etac synth_trans 1); 
2891  587 
by (Blast_tac 1); 
1913  588 
qed "synth_cut"; 
1839  589 

1946  590 
goal thy "Agent A : synth H"; 
2891  591 
by (Blast_tac 1); 
1946  592 
qed "Agent_synth"; 
593 

1913  594 
goal thy "(Nonce N : synth H) = (Nonce N : H)"; 
2891  595 
by (Blast_tac 1); 
1913  596 
qed "Nonce_synth_eq"; 
1839  597 

1913  598 
goal thy "(Key K : synth H) = (Key K : H)"; 
2891  599 
by (Blast_tac 1); 
1913  600 
qed "Key_synth_eq"; 
1839  601 

2373  602 
goal thy "!!K. Key K ~: H ==> (Crypt K X : synth H) = (Crypt K X : H)"; 
2891  603 
by (Blast_tac 1); 
2011  604 
qed "Crypt_synth_eq"; 
605 

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

1839  607 

608 

609 
goalw thy [keysFor_def] 

1913  610 
"keysFor (synth H) = keysFor H Un invKey``{K. Key K : H}"; 
2891  611 
by (Blast_tac 1); 
1913  612 
qed "keysFor_synth"; 
613 
Addsimps [keysFor_synth]; 

1839  614 

615 

1913  616 
(*** Combinations of parts, analz and synth ***) 
1839  617 

1913  618 
goal thy "parts (synth H) = parts H Un synth H"; 
2032  619 
by (rtac equalityI 1); 
620 
by (rtac subsetI 1); 

621 
by (etac parts.induct 1); 

1839  622 
by (ALLGOALS 
2922  623 
(blast_tac (!claset addIs ((synth_increasing RS parts_mono RS subsetD) 
2032  624 
::parts.intrs)))); 
1913  625 
qed "parts_synth"; 
626 
Addsimps [parts_synth]; 

1839  627 

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

630 
by (ALLGOALS Simp_tac); 

631 
qed "analz_analz_Un"; 

632 

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

2032  634 
by (rtac equalityI 1); 
635 
by (rtac subsetI 1); 

636 
by (etac analz.induct 1); 

2922  637 
by (blast_tac (!claset addIs [impOfSubs analz_mono]) 5); 
638 
by (ALLGOALS (blast_tac (!claset addIs analz.intrs))); 

2373  639 
qed "analz_synth_Un"; 
640 

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

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

643 
by (Full_simp_tac 1); 

1913  644 
qed "analz_synth"; 
2373  645 
Addsimps [analz_analz_Un, analz_synth_Un, analz_synth]; 
1839  646 

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

2032  650 
by (rtac equalityI 1); 
651 
by (rtac subsetI 1); 

652 
by (etac analz.induct 1); 

2922  653 
by (blast_tac 
654 
(!claset addIs [impOfSubs synth_increasing, 

2032  655 
impOfSubs analz_mono]) 5); 
2891  656 
by (Blast_tac 1); 
657 
by (blast_tac (!claset addIs [analz.Inj RS analz.Fst]) 1); 

658 
by (blast_tac (!claset addIs [analz.Inj RS analz.Snd]) 1); 

659 
by (blast_tac (!claset addIs [analz.Decrypt]) 1); 

1913  660 
qed "analz_UN1_synth"; 
661 
Addsimps [analz_UN1_synth]; 

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

662 

1946  663 

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

665 

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

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

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

670 

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

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

2032  674 
by (dtac parts_insert_subset_Un 1); 
1946  675 
by (Full_simp_tac 1); 
2891  676 
by (Blast_tac 1); 
1946  677 
qed "Fake_parts_insert"; 
678 

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

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

682 
\ ==> Crypt K Y : parts G Un parts H"; 
2061  683 
by (dtac (impOfSubs Fake_parts_insert) 1); 
2170  684 
by (assume_tac 1); 
3102  685 
by (blast_tac (!claset addDs [impOfSubs analz_subset_parts]) 1); 
2061  686 
qed "Crypt_Fake_parts_insert"; 
687 

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

690 
by (rtac subsetI 1); 

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

2922  692 
by (blast_tac (!claset addIs [impOfSubs analz_mono, 
693 
impOfSubs (analz_mono RS synth_mono)]) 2); 

2373  694 
by (Full_simp_tac 1); 
2891  695 
by (Blast_tac 1); 
2373  696 
qed "Fake_analz_insert"; 
697 

2011  698 
goal thy "(X: analz H & X: parts H) = (X: analz H)"; 
2891  699 
by (blast_tac (!claset addIs [impOfSubs analz_subset_parts]) 1); 
2011  700 
val analz_conj_parts = result(); 
701 

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

2891  703 
by (blast_tac (!claset addIs [impOfSubs analz_subset_parts]) 1); 
2011  704 
val analz_disj_parts = result(); 
705 

706 
AddIffs [analz_conj_parts, analz_disj_parts]; 

707 

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

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

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

710 
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

711 
\ (X : synth (analz H) & Y : synth (analz H))"; 
2891  712 
by (Blast_tac 1); 
1998
f8230821f1e8
Reordering of premises for cut theorems, and new law MPair_synth_analz
paulson
parents:
1994
diff
changeset

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

714 

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

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

716 

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

718 
\ ==> (Crypt K X : synth (analz H)) = (X : synth (analz H))"; 
2891  719 
by (Blast_tac 1); 
2154  720 
qed "Crypt_synth_analz"; 
721 

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

722 

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

723 
goal thy "!!K. X ~: synth (analz H) \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2484
diff
changeset

724 
\ ==> (Hash{X,Y} : synth (analz H)) = (Hash{X,Y} : analz H)"; 
2891  725 
by (Blast_tac 1); 
2373  726 
qed "Hash_synth_analz"; 
727 
Addsimps [Hash_synth_analz]; 

728 

729 

2484  730 
(**** HPair: a combination of Hash and MPair ****) 
731 

732 
(*** Freeness ***) 

733 

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

734 
goalw thy [HPair_def] "Agent A ~= Hash[X] Y"; 
2484  735 
by (Simp_tac 1); 
736 
qed "Agent_neq_HPair"; 

737 

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

738 
goalw thy [HPair_def] "Nonce N ~= Hash[X] Y"; 
2484  739 
by (Simp_tac 1); 
740 
qed "Nonce_neq_HPair"; 

741 

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

742 
goalw thy [HPair_def] "Key K ~= Hash[X] Y"; 
2484  743 
by (Simp_tac 1); 
744 
qed "Key_neq_HPair"; 

745 

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

746 
goalw thy [HPair_def] "Hash Z ~= Hash[X] Y"; 
2484  747 
by (Simp_tac 1); 
748 
qed "Hash_neq_HPair"; 

749 

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

750 
goalw thy [HPair_def] "Crypt K X' ~= Hash[X] Y"; 
2484  751 
by (Simp_tac 1); 
752 
qed "Crypt_neq_HPair"; 

753 

754 
val HPair_neqs = [Agent_neq_HPair, Nonce_neq_HPair, 

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

755 
Key_neq_HPair, Hash_neq_HPair, Crypt_neq_HPair]; 
2484  756 

757 
AddIffs HPair_neqs; 

758 
AddIffs (HPair_neqs RL [not_sym]); 

759 

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

760 
goalw thy [HPair_def] "(Hash[X'] Y' = Hash[X] Y) = (X' = X & Y'=Y)"; 
2484  761 
by (Simp_tac 1); 
762 
qed "HPair_eq"; 

763 

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

764 
goalw thy [HPair_def] "({X',Y'} = Hash[X] Y) = (X' = Hash{X,Y} & Y'=Y)"; 
2484  765 
by (Simp_tac 1); 
766 
qed "MPair_eq_HPair"; 

767 

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

768 
goalw thy [HPair_def] "(Hash[X] Y = {X',Y'}) = (X' = Hash{X,Y} & Y'=Y)"; 
2484  769 
by (Auto_tac()); 
770 
qed "HPair_eq_MPair"; 

771 

772 
AddIffs [HPair_eq, MPair_eq_HPair, HPair_eq_MPair]; 

773 

774 

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

776 

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

777 
goalw thy [HPair_def] "keysFor (insert (Hash[X] Y) H) = keysFor H"; 
2484  778 
by (Simp_tac 1); 
779 
qed "keysFor_insert_HPair"; 

780 

781 
goalw thy [HPair_def] 

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

782 
"parts (insert (Hash[X] Y) H) = \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2484
diff
changeset

783 
\ insert (Hash[X] Y) (insert (Hash{X,Y}) (parts (insert Y H)))"; 
2484  784 
by (Simp_tac 1); 
785 
qed "parts_insert_HPair"; 

786 

787 
goalw thy [HPair_def] 

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

788 
"analz (insert (Hash[X] Y) H) = \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2484
diff
changeset

789 
\ insert (Hash[X] Y) (insert (Hash{X,Y}) (analz (insert Y H)))"; 
2484  790 
by (Simp_tac 1); 
791 
qed "analz_insert_HPair"; 

792 

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

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

794 
\ ==> (Hash[X] Y : synth (analz H)) = \ 
2484  795 
\ (Hash {X, Y} : analz H & Y : synth (analz H))"; 
796 
by (Simp_tac 1); 

2891  797 
by (Blast_tac 1); 
2484  798 
qed "HPair_synth_analz"; 
799 

800 
Addsimps [keysFor_insert_HPair, parts_insert_HPair, analz_insert_HPair, 

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

801 
HPair_synth_analz, HPair_synth_analz]; 
2484  802 

803 

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

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

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

806 

2327  807 

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

809 
be pulled out using the analz_insert rules **) 

810 

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

812 
insert_commute; 

813 

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

2373  815 
["Agent ?C", "Nonce ?N", "Hash ?X", 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2484
diff
changeset

816 
"MPair ?X ?Y", "Crypt ?X ?K'"]; 
2327  817 

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

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

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

822 
val pushes = pushKeys@pushCrypts; 

823 

3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
3102
diff
changeset

824 

cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
3102
diff
changeset

825 
(*** Tactics useful for many protocol proofs ***) 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
3102
diff
changeset

826 

3470  827 
(*Prove base case (subgoal i) and simplify others. A typical base case 
828 
concerns Crypt K X ~: Key``shrK``lost and cannot be proved by rewriting 

829 
alone.*) 

3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
3102
diff
changeset

830 
fun prove_simple_subgoals_tac i = 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
3102
diff
changeset

831 
fast_tac (!claset addss (!simpset)) i THEN 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
3102
diff
changeset

832 
ALLGOALS Asm_simp_tac; 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
3102
diff
changeset

833 

cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
3102
diff
changeset

834 
fun Fake_parts_insert_tac i = 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
3102
diff
changeset

835 
blast_tac (!claset addDs [impOfSubs analz_subset_parts, 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
3102
diff
changeset

836 
impOfSubs Fake_parts_insert]) i; 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
3102
diff
changeset

837 

cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
3102
diff
changeset

838 
(*Apply rules to break down assumptions of the form 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
3102
diff
changeset

839 
Y : parts(insert X H) and Y : analz(insert X H) 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
3102
diff
changeset

840 
*) 
2373  841 
val Fake_insert_tac = 
842 
dresolve_tac [impOfSubs Fake_analz_insert, 

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

843 
impOfSubs Fake_parts_insert] THEN' 
2373  844 
eresolve_tac [asm_rl, synth.Inj]; 
845 

3449  846 
(*Analysis of Fake cases. Also works for messages that forward unknown parts, 
847 
but this application is no longer necessary if analz_insert_eq is used. 

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

850 
fun spy_analz_tac i = 

2373  851 
DETERM 
852 
(SELECT_GOAL 

853 
(EVERY 

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

855 
(REPEAT o CHANGED) 

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

857 
(*...allowing further simplifications*) 

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

3476
1be4fee7606b
spy_analz_tac: Restored iffI to the list of rules used to break down
paulson
parents:
3470
diff
changeset

859 
REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])), 
2373  860 
DEPTH_SOLVE 
861 
(REPEAT (Fake_insert_tac 1) THEN Asm_full_simp_tac 1 

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

862 
THEN 
3102  863 
IF_UNSOLVED (Blast.depth_tac 
864 
(!claset addIs [impOfSubs analz_mono, 

865 
impOfSubs analz_subset_parts]) 2 1)) 

2373  866 
]) i); 
2327  867 

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

871 

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

874 
fun prove_unique_tac lemma = 

875 
EVERY' [dtac lemma, 

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

876 
REPEAT o (mp_tac ORELSE' eresolve_tac [asm_rl,exE]), 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2484
diff
changeset

877 
(*Duplicate the assumption*) 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2484
diff
changeset

878 
forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl, 
3102  879 
Blast.depth_tac (!claset addSDs [spec]) 0]; 
2415  880 

2373  881 

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

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

2891  884 
by (Blast_tac 1); 
2373  885 
val Un_absorb3 = result(); 
886 
Addsimps [Un_absorb3]; 