author  paulson 
Fri, 11 Jul 1997 13:26:15 +0200  
changeset 3512  9dcb4daa15e8 
parent 3479  2aacd6f10654 
child 3519  ab0a9fbed4c0 
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 

2032  25 
goalw thy [keysFor_def] "keysFor (parts (initState lost C)) = {}"; 
1934  26 
by (agent.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 

32 
(*** Function "sees" ***) 

33 

1964  34 
(*Agents see their own shared keys!*) 
2032  35 
goal thy "A ~= Spy > Key (shrK A) : sees lost A evs"; 
1934  36 
by (list.induct_tac "evs" 1); 
37 
by (agent.induct_tac "A" 1); 

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

38 
by (ALLGOALS (asm_simp_tac (!simpset addsimps [sees_Cons]))); 
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3479
diff
changeset

39 
by (Blast_tac 1); 
2032  40 
qed_spec_mp "sees_own_shrK"; 
1934  41 

2032  42 
(*Spy sees shared keys of lost agents!*) 
2045
ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

43 
goal thy "!!A. A: lost ==> Key (shrK A) : sees lost Spy evs"; 
2032  44 
by (list.induct_tac "evs" 1); 
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3479
diff
changeset

45 
by (ALLGOALS (asm_simp_tac (!simpset addsimps [sees_Cons]))); 
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3479
diff
changeset

46 
by (Blast_tac 1); 
2045
ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

47 
qed "Spy_sees_lost"; 
1934  48 

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

49 
AddSIs [sees_own_shrK, Spy_sees_lost]; 
2032  50 

3443  51 
(*For not_lost_tac*) 
52 
goal thy "!!A. [ Crypt (shrK A) X : analz (sees lost Spy evs); A: lost ] \ 

53 
\ ==> X : analz (sees lost Spy evs)"; 

54 
by (fast_tac (!claset addSDs [analz.Decrypt] addss (!simpset)) 1); 

55 
qed "Crypt_Spy_analz_lost"; 

2072  56 

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

59 
fun not_lost_tac s = 

60 
case_tac ("(" ^ s ^ ") : lost") THEN' 

61 
SELECT_GOAL 

62 
(REPEAT_DETERM (dtac (Says_imp_sees_Spy RS analz.Inj) 1) THEN 

63 
REPEAT_DETERM (etac MPair_analz 1) THEN 

64 
THEN_BEST_FIRST 

65 
(dres_inst_tac [("A", s)] Crypt_Spy_analz_lost 1 THEN assume_tac 1) 

66 
(has_fewer_prems 1, size_of_thm) 

67 
(Step_tac 1)); 

1934  68 

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

69 

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

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

71 

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"; 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2922
diff
changeset

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

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

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

76 

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

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

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

79 
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

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

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

82 

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

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

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

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

87 

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

88 
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

89 

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

90 

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

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

92 

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

93 
goal thy "Nonce N ~: parts (initState lost B)"; 
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3479
diff
changeset

94 
by (agent.induct_tac "B" 1); 
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3479
diff
changeset

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

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

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

98 

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

99 
goal thy "Nonce N ~: used []"; 
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3479
diff
changeset

100 
by (simp_tac (!simpset addsimps [used_def]) 1); 
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3479
diff
changeset

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

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

103 

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 
(*** Supply fresh nonces for possibility theorems. ***) 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

106 

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

107 
(*In any trace, there is an upper bound N on the greatest nonce in use.*) 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

108 
goalw thy [used_def] "EX N. ALL n. N<=n > Nonce n ~: used evs"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

109 
by (list.induct_tac "evs" 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

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

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

113 
(*Inductive step*) 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

114 
by (event.induct_tac "a" 1); 
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3479
diff
changeset

115 
by (ALLGOALS (full_simp_tac 
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3479
diff
changeset

116 
(!simpset delsimps [sees_Notes] 
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3479
diff
changeset

117 
addsimps [UN_parts_sees_Says, 
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3479
diff
changeset

118 
UN_parts_sees_Notes]))); 
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3479
diff
changeset

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

120 
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

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

122 

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

123 
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

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

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

127 

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

128 
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

129 
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

130 
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

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

132 
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

133 
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

134 
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

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

136 
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

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

138 

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

139 
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

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

141 
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

142 
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

143 
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

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

145 
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

146 
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

147 
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

148 
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

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

150 
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

151 
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

152 
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

153 
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

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

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

156 

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

157 
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

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

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

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

162 

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

163 
(*** Supply fresh keys for possibility theorems. ***) 
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 
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

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

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

169 

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

170 
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

171 
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

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

173 
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

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

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

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

177 

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

178 
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

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

180 
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

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 Key_supply_ax) 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

185 
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

186 
(Finites.emptyI RS Finites.insertI 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 (Step_tac 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

189 
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

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

191 

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

192 
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

193 
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

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

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

197 

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

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

199 

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

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

201 
REPEAT (*omit used_Says so that Nonces, Keys start from different traces!*) 
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3479
diff
changeset

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

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

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

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

206 

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

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

208 
nonces and keys initially*) 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

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

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

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

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

214 

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

215 

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

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

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

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

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

221 

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

222 
goal thy "insert (Key K) H = Key `` {K} Un H"; 
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 "insert_Key_singleton"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

225 

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

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

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

229 

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

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

231 
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

232 
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

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

234 
!simpset delsimps [image_insert, image_Un] 
3479
2aacd6f10654
Reordered rules in analz_image_freshK_ss to improve clarity
paulson
parents:
3472
diff
changeset

235 
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

236 
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

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

238 
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

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

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

241 

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

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

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

244 
"!!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

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

247 
qed "analz_image_freshK_lemma"; 