author  nipkow 
Fri, 01 Aug 1997 09:41:38 +0200  
changeset 3583  5a47b869d16a 
parent 3519  ab0a9fbed4c0 
child 3650  282ffdc91884 
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 

3514
eb16b8e8d872
Moved some declarations to Message from Public and Shared
paulson
parents:
3476
diff
changeset

14 
(*Holds because Friend is injective: thus cannot prove for all f*) 
eb16b8e8d872
Moved some declarations to Message from Public and Shared
paulson
parents:
3476
diff
changeset

15 
goal thy "(Friend x : Friend``A) = (x:A)"; 
eb16b8e8d872
Moved some declarations to Message from Public and Shared
paulson
parents:
3476
diff
changeset

16 
by (Auto_tac()); 
eb16b8e8d872
Moved some declarations to Message from Public and Shared
paulson
parents:
3476
diff
changeset

17 
qed "Friend_image_eq"; 
eb16b8e8d872
Moved some declarations to Message from Public and Shared
paulson
parents:
3476
diff
changeset

18 
Addsimps [Friend_image_eq]; 
eb16b8e8d872
Moved some declarations to Message from Public and Shared
paulson
parents:
3476
diff
changeset

19 

eb16b8e8d872
Moved some declarations to Message from Public and Shared
paulson
parents:
3476
diff
changeset

20 

1839  21 
(** Inverse of keys **) 
22 

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

24 
by (Step_tac 1); 

2032  25 
by (rtac box_equals 1); 
1839  26 
by (REPEAT (rtac invKey 2)); 
27 
by (Asm_simp_tac 1); 

28 
qed "invKey_eq"; 

29 

30 
Addsimps [invKey, invKey_eq]; 

31 

32 

33 
(**** keysFor operator ****) 

34 

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

2891  36 
by (Blast_tac 1); 
1839  37 
qed "keysFor_empty"; 
38 

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

2891  40 
by (Blast_tac 1); 
1839  41 
qed "keysFor_Un"; 
42 

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

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

45 
qed "keysFor_UN1"; 
1839  46 

47 
(*Monotonicity*) 

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

2891  49 
by (Blast_tac 1); 
1839  50 
qed "keysFor_mono"; 
51 

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

3102  53 
by (Blast_tac 1); 
1839  54 
qed "keysFor_insert_Agent"; 
55 

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

3102  57 
by (Blast_tac 1); 
1839  58 
qed "keysFor_insert_Nonce"; 
59 

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

3102  61 
by (Blast_tac 1); 
1839  62 
qed "keysFor_insert_Key"; 
63 

2373  64 
goalw thy [keysFor_def] "keysFor (insert (Hash X) H) = keysFor H"; 
3102  65 
by (Blast_tac 1); 
2373  66 
qed "keysFor_insert_Hash"; 
67 

1839  68 
goalw thy [keysFor_def] "keysFor (insert {X,Y} H) = keysFor H"; 
3102  69 
by (Blast_tac 1); 
1839  70 
qed "keysFor_insert_MPair"; 
71 

72 
goalw thy [keysFor_def] 

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

73 
"keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)"; 
1839  74 
by (Auto_tac()); 
75 
qed "keysFor_insert_Crypt"; 

76 

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

77 
Addsimps [keysFor_empty, keysFor_Un, keysFor_UN1, 
2373  78 
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

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

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

81 
keysFor_UN1 RS equalityD1 RS subsetD RS UN1_E]; 
1839  82 

3514
eb16b8e8d872
Moved some declarations to Message from Public and Shared
paulson
parents:
3476
diff
changeset

83 
goalw thy [keysFor_def] "keysFor (Key``E) = {}"; 
eb16b8e8d872
Moved some declarations to Message from Public and Shared
paulson
parents:
3476
diff
changeset

84 
by (Auto_tac ()); 
eb16b8e8d872
Moved some declarations to Message from Public and Shared
paulson
parents:
3476
diff
changeset

85 
qed "keysFor_image_Key"; 
eb16b8e8d872
Moved some declarations to Message from Public and Shared
paulson
parents:
3476
diff
changeset

86 
Addsimps [keysFor_image_Key]; 
eb16b8e8d872
Moved some declarations to Message from Public and Shared
paulson
parents:
3476
diff
changeset

87 

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

88 
goalw thy [keysFor_def] "!!H. Crypt K X : H ==> invKey K : keysFor H"; 
2891  89 
by (Blast_tac 1); 
2068  90 
qed "Crypt_imp_invKey_keysFor"; 
91 

1839  92 

93 
(**** Inductive relation "parts" ****) 

94 

95 
val major::prems = 

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

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

98 
\ ] ==> P"; 

99 
by (cut_facts_tac [major] 1); 

2032  100 
by (resolve_tac prems 1); 
1839  101 
by (REPEAT (eresolve_tac [asm_rl, parts.Fst, parts.Snd] 1)); 
102 
qed "MPair_parts"; 

103 

104 
AddIs [parts.Inj]; 

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

105 

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

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

107 

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

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

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

110 
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

111 
proofs concern only atomic messages.*) 
1839  112 

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

2891  114 
by (Blast_tac 1); 
1839  115 
qed "parts_increasing"; 
116 

117 
(*Monotonicity*) 

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

119 
by (rtac lfp_mono 1); 

120 
by (REPEAT (ares_tac basic_monos 1)); 

121 
qed "parts_mono"; 

122 

2373  123 
val parts_insertI = impOfSubs (subset_insertI RS parts_mono); 
124 

1839  125 
goal thy "parts{} = {}"; 
126 
by (Step_tac 1); 

2032  127 
by (etac parts.induct 1); 
2891  128 
by (ALLGOALS Blast_tac); 
1839  129 
qed "parts_empty"; 
130 
Addsimps [parts_empty]; 

131 

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

133 
by (Asm_full_simp_tac 1); 

134 
qed "parts_emptyE"; 

135 
AddSEs [parts_emptyE]; 

136 

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

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

1839  143 

144 
(** Unions **) 

145 

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

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

148 
val parts_Un_subset1 = result(); 

149 

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

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

2891  153 
by (ALLGOALS Blast_tac); 
1839  154 
val parts_Un_subset2 = result(); 
155 

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

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

158 
qed "parts_Un"; 

159 

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

164 

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

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

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

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

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

1852  170 
qed "parts_insert2"; 
171 

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

174 
val parts_UN_subset1 = result(); 

175 

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

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

2891  179 
by (ALLGOALS Blast_tac); 
1839  180 
val parts_UN_subset2 = result(); 
181 

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

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

184 
qed "parts_UN"; 

185 

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

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

188 
qed "parts_UN1"; 

189 

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

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

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

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

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

195 
parts_UN1 RS equalityD1 RS subsetD RS UN1_E]; 
1839  196 

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

2922  198 
by (blast_tac (!claset addIs [impOfSubs parts_mono]) 1); 
1839  199 
qed "parts_insert_subset"; 
200 

201 
(** Idempotence and transitivity **) 

202 

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

2032  204 
by (etac parts.induct 1); 
2891  205 
by (ALLGOALS Blast_tac); 
2922  206 
qed "parts_partsD"; 
207 
AddSDs [parts_partsD]; 

1839  208 

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

2891  210 
by (Blast_tac 1); 
1839  211 
qed "parts_idem"; 
212 
Addsimps [parts_idem]; 

213 

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

215 
by (dtac parts_mono 1); 

2891  216 
by (Blast_tac 1); 
1839  217 
qed "parts_trans"; 
218 

219 
(*Cut*) 

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

2032  222 
by (etac parts_trans 1); 
2373  223 
by (Auto_tac()); 
1839  224 
qed "parts_cut"; 
225 

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

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

229 
addss (!simpset)) 1); 

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

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

231 

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

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

233 

1839  234 

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

236 

2373  237 
fun parts_tac i = 
238 
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

239 
etac parts.induct i, 
3102  240 
REPEAT (Blast_tac i)]; 
2373  241 

1839  242 
goal thy "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)"; 
2373  243 
by (parts_tac 1); 
1839  244 
qed "parts_insert_Agent"; 
245 

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

2373  247 
by (parts_tac 1); 
1839  248 
qed "parts_insert_Nonce"; 
249 

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

2373  251 
by (parts_tac 1); 
1839  252 
qed "parts_insert_Key"; 
253 

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

256 
qed "parts_insert_Hash"; 

257 

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

258 
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

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

262 
by (etac parts.induct 1); 

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

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

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

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

272 
by (etac parts.induct 1); 

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

2373  278 
Addsimps [parts_insert_Agent, parts_insert_Nonce, parts_insert_Key, 
279 
parts_insert_Hash, parts_insert_Crypt, parts_insert_MPair]; 

1839  280 

281 

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

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

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

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

286 
qed "parts_image_Key"; 
3514
eb16b8e8d872
Moved some declarations to Message from Public and Shared
paulson
parents:
3476
diff
changeset

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

288 

3514
eb16b8e8d872
Moved some declarations to Message from Public and Shared
paulson
parents:
3476
diff
changeset

289 

eb16b8e8d872
Moved some declarations to Message from Public and Shared
paulson
parents:
3476
diff
changeset

290 
(*In any message, there is an upper bound N on its greatest nonce.*) 
eb16b8e8d872
Moved some declarations to Message from Public and Shared
paulson
parents:
3476
diff
changeset

291 
goal thy "EX N. ALL n. N<=n > Nonce n ~: parts {msg}"; 
eb16b8e8d872
Moved some declarations to Message from Public and Shared
paulson
parents:
3476
diff
changeset

292 
by (msg.induct_tac "msg" 1); 
eb16b8e8d872
Moved some declarations to Message from Public and Shared
paulson
parents:
3476
diff
changeset

293 
by (ALLGOALS (asm_simp_tac (!simpset addsimps [exI, parts_insert2]))); 
eb16b8e8d872
Moved some declarations to Message from Public and Shared
paulson
parents:
3476
diff
changeset

294 
(*MPair case: blast_tac works out the necessary sum itself!*) 
eb16b8e8d872
Moved some declarations to Message from Public and Shared
paulson
parents:
3476
diff
changeset

295 
by (blast_tac (!claset addSEs [add_leE]) 2); 
eb16b8e8d872
Moved some declarations to Message from Public and Shared
paulson
parents:
3476
diff
changeset

296 
(*Nonce case*) 
eb16b8e8d872
Moved some declarations to Message from Public and Shared
paulson
parents:
3476
diff
changeset

297 
by (res_inst_tac [("x","N + Suc nat")] exI 1); 
eb16b8e8d872
Moved some declarations to Message from Public and Shared
paulson
parents:
3476
diff
changeset

298 
by (fast_tac (!claset addSEs [add_leE] addaltern trans_tac) 1); 
eb16b8e8d872
Moved some declarations to Message from Public and Shared
paulson
parents:
3476
diff
changeset

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

300 

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

301 

1913  302 
(**** Inductive relation "analz" ****) 
1839  303 

304 
val major::prems = 

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

1839  307 
\ ] ==> P"; 
308 
by (cut_facts_tac [major] 1); 

2032  309 
by (resolve_tac prems 1); 
1913  310 
by (REPEAT (eresolve_tac [asm_rl, analz.Fst, analz.Snd] 1)); 
311 
qed "MPair_analz"; 

1839  312 

1913  313 
AddIs [analz.Inj]; 
2011  314 
AddSEs [MPair_analz]; (*Perhaps it should NOT be deemed safe!*) 
1913  315 
AddDs [analz.Decrypt]; 
1839  316 

1913  317 
Addsimps [analz.Inj]; 
1885  318 

1913  319 
goal thy "H <= analz(H)"; 
2891  320 
by (Blast_tac 1); 
1913  321 
qed "analz_increasing"; 
1839  322 

1913  323 
goal thy "analz H <= parts H"; 
1839  324 
by (rtac subsetI 1); 
2032  325 
by (etac analz.induct 1); 
2891  326 
by (ALLGOALS Blast_tac); 
1913  327 
qed "analz_subset_parts"; 
1839  328 

1913  329 
bind_thm ("not_parts_not_analz", analz_subset_parts RS contra_subsetD); 
1839  330 

331 

1913  332 
goal thy "parts (analz H) = parts H"; 
2032  333 
by (rtac equalityI 1); 
334 
by (rtac (analz_subset_parts RS parts_mono RS subset_trans) 1); 

1839  335 
by (Simp_tac 1); 
2891  336 
by (blast_tac (!claset addIs [analz_increasing RS parts_mono RS subsetD]) 1); 
1913  337 
qed "parts_analz"; 
338 
Addsimps [parts_analz]; 

1839  339 

1913  340 
goal thy "analz (parts H) = parts H"; 
1885  341 
by (Auto_tac()); 
2032  342 
by (etac analz.induct 1); 
1885  343 
by (Auto_tac()); 
1913  344 
qed "analz_parts"; 
345 
Addsimps [analz_parts]; 

1885  346 

1839  347 
(*Monotonicity; Lemma 1 of Lowe*) 
1913  348 
goalw thy analz.defs "!!G H. G<=H ==> analz(G) <= analz(H)"; 
1839  349 
by (rtac lfp_mono 1); 
350 
by (REPEAT (ares_tac basic_monos 1)); 

1913  351 
qed "analz_mono"; 
1839  352 

2373  353 
val analz_insertI = impOfSubs (subset_insertI RS analz_mono); 
354 

1839  355 
(** General equational properties **) 
356 

1913  357 
goal thy "analz{} = {}"; 
1839  358 
by (Step_tac 1); 
2032  359 
by (etac analz.induct 1); 
2891  360 
by (ALLGOALS Blast_tac); 
1913  361 
qed "analz_empty"; 
362 
Addsimps [analz_empty]; 

1839  363 

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

368 
qed "analz_Un"; 

1839  369 

1913  370 
goal thy "insert X (analz H) <= analz(insert X H)"; 
2922  371 
by (blast_tac (!claset addIs [impOfSubs analz_mono]) 1); 
1913  372 
qed "analz_insert"; 
1839  373 

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

375 

2373  376 
fun analz_tac i = 
377 
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

378 
etac analz.induct i, 
3102  379 
REPEAT (Blast_tac i)]; 
2373  380 

1913  381 
goal thy "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)"; 
2373  382 
by (analz_tac 1); 
1913  383 
qed "analz_insert_Agent"; 
1839  384 

1913  385 
goal thy "analz (insert (Nonce N) H) = insert (Nonce N) (analz H)"; 
2373  386 
by (analz_tac 1); 
1913  387 
qed "analz_insert_Nonce"; 
1839  388 

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

391 
qed "analz_insert_Hash"; 

392 

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

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

2373  397 
by (analz_tac 1); 
1913  398 
qed "analz_insert_Key"; 
1839  399 

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

2032  402 
by (rtac equalityI 1); 
403 
by (rtac subsetI 1); 

404 
by (etac analz.induct 1); 

1885  405 
by (Auto_tac()); 
2032  406 
by (etac analz.induct 1); 
2922  407 
by (ALLGOALS (blast_tac (!claset addIs [analz.Fst, analz.Snd]))); 
1913  408 
qed "analz_insert_MPair"; 
1885  409 

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

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 H)"; 
2373  414 
by (analz_tac 1); 
1913  415 
qed "analz_insert_Crypt"; 
1839  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 
\ analz (insert (Crypt K X) H) <= \ 
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2170
diff
changeset

419 
\ insert (Crypt K X) (analz (insert X H))"; 
2032  420 
by (rtac subsetI 1); 
1913  421 
by (eres_inst_tac [("za","x")] analz.induct 1); 
3102  422 
by (ALLGOALS (Blast_tac)); 
1839  423 
val lemma1 = result(); 
424 

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

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

427 
\ analz (insert (Crypt K X) H)"; 
1839  428 
by (Auto_tac()); 
1913  429 
by (eres_inst_tac [("za","x")] analz.induct 1); 
1839  430 
by (Auto_tac()); 
3449  431 
by (blast_tac (!claset addIs [analz_insertI, analz.Decrypt]) 1); 
1839  432 
val lemma2 = result(); 
433 

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

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

436 
\ insert (Crypt K X) (analz (insert X H))"; 
1839  437 
by (REPEAT (ares_tac [equalityI, lemma1, lemma2] 1)); 
1913  438 
qed "analz_insert_Decrypt"; 
1839  439 

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

443 
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

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

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

447 
\ else insert (Crypt K X) (analz H))"; 
2102  448 
by (case_tac "Key (invKey K) : analz H " 1); 
1913  449 
by (ALLGOALS (asm_simp_tac (!simpset addsimps [analz_insert_Crypt, 
2032  450 
analz_insert_Decrypt]))); 
1913  451 
qed "analz_Crypt_if"; 
1885  452 

2373  453 
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

454 
analz_insert_Hash, analz_insert_MPair, analz_Crypt_if]; 
1839  455 

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

457 
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

458 
\ insert (Crypt K X) (analz (insert X H))"; 
2032  459 
by (rtac subsetI 1); 
460 
by (etac analz.induct 1); 

1839  461 
by (Auto_tac()); 
1913  462 
qed "analz_insert_Crypt_subset"; 
1839  463 

464 

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

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

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

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

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

470 

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

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

472 

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

473 

1839  474 
(** Idempotence and transitivity **) 
475 

1913  476 
goal thy "!!H. X: analz (analz H) ==> X: analz H"; 
2032  477 
by (etac analz.induct 1); 
2891  478 
by (ALLGOALS Blast_tac); 
2922  479 
qed "analz_analzD"; 
480 
AddSDs [analz_analzD]; 

1839  481 

1913  482 
goal thy "analz (analz H) = analz H"; 
2891  483 
by (Blast_tac 1); 
1913  484 
qed "analz_idem"; 
485 
Addsimps [analz_idem]; 

1839  486 

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

2891  489 
by (Blast_tac 1); 
1913  490 
qed "analz_trans"; 
1839  491 

492 
(*Cut; Lemma 2 of Lowe*) 

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

493 
goal thy "!!H. [ Y: analz (insert X H); X: analz H ] ==> Y: analz H"; 
2032  494 
by (etac analz_trans 1); 
2891  495 
by (Blast_tac 1); 
1913  496 
qed "analz_cut"; 
1839  497 

498 
(*Cut can be proved easily by induction on 

1913  499 
"!!H. Y: analz (insert X H) ==> X: analz H > Y: analz H" 
1839  500 
*) 
501 

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

504 
of X can be very complicated. *) 

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

507 
qed "analz_insert_eq"; 

508 

1885  509 

1913  510 
(** A congruence rule for "analz" **) 
1885  511 

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

1885  514 
by (Step_tac 1); 
2032  515 
by (etac analz.induct 1); 
1913  516 
by (ALLGOALS (best_tac (!claset addIs [analz_mono RS subsetD]))); 
517 
qed "analz_subset_cong"; 

1885  518 

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

521 
by (REPEAT_FIRST (ares_tac [equalityI, analz_subset_cong] 

2032  522 
ORELSE' etac equalityE)); 
1913  523 
qed "analz_cong"; 
1885  524 

525 

1913  526 
goal thy "!!H. analz H = analz H' ==> analz(insert X H) = analz(insert X H')"; 
3583
5a47b869d16a
Had to remove {x.x=a} = a from !simpset in one proof.
nipkow
parents:
3519
diff
changeset

527 
by (asm_simp_tac (!simpset addsimps [insert_def] delsimps [singleton_conv] 
2032  528 
setloop (rtac analz_cong)) 1); 
1913  529 
qed "analz_insert_cong"; 
1885  530 

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

532 
goal thy "!!H. [ ALL X Y. {X,Y} ~: H; ALL X K. Crypt K X ~: H ] ==> \ 
1913  533 
\ analz H = H"; 
1839  534 
by (Step_tac 1); 
2032  535 
by (etac analz.induct 1); 
2891  536 
by (ALLGOALS Blast_tac); 
1913  537 
qed "analz_trivial"; 
1839  538 

539 
(*Helps to prove Fake cases*) 

1913  540 
goal thy "!!X. X: analz (UN i. analz (H i)) ==> X: analz (UN i. H i)"; 
2032  541 
by (etac analz.induct 1); 
2922  542 
by (ALLGOALS (blast_tac (!claset addIs [impOfSubs analz_mono]))); 
1839  543 
val lemma = result(); 
544 

1913  545 
goal thy "analz (UN i. analz (H i)) = analz (UN i. H i)"; 
2922  546 
by (blast_tac (!claset addIs [lemma, impOfSubs analz_mono]) 1); 
1913  547 
qed "analz_UN_analz"; 
548 
Addsimps [analz_UN_analz]; 

1839  549 

550 

1913  551 
(**** Inductive relation "synth" ****) 
1839  552 

1913  553 
AddIs synth.intrs; 
1839  554 

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

557 
val mk_cases = synth.mk_cases msg.simps; 

558 

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

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

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

564 
val Crypt_synth = mk_cases "Crypt K X : synth H"; 
2011  565 

2373  566 
AddSEs [Nonce_synth, Key_synth, Hash_synth, MPair_synth, Crypt_synth]; 
2011  567 

1913  568 
goal thy "H <= synth(H)"; 
2891  569 
by (Blast_tac 1); 
1913  570 
qed "synth_increasing"; 
1839  571 

572 
(*Monotonicity*) 

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

1913  576 
qed "synth_mono"; 
1839  577 

578 
(** Unions **) 

579 

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

584 
qed "synth_Un"; 

1839  585 

1913  586 
goal thy "insert X (synth H) <= synth(insert X H)"; 
2922  587 
by (blast_tac (!claset addIs [impOfSubs synth_mono]) 1); 
1913  588 
qed "synth_insert"; 
1885  589 

1839  590 
(** Idempotence and transitivity **) 
591 

1913  592 
goal thy "!!H. X: synth (synth H) ==> X: synth H"; 
2032  593 
by (etac synth.induct 1); 
2891  594 
by (ALLGOALS Blast_tac); 
2922  595 
qed "synth_synthD"; 
596 
AddSDs [synth_synthD]; 

1839  597 

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

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

2891  604 
by (Blast_tac 1); 
1913  605 
qed "synth_trans"; 
1839  606 

607 
(*Cut; Lemma 2 of Lowe*) 

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

608 
goal thy "!!H. [ Y: synth (insert X H); X: synth H ] ==> Y: synth H"; 
2032  609 
by (etac synth_trans 1); 
2891  610 
by (Blast_tac 1); 
1913  611 
qed "synth_cut"; 
1839  612 

1946  613 
goal thy "Agent A : synth H"; 
2891  614 
by (Blast_tac 1); 
1946  615 
qed "Agent_synth"; 
616 

1913  617 
goal thy "(Nonce N : synth H) = (Nonce N : H)"; 
2891  618 
by (Blast_tac 1); 
1913  619 
qed "Nonce_synth_eq"; 
1839  620 

1913  621 
goal thy "(Key K : synth H) = (Key K : H)"; 
2891  622 
by (Blast_tac 1); 
1913  623 
qed "Key_synth_eq"; 
1839  624 

2373  625 
goal thy "!!K. Key K ~: H ==> (Crypt K X : synth H) = (Crypt K X : H)"; 
2891  626 
by (Blast_tac 1); 
2011  627 
qed "Crypt_synth_eq"; 
628 

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

1839  630 

631 

632 
goalw thy [keysFor_def] 

1913  633 
"keysFor (synth H) = keysFor H Un invKey``{K. Key K : H}"; 
2891  634 
by (Blast_tac 1); 
1913  635 
qed "keysFor_synth"; 
636 
Addsimps [keysFor_synth]; 

1839  637 

638 

1913  639 
(*** Combinations of parts, analz and synth ***) 
1839  640 

1913  641 
goal thy "parts (synth H) = parts H Un synth H"; 
2032  642 
by (rtac equalityI 1); 
643 
by (rtac subsetI 1); 

644 
by (etac parts.induct 1); 

1839  645 
by (ALLGOALS 
2922  646 
(blast_tac (!claset addIs ((synth_increasing RS parts_mono RS subsetD) 
2032  647 
::parts.intrs)))); 
1913  648 
qed "parts_synth"; 
649 
Addsimps [parts_synth]; 

1839  650 

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

653 
by (ALLGOALS Simp_tac); 

654 
qed "analz_analz_Un"; 

655 

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

2032  657 
by (rtac equalityI 1); 
658 
by (rtac subsetI 1); 

659 
by (etac analz.induct 1); 

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

2373  662 
qed "analz_synth_Un"; 
663 

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

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

666 
by (Full_simp_tac 1); 

1913  667 
qed "analz_synth"; 
2373  668 
Addsimps [analz_analz_Un, analz_synth_Un, analz_synth]; 
1839  669 

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

2032  673 
by (rtac equalityI 1); 
674 
by (rtac subsetI 1); 

675 
by (etac analz.induct 1); 

2922  676 
by (blast_tac 
677 
(!claset addIs [impOfSubs synth_increasing, 

2032  678 
impOfSubs analz_mono]) 5); 
2891  679 
by (Blast_tac 1); 
680 
by (blast_tac (!claset addIs [analz.Inj RS analz.Fst]) 1); 

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

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

1913  683 
qed "analz_UN1_synth"; 
684 
Addsimps [analz_UN1_synth]; 

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

685 

1946  686 

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

688 

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

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

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

693 

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

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

2032  697 
by (dtac parts_insert_subset_Un 1); 
1946  698 
by (Full_simp_tac 1); 
2891  699 
by (Blast_tac 1); 
1946  700 
qed "Fake_parts_insert"; 
701 

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

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

705 
\ ==> Crypt K Y : parts G Un parts H"; 
2061  706 
by (dtac (impOfSubs Fake_parts_insert) 1); 
2170  707 
by (assume_tac 1); 
3102  708 
by (blast_tac (!claset addDs [impOfSubs analz_subset_parts]) 1); 
2061  709 
qed "Crypt_Fake_parts_insert"; 
710 

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

713 
by (rtac subsetI 1); 

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

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

2373  717 
by (Full_simp_tac 1); 
2891  718 
by (Blast_tac 1); 
2373  719 
qed "Fake_analz_insert"; 
720 

2011  721 
goal thy "(X: analz H & X: parts H) = (X: analz H)"; 
2891  722 
by (blast_tac (!claset addIs [impOfSubs analz_subset_parts]) 1); 
2011  723 
val analz_conj_parts = result(); 
724 

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

2891  726 
by (blast_tac (!claset addIs [impOfSubs analz_subset_parts]) 1); 
2011  727 
val analz_disj_parts = result(); 
728 

729 
AddIffs [analz_conj_parts, analz_disj_parts]; 

730 

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

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

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

733 
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

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

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

737 

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

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

739 

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

741 
\ ==> (Crypt K X : synth (analz H)) = (X : synth (analz H))"; 
2891  742 
by (Blast_tac 1); 
2154  743 
qed "Crypt_synth_analz"; 
744 

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

745 

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

746 
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

747 
\ ==> (Hash{X,Y} : synth (analz H)) = (Hash{X,Y} : analz H)"; 
2891  748 
by (Blast_tac 1); 
2373  749 
qed "Hash_synth_analz"; 
750 
Addsimps [Hash_synth_analz]; 

751 

752 

2484  753 
(**** HPair: a combination of Hash and MPair ****) 
754 

755 
(*** Freeness ***) 

756 

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

757 
goalw thy [HPair_def] "Agent A ~= Hash[X] Y"; 
2484  758 
by (Simp_tac 1); 
759 
qed "Agent_neq_HPair"; 

760 

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

761 
goalw thy [HPair_def] "Nonce N ~= Hash[X] Y"; 
2484  762 
by (Simp_tac 1); 
763 
qed "Nonce_neq_HPair"; 

764 

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

765 
goalw thy [HPair_def] "Key K ~= Hash[X] Y"; 
2484  766 
by (Simp_tac 1); 
767 
qed "Key_neq_HPair"; 

768 

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

769 
goalw thy [HPair_def] "Hash Z ~= Hash[X] Y"; 
2484  770 
by (Simp_tac 1); 
771 
qed "Hash_neq_HPair"; 

772 

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

773 
goalw thy [HPair_def] "Crypt K X' ~= Hash[X] Y"; 
2484  774 
by (Simp_tac 1); 
775 
qed "Crypt_neq_HPair"; 

776 

777 
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

778 
Key_neq_HPair, Hash_neq_HPair, Crypt_neq_HPair]; 
2484  779 

780 
AddIffs HPair_neqs; 

781 
AddIffs (HPair_neqs RL [not_sym]); 

782 

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

783 
goalw thy [HPair_def] "(Hash[X'] Y' = Hash[X] Y) = (X' = X & Y'=Y)"; 
2484  784 
by (Simp_tac 1); 
785 
qed "HPair_eq"; 

786 

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

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

790 

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

791 
goalw thy [HPair_def] "(Hash[X] Y = {X',Y'}) = (X' = Hash{X,Y} & Y'=Y)"; 
2484  792 
by (Auto_tac()); 
793 
qed "HPair_eq_MPair"; 

794 

795 
AddIffs [HPair_eq, MPair_eq_HPair, HPair_eq_MPair]; 

796 

797 

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

799 

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

800 
goalw thy [HPair_def] "keysFor (insert (Hash[X] Y) H) = keysFor H"; 
2484  801 
by (Simp_tac 1); 
802 
qed "keysFor_insert_HPair"; 

803 

804 
goalw thy [HPair_def] 

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

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

806 
\ insert (Hash[X] Y) (insert (Hash{X,Y}) (parts (insert Y H)))"; 
2484  807 
by (Simp_tac 1); 
808 
qed "parts_insert_HPair"; 

809 

810 
goalw thy [HPair_def] 

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

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

812 
\ insert (Hash[X] Y) (insert (Hash{X,Y}) (analz (insert Y H)))"; 
2484  813 
by (Simp_tac 1); 
814 
qed "analz_insert_HPair"; 

815 

816 
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

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

2891  820 
by (Blast_tac 1); 
2484  821 
qed "HPair_synth_analz"; 
822 

823 
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

824 
HPair_synth_analz, HPair_synth_analz]; 
2484  825 

826 

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

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

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

829 

2327  830 

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

832 
be pulled out using the analz_insert rules **) 

833 

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

835 
insert_commute; 

836 

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

2373  838 
["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

839 
"MPair ?X ?Y", "Crypt ?X ?K'"]; 
2327  840 

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

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

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

845 
val pushes = pushKeys@pushCrypts; 

846 

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

847 

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

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

849 

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

852 
alone.*) 

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

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

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

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

856 

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

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

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

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

860 

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

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

862 
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

863 
*) 
2373  864 
val Fake_insert_tac = 
865 
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

866 
impOfSubs Fake_parts_insert] THEN' 
2373  867 
eresolve_tac [asm_rl, synth.Inj]; 
868 

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

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

873 
fun spy_analz_tac i = 

2373  874 
DETERM 
875 
(SELECT_GOAL 

876 
(EVERY 

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

878 
(REPEAT o CHANGED) 

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

880 
(*...allowing further simplifications*) 

881 
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

882 
REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])), 
2373  883 
DEPTH_SOLVE 
884 
(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

885 
THEN 
3102  886 
IF_UNSOLVED (Blast.depth_tac 
887 
(!claset addIs [impOfSubs analz_mono, 

888 
impOfSubs analz_subset_parts]) 2 1)) 

2373  889 
]) i); 
2327  890 

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

894 

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

897 
fun prove_unique_tac lemma = 

898 
EVERY' [dtac lemma, 

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

899 
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

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

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

2373  904 

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

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

2891  907 
by (Blast_tac 1); 
2373  908 
val Un_absorb3 = result(); 
909 
Addsimps [Un_absorb3]; 

3514
eb16b8e8d872
Moved some declarations to Message from Public and Shared
paulson
parents:
3476
diff
changeset

910 

eb16b8e8d872
Moved some declarations to Message from Public and Shared
paulson
parents:
3476
diff
changeset

911 
(*By default only o_apply is builtin. But in the presence of etaexpansion 
eb16b8e8d872
Moved some declarations to Message from Public and Shared
paulson
parents:
3476
diff
changeset

912 
this means that some terms displayed as (f o g) will be rewritten, and others 
eb16b8e8d872
Moved some declarations to Message from Public and Shared
paulson
parents:
3476
diff
changeset

913 
will not!*) 
eb16b8e8d872
Moved some declarations to Message from Public and Shared
paulson
parents:
3476
diff
changeset

914 
Addsimps [o_def]; 