author  paulson 
Fri, 17 Jan 1997 12:49:31 +0100  
changeset 2516  4d68fbe6378b 
parent 2451  ce85a2aafc7a 
child 2637  e9b203f854ae 
permissions  rwrr 
2002  1 
(* Title: HOL/Auth/OtwayRees_Bad 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1996 University of Cambridge 

5 

6 
Inductive relation "otway" for the OtwayRees protocol. 

7 

8 
The FAULTY version omitting encryption of Nonce NB, as suggested on page 247 of 

9 
Burrows, Abadi and Needham. A Logic of Authentication. 

10 
Proc. Royal Soc. 426 (1989) 

11 

12 
This file illustrates the consequences of such errors. We can still prove 

2032  13 
impressivelooking properties such as Spy_not_see_encrypted_key, yet the 
2002  14 
protocol is open to a middleperson attack. Attempting to prove some key lemmas 
15 
indicates the possibility of this attack. 

16 
*) 

17 

18 
open OtwayRees_Bad; 

19 

20 
proof_timing:=true; 

21 
HOL_quantifiers := false; 

22 

23 

24 
(*Weak liveness: there are traces that reach the end*) 

25 
goal thy 

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

27 
\ ==> EX K. EX NA. EX evs: otway. \ 

2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

28 
\ Says B A {Nonce NA, Crypt (shrK A) {Nonce NA, Key K}} \ 
2002  29 
\ : set_of_list evs"; 
30 
by (REPEAT (resolve_tac [exI,bexI] 1)); 

2032  31 
by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

32 
by possibility_tac; 
2002  33 
result(); 
34 

35 

36 
(**** Inductive proofs about otway ****) 

37 

38 
(*Nobody sends themselves messages*) 

39 
goal thy "!!evs. evs : otway ==> ALL A X. Says A A X ~: set_of_list evs"; 

2032  40 
by (etac otway.induct 1); 
2002  41 
by (Auto_tac()); 
42 
qed_spec_mp "not_Says_to_self"; 

43 
Addsimps [not_Says_to_self]; 

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

45 

46 

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

48 

49 
goal thy "!!evs. Says A' B {N, Agent A, Agent B, X} : set_of_list evs ==> \ 

2052  50 
\ X : analz (sees lost Spy evs)"; 
2032  51 
by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1); 
52 
qed "OR2_analz_sees_Spy"; 

2002  53 

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

54 
goal thy "!!evs. Says S B {N, X, Crypt (shrK B) X'} : set_of_list evs ==> \ 
2052  55 
\ X : analz (sees lost Spy evs)"; 
2032  56 
by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1); 
57 
qed "OR4_analz_sees_Spy"; 

2002  58 

2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

59 
goal thy "!!evs. Says Server B {NA, X, Crypt K' {NB,K}} : set_of_list evs \ 
2131  60 
\ ==> K : parts (sees lost Spy evs)"; 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

61 
by (fast_tac (!claset addSEs sees_Spy_partsEs) 1); 
2131  62 
qed "Oops_parts_sees_Spy"; 
2002  63 

64 
(*OR2_analz... and OR4_analz... let us treat those cases using the same 

65 
argument as for the Fake case. This is possible for most, but not all, 

66 
proofs: Fake does not invent new nonces (as in OR2), and of course Fake 

2032  67 
messages originate from the Spy. *) 
2002  68 

2052  69 
bind_thm ("OR2_parts_sees_Spy", 
70 
OR2_analz_sees_Spy RS (impOfSubs analz_subset_parts)); 

71 
bind_thm ("OR4_parts_sees_Spy", 

72 
OR4_analz_sees_Spy RS (impOfSubs analz_subset_parts)); 

73 

2002  74 
val parts_Fake_tac = 
2052  75 
forward_tac [OR2_parts_sees_Spy] 4 THEN 
76 
forward_tac [OR4_parts_sees_Spy] 6 THEN 

2131  77 
forward_tac [Oops_parts_sees_Spy] 7; 
78 

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

80 
fun parts_induct_tac i = SELECT_GOAL 

81 
(DETERM (etac otway.induct 1 THEN parts_Fake_tac THEN 

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

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

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

84 
impOfSubs Fake_parts_insert] 
2131  85 
addss (!simpset)) 2)) THEN 
86 
(*Base case*) 

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

88 
ALLGOALS Asm_simp_tac) i; 

2002  89 

90 

2052  91 
(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY 
2002  92 
sends messages containing X! **) 
93 

2131  94 
(*Spy never sees another agent's shared key! (unless it's lost at start)*) 
2002  95 
goal thy 
2131  96 
"!!evs. evs : otway \ 
97 
\ ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)"; 

98 
by (parts_induct_tac 1); 

2002  99 
by (Auto_tac()); 
2131  100 
qed "Spy_see_shrK"; 
101 
Addsimps [Spy_see_shrK]; 

2002  102 

2131  103 
goal thy 
104 
"!!evs. evs : otway \ 

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

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

107 
qed "Spy_analz_shrK"; 

108 
Addsimps [Spy_analz_shrK]; 

2002  109 

2131  110 
goal thy "!!A. [ Key (shrK A) : parts (sees lost Spy evs); \ 
111 
\ evs : otway ] ==> A:lost"; 

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

113 
qed "Spy_see_shrK_D"; 

2002  114 

2131  115 
bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D); 
116 
AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D]; 

2002  117 

118 

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

119 
(*Nobody can have used nonexistent keys!*) 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

121 
\ Key K ~: used evs > K ~: keysFor (parts (sees lost Spy evs))"; 
2160  122 
by (parts_induct_tac 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

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

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

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

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

128 
addss (!simpset)) 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

130 
by (REPEAT (fast_tac (!claset addss (!simpset)) 1)); 
2160  131 
qed_spec_mp "new_keys_not_used"; 
2002  132 

133 
bind_thm ("new_keys_not_analzd", 

2032  134 
[analz_subset_parts RS keysFor_mono, 
135 
new_keys_not_used] MRS contra_subsetD); 

2002  136 

137 
Addsimps [new_keys_not_used, new_keys_not_analzd]; 

138 

139 

2131  140 

141 
(*** Proofs involving analz ***) 

142 

143 
(*Describes the form of K and NA when the Server sends this message. Also 

144 
for Oops case.*) 

145 
goal thy 

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

146 
"!!evs. [ Says Server B \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

147 
\ {NA, X, Crypt (shrK B) {NB, Key K}} : set_of_list evs; \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

149 
\ ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)"; 
2131  150 
by (etac rev_mp 1); 
151 
by (etac otway.induct 1); 

152 
by (ALLGOALS (fast_tac (!claset addss (!simpset)))); 

153 
qed "Says_Server_message_form"; 

154 

155 

156 
(*For proofs involving analz.*) 

157 
val analz_Fake_tac = 

158 
dtac OR2_analz_sees_Spy 4 THEN 

159 
dtac OR4_analz_sees_Spy 6 THEN 

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

160 
forward_tac [Says_Server_message_form] 7 THEN assume_tac 7 THEN 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2417
diff
changeset

161 
REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7); 
2002  162 

163 

164 
(**** 

165 
The following is to prove theorems of the form 

166 

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

167 
Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==> 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2417
diff
changeset

168 
Key K : analz (sees lost Spy evs) 
2002  169 

170 
A more general formula must be proved inductively. 

171 
****) 

172 

173 

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

175 

176 
(*The equality makes the induction hypothesis easier to apply*) 

177 
goal thy 

178 
"!!evs. evs : otway ==> \ 

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

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

180 
\ (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:
2451
diff
changeset

181 
\ (K : KK  Key K : analz (sees lost Spy evs))"; 
2032  182 
by (etac otway.induct 1); 
2131  183 
by analz_Fake_tac; 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

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

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

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

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

189 
(*Fake, OR2, OR4*) 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

191 
qed_spec_mp "analz_image_freshK"; 
2002  192 

193 

194 
goal thy 

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

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

196 
\ 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:
2451
diff
changeset

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

198 
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:
2451
diff
changeset

199 
qed "analz_insert_freshK"; 
2002  200 

201 

2131  202 
(*** The Key K uniquely identifies the Server's message. **) 
2002  203 

204 
goal thy 

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

205 
"!!evs. evs : otway ==> \ 
2131  206 
\ EX B' NA' NB' X'. ALL B NA NB X. \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

207 
\ Says Server B {NA, X, Crypt (shrK B) {NB, K}} : set_of_list evs > \ 
2131  208 
\ B=B' & NA=NA' & NB=NB' & X=X'"; 
2032  209 
by (etac otway.induct 1); 
2002  210 
by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib]))); 
211 
by (Step_tac 1); 

212 
(*Remaining cases: OR3 and OR4*) 

213 
by (ex_strip_tac 2); 

214 
by (Fast_tac 2); 

2107
23e8f15ec95f
The new proof of the lemma for new_nonces_not_seen is faster
paulson
parents:
2052
diff
changeset

215 
by (expand_case_tac "K = ?y" 1); 
23e8f15ec95f
The new proof of the lemma for new_nonces_not_seen is faster
paulson
parents:
2052
diff
changeset

216 
by (REPEAT (ares_tac [refl,exI,impI,conjI] 2)); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

217 
(*...we assume X is a recent message, and handle this case by contradiction*) 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

218 
by (fast_tac (!claset addSEs sees_Spy_partsEs 
2032  219 
delrules [conjI] (*prevent splitup into 4 subgoals*) 
220 
addss (!simpset addsimps [parts_insertI])) 1); 

2002  221 
val lemma = result(); 
222 

223 
goal thy 

2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

224 
"!!evs. [ Says Server B {NA, X, Crypt (shrK B) {NB, K}} \ 
2002  225 
\ : set_of_list evs; \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

226 
\ Says Server B' {NA',X',Crypt (shrK B') {NB',K}} \ 
2002  227 
\ : set_of_list evs; \ 
2131  228 
\ evs : otway ] ==> X=X' & B=B' & NA=NA' & NB=NB'"; 
2417  229 
by (prove_unique_tac lemma 1); 
2002  230 
qed "unique_session_keys"; 
231 

232 

2131  233 
(*Crucial security property, but not itself enough to guarantee correctness!*) 
234 
goal thy 

2166  235 
"!!evs. [ A ~: lost; B ~: lost; evs : otway ] \ 
236 
\ ==> Says Server B \ 

2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

237 
\ {NA, Crypt (shrK A) {NA, Key K}, \ 
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

238 
\ Crypt (shrK B) {NB, Key K}} : set_of_list evs > \ 
2166  239 
\ Says B Spy {NA, NB, Key K} ~: set_of_list evs > \ 
240 
\ Key K ~: analz (sees lost Spy evs)"; 

2131  241 
by (etac otway.induct 1); 
242 
by analz_Fake_tac; 

243 
by (ALLGOALS 

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

244 
(asm_simp_tac (!simpset addcongs [conj_cong] 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

245 
addsimps [not_parts_not_analz, analz_insert_freshK] 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

246 
setloop split_tac [expand_if]))); 
2131  247 
(*OR3*) 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

248 
by (fast_tac (!claset delrules [impCE] 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

250 
addIs [impOfSubs analz_subset_parts] 
2131  251 
addss (!simpset addsimps [parts_insert2])) 3); 
252 
(*OR4, OR2, Fake*) 

2375  253 
by (REPEAT_FIRST spy_analz_tac); 
2131  254 
(*Oops*) (** LEVEL 5 **) 
255 
by (fast_tac (!claset delrules [disjE] 

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

256 
addDs [unique_session_keys] addss (!simpset)) 1); 
2131  257 
val lemma = result() RS mp RS mp RSN(2,rev_notE); 
258 

259 
goal thy 

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

260 
"!!evs. [ Says Server B \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

261 
\ {NA, Crypt (shrK A) {NA, Key K}, \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

262 
\ Crypt (shrK B) {NB, Key K}} : set_of_list evs; \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

263 
\ Says B Spy {NA, NB, Key K} ~: set_of_list evs; \ 
2131  264 
\ A ~: lost; B ~: lost; evs : otway ] \ 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

265 
\ ==> Key K ~: analz (sees lost Spy evs)"; 
2131  266 
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); 
267 
by (fast_tac (!claset addSEs [lemma]) 1); 

268 
qed "Spy_not_see_encrypted_key"; 

269 

270 

271 
(*** Attempting to prove stronger properties ***) 

272 

2052  273 
(*Only OR1 can have caused such a part of a message to appear. 
274 
I'm not sure why A ~= B premise is needed: OtwayRees.ML doesn't need it. 

275 
Perhaps it's because OR2 has two similarlooking encrypted messages in 

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

276 
this version.*) 
2002  277 
goal thy 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

278 
"!!evs. [ A ~: lost; A ~= B; evs : otway ] \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

279 
\ ==> Crypt (shrK A) {NA, Agent A, Agent B} \ 
2052  280 
\ : parts (sees lost Spy evs) > \ 
2131  281 
\ Says A B {NA, Agent A, Agent B, \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

282 
\ Crypt (shrK A) {NA, Agent A, Agent B}} \ 
2002  283 
\ : set_of_list evs"; 
2131  284 
by (parts_induct_tac 1); 
285 
by (Fast_tac 1); 

2002  286 
qed_spec_mp "Crypt_imp_OR1"; 
287 

288 

2131  289 
(*Crucial property: If the encrypted message appears, and A has used NA 
290 
to start a run, then it originated with the Server!*) 

291 
(*Only it is FALSE. Somebody could make a fake message to Server 

2002  292 
substituting some other nonce NA' for NB.*) 
293 
goal thy 

2052  294 
"!!evs. [ A ~: lost; A ~= Spy; evs : otway ] \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

295 
\ ==> Crypt (shrK A) {NA, Key K} : parts (sees lost Spy evs) > \ 
2131  296 
\ Says A B {NA, Agent A, Agent B, \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

297 
\ Crypt (shrK A) {NA, Agent A, Agent B}} \ 
2131  298 
\ : set_of_list evs > \ 
299 
\ (EX B NB. Says Server B \ 

300 
\ {NA, \ 

2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

301 
\ Crypt (shrK A) {NA, Key K}, \ 
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

302 
\ Crypt (shrK B) {NB, Key K}} \ 
2002  303 
\ : set_of_list evs)"; 
2131  304 
by (parts_induct_tac 1); 
2002  305 
(*OR1: it cannot be a new Nonce, contradiction.*) 
306 
by (fast_tac (!claset addSIs [parts_insertI] 

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

307 
addSEs sees_Spy_partsEs 
2032  308 
addss (!simpset)) 1); 
2002  309 
(*OR4*) 
310 
by (REPEAT (Safe_step_tac 2)); 

2052  311 
by (REPEAT (best_tac (!claset addSDs [parts_cut]) 3)); 
312 
by (fast_tac (!claset addSIs [Crypt_imp_OR1] 

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

313 
addEs sees_Spy_partsEs) 2); 
2131  314 
(*OR3*) (** LEVEL 5 **) 
2002  315 
by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib]))); 
2052  316 
by (step_tac (!claset delrules [disjCI, impCE]) 1); 
2002  317 
(*The hypotheses at this point suggest an attack in which nonce NA is used 
2052  318 
in two different roles: 
319 
Says B' Server 

320 
{Nonce NAa, Agent Aa, Agent A, 

2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

321 
Crypt (shrK Aa) {Nonce NAa, Agent Aa, Agent A}, Nonce NA, 
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

322 
Crypt (shrK A) {Nonce NAa, Agent Aa, Agent A}} 
2052  323 
: set_of_list evsa; 
324 
Says A B 

325 
{Nonce NA, Agent A, Agent B, 

2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

326 
Crypt (shrK A) {Nonce NA, Agent A, Agent B}} 
2052  327 
: set_of_list evsa 
328 
*) 

2131  329 
writeln "GIVE UP! on NA_Crypt_imp_Server_msg"; 
2002  330 

331 

2052  332 
(*Thus the key property A_can_trust probably fails too.*) 