author  paulson 
Wed, 10 Mar 1999 10:42:40 +0100  
changeset 6334  e53457213857 
parent 6308  76f3865a2b1d 
child 6915  4ab8e31a8421 
permissions  rwrr 
2320  1 
(* Title: HOL/Auth/Shared 
1934  2 
ID: $Id$ 
3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1996 University of Cambridge 

5 

6 
Theory of Shared Keys (common to all symmetrickey protocols) 

7 

3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3479
diff
changeset

8 
Shared, longterm keys; initial states of agents 
2032  9 
*) 
10 

3472
fb3c38c88c08
Deleted the obsolete operators newK, newN and nPair
paulson
parents:
3465
diff
changeset

11 
(*** Basic properties of shrK ***) 
1934  12 

3472
fb3c38c88c08
Deleted the obsolete operators newK, newN and nPair
paulson
parents:
3465
diff
changeset

13 
(*Injectiveness: Agents' longterm keys are distinct.*) 
fb3c38c88c08
Deleted the obsolete operators newK, newN and nPair
paulson
parents:
3465
diff
changeset

14 
AddIffs [inj_shrK RS inj_eq]; 
2376
f5c61fd9b9b6
Temporary additions (random) for the nested OtwayRees protocol
paulson
parents:
2320
diff
changeset

15 

3472
fb3c38c88c08
Deleted the obsolete operators newK, newN and nPair
paulson
parents:
3465
diff
changeset

16 
(* invKey(shrK A) = shrK A *) 
fb3c38c88c08
Deleted the obsolete operators newK, newN and nPair
paulson
parents:
3465
diff
changeset

17 
Addsimps [rewrite_rule [isSymKey_def] isSym_keys]; 
2320  18 

1934  19 
(** Rewrites should not refer to initState(Friend i) 
20 
 not in normal form! **) 

21 

5076  22 
Goalw [keysFor_def] "keysFor (parts (initState C)) = {}"; 
3667  23 
by (induct_tac "C" 1); 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4423
diff
changeset

24 
by Auto_tac; 
1934  25 
qed "keysFor_parts_initState"; 
26 
Addsimps [keysFor_parts_initState]; 

27 

4509
828148415197
Making proofs faster, especially using keysFor_parts_insert
paulson
parents:
4477
diff
changeset

28 
(*Specialized to sharedkey model: no need for addss in protocol proofs*) 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

29 
Goal "[ K: keysFor (parts (insert X H)); X : synth (analz H) ] \ 
4509
828148415197
Making proofs faster, especially using keysFor_parts_insert
paulson
parents:
4477
diff
changeset

30 
\ ==> K : keysFor (parts H)  Key K : parts H"; 
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

31 
by (force_tac 
4509
828148415197
Making proofs faster, especially using keysFor_parts_insert
paulson
parents:
4477
diff
changeset

32 
(claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono), 
828148415197
Making proofs faster, especially using keysFor_parts_insert
paulson
parents:
4477
diff
changeset

33 
impOfSubs (analz_subset_parts RS keysFor_mono)] 
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

34 
addIs [impOfSubs analz_subset_parts], 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

35 
simpset()) 1); 
4509
828148415197
Making proofs faster, especially using keysFor_parts_insert
paulson
parents:
4477
diff
changeset

36 
qed "keysFor_parts_insert"; 
828148415197
Making proofs faster, especially using keysFor_parts_insert
paulson
parents:
4477
diff
changeset

37 

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

38 
Goal "Crypt K X : H ==> K : keysFor H"; 
4238
679a233fb206
Crypt_imp_keysFor: version of Crypt_imp_invKey_keysFor for shared keys
paulson
parents:
4156
diff
changeset

39 
by (dtac Crypt_imp_invKey_keysFor 1); 
679a233fb206
Crypt_imp_keysFor: version of Crypt_imp_invKey_keysFor for shared keys
paulson
parents:
4156
diff
changeset

40 
by (Asm_full_simp_tac 1); 
679a233fb206
Crypt_imp_keysFor: version of Crypt_imp_invKey_keysFor for shared keys
paulson
parents:
4156
diff
changeset

41 
qed "Crypt_imp_keysFor"; 
679a233fb206
Crypt_imp_keysFor: version of Crypt_imp_invKey_keysFor for shared keys
paulson
parents:
4156
diff
changeset

42 

2032  43 

6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

44 
(*** Function "knows" ***) 
1934  45 

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3512
diff
changeset

46 
(*Spy sees shared keys of agents!*) 
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

47 
Goal "A: bad ==> Key (shrK A) : knows Spy evs"; 
3667  48 
by (induct_tac "evs" 1); 
3683  49 
by (ALLGOALS (asm_simp_tac 
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

50 
(simpset() addsimps [imageI, knows_Cons] 
4686  51 
addsplits [expand_event_case]))); 
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

52 
qed "Spy_knows_Spy_bad"; 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

53 
AddSIs [Spy_knows_Spy_bad]; 
2032  54 

3683  55 
(*For not_bad_tac*) 
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

56 
Goal "[ Crypt (shrK A) X : analz (knows Spy evs); A: bad ] \ 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

57 
\ ==> X : analz (knows Spy evs)"; 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

58 
by (force_tac (claset() addSDs [analz.Decrypt], simpset()) 1); 
3683  59 
qed "Crypt_Spy_analz_bad"; 
2072  60 

3443  61 
(*Prove that the agent is uncompromised by the confidentiality of 
62 
a component of a message she's said.*) 

3683  63 
fun not_bad_tac s = 
64 
case_tac ("(" ^ s ^ ") : bad") THEN' 

3443  65 
SELECT_GOAL 
6334  66 
(REPEAT_DETERM (etac exE 1) THEN 
67 
REPEAT_DETERM (dtac (Says_imp_spies RS analz.Inj) 1) THEN 

3443  68 
REPEAT_DETERM (etac MPair_analz 1) THEN 
69 
THEN_BEST_FIRST 

3683  70 
(dres_inst_tac [("A", s)] Crypt_Spy_analz_bad 1 THEN assume_tac 1) 
3443  71 
(has_fewer_prems 1, size_of_thm) 
72 
(Step_tac 1)); 

1934  73 

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

74 

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

75 
(** Fresh keys never clash with longterm shared keys **) 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

76 

3683  77 
(*Agents see their own shared keys!*) 
5076  78 
Goal "Key (shrK A) : initState A"; 
3683  79 
by (induct_tac "A" 1); 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4423
diff
changeset

80 
by Auto_tac; 
3683  81 
qed "shrK_in_initState"; 
82 
AddIffs [shrK_in_initState]; 

83 

5076  84 
Goal "Key (shrK A) : used evs"; 
4423  85 
by (rtac initState_into_used 1); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2922
diff
changeset

86 
by (Blast_tac 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

87 
qed "shrK_in_used"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

88 
AddIffs [shrK_in_used]; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

89 

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

90 
(*Used in parts_induct_tac and analz_Fake_tac to distinguish session keys 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

91 
from longterm shared keys*) 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

92 
Goal "Key K ~: used evs ==> K ~: range shrK"; 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2922
diff
changeset

93 
by (Blast_tac 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

94 
qed "Key_not_used"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

95 

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

96 
Goal "Key K ~: used evs ==> shrK B ~= K"; 
2891  97 
by (Blast_tac 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

98 
qed "shrK_neq"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

99 

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

100 
Addsimps [Key_not_used, shrK_neq, shrK_neq RS not_sym]; 
3961  101 

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

102 

3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3479
diff
changeset

103 
(*** Fresh nonces ***) 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

104 

5076  105 
Goal "Nonce N ~: parts (initState B)"; 
3667  106 
by (induct_tac "B" 1); 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4423
diff
changeset

107 
by Auto_tac; 
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3479
diff
changeset

108 
qed "Nonce_notin_initState"; 
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3479
diff
changeset

109 
AddIffs [Nonce_notin_initState]; 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

110 

5076  111 
Goal "Nonce N ~: used []"; 
4091  112 
by (simp_tac (simpset() addsimps [used_Nil]) 1); 
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3479
diff
changeset

113 
qed "Nonce_notin_used_empty"; 
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3479
diff
changeset

114 
Addsimps [Nonce_notin_used_empty]; 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

115 

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

116 

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

117 
(*** Supply fresh nonces for possibility theorems. ***) 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

118 

3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3479
diff
changeset

119 
(*In any trace, there is an upper bound N on the greatest nonce in use.*) 
5076  120 
Goal "EX N. ALL n. N<=n > Nonce n ~: used evs"; 
3667  121 
by (induct_tac "evs" 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

122 
by (res_inst_tac [("x","0")] exI 1); 
3683  123 
by (ALLGOALS (asm_simp_tac 
4091  124 
(simpset() addsimps [used_Cons] 
4686  125 
addsplits [expand_event_case]))); 
3730  126 
by Safe_tac; 
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3479
diff
changeset

127 
by (ALLGOALS (rtac (msg_Nonce_supply RS exE))); 
4091  128 
by (ALLGOALS (blast_tac (claset() addSEs [add_leE]))); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

129 
val lemma = result(); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

130 

5076  131 
Goal "EX N. Nonce N ~: used evs"; 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

132 
by (rtac (lemma RS exE) 1); 
2891  133 
by (Blast_tac 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

134 
qed "Nonce_supply1"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

135 

5076  136 
Goal "EX N N'. Nonce N ~: used evs & Nonce N' ~: used evs' & N ~= N'"; 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

137 
by (cut_inst_tac [("evs","evs")] lemma 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

138 
by (cut_inst_tac [("evs","evs'")] lemma 1); 
3708  139 
by (Clarify_tac 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

140 
by (res_inst_tac [("x","N")] exI 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

141 
by (res_inst_tac [("x","Suc (N+Na)")] exI 1); 
5502  142 
by (asm_simp_tac (simpset() addsimps [less_not_refl3, le_add1, le_add2, 
143 
less_Suc_eq_le]) 1); 

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

144 
qed "Nonce_supply2"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

145 

5076  146 
Goal "EX N N' N''. Nonce N ~: used evs & Nonce N' ~: used evs' & \ 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

147 
\ Nonce N'' ~: used evs'' & N ~= N' & N' ~= N'' & N ~= N''"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

148 
by (cut_inst_tac [("evs","evs")] lemma 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

149 
by (cut_inst_tac [("evs","evs'")] lemma 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

150 
by (cut_inst_tac [("evs","evs''")] lemma 1); 
3708  151 
by (Clarify_tac 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

152 
by (res_inst_tac [("x","N")] exI 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

153 
by (res_inst_tac [("x","Suc (N+Na)")] exI 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

154 
by (res_inst_tac [("x","Suc (Suc (N+Na+Nb))")] exI 1); 
5502  155 
by (asm_simp_tac (simpset() addsimps [less_not_refl3, le_add1, le_add2, 
156 
less_Suc_eq_le]) 1); 

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

157 
qed "Nonce_supply3"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

158 

5076  159 
Goal "Nonce (@ N. Nonce N ~: used evs) ~: used evs"; 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

160 
by (rtac (lemma RS exE) 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

161 
by (rtac selectI 1); 
2891  162 
by (Blast_tac 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

163 
qed "Nonce_supply"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

164 

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

165 
(*** Supply fresh keys for possibility theorems. ***) 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

166 

5076  167 
Goal "EX K. Key K ~: used evs"; 
3414
804c8a178a7f
Modified a few defs and proofs because of the changes to theory Finite.thy.
nipkow
parents:
3207
diff
changeset

168 
by (rtac (Finites.emptyI RS Key_supply_ax RS exE) 1); 
2891  169 
by (Blast_tac 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

170 
qed "Key_supply1"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

171 

5076  172 
Goal "EX K K'. Key K ~: used evs & Key K' ~: used evs' & K ~= K'"; 
3414
804c8a178a7f
Modified a few defs and proofs because of the changes to theory Finite.thy.
nipkow
parents:
3207
diff
changeset

173 
by (cut_inst_tac [("evs","evs")] (Finites.emptyI RS Key_supply_ax) 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

174 
by (etac exE 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

175 
by (cut_inst_tac [("evs","evs'")] 
3414
804c8a178a7f
Modified a few defs and proofs because of the changes to theory Finite.thy.
nipkow
parents:
3207
diff
changeset

176 
(Finites.emptyI RS Finites.insertI RS Key_supply_ax) 1); 
4633
d4a074973715
corrected problem with auto_tac: now uses a variant of depth_tac that avoids
oheimb
parents:
4509
diff
changeset

177 
by (Asm_full_simp_tac 1 THEN depth_tac (claset()) 2 1); (* replaces Auto_tac *) 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

178 
qed "Key_supply2"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

179 

5076  180 
Goal "EX K K' K''. Key K ~: used evs & Key K' ~: used evs' & \ 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

181 
\ Key K'' ~: used evs'' & K ~= K' & K' ~= K'' & K ~= K''"; 
3414
804c8a178a7f
Modified a few defs and proofs because of the changes to theory Finite.thy.
nipkow
parents:
3207
diff
changeset

182 
by (cut_inst_tac [("evs","evs")] (Finites.emptyI RS Key_supply_ax) 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

183 
by (etac exE 1); 
4156  184 
(*Blast_tac requires instantiation of the keys for some reason*) 
185 
by (cut_inst_tac [("evs","evs'"), ("a1","K")] 

3414
804c8a178a7f
Modified a few defs and proofs because of the changes to theory Finite.thy.
nipkow
parents:
3207
diff
changeset

186 
(Finites.emptyI RS Finites.insertI RS Key_supply_ax) 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

187 
by (etac exE 1); 
4156  188 
by (cut_inst_tac [("evs","evs''"), ("a1","Ka"), ("a2","K")] 
3414
804c8a178a7f
Modified a few defs and proofs because of the changes to theory Finite.thy.
nipkow
parents:
3207
diff
changeset

189 
(Finites.emptyI RS Finites.insertI RS Finites.insertI RS Key_supply_ax) 1); 
4156  190 
by (Blast_tac 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

191 
qed "Key_supply3"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

192 

5076  193 
Goal "Key (@ K. Key K ~: used evs) ~: used evs"; 
3414
804c8a178a7f
Modified a few defs and proofs because of the changes to theory Finite.thy.
nipkow
parents:
3207
diff
changeset

194 
by (rtac (Finites.emptyI RS Key_supply_ax RS exE) 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

195 
by (rtac selectI 1); 
2891  196 
by (Blast_tac 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

197 
qed "Key_supply"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

198 

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

199 
(*** Tactics for possibility theorems ***) 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

200 

3673
3b06747c3f37
Having "addcongs [if_weak_cong]" in analz_image_..._ss makes simplification
paulson
parents:
3667
diff
changeset

201 
(*Omitting used_Says makes the tactic much faster: it leaves expressions 
3b06747c3f37
Having "addcongs [if_weak_cong]" in analz_image_..._ss makes simplification
paulson
parents:
3667
diff
changeset

202 
such as Nonce ?N ~: used evs that match Nonce_supply*) 
3542
db5e9aceea49
Now possibility_tac and basic_possibility_tac are explicit functions, in order
paulson
parents:
3519
diff
changeset

203 
fun possibility_tac st = st > 
3673
3b06747c3f37
Having "addcongs [if_weak_cong]" in analz_image_..._ss makes simplification
paulson
parents:
3667
diff
changeset

204 
(REPEAT 
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

205 
(ALLGOALS (simp_tac (simpset() delsimps [used_Says, used_Notes, used_Gets] 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

206 
setSolver safe_solver)) 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

208 
REPEAT_FIRST (eq_assume_tac ORELSE' 
3542
db5e9aceea49
Now possibility_tac and basic_possibility_tac are explicit functions, in order
paulson
parents:
3519
diff
changeset

209 
resolve_tac [refl, conjI, Nonce_supply, Key_supply]))); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

210 

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

211 
(*For harder protocols (such as Recur) where we have to set up some 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

212 
nonces and keys initially*) 
3542
db5e9aceea49
Now possibility_tac and basic_possibility_tac are explicit functions, in order
paulson
parents:
3519
diff
changeset

213 
fun basic_possibility_tac st = st > 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

214 
REPEAT 
4091  215 
(ALLGOALS (asm_simp_tac (simpset() setSolver safe_solver)) 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

217 
REPEAT_FIRST (resolve_tac [refl, conjI])); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

218 

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

219 

3472
fb3c38c88c08
Deleted the obsolete operators newK, newN and nPair
paulson
parents:
3465
diff
changeset

220 
(*** Specialized rewriting for analz_insert_freshK ***) 
2320  221 

5492  222 
Goal "A <=  (range shrK) ==> shrK x ~: A"; 
2891  223 
by (Blast_tac 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

224 
qed "subset_Compl_range"; 
2045
ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

225 

5076  226 
Goal "insert (Key K) H = Key `` {K} Un H"; 
2891  227 
by (Blast_tac 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

228 
qed "insert_Key_singleton"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

229 

5076  230 
Goal "insert (Key K) (Key``KK Un C) = Key `` (insert K KK) Un C"; 
2891  231 
by (Blast_tac 1); 
232 
qed "insert_Key_image"; 

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

233 

3451
d10f100676d8
Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents:
3443
diff
changeset

234 
(*Reverse the normal simplification of "image" to build up (not break down) 
d10f100676d8
Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents:
3443
diff
changeset

235 
the set of keys. Use analz_insert_eq with (Un_upper2 RS analz_mono) to 
d10f100676d8
Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents:
3443
diff
changeset

236 
erase occurrences of forwarded message components (X).*) 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

237 
val analz_image_freshK_ss = 
4091  238 
simpset() addcongs [if_weak_cong] 
3673
3b06747c3f37
Having "addcongs [if_weak_cong]" in analz_image_..._ss makes simplification
paulson
parents:
3667
diff
changeset

239 
delsimps [image_insert, image_Un] 
3680
7588653475b2
Removed the simprule imp_disjL from the analz_image_..._ss to boost speed
paulson
parents:
3673
diff
changeset

240 
delsimps [imp_disjL] (*reduces blowup*) 
5535  241 
addsimps [image_insert RS sym, image_Un RS sym, 
242 
analz_insert_eq, impOfSubs (Un_upper2 RS analz_mono), 

243 
insert_Key_singleton, subset_Compl_range, 

244 
Key_not_used, insert_Key_image, Un_assoc RS sym] 

245 
@disj_comms; 

2045
ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

246 

ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

247 
(*Lemma for the trivial direction of the ifandonlyif*) 
5278  248 
Goal "(Key K : analz (Key``nE Un H)) > (K : nE  Key K : analz H) ==> \ 
2045
ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

249 
\ (Key K : analz (Key``nE Un H)) = (K : nE  Key K : analz H)"; 
4091  250 
by (blast_tac (claset() addIs [impOfSubs analz_mono]) 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

251 
qed "analz_image_freshK_lemma"; 