author  paulson 
Fri, 17 Jan 1997 12:49:31 +0100  
changeset 2516  4d68fbe6378b 
parent 2485  c4368c967c56 
child 2533  2d5604a51562 
permissions  rwrr 
2449  1 
(* Title: HOL/Auth/Recur 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1996 University of Cambridge 

5 

6 
Inductive relation "recur" for the Recursive Authentication protocol. 

7 
*) 

8 

9 
open Recur; 

10 

11 
proof_timing:=true; 

12 
HOL_quantifiers := false; 

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

13 
Pretty.setdepth 30; 
2449  14 

15 

16 
(** Possibility properties: traces that reach the end 

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

17 
ONE theorem would be more elegant and faster! 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

18 
By induction on a list of agents (no repetitions) 
2449  19 
**) 
20 

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

21 

2449  22 
(*Simplest case: Alice goes directly to the server*) 
2481  23 
goal thy 
2449  24 
"!!A. A ~= Server \ 
25 
\ ==> EX K NA. EX evs: recur lost. \ 

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

26 
\ Says Server A {Crypt (shrK A) {Key K, Agent Server, Nonce NA}, \ 
2449  27 
\ Agent Server} \ 
28 
\ : set_of_list evs"; 

29 
by (REPEAT (resolve_tac [exI,bexI] 1)); 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

30 
by (rtac (recur.Nil RS recur.RA1 RS 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

31 
(respond.One RSN (4,recur.RA3))) 2); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

32 
by possibility_tac; 
2449  33 
result(); 
34 

35 

36 
(*Case two: Alice, Bob and the server*) 

2481  37 
goal thy 
2449  38 
"!!A B. [ A ~= B; A ~= Server; B ~= Server ] \ 
39 
\ ==> EX K. EX NA. EX evs: recur lost. \ 

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

40 
\ Says B A {Crypt (shrK A) {Key K, Agent B, Nonce NA}, \ 
2449  41 
\ Agent Server} \ 
42 
\ : set_of_list evs"; 

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

43 
by (cut_facts_tac [Nonce_supply2, Key_supply2] 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

44 
by (REPEAT (eresolve_tac [exE, conjE] 1)); 
2449  45 
by (REPEAT (resolve_tac [exI,bexI] 1)); 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

46 
by (rtac (recur.Nil RS recur.RA1 RS recur.RA2 RS 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

47 
(respond.One RS respond.Cons RSN (4,recur.RA3)) RS 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

48 
recur.RA4) 2); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

49 
by basic_possibility_tac; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

50 
by (DEPTH_SOLVE (eresolve_tac [asm_rl, less_not_refl2, 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

51 
less_not_refl2 RS not_sym] 1)); 
2449  52 
result(); 
53 

54 

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

55 
(*Case three: Alice, Bob, Charlie and the server 
2481  56 
goal thy 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

57 
"!!A B. [ A ~= B; B ~= C; A ~= Server; B ~= Server; C ~= Server ] \ 
2449  58 
\ ==> EX K. EX NA. EX evs: recur lost. \ 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

59 
\ Says B A {Crypt (shrK A) {Key K, Agent B, Nonce NA}, \ 
2449  60 
\ Agent Server} \ 
61 
\ : set_of_list evs"; 

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

62 
by (cut_facts_tac [Nonce_supply3, Key_supply3] 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

63 
by (REPEAT (eresolve_tac [exE, conjE] 1)); 
2449  64 
by (REPEAT (resolve_tac [exI,bexI] 1)); 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

65 
by (rtac (recur.Nil RS recur.RA1 RS recur.RA2 RS recur.RA2 RS 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

66 
(respond.One RS respond.Cons RS respond.Cons RSN 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

67 
(4,recur.RA3)) RS recur.RA4 RS recur.RA4) 2); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

68 
(*SLOW: 70 seconds*) 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

69 
by basic_possibility_tac; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

70 
by (DEPTH_SOLVE (swap_res_tac [refl, conjI, disjCI] 1 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

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

72 
eresolve_tac [asm_rl, less_not_refl2, 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

73 
less_not_refl2 RS not_sym] 1)); 
2449  74 
result(); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

75 
****************) 
2449  76 

77 
(**** Inductive proofs about recur ****) 

78 

79 
(*Monotonicity*) 

80 
goal thy "!!evs. lost' <= lost ==> recur lost' <= recur lost"; 

81 
by (rtac subsetI 1); 

82 
by (etac recur.induct 1); 

83 
by (REPEAT_FIRST 

84 
(best_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono) 

85 
:: recur.intrs)))); 

86 
qed "recur_mono"; 

87 

88 
(*Nobody sends themselves messages*) 

89 
goal thy "!!evs. evs : recur lost ==> ALL A X. Says A A X ~: set_of_list evs"; 

90 
by (etac recur.induct 1); 

91 
by (Auto_tac()); 

92 
qed_spec_mp "not_Says_to_self"; 

93 
Addsimps [not_Says_to_self]; 

94 
AddSEs [not_Says_to_self RSN (2, rev_notE)]; 

95 

96 

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

97 

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

98 
goal thy "!!evs. (PA,RB,KAB) : respond evs ==> Key KAB : parts{RB}"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

99 
by (etac respond.induct 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

100 
by (ALLGOALS Simp_tac); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

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

102 

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

103 
goal thy "!!evs. (PA,RB,KAB) : respond evs ==> Key KAB ~: used evs"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

104 
by (etac respond.induct 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

105 
by (REPEAT (assume_tac 1)); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

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

107 

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

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

109 
"!!evs. [ Key K : parts {RB}; (PB,RB,K') : respond evs ] \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

110 
\ ==> Key K ~: used evs"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

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

112 
by (etac respond.induct 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

113 
by (auto_tac(!claset addDs [Key_not_used, respond_imp_not_used], 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

114 
!simpset)); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

115 
qed_spec_mp "Key_in_parts_respond"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

116 

2449  117 
(*Simple inductive reasoning about responses*) 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

118 
goal thy "!!evs. (PA,RB,KAB) : respond evs ==> RB : responses evs"; 
2449  119 
by (etac respond.induct 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

120 
by (REPEAT (ares_tac (respond_imp_not_used::responses.intrs) 1)); 
2449  121 
qed "respond_imp_responses"; 
122 

123 

124 
(** For reasoning about the encrypted portion of messages **) 

125 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

126 
val RA2_analz_sees_Spy = Says_imp_sees_Spy RS analz.Inj > standard; 
2449  127 

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

128 
goal thy "!!evs. Says C' B {X, X', RA} : set_of_list evs \ 
2449  129 
\ ==> RA : analz (sees lost Spy evs)"; 
130 
by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1); 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

131 
qed "RA4_analz_sees_Spy"; 
2449  132 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

133 
(*RA2_analz... and RA4_analz... let us treat those cases using the same 
2449  134 
argument as for the Fake case. This is possible for most, but not all, 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

135 
proofs: Fake does not invent new nonces (as in RA2), and of course Fake 
2449  136 
messages originate from the Spy. *) 
137 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

138 
bind_thm ("RA2_parts_sees_Spy", 
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

139 
RA2_analz_sees_Spy RS (impOfSubs analz_subset_parts)); 
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

140 
bind_thm ("RA4_parts_sees_Spy", 
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

141 
RA4_analz_sees_Spy RS (impOfSubs analz_subset_parts)); 
2449  142 

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

144 
harder to complete, since simplification does less for us.*) 

145 
val parts_Fake_tac = 

146 
let val tac = forw_inst_tac [("lost","lost")] 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

147 
in tac RA2_parts_sees_Spy 4 THEN 
2485
c4368c967c56
Simplification of some proofs, especially by eliminating
paulson
parents:
2481
diff
changeset

148 
etac subst 4 (*RA2: DELETE needless definition of PA!*) THEN 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

149 
forward_tac [respond_imp_responses] 5 THEN 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

150 
tac RA4_parts_sees_Spy 6 
2449  151 
end; 
152 

153 
(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *) 

154 
fun parts_induct_tac i = SELECT_GOAL 

155 
(DETERM (etac recur.induct 1 THEN parts_Fake_tac THEN 

156 
(*Fake message*) 

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

158 
impOfSubs Fake_parts_insert] 

159 
addss (!simpset)) 2)) THEN 

160 
(*Base case*) 

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

162 
ALLGOALS Asm_simp_tac) i; 

163 

164 
(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY 

165 
sends messages containing X! **) 

166 

167 

168 
(** Spy never sees another agent's longterm key (unless initially lost) **) 

169 

170 
goal thy 

171 
"!!evs. evs : recur lost \ 

172 
\ ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)"; 

173 
by (parts_induct_tac 1); 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

174 
(*RA2*) 
2449  175 
by (best_tac (!claset addSEs partsEs addSDs [parts_cut] 
176 
addss (!simpset)) 1); 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

177 
(*RA3*) 
2449  178 
by (fast_tac (!claset addDs [Key_in_parts_respond] 
179 
addss (!simpset addsimps [parts_insert_sees])) 1); 

180 
qed "Spy_see_shrK"; 

181 
Addsimps [Spy_see_shrK]; 

182 

183 
goal thy 

184 
"!!evs. evs : recur lost \ 

185 
\ ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)"; 

186 
by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset)); 

187 
qed "Spy_analz_shrK"; 

188 
Addsimps [Spy_analz_shrK]; 

189 

190 
goal thy "!!A. [ Key (shrK A) : parts (sees lost Spy evs); \ 

191 
\ evs : recur lost ] ==> A:lost"; 

192 
by (fast_tac (!claset addDs [Spy_see_shrK]) 1); 

193 
qed "Spy_see_shrK_D"; 

194 

195 
bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D); 

196 
AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D]; 

197 

198 

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

199 

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

200 
(** Nobody can have used nonexistent keys! **) 
2449  201 

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

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

203 
"!!evs. [ K : keysFor (parts {RB}); (PB,RB,K') : respond evs ] \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

204 
\ ==> K : range shrK"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

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

206 
by (etac (respond_imp_responses RS responses.induct) 1); 
2449  207 
by (Auto_tac()); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

208 
qed_spec_mp "Key_in_keysFor_parts"; 
2449  209 

210 

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

211 
goal thy "!!evs. evs : recur lost ==> \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

212 
\ Key K ~: used evs > K ~: keysFor (parts (sees lost Spy evs))"; 
2449  213 
by (parts_induct_tac 1); 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

214 
(*RA3*) 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

215 
by (best_tac (!claset addDs [Key_in_keysFor_parts] 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

216 
addss (!simpset addsimps [parts_insert_sees])) 2); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

217 
(*Fake*) 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

218 
by (best_tac 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

219 
(!claset addIs [impOfSubs analz_subset_parts] 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

220 
addDs [impOfSubs (analz_subset_parts RS keysFor_mono), 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

221 
impOfSubs (parts_insert_subset_Un RS keysFor_mono)] 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

222 
addss (!simpset)) 1); 
2449  223 
qed_spec_mp "new_keys_not_used"; 
224 

225 

226 
bind_thm ("new_keys_not_analzd", 

227 
[analz_subset_parts RS keysFor_mono, 

228 
new_keys_not_used] MRS contra_subsetD); 

229 

230 
Addsimps [new_keys_not_used, new_keys_not_analzd]; 

231 

232 

233 

234 
(*** Proofs involving analz ***) 

235 

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

237 
val analz_Fake_tac = 

2485
c4368c967c56
Simplification of some proofs, especially by eliminating
paulson
parents:
2481
diff
changeset

238 
etac subst 4 (*RA2: DELETE needless definition of PA!*) THEN 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

239 
dres_inst_tac [("lost","lost")] RA2_analz_sees_Spy 4 THEN 
2449  240 
forward_tac [respond_imp_responses] 5 THEN 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

241 
dres_inst_tac [("lost","lost")] RA4_analz_sees_Spy 6; 
2449  242 

243 

244 
(** Session keys are not used to encrypt other session keys **) 

245 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

246 
(*Version for "responses" relation. Handles case RA3 in the theorem below. 
2449  247 
Note that it holds for *any* set H (not just "sees lost Spy evs") 
248 
satisfying the inductive hypothesis.*) 

249 
goal thy 

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

250 
"!!evs. [ RB : responses evs; \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

251 
\ ALL K KK. KK <= Compl (range shrK) > \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

252 
\ (Key K : analz (Key``KK Un H)) = \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

253 
\ (K : KK  Key K : analz H) ] \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

254 
\ ==> ALL K KK. KK <= Compl (range shrK) > \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

255 
\ (Key K : analz (insert RB (Key``KK Un H))) = \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

256 
\ (K : KK  Key K : analz (insert RB H))"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

257 
by (etac responses.induct 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

258 
by (ALLGOALS (asm_simp_tac analz_image_freshK_ss)); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

259 
qed "resp_analz_image_freshK_lemma"; 
2449  260 

261 
(*Version for the protocol. Proof is almost trivial, thanks to the lemma.*) 

262 
goal thy 

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

263 
"!!evs. evs : recur lost ==> \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

264 
\ ALL K KK. KK <= Compl (range shrK) > \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

265 
\ (Key K : analz (Key``KK Un (sees lost Spy evs))) = \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

266 
\ (K : KK  Key K : analz (sees lost Spy evs))"; 
2449  267 
by (etac recur.induct 1); 
268 
by analz_Fake_tac; 

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

269 
by (REPEAT_FIRST (resolve_tac [allI, impI])); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

270 
by (REPEAT_FIRST (rtac analz_image_freshK_lemma )); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

271 
by (ALLGOALS 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

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

273 
(analz_image_freshK_ss addsimps [resp_analz_image_freshK_lemma]))); 
2449  274 
(*Base*) 
275 
by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1); 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

276 
(*RA4, RA2, Fake*) 
2449  277 
by (REPEAT (spy_analz_tac 1)); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

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

279 
qed_spec_mp "analz_image_freshK"; 
2449  280 

281 

282 
(*Instance of the lemma with H replaced by (sees lost Spy evs): 

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

283 
[ RB : responses evs; evs : recur lost; ] 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

284 
==> KK <= Compl (range shrK) > 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

285 
Key K : analz (insert RB (Key``KK Un sees lost Spy evs)) = 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

286 
(K : KK  Key K : analz (insert RB (sees lost Spy evs))) 
2449  287 
*) 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

288 
bind_thm ("resp_analz_image_freshK", 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

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

290 
(2, resp_analz_image_freshK_lemma) RS spec RS spec); 
2449  291 

292 
goal thy 

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

293 
"!!evs. [ evs : recur lost; KAB ~: range shrK ] ==> \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

294 
\ Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

295 
\ (K = KAB  Key K : analz (sees lost Spy evs))"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

296 
by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

297 
qed "analz_insert_freshK"; 
2449  298 

299 

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

300 
(*Everything that's hashed is already in past traffic. *) 
2485
c4368c967c56
Simplification of some proofs, especially by eliminating
paulson
parents:
2481
diff
changeset

301 
goal thy "!!i. [ evs : recur lost; A ~: lost ] ==> \ 
c4368c967c56
Simplification of some proofs, especially by eliminating
paulson
parents:
2481
diff
changeset

302 
\ Hash {Key(shrK A), X} : parts (sees lost Spy evs) > \ 
c4368c967c56
Simplification of some proofs, especially by eliminating
paulson
parents:
2481
diff
changeset

303 
\ X : parts (sees lost Spy evs)"; 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

304 
by (etac recur.induct 1); 
2449  305 
by parts_Fake_tac; 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

306 
(*RA3 requires a further induction*) 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

307 
by (etac responses.induct 5); 
2449  308 
by (ALLGOALS Asm_simp_tac); 
309 
(*Fake*) 

2485
c4368c967c56
Simplification of some proofs, especially by eliminating
paulson
parents:
2481
diff
changeset

310 
by (best_tac (!claset addDs [impOfSubs analz_subset_parts, 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

311 
impOfSubs Fake_parts_insert] 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

312 
addss (!simpset addsimps [parts_insert_sees])) 2); 
2485
c4368c967c56
Simplification of some proofs, especially by eliminating
paulson
parents:
2481
diff
changeset

313 
(*Two others*) 
c4368c967c56
Simplification of some proofs, especially by eliminating
paulson
parents:
2481
diff
changeset

314 
by (REPEAT (fast_tac (!claset addss (!simpset)) 1)); 
c4368c967c56
Simplification of some proofs, especially by eliminating
paulson
parents:
2481
diff
changeset

315 
bind_thm ("Hash_imp_body", result() RSN (2, rev_mp)); 
2449  316 

317 

318 
(** The Nonce NA uniquely identifies A's message. 

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

319 
This theorem applies to steps RA1 and RA2! 
2455
9c4444bfd44e
Simplification and generalization of the guarantees.
paulson
parents:
2451
diff
changeset

320 

9c4444bfd44e
Simplification and generalization of the guarantees.
paulson
parents:
2451
diff
changeset

321 
Unicity is not used in other proofs but is desirable in its own right. 
2449  322 
**) 
323 

324 
goal thy 

325 
"!!evs. [ evs : recur lost; A ~: lost ] \ 

326 
\ ==> EX B' P'. ALL B P. \ 

327 
\ Hash {Key(shrK A), Agent A, Agent B, Nonce NA, P} \ 

328 
\ : parts (sees lost Spy evs) > B=B' & P=P'"; 

2485
c4368c967c56
Simplification of some proofs, especially by eliminating
paulson
parents:
2481
diff
changeset

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

330 
by (etac responses.induct 3); 
2485
c4368c967c56
Simplification of some proofs, especially by eliminating
paulson
parents:
2481
diff
changeset

331 
by (ALLGOALS (simp_tac (!simpset addsimps [all_conj_distrib]))); 
2449  332 
by (step_tac (!claset addSEs partsEs) 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

333 
(*RA1,2: creation of new Nonce. Move assertion into global context*) 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

334 
by (ALLGOALS (expand_case_tac "NA = ?y")); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

335 
by (REPEAT_FIRST (ares_tac [exI])); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

336 
by (REPEAT (best_tac (!claset addSDs [Hash_imp_body] 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

337 
addSEs sees_Spy_partsEs) 1)); 
2449  338 
val lemma = result(); 
339 

2481  340 
goalw thy [HPair_def] 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

341 
"!!evs.[ Hash[Key(shrK A)] {Agent A, Agent B, Nonce NA, P} \ 
2485
c4368c967c56
Simplification of some proofs, especially by eliminating
paulson
parents:
2481
diff
changeset

342 
\ : parts (sees lost Spy evs); \ 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

343 
\ Hash[Key(shrK A)] {Agent A, Agent B', Nonce NA, P'} \ 
2485
c4368c967c56
Simplification of some proofs, especially by eliminating
paulson
parents:
2481
diff
changeset

344 
\ : parts (sees lost Spy evs); \ 
c4368c967c56
Simplification of some proofs, especially by eliminating
paulson
parents:
2481
diff
changeset

345 
\ evs : recur lost; A ~: lost ] \ 
2449  346 
\ ==> B=B' & P=P'"; 
2481  347 
by (REPEAT (eresolve_tac partsEs 1)); 
2449  348 
by (prove_unique_tac lemma 1); 
349 
qed "unique_NA"; 

350 

351 

352 
(*** Lemmas concerning the Server's response 

353 
(relations "respond" and "responses") 

354 
***) 

355 

356 
goal thy 

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

357 
"!!evs. [ RB : responses evs; evs : recur lost ] \ 
2449  358 
\ ==> (Key (shrK B) : analz (insert RB (sees lost Spy evs))) = (B:lost)"; 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

359 
by (etac responses.induct 1); 
2449  360 
by (ALLGOALS 
361 
(asm_simp_tac 

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

362 
(analz_image_freshK_ss addsimps [Spy_analz_shrK, 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

363 
resp_analz_image_freshK]))); 
2449  364 
qed "shrK_in_analz_respond"; 
365 
Addsimps [shrK_in_analz_respond]; 

366 

367 

368 
goal thy 

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

369 
"!!evs. [ RB : responses evs; \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

370 
\ ALL K KK. KK <= Compl (range shrK) > \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

371 
\ (Key K : analz (Key``KK Un H)) = \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

372 
\ (K : KK  Key K : analz H) ] \ 
2449  373 
\ ==> (Key K : analz (insert RB H)) > \ 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

374 
\ (Key K : parts{RB}  Key K : analz H)"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

375 
by (etac responses.induct 1); 
2449  376 
by (ALLGOALS 
377 
(asm_simp_tac 

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

378 
(analz_image_freshK_ss addsimps [resp_analz_image_freshK_lemma]))); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

379 
(*Simplification using two distinct treatments of "image"*) 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

380 
by (simp_tac (!simpset addsimps [parts_insert2]) 1); 
2449  381 
by (fast_tac (!claset delrules [allE]) 1); 
382 
qed "resp_analz_insert_lemma"; 

383 

384 
bind_thm ("resp_analz_insert", 

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

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

386 
(2, resp_analz_insert_lemma) RSN(2, rev_mp)); 
2449  387 

388 

389 
(*The Server does not send such messages. This theorem lets us avoid 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

390 
assuming B~=Server in RA4.*) 
2449  391 
goal thy 
392 
"!!evs. evs : recur lost \ 

393 
\ ==> ALL C X Y P. Says Server C {X, Agent Server, Agent C, Y, P} \ 

394 
\ ~: set_of_list evs"; 

395 
by (etac recur.induct 1); 

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

396 
by (etac (respond.induct) 5); 
2449  397 
by (Auto_tac()); 
398 
qed_spec_mp "Says_Server_not"; 

399 
AddSEs [Says_Server_not RSN (2,rev_notE)]; 

400 

401 

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

402 
(*The last key returned by respond indeed appears in a certificate*) 
2449  403 
goal thy 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

404 
"!!K. (Hash[Key(shrK A)] {Agent A, B, NA, P}, RA, K) : respond evs \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

405 
\ ==> Crypt (shrK A) {Key K, B, NA} : parts {RA}"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

406 
by (etac respond.elim 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

407 
by (ALLGOALS Asm_full_simp_tac); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

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

409 

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

410 

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

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

412 
"!!K'. (PB,RB,KXY) : respond evs \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

413 
\ ==> EX A' B'. ALL A B N. \ 
2449  414 
\ Crypt (shrK A) {Key K, Agent B, N} : parts {RB} \ 
415 
\ > (A'=A & B'=B)  (A'=B & B'=A)"; 

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

416 
by (etac respond.induct 1); 
2449  417 
by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [all_conj_distrib]))); 
418 
(*Base case*) 

419 
by (Fast_tac 1); 

420 
by (Step_tac 1); 

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

421 
(*Case analysis on K=KBC*) 
2449  422 
by (expand_case_tac "K = ?y" 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

423 
by (dtac respond_Key_in_parts 1); 
2449  424 
by (best_tac (!claset addSIs [exI] 
425 
addSEs partsEs 

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

426 
addDs [Key_in_parts_respond]) 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

427 
(*Case analysis on K=KAB*) 
2449  428 
by (expand_case_tac "K = ?y" 1); 
429 
by (REPEAT (ares_tac [exI] 2)); 

430 
by (ex_strip_tac 1); 

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

431 
by (dtac respond_certificate 1); 
2449  432 
by (Fast_tac 1); 
433 
val lemma = result(); 

434 

435 
goal thy 

436 
"!!RB. [ Crypt (shrK A) {Key K, Agent B, N} : parts {RB}; \ 

437 
\ Crypt (shrK A') {Key K, Agent B', N'} : parts {RB}; \ 

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

438 
\ (PB,RB,KXY) : respond evs ] \ 
2449  439 
\ ==> (A'=A & B'=B)  (A'=B & B'=A)"; 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

440 
by (prove_unique_tac lemma 1); (*50 seconds??, due to the disjunctions*) 
2449  441 
qed "unique_session_keys"; 
442 

443 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

444 
(** Crucial secrecy property: Spy does not see the keys sent in msg RA3 
2449  445 
Does not in itself guarantee security: an attack could violate 
446 
the premises, e.g. by having A=Spy **) 

447 

448 
goal thy 

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

449 
"!!evs. [ (PB,RB,KAB) : respond evs; evs : recur lost ] \ 
2449  450 
\ ==> ALL A A' N. A ~: lost & A' ~: lost > \ 
451 
\ Crypt (shrK A) {Key K, Agent A', N} : parts{RB} > \ 

452 
\ Key K ~: analz (insert RB (sees lost Spy evs))"; 

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

453 
by (etac respond.induct 1); 
2449  454 
by (forward_tac [respond_imp_responses] 2); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

455 
by (forward_tac [respond_imp_not_used] 2); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

456 
by (ALLGOALS (*43 seconds*) 
2449  457 
(asm_simp_tac 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

458 
(analz_image_freshK_ss addsimps 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

459 
[analz_image_freshK, not_parts_not_analz, 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

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

461 
read_instantiate [("H", "?ff``?xx")] parts_insert, 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

462 
resp_analz_image_freshK, analz_insert_freshK]))); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

463 
by (ALLGOALS Simp_tac); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

464 
by (fast_tac (!claset addIs [impOfSubs analz_subset_parts]) 1); 
2449  465 
by (step_tac (!claset addSEs [MPair_parts]) 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

466 
(** LEVEL 7 **) 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

467 
by (fast_tac (!claset addSDs [resp_analz_insert, Key_in_parts_respond] 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

468 
addDs [impOfSubs analz_subset_parts]) 4); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

469 
by (fast_tac (!claset addSDs [respond_certificate]) 3); 
2449  470 
by (best_tac (!claset addSEs partsEs 
471 
addDs [Key_in_parts_respond] 

472 
addss (!simpset)) 2); 

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

473 
by (dtac unique_session_keys 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

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

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

476 
by (Fast_tac 1); 
2449  477 
qed_spec_mp "respond_Spy_not_see_encrypted_key"; 
478 

479 

480 
goal thy 

2455
9c4444bfd44e
Simplification and generalization of the guarantees.
paulson
parents:
2451
diff
changeset

481 
"!!evs. [ A ~: lost; A' ~: lost; evs : recur lost ] \ 
9c4444bfd44e
Simplification and generalization of the guarantees.
paulson
parents:
2451
diff
changeset

482 
\ ==> Says Server B RB : set_of_list evs > \ 
2449  483 
\ Crypt (shrK A) {Key K, Agent A', N} : parts{RB} > \ 
484 
\ Key K ~: analz (sees lost Spy evs)"; 

485 
by (etac recur.induct 1); 

486 
by analz_Fake_tac; 

487 
by (ALLGOALS 

488 
(asm_simp_tac 

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

489 
(!simpset addsimps [not_parts_not_analz, analz_insert_freshK] 
2449  490 
setloop split_tac [expand_if]))); 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

491 
(*RA4*) 
2449  492 
by (spy_analz_tac 4); 
493 
(*Fake*) 

494 
by (spy_analz_tac 1); 

495 
by (step_tac (!claset delrules [impCE]) 1); 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

496 
(*RA2*) 
2449  497 
by (spy_analz_tac 1); 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

498 
(*RA3, case 2: K is an old key*) 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

499 
by (best_tac (!claset addSDs [resp_analz_insert] 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

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

501 
addDs [Key_in_parts_respond, 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

502 
Says_imp_sees_Spy RS parts.Inj RSN (2, parts_cut)] 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

503 
addss (!simpset)) 2); 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

504 
(*RA3, case 1: use lemma previously proved by induction*) 
2449  505 
by (fast_tac (!claset addSEs [respond_Spy_not_see_encrypted_key RSN 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

506 
(2,rev_notE)]) 1); 
2449  507 
bind_thm ("Spy_not_see_encrypted_key", result() RS mp RSN (2, rev_mp)); 
508 

509 

510 
goal thy 

2455
9c4444bfd44e
Simplification and generalization of the guarantees.
paulson
parents:
2451
diff
changeset

511 
"!!evs. [ Says Server B RB : set_of_list evs; \ 
2449  512 
\ Crypt (shrK A) {Key K, Agent A', N} : parts{RB}; \ 
2455
9c4444bfd44e
Simplification and generalization of the guarantees.
paulson
parents:
2451
diff
changeset

513 
\ C ~: {A,A',Server}; \ 
9c4444bfd44e
Simplification and generalization of the guarantees.
paulson
parents:
2451
diff
changeset

514 
\ A ~: lost; A' ~: lost; evs : recur lost ] \ 
2449  515 
\ ==> Key K ~: analz (sees lost C evs)"; 
516 
by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1); 

517 
by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1); 

518 
by (FIRSTGOAL (rtac Spy_not_see_encrypted_key)); 

519 
by (REPEAT_FIRST (fast_tac (!claset addIs [recur_mono RS subsetD]))); 

520 
qed "Agent_not_see_encrypted_key"; 

521 

522 

523 
(**** Authenticity properties for Agents ****) 

524 

2481  525 
(*The response never contains Hashes*) 
526 
goal thy 

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

527 
"!!evs. (PB,RB,K) : respond evs \ 
2481  528 
\ ==> Hash {Key (shrK B), M} : parts (insert RB H) > \ 
529 
\ Hash {Key (shrK B), M} : parts H"; 

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

530 
by (etac (respond_imp_responses RS responses.induct) 1); 
2481  531 
by (Auto_tac()); 
532 
bind_thm ("Hash_in_parts_respond", result() RSN (2, rev_mp)); 

533 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

534 
(*Only RA1 or RA2 can have caused such a part of a message to appear.*) 
2481  535 
goalw thy [HPair_def] 
2449  536 
"!!evs. [ Hash {Key(shrK A), Agent A, Agent B, NA, P} \ 
537 
\ : parts (sees lost Spy evs); \ 

538 
\ A ~: lost; evs : recur lost ] \ 

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

539 
\ ==> Says A B (Hash[Key(shrK A)] {Agent A, Agent B, NA, P}) \ 
2449  540 
\ : set_of_list evs"; 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2485
diff
changeset

541 
by (etac rev_mp 1); 
2449  542 
by (parts_induct_tac 1); 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

543 
(*RA3*) 
2485
c4368c967c56
Simplification of some proofs, especially by eliminating
paulson
parents:
2481
diff
changeset

544 
by (fast_tac (!claset addSDs [Hash_in_parts_respond]) 1); 
2449  545 
qed_spec_mp "Hash_auth_sender"; 
546 

547 

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

548 
(** These two results subsume (for all agents) the guarantees proved 
2449  549 
separately for A and B in the OtwayRees protocol. 
550 
**) 

551 

552 

2455
9c4444bfd44e
Simplification and generalization of the guarantees.
paulson
parents:
2451
diff
changeset

553 
(*Encrypted messages can only originate with the Server.*) 
2449  554 
goal thy 
2455
9c4444bfd44e
Simplification and generalization of the guarantees.
paulson
parents:
2451
diff
changeset

555 
"!!evs. [ A ~: lost; A ~= Spy; evs : recur lost ] \ 
9c4444bfd44e
Simplification and generalization of the guarantees.
paulson
parents:
2451
diff
changeset

556 
\ ==> Crypt (shrK A) Y : parts (sees lost Spy evs) \ 
9c4444bfd44e
Simplification and generalization of the guarantees.
paulson
parents:
2451
diff
changeset

557 
\ > (EX C RC. Says Server C RC : set_of_list evs & \ 
9c4444bfd44e
Simplification and generalization of the guarantees.
paulson
parents:
2451
diff
changeset

558 
\ Crypt (shrK A) Y : parts {RC})"; 
2449  559 
by (parts_induct_tac 1); 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

560 
(*RA4*) 
2455
9c4444bfd44e
Simplification and generalization of the guarantees.
paulson
parents:
2451
diff
changeset

561 
by (Fast_tac 4); 
9c4444bfd44e
Simplification and generalization of the guarantees.
paulson
parents:
2451
diff
changeset

562 
(*RA3*) 
9c4444bfd44e
Simplification and generalization of the guarantees.
paulson
parents:
2451
diff
changeset

563 
by (full_simp_tac (!simpset addsimps [parts_insert_sees]) 3 
9c4444bfd44e
Simplification and generalization of the guarantees.
paulson
parents:
2451
diff
changeset

564 
THEN Fast_tac 3); 
9c4444bfd44e
Simplification and generalization of the guarantees.
paulson
parents:
2451
diff
changeset

565 
(*RA1*) 
9c4444bfd44e
Simplification and generalization of the guarantees.
paulson
parents:
2451
diff
changeset

566 
by (Fast_tac 1); 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

567 
(*RA2: it cannot be a new Nonce, contradiction.*) 
2449  568 
by (deepen_tac (!claset delrules [impCE] 
569 
addSIs [disjI2] 

2455
9c4444bfd44e
Simplification and generalization of the guarantees.
paulson
parents:
2451
diff
changeset

570 
addSEs [MPair_parts] 
2449  571 
addDs [parts_cut, parts.Body] 
572 
addss (!simpset)) 0 1); 

573 
qed_spec_mp "Crypt_imp_Server_msg"; 

574 

575 

2455
9c4444bfd44e
Simplification and generalization of the guarantees.
paulson
parents:
2451
diff
changeset

576 
(*Corollary: if A receives B's message then the key came from the Server*) 
2449  577 
goal thy 
578 
"!!evs. [ Says B' A RA : set_of_list evs; \ 

2455
9c4444bfd44e
Simplification and generalization of the guarantees.
paulson
parents:
2451
diff
changeset

579 
\ Crypt (shrK A) {Key K, Agent A', NA} : parts {RA}; \ 
2449  580 
\ A ~: lost; A ~= Spy; evs : recur lost ] \ 
2455
9c4444bfd44e
Simplification and generalization of the guarantees.
paulson
parents:
2451
diff
changeset

581 
\ ==> EX C RC. Says Server C RC : set_of_list evs & \ 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

582 
\ Crypt (shrK A) {Key K, Agent A', NA} : parts {RC}"; 
2449  583 
by (best_tac (!claset addSIs [Crypt_imp_Server_msg] 
584 
addDs [Says_imp_sees_Spy RS parts.Inj RSN (2,parts_cut)] 

585 
addss (!simpset)) 1); 

586 
qed "Agent_trust"; 

587 

588 

2455
9c4444bfd44e
Simplification and generalization of the guarantees.
paulson
parents:
2451
diff
changeset

589 
(*Overall guarantee: if A receives a certificant mentioning A' 
9c4444bfd44e
Simplification and generalization of the guarantees.
paulson
parents:
2451
diff
changeset

590 
then the only other agent who knows the key is A'.*) 
2449  591 
goal thy 
592 
"!!evs. [ Says B' A RA : set_of_list evs; \ 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

593 
\ Crypt (shrK A) {Key K, Agent A', NA} : parts {RA}; \ 
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

594 
\ C ~: {A,A',Server}; \ 
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2449
diff
changeset

595 
\ A ~: lost; A' ~: lost; A ~= Spy; evs : recur lost ] \ 
2449  596 
\ ==> Key K ~: analz (sees lost C evs)"; 
597 
by (dtac Agent_trust 1 THEN REPEAT_FIRST assume_tac); 

598 
by (fast_tac (!claset addSEs [Agent_not_see_encrypted_key RSN(2,rev_notE)]) 1); 

599 
qed "Agent_secrecy"; 

600 