author  paulson 
Mon, 29 Sep 1997 11:47:01 +0200  
changeset 3730  6933d20f335f 
parent 3708  56facaebf3e3 
child 3908  4f19a40a9343 
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 

1934  11 

12 
open Shared; 

13 

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

14 
(*** Basic properties of shrK ***) 
1934  15 

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

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

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

18 

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

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

20 
Addsimps [rewrite_rule [isSymKey_def] isSym_keys]; 
2320  21 

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

24 

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

25 
goalw thy [keysFor_def] "keysFor (parts (initState C)) = {}"; 
3667  26 
by (induct_tac "C" 1); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2922
diff
changeset

27 
by (Auto_tac ()); 
1934  28 
qed "keysFor_parts_initState"; 
29 
Addsimps [keysFor_parts_initState]; 

30 

2032  31 

3683  32 
(*** Function "spies" ***) 
1934  33 

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

34 
(*Spy sees shared keys of agents!*) 
3683  35 
goal thy "!!A. A: bad ==> Key (shrK A) : spies evs"; 
3667  36 
by (induct_tac "evs" 1); 
3683  37 
by (ALLGOALS (asm_simp_tac 
38 
(!simpset addsimps [imageI, spies_Cons] 

39 
setloop split_tac [expand_event_case, expand_if]))); 

40 
qed "Spy_spies_bad"; 

1934  41 

3683  42 
AddSIs [Spy_spies_bad]; 
2032  43 

3683  44 
(*For not_bad_tac*) 
45 
goal thy "!!A. [ Crypt (shrK A) X : analz (spies evs); A: bad ] \ 

46 
\ ==> X : analz (spies evs)"; 

3443  47 
by (fast_tac (!claset addSDs [analz.Decrypt] addss (!simpset)) 1); 
3683  48 
qed "Crypt_Spy_analz_bad"; 
2072  49 

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

3683  52 
fun not_bad_tac s = 
53 
case_tac ("(" ^ s ^ ") : bad") THEN' 

3443  54 
SELECT_GOAL 
3683  55 
(REPEAT_DETERM (dtac (Says_imp_spies RS analz.Inj) 1) THEN 
3443  56 
REPEAT_DETERM (etac MPair_analz 1) THEN 
57 
THEN_BEST_FIRST 

3683  58 
(dres_inst_tac [("A", s)] Crypt_Spy_analz_bad 1 THEN assume_tac 1) 
3443  59 
(has_fewer_prems 1, size_of_thm) 
60 
(Step_tac 1)); 

1934  61 

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

62 

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

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

64 

3683  65 
(*Agents see their own shared keys!*) 
66 
goal thy "Key (shrK A) : initState A"; 

67 
by (induct_tac "A" 1); 

68 
by (Auto_tac()); 

69 
qed "shrK_in_initState"; 

70 
AddIffs [shrK_in_initState]; 

71 

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

72 
goal thy "Key (shrK A) : used evs"; 
3683  73 
br initState_into_used 1; 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2922
diff
changeset

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

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

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

77 

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

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

79 
from longterm shared keys*) 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

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

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

83 

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

84 
(*A session key cannot clash with a longterm shared key*) 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

85 
goal thy "!!K. K ~: range shrK ==> shrK B ~= K"; 
2891  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_neq"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

88 

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

89 
Addsimps [Key_not_used, shrK_neq, shrK_neq RS not_sym]; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

90 

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

91 

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

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

93 

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

94 
goal thy "Nonce N ~: parts (initState B)"; 
3667  95 
by (induct_tac "B" 1); 
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3479
diff
changeset

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

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

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

99 

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

100 
goal thy "Nonce N ~: used []"; 
3683  101 
by (simp_tac (!simpset addsimps [used_Nil]) 1); 
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3479
diff
changeset

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

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

104 

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

105 

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

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

107 

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

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

111 
by (res_inst_tac [("x","0")] exI 1); 
3683  112 
by (ALLGOALS (asm_simp_tac 
113 
(!simpset addsimps [used_Cons] 

114 
setloop split_tac [expand_event_case, expand_if]))); 

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

116 
by (ALLGOALS (rtac (msg_Nonce_supply RS exE))); 
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3479
diff
changeset

117 
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

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

119 

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

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

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

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

124 

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

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

126 
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

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

129 
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

130 
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

131 
by (asm_simp_tac (!simpset addsimps [less_not_refl2 RS not_sym, 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

133 
le_eq_less_Suc RS sym]) 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

135 

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

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

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

138 
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

139 
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

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

142 
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

143 
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

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

145 
by (asm_simp_tac (!simpset addsimps [less_not_refl2 RS not_sym, 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

147 
le_eq_less_Suc RS sym]) 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

149 
by (stac (le_eq_less_Suc RS sym) 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

150 
by (asm_simp_tac (!simpset addsimps [le_eq_less_Suc RS sym]) 2); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

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

153 

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

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

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

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

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

159 

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

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

161 

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

162 
goal thy "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

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

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

166 

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

167 
goal thy "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

168 
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

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

170 
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

171 
(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

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

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

174 

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

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

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

177 
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

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

179 
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

180 
(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

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

182 
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

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

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

186 
by (fast_tac (!claset addSEs [allE]) 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

188 

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

189 
goal thy "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

190 
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

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

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

194 

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

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

196 

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

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

198 
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

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

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

201 
(ALLGOALS (simp_tac (!simpset delsimps [used_Says] setSolver safe_solver)) 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

203 
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

204 
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

205 

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

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

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

208 
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

209 
REPEAT 
2637
e9b203f854ae
reflecting my recent changes of the simplifier and classical reasoner
oheimb
parents:
2516
diff
changeset

210 
(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

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

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

213 

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

214 

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

215 
(*** Specialized rewriting for analz_insert_freshK ***) 
2320  216 

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

217 
goal thy "!!A. A <= Compl (range shrK) ==> shrK x ~: A"; 
2891  218 
by (Blast_tac 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

220 

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

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

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

224 

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

225 
goal thy "insert (Key K) (Key``KK Un C) = Key `` (insert K KK) Un C"; 
2891  226 
by (Blast_tac 1); 
227 
qed "insert_Key_image"; 

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

228 

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

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

230 
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

231 
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

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

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

234 
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

235 
delsimps [imp_disjL] (*reduces blowup*) 
3479
2aacd6f10654
Reordered rules in analz_image_freshK_ss to improve clarity
paulson
parents:
3472
diff
changeset

236 
addsimps ([image_insert RS sym, image_Un RS sym, 
2aacd6f10654
Reordered rules in analz_image_freshK_ss to improve clarity
paulson
parents:
3472
diff
changeset

237 
analz_insert_eq, impOfSubs (Un_upper2 RS analz_mono), 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

238 
insert_Key_singleton, subset_Compl_range, 
3479
2aacd6f10654
Reordered rules in analz_image_freshK_ss to improve clarity
paulson
parents:
3472
diff
changeset

239 
Key_not_used, insert_Key_image, Un_assoc RS sym] 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

241 
setloop split_tac [expand_if]; 
2045
ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

242 

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

243 
(*Lemma for the trivial direction of the ifandonlyif*) 
ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

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

245 
"!!evs. (Key K : analz (Key``nE Un H)) > (K : nE  Key K : analz H) ==> \ 
ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

246 
\ (Key K : analz (Key``nE Un H)) = (K : nE  Key K : analz H)"; 
2922  247 
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

248 
qed "analz_image_freshK_lemma"; 