author  paulson 
Fri, 18 Oct 1996 11:42:41 +0200  
changeset 2110  d01151e66cd4 
parent 2060  275ef0f28e1f 
child 2133  f00a688760b9 
permissions  rwrr 
1995  1 
(* Title: HOL/Auth/Yahalom 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

2 
ID: $Id$ 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

4 
Copyright 1996 University of Cambridge 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

5 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

6 
Inductive relation "otway" for the Yahalom protocol. 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

7 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

8 
From page 257 of 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

9 
Burrows, Abadi and Needham. A Logic of Authentication. 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

10 
Proc. Royal Soc. 426 (1989) 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

11 
*) 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

12 

1995  13 
open Yahalom; 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

14 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

15 
proof_timing:=true; 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

16 
HOL_quantifiers := false; 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

17 

1995  18 

2013  19 
(*Weak liveness: there are traces that reach the end*) 
1995  20 

21 
goal thy 

22 
"!!A B. [ A ~= B; A ~= Server; B ~= Server ] \ 

2032  23 
\ ==> EX X NB K. EX evs: yahalom lost. \ 
1995  24 
\ Says A B {X, Crypt (Nonce NB) K} : set_of_list evs"; 
25 
by (REPEAT (resolve_tac [exI,bexI] 1)); 

2032  26 
by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS yahalom.YM4) 2); 
1995  27 
by (ALLGOALS (simp_tac (!simpset setsolver safe_solver))); 
28 
by (ALLGOALS Fast_tac); 

2013  29 
result(); 
1995  30 

31 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

32 
(**** Inductive proofs about yahalom ****) 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

33 

2110  34 
(*Monotonicity*) 
2045
ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

35 
goal thy "!!evs. lost' <= lost ==> yahalom lost' <= yahalom lost"; 
ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

36 
by (rtac subsetI 1); 
ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

37 
by (etac yahalom.induct 1); 
ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

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

39 
(best_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono) 
ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

40 
:: yahalom.intrs)))); 
ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

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

42 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

43 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

44 
(*Nobody sends themselves messages*) 
2051  45 
goal thy "!!evs. evs: yahalom lost ==> ALL A X. Says A A X ~: set_of_list evs"; 
2032  46 
by (etac yahalom.induct 1); 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

47 
by (Auto_tac()); 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

48 
qed_spec_mp "not_Says_to_self"; 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

49 
Addsimps [not_Says_to_self]; 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

50 
AddSEs [not_Says_to_self RSN (2, rev_notE)]; 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

51 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

52 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

53 
(** For reasoning about the encrypted portion of messages **) 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

54 

1995  55 
(*Lets us treat YM4 using a similar argument as for the Fake case.*) 
56 
goal thy "!!evs. Says S A {Crypt Y (shrK A), X} : set_of_list evs ==> \ 

2032  57 
\ X : analz (sees lost Spy evs)"; 
58 
by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1); 

59 
qed "YM4_analz_sees_Spy"; 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

60 

2110  61 
bind_thm ("YM4_parts_sees_Spy", 
62 
YM4_analz_sees_Spy RS (impOfSubs analz_subset_parts)); 

63 

64 
(*Relates to both YM4 and Revl*) 

1995  65 
goal thy "!!evs. Says S A {Crypt {B, K, NA, NB} (shrK A), X} \ 
66 
\ : set_of_list evs ==> \ 

2032  67 
\ K : parts (sees lost Spy evs)"; 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

68 
by (fast_tac (!claset addSEs partsEs 
2032  69 
addSDs [Says_imp_sees_Spy RS parts.Inj]) 1); 
2110  70 
qed "YM4_Key_parts_sees_Spy"; 
71 

72 
(*We instantiate the variable to "lost". Leaving it as a Var makes proofs 

73 
harder: the simplifier does less.*) 

74 
val parts_Fake_tac = 

75 
forw_inst_tac [("lost","lost")] YM4_parts_sees_Spy 6 THEN 

76 
forw_inst_tac [("lost","lost")] YM4_Key_parts_sees_Spy 7; 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

77 

2110  78 
(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *) 
79 
fun parts_induct_tac i = SELECT_GOAL 

80 
(DETERM (etac yahalom.induct 1 THEN parts_Fake_tac THEN 

81 
(*Fake message*) 

82 
TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts, 

83 
impOfSubs Fake_parts_insert] 

84 
addss (!simpset)) 2)) THEN 

85 
(*Base case*) 

86 
fast_tac (!claset addss (!simpset)) 1 THEN 

87 
ALLGOALS Asm_simp_tac) i; 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

88 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

89 

2032  90 
(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY 
2013  91 
sends messages containing X! **) 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

92 

2110  93 
(*Spy never sees another agent's shared key! (unless it is leaked at start)*) 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

94 
goal thy 
2032  95 
"!!evs. [ evs : yahalom lost; A ~: lost ] \ 
96 
\ ==> Key (shrK A) ~: parts (sees lost Spy evs)"; 

2110  97 
by (parts_induct_tac 1); 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

98 
by (Auto_tac()); 
2032  99 
qed "Spy_not_see_shrK"; 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

100 

2032  101 
bind_thm ("Spy_not_analz_shrK", 
102 
[analz_subset_parts, Spy_not_see_shrK] MRS contra_subsetD); 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

103 

2032  104 
Addsimps [Spy_not_see_shrK, Spy_not_analz_shrK]; 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

105 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

106 
(*We go to some trouble to preserve R in the 3rd and 4th subgoals 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

107 
As usual fast_tac cannot be used because it uses the equalities too soon*) 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

108 
val major::prems = 
2032  109 
goal thy "[ Key (shrK A) : parts (sees lost Spy evs); \ 
110 
\ evs : yahalom lost; \ 

111 
\ A:lost ==> R \ 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

112 
\ ] ==> R"; 
2032  113 
by (rtac ccontr 1); 
114 
by (rtac ([major, Spy_not_see_shrK] MRS rev_notE) 1); 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

115 
by (swap_res_tac prems 2); 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

116 
by (ALLGOALS (fast_tac (!claset addIs prems))); 
2032  117 
qed "Spy_see_shrK_E"; 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

118 

2032  119 
bind_thm ("Spy_analz_shrK_E", 
120 
analz_subset_parts RS subsetD RS Spy_see_shrK_E); 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

121 

2032  122 
AddSEs [Spy_see_shrK_E, Spy_analz_shrK_E]; 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

123 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

124 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

125 
(*** Future keys can't be seen or used! ***) 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

126 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

127 
(*Nobody can have SEEN keys that will be generated in the future. 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

128 
This has to be proved anew for each protocol description, 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

129 
but should go by similar reasoning every time. Hardest case is the 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

130 
standard Fake rule. 
2110  131 
The Union over C is essential for the induction! *) 
2032  132 
goal thy "!!evs. evs : yahalom lost ==> \ 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

133 
\ length evs <= length evs' > \ 
2032  134 
\ Key (newK evs') ~: (UN C. parts (sees lost C evs))"; 
2110  135 
by (parts_induct_tac 1); 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

136 
by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts, 
2032  137 
impOfSubs parts_insert_subset_Un, 
138 
Suc_leD] 

139 
addss (!simpset)))); 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

140 
val lemma = result(); 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

141 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

142 
(*Variant needed for the main theorem below*) 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

143 
goal thy 
2032  144 
"!!evs. [ evs : yahalom lost; length evs <= length evs' ] \ 
145 
\ ==> Key (newK evs') ~: parts (sees lost C evs)"; 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

146 
by (fast_tac (!claset addDs [lemma]) 1); 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

147 
qed "new_keys_not_seen"; 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

148 
Addsimps [new_keys_not_seen]; 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

149 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

150 
(*Another variant: old messages must contain old keys!*) 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

151 
goal thy 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

152 
"!!evs. [ Says A B X : set_of_list evs; \ 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

153 
\ Key (newK evt) : parts {X}; \ 
2032  154 
\ evs : yahalom lost \ 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

155 
\ ] ==> length evt < length evs"; 
2032  156 
by (rtac ccontr 1); 
157 
by (dtac leI 1); 

158 
by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy] 

2013  159 
addIs [impOfSubs parts_mono]) 1); 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

160 
qed "Says_imp_old_keys"; 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

161 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

162 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

163 
(*Nobody can have USED keys that will be generated in the future. 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

164 
...very like new_keys_not_seen*) 
2032  165 
goal thy "!!evs. evs : yahalom lost ==> \ 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

166 
\ length evs <= length evs' > \ 
2032  167 
\ newK evs' ~: keysFor (UN C. parts (sees lost C evs))"; 
2110  168 
by (parts_induct_tac 1); 
169 
by (dresolve_tac [YM4_Key_parts_sees_Spy] 5); 

170 

1995  171 
(*YM1, YM2 and YM3*) 
172 
by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,3,2])); 

173 
(*Fake and YM4: these messages send unknown (X) components*) 

174 
by (stac insert_commute 2); 

175 
by (Simp_tac 2); 

176 
(*YM4: the only way K could have been used is if it had been seen, 

177 
contradicting new_keys_not_seen*) 

2110  178 
by (REPEAT 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

179 
(best_tac 
2026
0df5a96bf77e
Last working version prior to introduction of "lost"
paulson
parents:
2013
diff
changeset

180 
(!claset addDs [impOfSubs analz_subset_parts, 
2032  181 
impOfSubs (analz_subset_parts RS keysFor_mono), 
182 
impOfSubs (parts_insert_subset_Un RS keysFor_mono), 

183 
Suc_leD] 

184 
addEs [new_keys_not_seen RSN(2,rev_notE)] 

2110  185 
addss (!simpset)) 1)); 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

186 
val lemma = result(); 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

187 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

188 
goal thy 
2032  189 
"!!evs. [ evs : yahalom lost; length evs <= length evs' ] \ 
190 
\ ==> newK evs' ~: keysFor (parts (sees lost C evs))"; 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

191 
by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1); 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

192 
qed "new_keys_not_used"; 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

193 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

194 
bind_thm ("new_keys_not_analzd", 
2032  195 
[analz_subset_parts RS keysFor_mono, 
196 
new_keys_not_used] MRS contra_subsetD); 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

197 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

198 
Addsimps [new_keys_not_used, new_keys_not_analzd]; 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

199 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

200 

2110  201 
(*Describes the form of Key K when the following message is sent. The use of 
202 
"parts" strengthens the induction hyp for proving the Fake case. The 

203 
assumption A ~: lost prevents its being a Faked message. (Based 

204 
on NS_Shared/Says_S_message_form) *) 

205 
goal thy 

206 
"!!evs. evs: yahalom lost ==> \ 

207 
\ Crypt {B, Key K, NA, NB} (shrK A) : parts (sees lost Spy evs) \ 

208 
\ > A ~: lost > (EX evt: yahalom lost. K = newK evt)"; 

209 
by (parts_induct_tac 1); 

210 
by (Auto_tac()); 

211 
qed_spec_mp "Reveal_message_lemma"; 

212 

213 
(*EITHER describes the form of Key K when the following message is sent, 

214 
OR reduces it to the Fake case.*) 

215 

216 
goal thy 

217 
"!!evs. [ Says S A {Crypt {B, Key K, NA, NB} (shrK A), X} \ 

218 
\ : set_of_list evs; \ 

219 
\ evs : yahalom lost ] \ 

220 
\ ==> (EX evt: yahalom lost. K = newK evt) \ 

221 
\  Key K : analz (sees lost Spy evs)"; 

222 
br (Reveal_message_lemma RS disjCI) 1; 

223 
ba 1; 

224 
by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj] 

225 
addDs [impOfSubs analz_subset_parts]) 1); 

226 
by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj] 

227 
addss (!simpset)) 1); 

228 
qed "Reveal_message_form"; 

229 

230 

231 
(*For proofs involving analz. We again instantiate the variable to "lost".*) 

232 
val analz_Fake_tac = 

233 
dres_inst_tac [("lost","lost")] YM4_analz_sees_Spy 6 THEN 

234 
forw_inst_tac [("lost","lost")] Reveal_message_form 7; 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

235 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

236 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

237 
(**** 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

238 
The following is to prove theorems of the form 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

239 

2032  240 
Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) ==> 
241 
Key K : analz (sees lost Spy evs) 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

242 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

243 
A more general formula must be proved inductively. 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

244 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

245 
****) 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

246 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

247 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

248 
(*NOT useful in this form, but it says that session keys are not used 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

249 
to encrypt messages containing other keys, in the actual protocol. 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

250 
We require that agents should behave like this subsequently also.*) 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

251 
goal thy 
2032  252 
"!!evs. evs : yahalom lost ==> \ 
253 
\ (Crypt X (newK evt)) : parts (sees lost Spy evs) & \ 

254 
\ Key K : parts {X} > Key K : parts (sees lost Spy evs)"; 

255 
by (etac yahalom.induct 1); 

2110  256 
by parts_Fake_tac; 
2060  257 
by (ALLGOALS Asm_simp_tac); 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

258 
(*Deals with Faked messages*) 
2110  259 
by (best_tac (!claset addSEs partsEs 
260 
addDs [impOfSubs parts_insert_subset_Un] 

261 
addss (!simpset)) 2); 

1995  262 
(*Base case*) 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

263 
by (Auto_tac()); 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

264 
result(); 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

265 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

266 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

267 
(** Session keys are not used to encrypt other session keys **) 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

268 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

269 
goal thy 
2032  270 
"!!evs. evs : yahalom lost ==> \ 
271 
\ ALL K E. (Key K : analz (Key``(newK``E) Un (sees lost Spy evs))) = \ 

272 
\ (K : newK``E  Key K : analz (sees lost Spy evs))"; 

273 
by (etac yahalom.induct 1); 

2110  274 
by analz_Fake_tac; 
2045
ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

275 
by (REPEAT_FIRST (resolve_tac [allI, analz_image_newK_lemma])); 
2110  276 
by (REPEAT ((eresolve_tac [bexE, disjE] ORELSE' hyp_subst_tac) 8)); 
277 
by (ALLGOALS (*Takes 26 secs*) 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

278 
(asm_simp_tac 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

279 
(!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK] 
2032  280 
@ pushes) 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

281 
setloop split_tac [expand_if]))); 
2110  282 
(** LEVEL 5 **) 
283 
(*Reveal case 2, YM4, Fake*) 

284 
by (EVERY (map spy_analz_tac [6, 4, 2])); 

285 
(*Reveal case 1, YM3, Base*) 

286 
by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1)); 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

287 
qed_spec_mp "analz_image_newK"; 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

288 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

289 
goal thy 
2032  290 
"!!evs. evs : yahalom lost ==> \ 
291 
\ Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) = \ 

292 
\ (K = newK evt  Key K : analz (sees lost Spy evs))"; 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

293 
by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, 
2032  294 
insert_Key_singleton]) 1); 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

295 
by (Fast_tac 1); 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

296 
qed "analz_insert_Key_newK"; 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

297 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

298 

2110  299 
(*** The Key K uniquely identifies the Server's message. **) 
300 

301 
goal thy 

302 
"!!evs. evs : yahalom lost ==> \ 

303 
\ EX A' B' NA' NB'. ALL A B NA NB. \ 

304 
\ Says Server A \ 

305 
\ {Crypt {Agent B, Key K, NA, NB} (shrK A), \ 

306 
\ Crypt {Agent A, Key K} (shrK B)} \ 

307 
\ : set_of_list evs > A=A' & B=B' & NA=NA' & NB=NB'"; 

308 
by (etac yahalom.induct 1); 

309 
by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib]))); 

310 
by (Step_tac 1); 

311 
(*Remaining case: YM3*) 

312 
by (expand_case_tac "K = ?y" 1); 

313 
by (REPEAT (ares_tac [refl,exI,impI,conjI] 2)); 

314 
(*...we assume X is a very new message, and handle this case by contradiction*) 

315 
by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl] 

316 
delrules [conjI] (*prevent splitup into 4 subgoals*) 

317 
addss (!simpset addsimps [parts_insertI])) 1); 

318 
val lemma = result(); 

319 

320 
goal thy 

321 
"!!evs. [ Says Server A \ 

322 
\ {Crypt {Agent B, Key K, NA, NB} (shrK A), \ 

323 
\ Crypt {Agent A, Key K} (shrK B)} \ 

324 
\ : set_of_list evs; \ 

325 
\ Says Server A' \ 

326 
\ {Crypt {Agent B', Key K, NA', NB'} (shrK A'), \ 

327 
\ Crypt {Agent A', Key K} (shrK B')} \ 

328 
\ : set_of_list evs; \ 

329 
\ evs : yahalom lost ] \ 

330 
\ ==> A=A' & B=B' & NA=NA' & NB=NB'"; 

331 
by (dtac lemma 1); 

332 
by (REPEAT (etac exE 1)); 

333 
(*Duplicate the assumption*) 

334 
by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1); 

335 
by (fast_tac (!claset addSDs [spec]) 1); 

336 
qed "unique_session_keys"; 

337 

338 

339 
(*If the encrypted message appears then it originated with the Server*) 

340 
goal thy 

341 
"!!evs. [ Crypt {Agent B, Key K, NA, NB} (shrK A) \ 

342 
\ : parts (sees lost Spy evs); \ 

343 
\ A ~: lost; evs : yahalom lost ] \ 

344 
\ ==> Says Server A \ 

345 
\ {Crypt {Agent B, Key K, NA, NB} (shrK A), \ 

346 
\ Crypt {Agent A, Key K} (shrK B)} \ 

347 
\ : set_of_list evs"; 

348 
by (etac rev_mp 1); 

349 
by (parts_induct_tac 1); 

350 
qed "A_trust_YM3"; 

351 

352 

2013  353 
(*Describes the form of K when the Server sends this message.*) 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

354 
goal thy 
1995  355 
"!!evs. [ Says Server A \ 
356 
\ {Crypt {Agent B, K, NA, NB} (shrK A), \ 

357 
\ Crypt {Agent A, K} (shrK B)} : set_of_list evs; \ 

2110  358 
\ evs : yahalom lost ] \ 
2032  359 
\ ==> (EX evt: yahalom lost. K = Key(newK evt))"; 
360 
by (etac rev_mp 1); 

361 
by (etac yahalom.induct 1); 

2013  362 
by (ALLGOALS (fast_tac (!claset addss (!simpset)))); 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

363 
qed "Says_Server_message_form"; 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

364 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

365 

2110  366 
(** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **) 
2013  367 

368 
goal thy 

2051  369 
"!!evs. [ A ~: lost; B ~: lost; \ 
370 
\ evs : yahalom lost; evt : yahalom lost ] \ 

371 
\ ==> Says Server A \ 

372 
\ {Crypt {Agent B, Key K, NA, NB} (shrK A), \ 

373 
\ Crypt {Agent A, Key K} (shrK B)} \ 

2110  374 
\ : set_of_list evs > \ 
375 
\ Says A Spy {NA, NB, Key K} ~: set_of_list evs > \ 

2051  376 
\ Key K ~: analz (sees lost Spy evs)"; 
2032  377 
by (etac yahalom.induct 1); 
2110  378 
by analz_Fake_tac; 
379 
by (REPEAT_FIRST (eresolve_tac [asm_rl, bexE, disjE] ORELSE' hyp_subst_tac)); 

2013  380 
by (ALLGOALS 
381 
(asm_simp_tac 

382 
(!simpset addsimps ([analz_subset_parts RS contra_subsetD, 

2032  383 
analz_insert_Key_newK] @ pushes) 
2013  384 
setloop split_tac [expand_if]))); 
385 
(*YM3*) 

386 
by (fast_tac (!claset addIs [parts_insertI] 

2032  387 
addEs [Says_imp_old_keys RS less_irrefl] 
388 
addss (!simpset)) 2); 

2110  389 
(*Reveal case 2, OR4, Fake*) 
390 
by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' spy_analz_tac)); 

391 
(*Reveal case 1*) (** LEVEL 6 **) 

392 
by (case_tac "Aa : lost" 1); 

393 
(*But this contradicts Key K ~: analz (sees lost Spy evsa) *) 

394 
by (dtac (Says_imp_sees_Spy RS analz.Inj) 1); 

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

396 
(*So now we have Aa ~: lost *) 

397 
bd (Says_imp_sees_Spy RS parts.Inj) 1; 

398 
by (fast_tac (!claset delrules [disjE] 

399 
addSEs [MPair_parts] 

400 
addDs [A_trust_YM3, unique_session_keys] 

401 
addss (!simpset)) 1); 

402 
val lemma = result() RS mp RS mp RSN(2,rev_notE); 

2013  403 

404 

405 
(*Final version: Server's message in the most abstract form*) 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

406 
goal thy 
2110  407 
"!!evs. [ Says Server A \ 
1995  408 
\ {Crypt {Agent B, K, NA, NB} (shrK A), \ 
409 
\ Crypt {Agent A, K} (shrK B)} : set_of_list evs; \ 

2110  410 
\ Says A Spy {NA, NB, K} ~: set_of_list evs; \ 
411 
\ A ~: lost; B ~: lost; evs : yahalom lost ] ==> \ 

2032  412 
\ K ~: analz (sees lost Spy evs)"; 
2013  413 
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); 
414 
by (fast_tac (!claset addSEs [lemma]) 1); 

2032  415 
qed "Spy_not_see_encrypted_key"; 
2001  416 

417 

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

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

419 
"!!evs. [ C ~: {A,B,Server}; \ 
ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

420 
\ Says Server A \ 
ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

421 
\ {Crypt {Agent B, K, NA, NB} (shrK A), \ 
ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

422 
\ Crypt {Agent A, K} (shrK B)} : set_of_list evs; \ 
2110  423 
\ Says A Spy {NA, NB, K} ~: set_of_list evs; \ 
2045
ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

424 
\ A ~: lost; B ~: lost; evs : yahalom lost ] ==> \ 
ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

425 
\ K ~: analz (sees lost C evs)"; 
ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

426 
by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1); 
ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

427 
by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1); 
ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

428 
by (FIRSTGOAL (rtac Spy_not_see_encrypted_key)); 
ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

429 
by (REPEAT_FIRST (fast_tac (!claset addIs [yahalom_mono RS subsetD]))); 
ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

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

431 

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

432 

2110  433 
(*** Security Guarantee for B upon receiving YM4 ***) 
2013  434 

2110  435 
(*B knows, by the first part of A's message, that the Server distributed 
436 
the key for A and B. But this part says nothing about nonces.*) 

2001  437 
goal thy 
2032  438 
"!!evs. [ Crypt {Agent A, Key K} (shrK B) : parts (sees lost Spy evs); \ 
2051  439 
\ B ~: lost; evs : yahalom lost ] \ 
2001  440 
\ ==> EX NA NB. Says Server A \ 
2013  441 
\ {Crypt {Agent B, Key K, \ 
442 
\ Nonce NA, Nonce NB} (shrK A), \ 

443 
\ Crypt {Agent A, Key K} (shrK B)} \ 

444 
\ : set_of_list evs"; 

2032  445 
by (etac rev_mp 1); 
2110  446 
by (parts_induct_tac 1); 
447 
(*YM3*) 

448 
by (Fast_tac 1); 

449 
qed "B_trusts_YM4_shrK"; 

450 

451 
(*B knows, by the second part of A's message, that the Server distributed 

452 
the key quoting nonce NB. This part says nothing about agent names.*) 

453 
goal thy 

454 
"!!evs. evs : yahalom lost \ 

455 
\ ==> Key K ~: analz (sees lost Spy evs) > \ 

456 
\ Crypt (Nonce NB) K : parts (sees lost Spy evs) > \ 

457 
\ (EX A B NA. Says Server A \ 

458 
\ {Crypt {Agent B, Key K, \ 

459 
\ Nonce NA, Nonce NB} (shrK A), \ 

460 
\ Crypt {Agent A, Key K} (shrK B)} \ 

461 
\ : set_of_list evs)"; 

2032  462 
by (etac yahalom.induct 1); 
2110  463 
by parts_Fake_tac; 
2001  464 
by (fast_tac (!claset addss (!simpset)) 1); 
2110  465 
by (TRYALL (rtac impI)); 
466 
by (REPEAT_FIRST 

467 
(dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD))); 

468 
by (ALLGOALS Asm_simp_tac); 

469 
(*Fake, YM3, YM4*) 

470 
by (fast_tac (!claset addSDs [Crypt_Fake_parts_insert] 

471 
addDs [impOfSubs analz_subset_parts]) 1); 

472 
by (Fast_tac 1); 

473 
(*YM4*) 

474 
by (Step_tac 1); 

475 
by (case_tac "A : lost" 1); 

476 
(*But this contradicts Key K ~: analz (sees lost Spy evsa) *) 

477 
by (dtac (Says_imp_sees_Spy RS analz.Inj) 1); 

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

479 
by (fast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS 

480 
A_trust_YM3]) 1); 

481 
val B_trusts_YM4_newK = result() RS mp RSN (2, rev_mp); 

2001  482 

2110  483 
(*What can B deduce from receipt of YM4? Note how the two components of 
484 
the message contribute to a single conclusion about the Server's message. 

485 
It's annoying that the "Says A Spy" assumption must quantify over 

486 
ALL POSSIBLE nonces instead of our particular NB. Perhaps a different 

487 
proof of B_trusts_YM4_newK could eliminate this problem.*) 

2001  488 
goal thy 
489 
"!!evs. [ Says A' B {Crypt {Agent A, Key K} (shrK B), \ 

490 
\ Crypt (Nonce NB) K} : set_of_list evs; \ 

2110  491 
\ ALL N N'. Says A Spy {N,N', Key K} ~: set_of_list evs; \ 
492 
\ A ~: lost; B ~: lost; evs : yahalom lost ] \ 

493 
\ ==> EX NA. Says Server A \ 

2001  494 
\ {Crypt {Agent B, Key K, \ 
495 
\ Nonce NA, Nonce NB} (shrK A), \ 

496 
\ Crypt {Agent A, Key K} (shrK B)} \ 

497 
\ : set_of_list evs"; 

2110  498 
be (Says_imp_sees_Spy RS parts.Inj RS MPair_parts) 1; 
499 
bd B_trusts_YM4_shrK 1; 

500 
bd B_trusts_YM4_newK 3; 

501 
by (REPEAT_FIRST (eresolve_tac [asm_rl, exE])); 

502 
by (fast_tac (!claset addDs [unique_session_keys]) 2); 

503 
by (fast_tac (!claset addDs [Spy_not_see_encrypted_key]) 1); 

504 
qed "B_trust_YM4"; 