author  nipkow 
Fri, 24 Nov 2000 16:49:27 +0100  
changeset 10519  ade64af4c57c 
parent 8054  2ce57ef2a4aa 
child 10833  c0844a30ea4e 
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 

3702  10 

11 
(*Eliminates a commonlyoccurring expression*) 

12 
goal HOL.thy "~ (ALL x. x~=y)"; 

13 
by (Blast_tac 1); 

14 
Addsimps [result()]; 

15 

3668  16 
AddIffs msg.inject; 
1839  17 

4422
21238c9d363e
Simplified proofs using rewrites for f``A where f is injective
paulson
parents:
4157
diff
changeset

18 
(*Equations hold because constructors are injective; cannot prove for all f*) 
5076  19 
Goal "(Friend x : Friend``A) = (x:A)"; 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4422
diff
changeset

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

21 
qed "Friend_image_eq"; 
4422
21238c9d363e
Simplified proofs using rewrites for f``A where f is injective
paulson
parents:
4157
diff
changeset

22 

5076  23 
Goal "(Key x : Key``A) = (x:A)"; 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4422
diff
changeset

24 
by Auto_tac; 
4422
21238c9d363e
Simplified proofs using rewrites for f``A where f is injective
paulson
parents:
4157
diff
changeset

25 
qed "Key_image_eq"; 
21238c9d363e
Simplified proofs using rewrites for f``A where f is injective
paulson
parents:
4157
diff
changeset

26 

5076  27 
Goal "(Nonce x ~: Key``A)"; 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4422
diff
changeset

28 
by Auto_tac; 
4422
21238c9d363e
Simplified proofs using rewrites for f``A where f is injective
paulson
parents:
4157
diff
changeset

29 
qed "Nonce_Key_image_eq"; 
21238c9d363e
Simplified proofs using rewrites for f``A where f is injective
paulson
parents:
4157
diff
changeset

30 
Addsimps [Friend_image_eq, Key_image_eq, Nonce_Key_image_eq]; 
3514
eb16b8e8d872
Moved some declarations to Message from Public and Shared
paulson
parents:
3476
diff
changeset

31 

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

32 

1839  33 
(** Inverse of keys **) 
34 

5493  35 
Goal "(invKey K = invKey K') = (K=K')"; 
3730  36 
by Safe_tac; 
2032  37 
by (rtac box_equals 1); 
1839  38 
by (REPEAT (rtac invKey 2)); 
39 
by (Asm_simp_tac 1); 

40 
qed "invKey_eq"; 

41 

42 
Addsimps [invKey, invKey_eq]; 

43 

44 

45 
(**** keysFor operator ****) 

46 

5076  47 
Goalw [keysFor_def] "keysFor {} = {}"; 
2891  48 
by (Blast_tac 1); 
1839  49 
qed "keysFor_empty"; 
50 

5076  51 
Goalw [keysFor_def] "keysFor (H Un H') = keysFor H Un keysFor H'"; 
2891  52 
by (Blast_tac 1); 
1839  53 
qed "keysFor_Un"; 
54 

5076  55 
Goalw [keysFor_def] "keysFor (UN i:A. H i) = (UN i:A. keysFor (H i))"; 
2891  56 
by (Blast_tac 1); 
4157  57 
qed "keysFor_UN"; 
1839  58 

59 
(*Monotonicity*) 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5102
diff
changeset

60 
Goalw [keysFor_def] "G<=H ==> keysFor(G) <= keysFor(H)"; 
2891  61 
by (Blast_tac 1); 
1839  62 
qed "keysFor_mono"; 
63 

5076  64 
Goalw [keysFor_def] "keysFor (insert (Agent A) H) = keysFor H"; 
7057
b9ddbb925939
tweaked proofs to handle new freeness reasoning for data c onstructors
paulson
parents:
6915
diff
changeset

65 
by Auto_tac; 
1839  66 
qed "keysFor_insert_Agent"; 
67 

5076  68 
Goalw [keysFor_def] "keysFor (insert (Nonce N) H) = keysFor H"; 
7057
b9ddbb925939
tweaked proofs to handle new freeness reasoning for data c onstructors
paulson
parents:
6915
diff
changeset

69 
by Auto_tac; 
1839  70 
qed "keysFor_insert_Nonce"; 
71 

5076  72 
Goalw [keysFor_def] "keysFor (insert (Number N) H) = keysFor H"; 
7057
b9ddbb925939
tweaked proofs to handle new freeness reasoning for data c onstructors
paulson
parents:
6915
diff
changeset

73 
by Auto_tac; 
3668  74 
qed "keysFor_insert_Number"; 
75 

5076  76 
Goalw [keysFor_def] "keysFor (insert (Key K) H) = keysFor H"; 
7057
b9ddbb925939
tweaked proofs to handle new freeness reasoning for data c onstructors
paulson
parents:
6915
diff
changeset

77 
by Auto_tac; 
1839  78 
qed "keysFor_insert_Key"; 
79 

5076  80 
Goalw [keysFor_def] "keysFor (insert (Hash X) H) = keysFor H"; 
7057
b9ddbb925939
tweaked proofs to handle new freeness reasoning for data c onstructors
paulson
parents:
6915
diff
changeset

81 
by Auto_tac; 
2373  82 
qed "keysFor_insert_Hash"; 
83 

5076  84 
Goalw [keysFor_def] "keysFor (insert {X,Y} H) = keysFor H"; 
7057
b9ddbb925939
tweaked proofs to handle new freeness reasoning for data c onstructors
paulson
parents:
6915
diff
changeset

85 
by Auto_tac; 
1839  86 
qed "keysFor_insert_MPair"; 
87 

5076  88 
Goalw [keysFor_def] 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2170
diff
changeset

89 
"keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)"; 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4422
diff
changeset

90 
by Auto_tac; 
1839  91 
qed "keysFor_insert_Crypt"; 
92 

4157  93 
Addsimps [keysFor_empty, keysFor_Un, keysFor_UN, 
3668  94 
keysFor_insert_Agent, keysFor_insert_Nonce, 
95 
keysFor_insert_Number, keysFor_insert_Key, 

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

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

97 
AddSEs [keysFor_Un RS equalityD1 RS subsetD RS UnE, 
4157  98 
keysFor_UN RS equalityD1 RS subsetD RS UN_E]; 
1839  99 

5076  100 
Goalw [keysFor_def] "keysFor (Key``E) = {}"; 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4422
diff
changeset

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

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

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

104 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5102
diff
changeset

105 
Goalw [keysFor_def] "Crypt K X : H ==> invKey K : keysFor H"; 
2891  106 
by (Blast_tac 1); 
2068  107 
qed "Crypt_imp_invKey_keysFor"; 
108 

1839  109 

110 
(**** Inductive relation "parts" ****) 

111 

112 
val major::prems = 

5076  113 
Goal "[ {X,Y} : parts H; \ 
1839  114 
\ [ X : parts H; Y : parts H ] ==> P \ 
115 
\ ] ==> P"; 

116 
by (cut_facts_tac [major] 1); 

2032  117 
by (resolve_tac prems 1); 
1839  118 
by (REPEAT (eresolve_tac [asm_rl, parts.Fst, parts.Snd] 1)); 
119 
qed "MPair_parts"; 

120 

121 
AddIs [parts.Inj]; 

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

122 

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

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

124 

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

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

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

127 
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

128 
proofs concern only atomic messages.*) 
1839  129 

5076  130 
Goal "H <= parts(H)"; 
2891  131 
by (Blast_tac 1); 
1839  132 
qed "parts_increasing"; 
133 

134 
(*Monotonicity*) 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5102
diff
changeset

135 
Goalw parts.defs "G<=H ==> parts(G) <= parts(H)"; 
1839  136 
by (rtac lfp_mono 1); 
137 
by (REPEAT (ares_tac basic_monos 1)); 

138 
qed "parts_mono"; 

139 

2373  140 
val parts_insertI = impOfSubs (subset_insertI RS parts_mono); 
141 

5076  142 
Goal "parts{} = {}"; 
3730  143 
by Safe_tac; 
2032  144 
by (etac parts.induct 1); 
2891  145 
by (ALLGOALS Blast_tac); 
1839  146 
qed "parts_empty"; 
147 
Addsimps [parts_empty]; 

148 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5102
diff
changeset

149 
Goal "X: parts{} ==> P"; 
1839  150 
by (Asm_full_simp_tac 1); 
151 
qed "parts_emptyE"; 

152 
AddSEs [parts_emptyE]; 

153 

1893  154 
(*WARNING: loops if H = {Y}, therefore must not be repeated!*) 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5102
diff
changeset

155 
Goal "X: parts H ==> EX Y:H. X: parts {Y}"; 
2032  156 
by (etac parts.induct 1); 
2891  157 
by (ALLGOALS Blast_tac); 
1893  158 
qed "parts_singleton"; 
159 

1839  160 

161 
(** Unions **) 

162 

5076  163 
Goal "parts(G) Un parts(H) <= parts(G Un H)"; 
1839  164 
by (REPEAT (ares_tac [Un_least, parts_mono, Un_upper1, Un_upper2] 1)); 
165 
val parts_Un_subset1 = result(); 

166 

5076  167 
Goal "parts(G Un H) <= parts(G) Un parts(H)"; 
2032  168 
by (rtac subsetI 1); 
169 
by (etac parts.induct 1); 

2891  170 
by (ALLGOALS Blast_tac); 
1839  171 
val parts_Un_subset2 = result(); 
172 

5076  173 
Goal "parts(G Un H) = parts(G) Un parts(H)"; 
1839  174 
by (REPEAT (ares_tac [equalityI, parts_Un_subset1, parts_Un_subset2] 1)); 
175 
qed "parts_Un"; 

176 

5076  177 
Goal "parts (insert X H) = parts {X} Un parts H"; 
1852  178 
by (stac (read_instantiate [("A","H")] insert_is_Un) 1); 
2011  179 
by (simp_tac (HOL_ss addsimps [parts_Un]) 1); 
180 
qed "parts_insert"; 

181 

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

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

5076  184 
Goal "parts (insert X (insert Y H)) = parts {X} Un parts {Y} Un parts H"; 
4091  185 
by (simp_tac (simpset() addsimps [Un_assoc]) 1); 
186 
by (simp_tac (simpset() addsimps [parts_insert RS sym]) 1); 

1852  187 
qed "parts_insert2"; 
188 

5076  189 
Goal "(UN x:A. parts(H x)) <= parts(UN x:A. H x)"; 
1839  190 
by (REPEAT (ares_tac [UN_least, parts_mono, UN_upper] 1)); 
191 
val parts_UN_subset1 = result(); 

192 

5076  193 
Goal "parts(UN x:A. H x) <= (UN x:A. parts(H x))"; 
2032  194 
by (rtac subsetI 1); 
195 
by (etac parts.induct 1); 

2891  196 
by (ALLGOALS Blast_tac); 
1839  197 
val parts_UN_subset2 = result(); 
198 

5076  199 
Goal "parts(UN x:A. H x) = (UN x:A. parts(H x))"; 
1839  200 
by (REPEAT (ares_tac [equalityI, parts_UN_subset1, parts_UN_subset2] 1)); 
201 
qed "parts_UN"; 

202 

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

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

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

206 
AddSEs [parts_Un RS equalityD1 RS subsetD RS UnE, 
4157  207 
parts_UN RS equalityD1 RS subsetD RS UN_E]; 
1839  208 

5076  209 
Goal "insert X (parts H) <= parts(insert X H)"; 
4091  210 
by (blast_tac (claset() addIs [impOfSubs parts_mono]) 1); 
1839  211 
qed "parts_insert_subset"; 
212 

213 
(** Idempotence and transitivity **) 

214 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5102
diff
changeset

215 
Goal "X: parts (parts H) ==> X: parts H"; 
2032  216 
by (etac parts.induct 1); 
2891  217 
by (ALLGOALS Blast_tac); 
2922  218 
qed "parts_partsD"; 
219 
AddSDs [parts_partsD]; 

1839  220 

5076  221 
Goal "parts (parts H) = parts H"; 
2891  222 
by (Blast_tac 1); 
1839  223 
qed "parts_idem"; 
224 
Addsimps [parts_idem]; 

225 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5102
diff
changeset

226 
Goal "[ X: parts G; G <= parts H ] ==> X: parts H"; 
1839  227 
by (dtac parts_mono 1); 
2891  228 
by (Blast_tac 1); 
1839  229 
qed "parts_trans"; 
230 

231 
(*Cut*) 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5102
diff
changeset

232 
Goal "[ Y: parts (insert X G); X: parts H ] \ 
2373  233 
\ ==> Y: parts (G Un H)"; 
2032  234 
by (etac parts_trans 1); 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4422
diff
changeset

235 
by Auto_tac; 
1839  236 
qed "parts_cut"; 
237 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5102
diff
changeset

238 
Goal "X: parts H ==> parts (insert X H) = parts H"; 
4091  239 
by (fast_tac (claset() addSDs [parts_cut] 
4556
e7a4683c0026
Tidying, mostly to do with handling a more specific version of Fake_parts_insert
paulson
parents:
4477
diff
changeset

240 
addIs [parts_insertI] 
e7a4683c0026
Tidying, mostly to do with handling a more specific version of Fake_parts_insert
paulson
parents:
4477
diff
changeset

241 
addss (simpset())) 1); 
1929
f0839bab4b00
Working version of NS, messages 13, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset

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

243 

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

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

245 

1839  246 

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

248 

2373  249 
fun parts_tac i = 
250 
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

251 
etac parts.induct i, 
7057
b9ddbb925939
tweaked proofs to handle new freeness reasoning for data c onstructors
paulson
parents:
6915
diff
changeset

252 
Auto_tac]; 
2373  253 

5076  254 
Goal "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)"; 
2373  255 
by (parts_tac 1); 
1839  256 
qed "parts_insert_Agent"; 
257 

5076  258 
Goal "parts (insert (Nonce N) H) = insert (Nonce N) (parts H)"; 
2373  259 
by (parts_tac 1); 
1839  260 
qed "parts_insert_Nonce"; 
261 

5076  262 
Goal "parts (insert (Number N) H) = insert (Number N) (parts H)"; 
3668  263 
by (parts_tac 1); 
264 
qed "parts_insert_Number"; 

265 

5076  266 
Goal "parts (insert (Key K) H) = insert (Key K) (parts H)"; 
2373  267 
by (parts_tac 1); 
1839  268 
qed "parts_insert_Key"; 
269 

5076  270 
Goal "parts (insert (Hash X) H) = insert (Hash X) (parts H)"; 
2373  271 
by (parts_tac 1); 
272 
qed "parts_insert_Hash"; 

273 

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

275 
\ insert (Crypt K X) (parts (insert X H))"; 
2032  276 
by (rtac equalityI 1); 
277 
by (rtac subsetI 1); 

278 
by (etac parts.induct 1); 

4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4422
diff
changeset

279 
by Auto_tac; 
2032  280 
by (etac parts.induct 1); 
4091  281 
by (ALLGOALS (blast_tac (claset() addIs [parts.Body]))); 
1839  282 
qed "parts_insert_Crypt"; 
283 

5076  284 
Goal "parts (insert {X,Y} H) = \ 
1839  285 
\ insert {X,Y} (parts (insert X (insert Y H)))"; 
2032  286 
by (rtac equalityI 1); 
287 
by (rtac subsetI 1); 

288 
by (etac parts.induct 1); 

4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4422
diff
changeset

289 
by Auto_tac; 
2032  290 
by (etac parts.induct 1); 
4091  291 
by (ALLGOALS (blast_tac (claset() addIs [parts.Fst, parts.Snd]))); 
1839  292 
qed "parts_insert_MPair"; 
293 

3668  294 
Addsimps [parts_insert_Agent, parts_insert_Nonce, 
295 
parts_insert_Number, parts_insert_Key, 

2373  296 
parts_insert_Hash, parts_insert_Crypt, parts_insert_MPair]; 
1839  297 

298 

5076  299 
Goal "parts (Key``N) = Key``N"; 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4422
diff
changeset

300 
by Auto_tac; 
2032  301 
by (etac parts.induct 1); 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4422
diff
changeset

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

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

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

305 

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

306 

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

307 
(*In any message, there is an upper bound N on its greatest nonce.*) 
5076  308 
Goal "EX N. ALL n. N<=n > Nonce n ~: parts {msg}"; 
3668  309 
by (induct_tac "msg" 1); 
4091  310 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [exI, parts_insert2]))); 
3514
eb16b8e8d872
Moved some declarations to Message from Public and Shared
paulson
parents:
3476
diff
changeset

311 
(*MPair case: blast_tac works out the necessary sum itself!*) 
4091  312 
by (blast_tac (claset() addSEs [add_leE]) 2); 
3514
eb16b8e8d872
Moved some declarations to Message from Public and Shared
paulson
parents:
3476
diff
changeset

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

314 
by (res_inst_tac [("x","N + Suc nat")] exI 1); 
5983  315 
by (auto_tac (claset() addSEs [add_leE], simpset())); 
3514
eb16b8e8d872
Moved some declarations to Message from Public and Shared
paulson
parents:
3476
diff
changeset

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

317 

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

318 

1913  319 
(**** Inductive relation "analz" ****) 
1839  320 

321 
val major::prems = 

5076  322 
Goal "[ {X,Y} : analz H; \ 
1913  323 
\ [ X : analz H; Y : analz H ] ==> P \ 
1839  324 
\ ] ==> P"; 
325 
by (cut_facts_tac [major] 1); 

2032  326 
by (resolve_tac prems 1); 
1913  327 
by (REPEAT (eresolve_tac [asm_rl, analz.Fst, analz.Snd] 1)); 
328 
qed "MPair_analz"; 

1839  329 

1913  330 
AddIs [analz.Inj]; 
2011  331 
AddSEs [MPair_analz]; (*Perhaps it should NOT be deemed safe!*) 
1913  332 
AddDs [analz.Decrypt]; 
1839  333 

1913  334 
Addsimps [analz.Inj]; 
1885  335 

5076  336 
Goal "H <= analz(H)"; 
2891  337 
by (Blast_tac 1); 
1913  338 
qed "analz_increasing"; 
1839  339 

5076  340 
Goal "analz H <= parts H"; 
1839  341 
by (rtac subsetI 1); 
2032  342 
by (etac analz.induct 1); 
2891  343 
by (ALLGOALS Blast_tac); 
1913  344 
qed "analz_subset_parts"; 
1839  345 

1913  346 
bind_thm ("not_parts_not_analz", analz_subset_parts RS contra_subsetD); 
1839  347 

348 

5076  349 
Goal "parts (analz H) = parts H"; 
2032  350 
by (rtac equalityI 1); 
351 
by (rtac (analz_subset_parts RS parts_mono RS subset_trans) 1); 

1839  352 
by (Simp_tac 1); 
4091  353 
by (blast_tac (claset() addIs [analz_increasing RS parts_mono RS subsetD]) 1); 
1913  354 
qed "parts_analz"; 
355 
Addsimps [parts_analz]; 

1839  356 

5076  357 
Goal "analz (parts H) = parts H"; 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4422
diff
changeset

358 
by Auto_tac; 
2032  359 
by (etac analz.induct 1); 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4422
diff
changeset

360 
by Auto_tac; 
1913  361 
qed "analz_parts"; 
362 
Addsimps [analz_parts]; 

1885  363 

1839  364 
(*Monotonicity; Lemma 1 of Lowe*) 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5102
diff
changeset

365 
Goalw analz.defs "G<=H ==> analz(G) <= analz(H)"; 
1839  366 
by (rtac lfp_mono 1); 
367 
by (REPEAT (ares_tac basic_monos 1)); 

1913  368 
qed "analz_mono"; 
1839  369 

2373  370 
val analz_insertI = impOfSubs (subset_insertI RS analz_mono); 
371 

1839  372 
(** General equational properties **) 
373 

5076  374 
Goal "analz{} = {}"; 
3730  375 
by Safe_tac; 
2032  376 
by (etac analz.induct 1); 
2891  377 
by (ALLGOALS Blast_tac); 
1913  378 
qed "analz_empty"; 
379 
Addsimps [analz_empty]; 

1839  380 

1913  381 
(*Converse fails: we can analz more from the union than from the 
1839  382 
separate parts, as a key in one might decrypt a message in the other*) 
5076  383 
Goal "analz(G) Un analz(H) <= analz(G Un H)"; 
1913  384 
by (REPEAT (ares_tac [Un_least, analz_mono, Un_upper1, Un_upper2] 1)); 
385 
qed "analz_Un"; 

1839  386 

5076  387 
Goal "insert X (analz H) <= analz(insert X H)"; 
4091  388 
by (blast_tac (claset() addIs [impOfSubs analz_mono]) 1); 
1913  389 
qed "analz_insert"; 
1839  390 

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

392 

2373  393 
fun analz_tac i = 
394 
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

395 
etac analz.induct i, 
7057
b9ddbb925939
tweaked proofs to handle new freeness reasoning for data c onstructors
paulson
parents:
6915
diff
changeset

396 
Auto_tac]; 
2373  397 

5076  398 
Goal "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)"; 
2373  399 
by (analz_tac 1); 
1913  400 
qed "analz_insert_Agent"; 
1839  401 

5076  402 
Goal "analz (insert (Nonce N) H) = insert (Nonce N) (analz H)"; 
2373  403 
by (analz_tac 1); 
1913  404 
qed "analz_insert_Nonce"; 
1839  405 

5076  406 
Goal "analz (insert (Number N) H) = insert (Number N) (analz H)"; 
3668  407 
by (analz_tac 1); 
408 
qed "analz_insert_Number"; 

409 

5076  410 
Goal "analz (insert (Hash X) H) = insert (Hash X) (analz H)"; 
2373  411 
by (analz_tac 1); 
412 
qed "analz_insert_Hash"; 

413 

1839  414 
(*Can only pull out Keys if they are not needed to decrypt the rest*) 
5076  415 
Goalw [keysFor_def] 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5102
diff
changeset

416 
"K ~: keysFor (analz H) ==> \ 
1913  417 
\ analz (insert (Key K) H) = insert (Key K) (analz H)"; 
2373  418 
by (analz_tac 1); 
1913  419 
qed "analz_insert_Key"; 
1839  420 

5076  421 
Goal "analz (insert {X,Y} H) = \ 
1913  422 
\ insert {X,Y} (analz (insert X (insert Y H)))"; 
2032  423 
by (rtac equalityI 1); 
424 
by (rtac subsetI 1); 

425 
by (etac analz.induct 1); 

4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4422
diff
changeset

426 
by Auto_tac; 
2032  427 
by (etac analz.induct 1); 
4091  428 
by (ALLGOALS (blast_tac (claset() addIs [analz.Fst, analz.Snd]))); 
1913  429 
qed "analz_insert_MPair"; 
1885  430 

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

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5102
diff
changeset

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

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

434 
\ insert (Crypt K X) (analz H)"; 
2373  435 
by (analz_tac 1); 
1913  436 
qed "analz_insert_Crypt"; 
1839  437 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5102
diff
changeset

438 
Goal "Key (invKey K) : analz H ==> \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2170
diff
changeset

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

440 
\ insert (Crypt K X) (analz (insert X H))"; 
2032  441 
by (rtac subsetI 1); 
5102  442 
by (eres_inst_tac [("xa","x")] analz.induct 1); 
7057
b9ddbb925939
tweaked proofs to handle new freeness reasoning for data c onstructors
paulson
parents:
6915
diff
changeset

443 
by Auto_tac; 
1839  444 
val lemma1 = result(); 
445 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5102
diff
changeset

446 
Goal "Key (invKey K) : analz H ==> \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2170
diff
changeset

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

448 
\ analz (insert (Crypt K X) H)"; 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4422
diff
changeset

449 
by Auto_tac; 
5102  450 
by (eres_inst_tac [("xa","x")] analz.induct 1); 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4422
diff
changeset

451 
by Auto_tac; 
4091  452 
by (blast_tac (claset() addIs [analz_insertI, analz.Decrypt]) 1); 
1839  453 
val lemma2 = result(); 
454 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5102
diff
changeset

455 
Goal "Key (invKey K) : analz H ==> \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2170
diff
changeset

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

457 
\ insert (Crypt K X) (analz (insert X H))"; 
1839  458 
by (REPEAT (ares_tac [equalityI, lemma1, lemma2] 1)); 
1913  459 
qed "analz_insert_Decrypt"; 
1839  460 

1885  461 
(*Case analysis: either the message is secure, or it is not! 
1946  462 
Effective, but can cause subgoals to blow up! 
5055  463 
Use with split_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

464 
such as "analz (insert (Crypt K X) H)" *) 
5076  465 
Goal "analz (insert (Crypt K X) H) = \ 
2154  466 
\ (if (Key (invKey K) : analz H) \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2170
diff
changeset

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

468 
\ else insert (Crypt K X) (analz H))"; 
2102  469 
by (case_tac "Key (invKey K) : analz H " 1); 
4091  470 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [analz_insert_Crypt, 
4556
e7a4683c0026
Tidying, mostly to do with handling a more specific version of Fake_parts_insert
paulson
parents:
4477
diff
changeset

471 
analz_insert_Decrypt]))); 
1913  472 
qed "analz_Crypt_if"; 
1885  473 

3668  474 
Addsimps [analz_insert_Agent, analz_insert_Nonce, 
475 
analz_insert_Number, analz_insert_Key, 

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

476 
analz_insert_Hash, analz_insert_MPair, analz_Crypt_if]; 
1839  477 

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

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

480 
\ insert (Crypt K X) (analz (insert X H))"; 
2032  481 
by (rtac subsetI 1); 
482 
by (etac analz.induct 1); 

4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4422
diff
changeset

483 
by Auto_tac; 
1913  484 
qed "analz_insert_Crypt_subset"; 
1839  485 

486 

5076  487 
Goal "analz (Key``N) = Key``N"; 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4422
diff
changeset

488 
by Auto_tac; 
2032  489 
by (etac analz.induct 1); 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4422
diff
changeset

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

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

492 

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

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

494 

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

495 

1839  496 
(** Idempotence and transitivity **) 
497 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5102
diff
changeset

498 
Goal "X: analz (analz H) ==> X: analz H"; 
2032  499 
by (etac analz.induct 1); 
2891  500 
by (ALLGOALS Blast_tac); 
2922  501 
qed "analz_analzD"; 
502 
AddSDs [analz_analzD]; 

1839  503 

5076  504 
Goal "analz (analz H) = analz H"; 
2891  505 
by (Blast_tac 1); 
1913  506 
qed "analz_idem"; 
507 
Addsimps [analz_idem]; 

1839  508 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5102
diff
changeset

509 
Goal "[ X: analz G; G <= analz H ] ==> X: analz H"; 
1913  510 
by (dtac analz_mono 1); 
2891  511 
by (Blast_tac 1); 
1913  512 
qed "analz_trans"; 
1839  513 

514 
(*Cut; Lemma 2 of Lowe*) 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5102
diff
changeset

515 
Goal "[ Y: analz (insert X H); X: analz H ] ==> Y: analz H"; 
2032  516 
by (etac analz_trans 1); 
2891  517 
by (Blast_tac 1); 
1913  518 
qed "analz_cut"; 
1839  519 

520 
(*Cut can be proved easily by induction on 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5102
diff
changeset

521 
"Y: analz (insert X H) ==> X: analz H > Y: analz H" 
1839  522 
*) 
523 

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

526 
of X can be very complicated. *) 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5102
diff
changeset

527 
Goal "X: analz H ==> analz (insert X H) = analz H"; 
4091  528 
by (blast_tac (claset() addIs [analz_cut, analz_insertI]) 1); 
3431  529 
qed "analz_insert_eq"; 
530 

1885  531 

1913  532 
(** A congruence rule for "analz" **) 
1885  533 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5102
diff
changeset

534 
Goal "[ analz G <= analz G'; analz H <= analz H' \ 
1913  535 
\ ] ==> analz (G Un H) <= analz (G' Un H')"; 
3714  536 
by (Clarify_tac 1); 
2032  537 
by (etac analz.induct 1); 
4091  538 
by (ALLGOALS (best_tac (claset() addIs [analz_mono RS subsetD]))); 
1913  539 
qed "analz_subset_cong"; 
1885  540 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5102
diff
changeset

541 
Goal "[ analz G = analz G'; analz H = analz H' \ 
1913  542 
\ ] ==> analz (G Un H) = analz (G' Un H')"; 
543 
by (REPEAT_FIRST (ares_tac [equalityI, analz_subset_cong] 

2032  544 
ORELSE' etac equalityE)); 
1913  545 
qed "analz_cong"; 
1885  546 

547 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5102
diff
changeset

548 
Goal "analz H = analz H' ==> analz(insert X H) = analz(insert X H')"; 
4091  549 
by (asm_simp_tac (simpset() addsimps [insert_def] delsimps [singleton_conv] 
4556
e7a4683c0026
Tidying, mostly to do with handling a more specific version of Fake_parts_insert
paulson
parents:
4477
diff
changeset

550 
setloop (rtac analz_cong)) 1); 
1913  551 
qed "analz_insert_cong"; 
1885  552 

1913  553 
(*If there are no pairs or encryptions then analz does nothing*) 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5102
diff
changeset

554 
Goal "[ ALL X Y. {X,Y} ~: H; ALL X K. Crypt K X ~: H ] ==> \ 
1913  555 
\ analz H = H"; 
3730  556 
by Safe_tac; 
2032  557 
by (etac analz.induct 1); 
2891  558 
by (ALLGOALS Blast_tac); 
1913  559 
qed "analz_trivial"; 
1839  560 

4157  561 
(*These two are obsolete (with a single Spy) but cost little to prove...*) 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5102
diff
changeset

562 
Goal "X: analz (UN i:A. analz (H i)) ==> X: analz (UN i:A. H i)"; 
2032  563 
by (etac analz.induct 1); 
4091  564 
by (ALLGOALS (blast_tac (claset() addIs [impOfSubs analz_mono]))); 
1839  565 
val lemma = result(); 
566 

5076  567 
Goal "analz (UN i:A. analz (H i)) = analz (UN i:A. H i)"; 
4091  568 
by (blast_tac (claset() addIs [lemma, impOfSubs analz_mono]) 1); 
1913  569 
qed "analz_UN_analz"; 
570 
Addsimps [analz_UN_analz]; 

1839  571 

572 

1913  573 
(**** Inductive relation "synth" ****) 
1839  574 

1913  575 
AddIs synth.intrs; 
1839  576 

3668  577 
(*NO Agent_synth, as any Agent name can be synthesized. Ditto for Number*) 
6141  578 
val Nonce_synth = synth.mk_cases "Nonce n : synth H"; 
579 
val Key_synth = synth.mk_cases "Key K : synth H"; 

580 
val Hash_synth = synth.mk_cases "Hash X : synth H"; 

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

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

2011  583 

2373  584 
AddSEs [Nonce_synth, Key_synth, Hash_synth, MPair_synth, Crypt_synth]; 
2011  585 

5076  586 
Goal "H <= synth(H)"; 
2891  587 
by (Blast_tac 1); 
1913  588 
qed "synth_increasing"; 
1839  589 

590 
(*Monotonicity*) 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5102
diff
changeset

591 
Goalw synth.defs "G<=H ==> synth(G) <= synth(H)"; 
1839  592 
by (rtac lfp_mono 1); 
593 
by (REPEAT (ares_tac basic_monos 1)); 

1913  594 
qed "synth_mono"; 
1839  595 

596 
(** Unions **) 

597 

1913  598 
(*Converse fails: we can synth more from the union than from the 
1839  599 
separate parts, building a compound message using elements of each.*) 
5076  600 
Goal "synth(G) Un synth(H) <= synth(G Un H)"; 
1913  601 
by (REPEAT (ares_tac [Un_least, synth_mono, Un_upper1, Un_upper2] 1)); 
602 
qed "synth_Un"; 

1839  603 

5076  604 
Goal "insert X (synth H) <= synth(insert X H)"; 
4091  605 
by (blast_tac (claset() addIs [impOfSubs synth_mono]) 1); 
1913  606 
qed "synth_insert"; 
1885  607 

1839  608 
(** Idempotence and transitivity **) 
609 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5102
diff
changeset

610 
Goal "X: synth (synth H) ==> X: synth H"; 
2032  611 
by (etac synth.induct 1); 
2891  612 
by (ALLGOALS Blast_tac); 
2922  613 
qed "synth_synthD"; 
614 
AddSDs [synth_synthD]; 

1839  615 

5076  616 
Goal "synth (synth H) = synth H"; 
2891  617 
by (Blast_tac 1); 
1913  618 
qed "synth_idem"; 
1839  619 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5102
diff
changeset

620 
Goal "[ X: synth G; G <= synth H ] ==> X: synth H"; 
1913  621 
by (dtac synth_mono 1); 
2891  622 
by (Blast_tac 1); 
1913  623 
qed "synth_trans"; 
1839  624 

625 
(*Cut; Lemma 2 of Lowe*) 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5102
diff
changeset

626 
Goal "[ Y: synth (insert X H); X: synth H ] ==> Y: synth H"; 
2032  627 
by (etac synth_trans 1); 
2891  628 
by (Blast_tac 1); 
1913  629 
qed "synth_cut"; 
1839  630 

5076  631 
Goal "Agent A : synth H"; 
2891  632 
by (Blast_tac 1); 
1946  633 
qed "Agent_synth"; 
634 

5076  635 
Goal "Number n : synth H"; 
3668  636 
by (Blast_tac 1); 
637 
qed "Number_synth"; 

638 

5076  639 
Goal "(Nonce N : synth H) = (Nonce N : H)"; 
2891  640 
by (Blast_tac 1); 
1913  641 
qed "Nonce_synth_eq"; 
1839  642 

5076  643 
Goal "(Key K : synth H) = (Key K : H)"; 
2891  644 
by (Blast_tac 1); 
1913  645 
qed "Key_synth_eq"; 
1839  646 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5102
diff
changeset

647 
Goal "Key K ~: H ==> (Crypt K X : synth H) = (Crypt K X : H)"; 
2891  648 
by (Blast_tac 1); 
2011  649 
qed "Crypt_synth_eq"; 
650 

3668  651 
Addsimps [Agent_synth, Number_synth, 
652 
Nonce_synth_eq, Key_synth_eq, Crypt_synth_eq]; 

1839  653 

654 

5076  655 
Goalw [keysFor_def] 
1913  656 
"keysFor (synth H) = keysFor H Un invKey``{K. Key K : H}"; 
2891  657 
by (Blast_tac 1); 
1913  658 
qed "keysFor_synth"; 
659 
Addsimps [keysFor_synth]; 

1839  660 

661 

1913  662 
(*** Combinations of parts, analz and synth ***) 
1839  663 

5076  664 
Goal "parts (synth H) = parts H Un synth H"; 
2032  665 
by (rtac equalityI 1); 
666 
by (rtac subsetI 1); 

667 
by (etac parts.induct 1); 

1839  668 
by (ALLGOALS 
4091  669 
(blast_tac (claset() addIs ((synth_increasing RS parts_mono RS subsetD) 
4556
e7a4683c0026
Tidying, mostly to do with handling a more specific version of Fake_parts_insert
paulson
parents:
4477
diff
changeset

670 
::parts.intrs)))); 
1913  671 
qed "parts_synth"; 
672 
Addsimps [parts_synth]; 

1839  673 

5076  674 
Goal "analz (analz G Un H) = analz (G Un H)"; 
2373  675 
by (REPEAT_FIRST (resolve_tac [equalityI, analz_subset_cong])); 
676 
by (ALLGOALS Simp_tac); 

677 
qed "analz_analz_Un"; 

678 

5076  679 
Goal "analz (synth G Un H) = analz (G Un H) Un synth G"; 
2032  680 
by (rtac equalityI 1); 
681 
by (rtac subsetI 1); 

682 
by (etac analz.induct 1); 

4091  683 
by (blast_tac (claset() addIs [impOfSubs analz_mono]) 5); 
684 
by (ALLGOALS (blast_tac (claset() addIs analz.intrs))); 

2373  685 
qed "analz_synth_Un"; 
686 

5076  687 
Goal "analz (synth H) = analz H Un synth H"; 
2373  688 
by (cut_inst_tac [("H","{}")] analz_synth_Un 1); 
689 
by (Full_simp_tac 1); 

1913  690 
qed "analz_synth"; 
2373  691 
Addsimps [analz_analz_Un, analz_synth_Un, analz_synth]; 
1839  692 

1946  693 

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

695 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5102
diff
changeset

696 
Goal "X: G ==> parts(insert X H) <= parts G Un parts H"; 
2032  697 
by (rtac ([parts_mono, parts_Un_subset2] MRS subset_trans) 1); 
2891  698 
by (Blast_tac 1); 
1929
f0839bab4b00
Working version of NS, messages 13, WITH INTERLEAVING
paulson
parents:
1913
diff
changeset

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

700 

4556
e7a4683c0026
Tidying, mostly to do with handling a more specific version of Fake_parts_insert
paulson
parents:
4477
diff
changeset

701 
(*More specifically for Fake. Very occasionally we could do with a version 
e7a4683c0026
Tidying, mostly to do with handling a more specific version of Fake_parts_insert
paulson
parents:
4477
diff
changeset

702 
of the form parts{X} <= synth (analz H) Un parts H *) 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5102
diff
changeset

703 
Goal "X: synth (analz H) ==> \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5102
diff
changeset

704 
\ parts (insert X H) <= synth (analz H) Un parts H"; 
2032  705 
by (dtac parts_insert_subset_Un 1); 
1946  706 
by (Full_simp_tac 1); 
2891  707 
by (Blast_tac 1); 
1946  708 
qed "Fake_parts_insert"; 
709 

4556
e7a4683c0026
Tidying, mostly to do with handling a more specific version of Fake_parts_insert
paulson
parents:
4477
diff
changeset

710 
(*H is sometimes (Key `` KK Un spies evs), so can't put G=H*) 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5102
diff
changeset

711 
Goal "X: synth (analz G) ==> \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5102
diff
changeset

712 
\ analz (insert X H) <= synth (analz G) Un analz (G Un H)"; 
2373  713 
by (rtac subsetI 1); 
714 
by (subgoal_tac "x : analz (synth (analz G) Un H)" 1); 

4091  715 
by (blast_tac (claset() addIs [impOfSubs analz_mono, 
4556
e7a4683c0026
Tidying, mostly to do with handling a more specific version of Fake_parts_insert
paulson
parents:
4477
diff
changeset

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 

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

5076  725 
Goal "(X: analz H  X: parts H) = (X: parts H)"; 
4091  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*) 
5076  733 
Goal "({X,Y} : synth (analz H)) = \ 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5102
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 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5102
diff
changeset

740 
Goal "[ Key K : analz H; Key (invKey K) : analz H ] \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5102
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 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5102
diff
changeset

746 
Goal "X ~: synth (analz H) \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5102
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 

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

760 

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

764 

5076  765 
Goalw [HPair_def] "Number N ~= Hash[X] Y"; 
3668  766 
by (Simp_tac 1); 
767 
qed "Number_neq_HPair"; 

768 

5076  769 
Goalw [HPair_def] "Key K ~= Hash[X] Y"; 
2484  770 
by (Simp_tac 1); 
771 
qed "Key_neq_HPair"; 

772 

5076  773 
Goalw [HPair_def] "Hash Z ~= Hash[X] Y"; 
2484  774 
by (Simp_tac 1); 
775 
qed "Hash_neq_HPair"; 

776 

5076  777 
Goalw [HPair_def] "Crypt K X' ~= Hash[X] Y"; 
2484  778 
by (Simp_tac 1); 
779 
qed "Crypt_neq_HPair"; 

780 

3668  781 
val HPair_neqs = [Agent_neq_HPair, Nonce_neq_HPair, Number_neq_HPair, 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2484
diff
changeset

782 
Key_neq_HPair, Hash_neq_HPair, Crypt_neq_HPair]; 
2484  783 

784 
AddIffs HPair_neqs; 

785 
AddIffs (HPair_neqs RL [not_sym]); 

786 

5076  787 
Goalw [HPair_def] "(Hash[X'] Y' = Hash[X] Y) = (X' = X & Y'=Y)"; 
2484  788 
by (Simp_tac 1); 
789 
qed "HPair_eq"; 

790 

5076  791 
Goalw [HPair_def] "({X',Y'} = Hash[X] Y) = (X' = Hash{X,Y} & Y'=Y)"; 
2484  792 
by (Simp_tac 1); 
793 
qed "MPair_eq_HPair"; 

794 

5076  795 
Goalw [HPair_def] "(Hash[X] Y = {X',Y'}) = (X' = Hash{X,Y} & Y'=Y)"; 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4422
diff
changeset

796 
by Auto_tac; 
2484  797 
qed "HPair_eq_MPair"; 
798 

799 
AddIffs [HPair_eq, MPair_eq_HPair, HPair_eq_MPair]; 

800 

801 

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

803 

5076  804 
Goalw [HPair_def] "keysFor (insert (Hash[X] Y) H) = keysFor H"; 
2484  805 
by (Simp_tac 1); 
806 
qed "keysFor_insert_HPair"; 

807 

5076  808 
Goalw [HPair_def] 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2484
diff
changeset

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

810 
\ insert (Hash[X] Y) (insert (Hash{X,Y}) (parts (insert Y H)))"; 
2484  811 
by (Simp_tac 1); 
812 
qed "parts_insert_HPair"; 

813 

5076  814 
Goalw [HPair_def] 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2484
diff
changeset

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

816 
\ insert (Hash[X] Y) (insert (Hash{X,Y}) (analz (insert Y H)))"; 
2484  817 
by (Simp_tac 1); 
818 
qed "analz_insert_HPair"; 

819 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5102
diff
changeset

820 
Goalw [HPair_def] "X ~: synth (analz H) \ 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2484
diff
changeset

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

2891  824 
by (Blast_tac 1); 
2484  825 
qed "HPair_synth_analz"; 
826 

827 
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

828 
HPair_synth_analz, HPair_synth_analz]; 
2484  829 

830 

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

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

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

833 

2327  834 

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

836 
be pulled out using the analz_insert rules **) 

837 

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

839 
insert_commute; 

840 

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

3668  842 
["Agent ?C", "Nonce ?N", "Number ?N", 
843 
"Hash ?X", "MPair ?X ?Y", "Crypt ?X ?K'"]; 

2327  844 

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

3668  846 
["Agent ?C", "Nonce ?N", "Number ?N", 
847 
"Hash ?X'", "MPair ?X' ?Y"]; 

2327  848 

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

850 
val pushes = pushKeys@pushCrypts; 

851 

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

852 

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

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

854 

3470  855 
(*Prove base case (subgoal i) and simplify others. A typical base case 
3683  856 
concerns Crypt K X ~: Key``shrK``bad and cannot be proved by rewriting 
3470  857 
alone.*) 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
3102
diff
changeset

858 
fun prove_simple_subgoals_tac i = 
8054
2ce57ef2a4aa
used image_eq_UN to speed up slow proofs of base cases
paulson
parents:
7057
diff
changeset

859 
force_tac (claset(), simpset() addsimps [image_eq_UN]) i THEN 
2ce57ef2a4aa
used image_eq_UN to speed up slow proofs of base cases
paulson
parents:
7057
diff
changeset

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

861 

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

862 
fun Fake_parts_insert_tac i = 
4556
e7a4683c0026
Tidying, mostly to do with handling a more specific version of Fake_parts_insert
paulson
parents:
4477
diff
changeset

863 
blast_tac (claset() addIs [parts_insertI] 
e7a4683c0026
Tidying, mostly to do with handling a more specific version of Fake_parts_insert
paulson
parents:
4477
diff
changeset

864 
addDs [impOfSubs analz_subset_parts, 
e7a4683c0026
Tidying, mostly to do with handling a more specific version of Fake_parts_insert
paulson
parents:
4477
diff
changeset

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

866 

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

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

868 
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

869 
*) 
2373  870 
val Fake_insert_tac = 
871 
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

872 
impOfSubs Fake_parts_insert] THEN' 
2373  873 
eresolve_tac [asm_rl, synth.Inj]; 
874 

3702  875 
fun Fake_insert_simp_tac i = 
876 
REPEAT (Fake_insert_tac i) THEN Asm_full_simp_tac i; 

877 

878 

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

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

4735
6d544b44a70e
spy_analz_tac now handles individual conjuncts properly
paulson
parents:
4686
diff
changeset

883 

6d544b44a70e
spy_analz_tac now handles individual conjuncts properly
paulson
parents:
4686
diff
changeset

884 
val atomic_spy_analz_tac = SELECT_GOAL 
6d544b44a70e
spy_analz_tac now handles individual conjuncts properly
paulson
parents:
4686
diff
changeset

885 
(Fake_insert_simp_tac 1 
6d544b44a70e
spy_analz_tac now handles individual conjuncts properly
paulson
parents:
4686
diff
changeset

886 
THEN 
6d544b44a70e
spy_analz_tac now handles individual conjuncts properly
paulson
parents:
4686
diff
changeset

887 
IF_UNSOLVED (Blast.depth_tac 
6d544b44a70e
spy_analz_tac now handles individual conjuncts properly
paulson
parents:
4686
diff
changeset

888 
(claset() addIs [analz_insertI, 
6d544b44a70e
spy_analz_tac now handles individual conjuncts properly
paulson
parents:
4686
diff
changeset

889 
impOfSubs analz_subset_parts]) 4 1)); 
6d544b44a70e
spy_analz_tac now handles individual conjuncts properly
paulson
parents:
4686
diff
changeset

890 

2327  891 
fun spy_analz_tac i = 
2373  892 
DETERM 
893 
(SELECT_GOAL 

894 
(EVERY 

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

896 
(REPEAT o CHANGED) 

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

898 
(*...allowing further simplifications*) 

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

900 
REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])), 
4735
6d544b44a70e
spy_analz_tac now handles individual conjuncts properly
paulson
parents:
4686
diff
changeset

901 
DEPTH_SOLVE (atomic_spy_analz_tac 1)]) i); 
6d544b44a70e
spy_analz_tac now handles individual conjuncts properly
paulson
parents:
4686
diff
changeset

902 

2327  903 

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

907 

6915  908 
(*Apply the EXALL quantification to prove uniqueness theorems in 
2415  909 
their standard form*) 
910 
fun prove_unique_tac lemma = 

911 
EVERY' [dtac lemma, 

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

912 
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

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

914 
forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl, 
4091  915 
Blast.depth_tac (claset() addSDs [spec]) 0]; 
2415  916 

2373  917 

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

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

2891  920 
by (Blast_tac 1); 
2373  921 
val Un_absorb3 = result(); 
922 
Addsimps [Un_absorb3]; 

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

923 

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

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

925 
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

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

927 
Addsimps [o_def]; 