author  paulson 
Tue, 05 Nov 1996 11:20:52 +0100  
changeset 2160  ad4382e546fc 
parent 2135  80477862ab33 
child 2166  d276a806cc10 
permissions  rwrr 
1941  1 
(* Title: HOL/Auth/OtwayRees 
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 

2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

8 
Version that encrypts Nonce NB 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

9 

1941  10 
From page 244 of 
11 
Burrows, Abadi and Needham. A Logic of Authentication. 

12 
Proc. Royal Soc. 426 (1989) 

13 
*) 

14 

15 
open OtwayRees; 

16 

17 
proof_timing:=true; 

18 
HOL_quantifiers := false; 

2135  19 
Pretty.setdepth 15; 
1941  20 

1996
33c42cae3dd0
Uses the improved enemy_analz_tac of Shared.ML, with simpler proofs
paulson
parents:
1967
diff
changeset

21 

2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

22 
(*Weak liveness: there are traces that reach the end*) 
1996
33c42cae3dd0
Uses the improved enemy_analz_tac of Shared.ML, with simpler proofs
paulson
parents:
1967
diff
changeset

23 
goal thy 
33c42cae3dd0
Uses the improved enemy_analz_tac of Shared.ML, with simpler proofs
paulson
parents:
1967
diff
changeset

24 
"!!A B. [ A ~= B; A ~= Server; B ~= Server ] \ 
2032  25 
\ ==> EX K. EX NA. EX evs: otway lost. \ 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

26 
\ Says B A {Nonce NA, Crypt {Nonce NA, Key K} (shrK A)} \ 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

27 
\ : set_of_list evs"; 
1996
33c42cae3dd0
Uses the improved enemy_analz_tac of Shared.ML, with simpler proofs
paulson
parents:
1967
diff
changeset

28 
by (REPEAT (resolve_tac [exI,bexI] 1)); 
2032  29 
by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2); 
1996
33c42cae3dd0
Uses the improved enemy_analz_tac of Shared.ML, with simpler proofs
paulson
parents:
1967
diff
changeset

30 
by (ALLGOALS (simp_tac (!simpset setsolver safe_solver))); 
33c42cae3dd0
Uses the improved enemy_analz_tac of Shared.ML, with simpler proofs
paulson
parents:
1967
diff
changeset

31 
by (REPEAT_FIRST (resolve_tac [refl, conjI])); 
2104
f5c9a91e4b50
Replaced excluded_middle_tac by case_tac; tidied proofs
paulson
parents:
2071
diff
changeset

32 
by (REPEAT_FIRST (fast_tac (!claset addss (!simpset setsolver safe_solver)))); 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

33 
result(); 
1996
33c42cae3dd0
Uses the improved enemy_analz_tac of Shared.ML, with simpler proofs
paulson
parents:
1967
diff
changeset

34 

33c42cae3dd0
Uses the improved enemy_analz_tac of Shared.ML, with simpler proofs
paulson
parents:
1967
diff
changeset

35 

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

2104
f5c9a91e4b50
Replaced excluded_middle_tac by case_tac; tidied proofs
paulson
parents:
2071
diff
changeset

38 
(*Monotonicity*) 
2032  39 
goal thy "!!evs. lost' <= lost ==> otway lost' <= otway lost"; 
40 
by (rtac subsetI 1); 

41 
by (etac otway.induct 1); 

42 
by (REPEAT_FIRST 

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

44 
:: otway.intrs)))); 

45 
qed "otway_mono"; 

46 

1941  47 
(*Nobody sends themselves messages*) 
2032  48 
goal thy "!!evs. evs : otway lost ==> ALL A X. Says A A X ~: set_of_list evs"; 
49 
by (etac otway.induct 1); 

1941  50 
by (Auto_tac()); 
51 
qed_spec_mp "not_Says_to_self"; 

52 
Addsimps [not_Says_to_self]; 

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

54 

55 

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

57 

2135  58 
goal thy "!!evs. Says A' B {N, Agent A, Agent B, X} : set_of_list evs \ 
59 
\ ==> X : analz (sees lost Spy evs)"; 

2032  60 
by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1); 
61 
qed "OR2_analz_sees_Spy"; 

1941  62 

2135  63 
goal thy "!!evs. Says S B {N, X, X'} : set_of_list evs \ 
64 
\ ==> X : analz (sees lost Spy evs)"; 

2032  65 
by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1); 
66 
qed "OR4_analz_sees_Spy"; 

1941  67 

2135  68 
goal thy "!!evs. Says Server B {NA, X, Crypt {NB,K} K'} : set_of_list evs \ 
69 
\ ==> K : parts (sees lost Spy evs)"; 

1941  70 
by (fast_tac (!claset addSEs partsEs 
2032  71 
addSDs [Says_imp_sees_Spy RS parts.Inj]) 1); 
2135  72 
qed "Oops_parts_sees_Spy"; 
1941  73 

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

1964  75 
argument as for the Fake case. This is possible for most, but not all, 
76 
proofs: Fake does not invent new nonces (as in OR2), and of course Fake 

2032  77 
messages originate from the Spy. *) 
1964  78 

2032  79 
bind_thm ("OR2_parts_sees_Spy", 
80 
OR2_analz_sees_Spy RS (impOfSubs analz_subset_parts)); 

81 
bind_thm ("OR4_parts_sees_Spy", 

82 
OR4_analz_sees_Spy RS (impOfSubs analz_subset_parts)); 

83 

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

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

2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

86 
val parts_Fake_tac = 
2032  87 
let val tac = forw_inst_tac [("lost","lost")] 
88 
in tac OR2_parts_sees_Spy 4 THEN 

89 
tac OR4_parts_sees_Spy 6 THEN 

2135  90 
tac Oops_parts_sees_Spy 7 
2032  91 
end; 
1941  92 

2064  93 
(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *) 
94 
fun parts_induct_tac i = SELECT_GOAL 

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

96 
(*Fake message*) 

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

98 
impOfSubs Fake_parts_insert] 

99 
addss (!simpset)) 2)) THEN 

100 
(*Base case*) 

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

102 
ALLGOALS Asm_simp_tac) i; 

1941  103 

2032  104 
(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

105 
sends messages containing X! **) 
1941  106 

2064  107 
(*Spy never sees another agent's shared key! (unless it's lost at start)*) 
1941  108 
goal thy 
2135  109 
"!!evs. evs : otway lost \ 
110 
\ ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)"; 

2064  111 
by (parts_induct_tac 1); 
1941  112 
by (Auto_tac()); 
2135  113 
qed "Spy_see_shrK"; 
114 
Addsimps [Spy_see_shrK]; 

1941  115 

2135  116 
goal thy 
117 
"!!evs. evs : otway lost \ 

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

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

120 
qed "Spy_analz_shrK"; 

121 
Addsimps [Spy_analz_shrK]; 

1941  122 

2135  123 
goal thy "!!A. [ Key (shrK A) : parts (sees lost Spy evs); \ 
124 
\ evs : otway lost ] ==> A:lost"; 

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

126 
qed "Spy_see_shrK_D"; 

1941  127 

2135  128 
bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D); 
129 
AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D]; 

1941  130 

131 

132 
(*** Future keys can't be seen or used! ***) 

133 

2160  134 
(*Nobody can have SEEN keys that will be generated in the future. *) 
2032  135 
goal thy "!!evs. evs : otway lost ==> \ 
1941  136 
\ length evs <= length evs' > \ 
2160  137 
\ Key (newK evs') ~: parts (sees lost Spy evs)"; 
2064  138 
by (parts_induct_tac 1); 
1941  139 
by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts, 
2032  140 
impOfSubs parts_insert_subset_Un, 
141 
Suc_leD] 

142 
addss (!simpset)))); 

2160  143 
qed_spec_mp "new_keys_not_seen"; 
1941  144 
Addsimps [new_keys_not_seen]; 
145 

2160  146 
(*Variant: old messages must contain old keys!*) 
1941  147 
goal thy 
148 
"!!evs. [ Says A B X : set_of_list evs; \ 

149 
\ Key (newK evt) : parts {X}; \ 

2032  150 
\ evs : otway lost \ 
1941  151 
\ ] ==> length evt < length evs"; 
2032  152 
by (rtac ccontr 1); 
153 
by (dtac leI 1); 

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

2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

155 
addIs [impOfSubs parts_mono]) 1); 
1941  156 
qed "Says_imp_old_keys"; 
157 

158 

2160  159 
(*** Future nonces can't be seen or used! ***) 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

160 

2032  161 
goal thy "!!evs. evs : otway lost ==> \ 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

162 
\ length evs <= length evt > \ 
2160  163 
\ Nonce (newN evt) ~: parts (sees lost Spy evs)"; 
164 
by (parts_induct_tac 1); 

2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

165 
by (REPEAT_FIRST (fast_tac (!claset 
2032  166 
addSEs partsEs 
167 
addSDs [Says_imp_sees_Spy RS parts.Inj] 

168 
addDs [impOfSubs analz_subset_parts, 

169 
impOfSubs parts_insert_subset_Un, 

170 
Suc_leD] 

171 
addss (!simpset)))); 

2160  172 
qed_spec_mp "new_nonces_not_seen"; 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

173 
Addsimps [new_nonces_not_seen]; 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

174 

2160  175 
(*Variant: old messages must contain old nonces!*) 
176 
goal thy "!!evs. [ Says A B X : set_of_list evs; \ 

177 
\ Nonce (newN evt) : parts {X}; \ 

178 
\ evs : otway lost \ 

179 
\ ] ==> length evt < length evs"; 

2032  180 
by (rtac ccontr 1); 
181 
by (dtac leI 1); 

182 
by (fast_tac (!claset addSDs [new_nonces_not_seen, Says_imp_sees_Spy] 

183 
addIs [impOfSubs parts_mono]) 1); 

2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

184 
qed "Says_imp_old_nonces"; 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

185 

5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

186 

1941  187 
(*Nobody can have USED keys that will be generated in the future. 
188 
...very like new_keys_not_seen*) 

2160  189 
goal thy "!!evs. evs : otway lost ==> \ 
1941  190 
\ length evs <= length evs' > \ 
2160  191 
\ newK evs' ~: keysFor (parts (sees lost Spy evs))"; 
2064  192 
by (parts_induct_tac 1); 
1941  193 
(*OR1 and OR3*) 
194 
by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,2])); 

195 
(*Fake, OR2, OR4: these messages send unknown (X) components*) 

2104
f5c9a91e4b50
Replaced excluded_middle_tac by case_tac; tidied proofs
paulson
parents:
2071
diff
changeset

196 
by (REPEAT 
f5c9a91e4b50
Replaced excluded_middle_tac by case_tac; tidied proofs
paulson
parents:
2071
diff
changeset

197 
(best_tac 
1996
33c42cae3dd0
Uses the improved enemy_analz_tac of Shared.ML, with simpler proofs
paulson
parents:
1967
diff
changeset

198 
(!claset addDs [impOfSubs (analz_subset_parts RS keysFor_mono), 
2032  199 
impOfSubs (parts_insert_subset_Un RS keysFor_mono), 
200 
Suc_leD] 

201 
addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)] 

2104
f5c9a91e4b50
Replaced excluded_middle_tac by case_tac; tidied proofs
paulson
parents:
2071
diff
changeset

202 
addss (!simpset)) 1)); 
2160  203 
qed_spec_mp "new_keys_not_used"; 
1941  204 

205 
bind_thm ("new_keys_not_analzd", 

2032  206 
[analz_subset_parts RS keysFor_mono, 
207 
new_keys_not_used] MRS contra_subsetD); 

1941  208 

209 
Addsimps [new_keys_not_used, new_keys_not_analzd]; 

210 

211 

2064  212 

213 
(*** Proofs involving analz ***) 

214 

2135  215 
(*Describes the form of K and NA when the Server sends this message. Also 
216 
for Oops case.*) 

2064  217 
goal thy 
2135  218 
"!!evs. [ Says Server B \ 
219 
\ {NA, X, Crypt {NB, K} (shrK B)} : set_of_list evs; \ 

220 
\ evs : otway lost ] \ 

221 
\ ==> (EX evt: otway lost. K = Key(newK evt)) & \ 

222 
\ (EX i. NA = Nonce i) & (EX j. NB = Nonce j)"; 

223 
by (etac rev_mp 1); 

224 
by (etac otway.induct 1); 

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

226 
qed "Says_Server_message_form"; 

2064  227 

228 

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

230 
val analz_Fake_tac = 

231 
dres_inst_tac [("lost","lost")] OR2_analz_sees_Spy 4 THEN 

232 
dres_inst_tac [("lost","lost")] OR4_analz_sees_Spy 6 THEN 

2135  233 
forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN 
234 
assume_tac 7 THEN Full_simp_tac 7 THEN 

235 
REPEAT ((eresolve_tac [bexE, exE, conjE] ORELSE' hyp_subst_tac) 7); 

1941  236 

237 

238 
(**** 

239 
The following is to prove theorems of the form 

240 

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

1941  243 

244 
A more general formula must be proved inductively. 

245 
****) 

246 

247 

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

249 

2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

250 
(*The equality makes the induction hypothesis easier to apply*) 
1941  251 
goal thy 
2032  252 
"!!evs. evs : otway lost ==> \ 
253 
\ ALL K E. (Key K : analz (Key``(newK``E) Un (sees lost Spy evs))) = \ 

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

255 
by (etac otway.induct 1); 

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

257 
by (REPEAT_FIRST (ares_tac [allI, analz_image_newK_lemma])); 
2160  258 
by (ALLGOALS (*Takes 14 secs*) 
1941  259 
(asm_simp_tac 
260 
(!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK] 

2032  261 
@ pushes) 
1941  262 
setloop split_tac [expand_if]))); 
2135  263 
(*OR4, OR2, Fake*) 
264 
by (EVERY (map spy_analz_tac [5,3,2])); 

265 
(*Oops, OR3, Base*) 

2064  266 
by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1)); 
1941  267 
qed_spec_mp "analz_image_newK"; 
268 

269 

270 
goal thy 

2032  271 
"!!evs. evs : otway lost ==> \ 
272 
\ Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) = \ 

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

1941  274 
by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, 
2032  275 
insert_Key_singleton]) 1); 
1941  276 
by (Fast_tac 1); 
277 
qed "analz_insert_Key_newK"; 

278 

279 

2026
0df5a96bf77e
Last working version prior to introduction of "lost"
paulson
parents:
2014
diff
changeset

280 
(*** The Key K uniquely identifies the Server's message. **) 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

281 

5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

282 
goal thy 
2135  283 
"!!evs. evs : otway lost ==> \ 
284 
\ EX B' NA' NB' X'. ALL B NA NB X. \ 

285 
\ Says Server B {NA, X, Crypt {NB, K} (shrK B)} : set_of_list evs > \ 

286 
\ B=B' & NA=NA' & NB=NB' & X=X'"; 

2032  287 
by (etac otway.induct 1); 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

288 
by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib]))); 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

289 
by (Step_tac 1); 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

290 
(*Remaining cases: OR3 and OR4*) 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

291 
by (ex_strip_tac 2); 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

292 
by (Fast_tac 2); 
2064  293 
by (expand_case_tac "K = ?y" 1); 
294 
by (REPEAT (ares_tac [refl,exI,impI,conjI] 2)); 

2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

295 
(*...we assume X is a very new message, and handle this case by contradiction*) 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

296 
by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl] 
2032  297 
delrules [conjI] (*prevent splitup into 4 subgoals*) 
298 
addss (!simpset addsimps [parts_insertI])) 1); 

2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

299 
val lemma = result(); 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

300 

5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

301 
goal thy 
2135  302 
"!!evs. [ Says Server B {NA, X, Crypt {NB, K} (shrK B)} \ 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

303 
\ : set_of_list evs; \ 
2135  304 
\ Says Server B' {NA',X',Crypt {NB',K} (shrK B')} \ 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

305 
\ : set_of_list evs; \ 
2135  306 
\ evs : otway lost ] ==> X=X' & B=B' & NA=NA' & NB=NB'"; 
2032  307 
by (dtac lemma 1); 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

308 
by (REPEAT (etac exE 1)); 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

309 
(*Duplicate the assumption*) 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

310 
by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1); 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

311 
by (fast_tac (!claset addSDs [spec]) 1); 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

312 
qed "unique_session_keys"; 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

313 

5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

314 

5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

315 

2048  316 
(**** Authenticity properties relating to NA ****) 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

317 

5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

318 
(*Only OR1 can have caused such a part of a message to appear.*) 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

319 
goal thy 
2064  320 
"!!evs. [ A ~: lost; evs : otway lost ] \ 
321 
\ ==> Crypt {NA, Agent A, Agent B} (shrK A) \ 

322 
\ : parts (sees lost Spy evs) > \ 

323 
\ Says A B {NA, Agent A, Agent B, \ 

2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

324 
\ Crypt {NA, Agent A, Agent B} (shrK A)} \ 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

325 
\ : set_of_list evs"; 
2064  326 
by (parts_induct_tac 1); 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

327 
qed_spec_mp "Crypt_imp_OR1"; 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

328 

5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

329 

2064  330 
(** The Nonce NA uniquely identifies A's message. **) 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

331 

5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

332 
goal thy 
2032  333 
"!!evs. [ evs : otway lost; A ~: lost ] \ 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

334 
\ ==> EX B'. ALL B. \ 
2048  335 
\ Crypt {NA, Agent A, Agent B} (shrK A) : parts (sees lost Spy evs) \ 
336 
\ > B = B'"; 

2064  337 
by (parts_induct_tac 1); 
338 
by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 

2026
0df5a96bf77e
Last working version prior to introduction of "lost"
paulson
parents:
2014
diff
changeset

339 
(*OR1: creation of new Nonce. Move assertion into global context*) 
2064  340 
by (expand_case_tac "NA = ?y" 1); 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

341 
by (best_tac (!claset addSEs partsEs 
2032  342 
addEs [new_nonces_not_seen RSN(2,rev_notE)]) 1); 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

343 
val lemma = result(); 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

344 

5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

345 
goal thy 
2048  346 
"!!evs.[ Crypt {NA, Agent A, Agent B} (shrK A): parts(sees lost Spy evs); \ 
347 
\ Crypt {NA, Agent A, Agent C} (shrK A): parts(sees lost Spy evs); \ 

348 
\ evs : otway lost; A ~: lost ] \ 

2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

349 
\ ==> B = C"; 
2032  350 
by (dtac lemma 1); 
351 
by (assume_tac 1); 

2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

352 
by (etac exE 1); 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

353 
(*Duplicate the assumption*) 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

354 
by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1); 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

355 
by (fast_tac (!claset addSDs [spec]) 1); 
2048  356 
qed "unique_NA"; 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

357 

5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

358 

5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

359 
val nonce_not_seen_now = le_refl RSN (2, new_nonces_not_seen) RSN (2,rev_notE); 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

360 

5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

361 
(*It is impossible to reuse a nonce in both OR1 and OR2. This holds because 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

362 
OR2 encrypts Nonce NB. It prevents the attack that can occur in the 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

363 
oversimplified version of this protocol: see OtwayRees_Bad.*) 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

364 
goal thy 
2032  365 
"!!evs. [ A ~: lost; evs : otway lost ] \ 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

366 
\ ==> Crypt {NA, Agent A, Agent B} (shrK A) \ 
2032  367 
\ : parts (sees lost Spy evs) > \ 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

368 
\ Crypt {NA', NA, Agent A', Agent A} (shrK A) \ 
2032  369 
\ ~: parts (sees lost Spy evs)"; 
2071
0debdc018d26
Put in a simpler and *much* faster proof of no_nonce_OR1_OR2
paulson
parents:
2064
diff
changeset

370 
by (parts_induct_tac 1); 
0debdc018d26
Put in a simpler and *much* faster proof of no_nonce_OR1_OR2
paulson
parents:
2064
diff
changeset

371 
by (REPEAT (fast_tac (!claset addSEs (partsEs@[nonce_not_seen_now]) 
2026
0df5a96bf77e
Last working version prior to introduction of "lost"
paulson
parents:
2014
diff
changeset

372 
addSDs [impOfSubs parts_insert_subset_Un] 
2071
0debdc018d26
Put in a simpler and *much* faster proof of no_nonce_OR1_OR2
paulson
parents:
2064
diff
changeset

373 
addss (!simpset)) 1)); 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

374 
qed_spec_mp"no_nonce_OR1_OR2"; 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

375 

5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

376 

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

2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

379 
goal thy 
2048  380 
"!!evs. [ A ~: lost; A ~= Spy; evs : otway lost ] \ 
381 
\ ==> Crypt {NA, Key K} (shrK A) : parts (sees lost Spy evs) \ 

382 
\ > Says A B {NA, Agent A, Agent B, \ 

383 
\ Crypt {NA, Agent A, Agent B} (shrK A)} \ 

384 
\ : set_of_list evs > \ 

385 
\ (EX NB. Says Server B \ 

386 
\ {NA, \ 

387 
\ Crypt {NA, Key K} (shrK A), \ 

388 
\ Crypt {NB, Key K} (shrK B)} \ 

2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

389 
\ : set_of_list evs)"; 
2064  390 
by (parts_induct_tac 1); 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

391 
(*OR1: it cannot be a new Nonce, contradiction.*) 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

392 
by (fast_tac (!claset addSIs [parts_insertI] 
2032  393 
addSEs partsEs 
394 
addEs [Says_imp_old_nonces RS less_irrefl] 

395 
addss (!simpset)) 1); 

2064  396 
(*OR3 and OR4*) 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

397 
(*OR4*) 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

398 
by (REPEAT (Safe_step_tac 2)); 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

399 
by (REPEAT (best_tac (!claset addSDs [parts_cut]) 3)); 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

400 
by (fast_tac (!claset addSIs [Crypt_imp_OR1] 
2032  401 
addEs partsEs 
402 
addDs [Says_imp_sees_Spy RS parts.Inj]) 2); 

2064  403 
(*OR3*) (** LEVEL 5 **) 
404 
by (asm_simp_tac (!simpset addsimps [ex_disj_distrib]) 1); 

2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

405 
by (step_tac (!claset delrules [disjCI, impCE]) 1); 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

406 
by (fast_tac (!claset addSEs [MPair_parts] 
2032  407 
addSDs [Says_imp_sees_Spy RS parts.Inj] 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

408 
addEs [no_nonce_OR1_OR2 RSN (2, rev_notE)] 
2048  409 
delrules [conjI] (*stop splitup into 4 subgoals*)) 2); 
410 
by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj] 

411 
addSEs [MPair_parts] 

412 
addEs [unique_NA]) 1); 

413 
qed_spec_mp "NA_Crypt_imp_Server_msg"; 

2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

414 

5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

415 

2053  416 
(*Corollary: if A receives B's OR4 message and the nonce NA agrees 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

417 
then the key really did come from the Server! CANNOT prove this of the 
2048  418 
bad form of this protocol, even though we can prove 
2032  419 
Spy_not_see_encrypted_key*) 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

420 
goal thy 
2053  421 
"!!evs. [ Says B' A {NA, Crypt {NA, Key K} (shrK A)} \ 
422 
\ : set_of_list evs; \ 

423 
\ Says A B {NA, Agent A, Agent B, \ 

424 
\ Crypt {NA, Agent A, Agent B} (shrK A)} \ 

425 
\ : set_of_list evs; \ 

426 
\ A ~: lost; A ~= Spy; evs : otway lost ] \ 

427 
\ ==> EX NB. Says Server B \ 

2048  428 
\ {NA, \ 
429 
\ Crypt {NA, Key K} (shrK A), \ 

430 
\ Crypt {NB, Key K} (shrK B)} \ 

2053  431 
\ : set_of_list evs"; 
2048  432 
by (fast_tac (!claset addSIs [NA_Crypt_imp_Server_msg] 
2032  433 
addEs partsEs 
434 
addDs [Says_imp_sees_Spy RS parts.Inj]) 1); 

2064  435 
qed "A_trust_OR4"; 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

436 

5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

437 

2048  438 
(** Crucial secrecy property: Spy does not see the keys sent in msg OR3 
439 
Does not in itself guarantee security: an attack could violate 

440 
the premises, e.g. by having A=Spy **) 

2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

441 

1941  442 
goal thy 
2032  443 
"!!evs. [ A ~: lost; B ~: lost; evs : otway lost; evt : otway lost ] \ 
2048  444 
\ ==> Says Server B \ 
445 
\ {NA, Crypt {NA, Key K} (shrK A), \ 

446 
\ Crypt {NB, Key K} (shrK B)} : set_of_list evs > \ 

2135  447 
\ Says B Spy {NA, NB, Key K} ~: set_of_list evs > \ 
2048  448 
\ Key K ~: analz (sees lost Spy evs)"; 
2032  449 
by (etac otway.induct 1); 
2064  450 
by analz_Fake_tac; 
1964  451 
by (ALLGOALS 
1941  452 
(asm_full_simp_tac 
453 
(!simpset addsimps ([analz_subset_parts RS contra_subsetD, 

2032  454 
analz_insert_Key_newK] @ pushes) 
1941  455 
setloop split_tac [expand_if]))); 
456 
(*OR3*) 

2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

457 
by (fast_tac (!claset addSIs [parts_insertI] 
2032  458 
addEs [Says_imp_old_keys RS less_irrefl] 
2048  459 
addss (!simpset addsimps [parts_insert2])) 3); 
2135  460 
(*OR4, OR2, Fake*) 
2032  461 
by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' spy_analz_tac)); 
2135  462 
(*Oops*) (** LEVEL 5 **) 
463 
by (fast_tac (!claset delrules [disjE] 

464 
addDs [unique_session_keys] addss (!simpset)) 1); 

2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

465 
val lemma = result() RS mp RS mp RSN(2,rev_notE); 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

466 

5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

467 
goal thy 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

468 
"!!evs. [ Says Server B \ 
2048  469 
\ {NA, Crypt {NA, K} (shrK A), \ 
470 
\ Crypt {NB, K} (shrK B)} : set_of_list evs; \ 

2135  471 
\ Says B Spy {NA, NB, K} ~: set_of_list evs; \ 
2032  472 
\ A ~: lost; B ~: lost; evs : otway lost ] \ 
473 
\ ==> K ~: analz (sees lost Spy evs)"; 

2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

474 
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

475 
by (fast_tac (!claset addSEs [lemma]) 1); 
2032  476 
qed "Spy_not_see_encrypted_key"; 
477 

1945  478 

2032  479 
goal thy 
2048  480 
"!!evs. [ C ~: {A,B,Server}; \ 
481 
\ Says Server B \ 

482 
\ {NA, Crypt {NA, K} (shrK A), \ 

483 
\ Crypt {NB, K} (shrK B)} : set_of_list evs; \ 

2135  484 
\ Says B Spy {NA, NB, K} ~: set_of_list evs; \ 
2032  485 
\ A ~: lost; B ~: lost; evs : otway lost ] \ 
486 
\ ==> K ~: analz (sees lost C evs)"; 

487 
by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1); 

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

489 
by (FIRSTGOAL (rtac Spy_not_see_encrypted_key)); 

490 
by (REPEAT_FIRST (fast_tac (!claset addIs [otway_mono RS subsetD]))); 

491 
qed "Agent_not_see_encrypted_key"; 

1945  492 

493 

2048  494 
(**** Authenticity properties relating to NB ****) 
495 

496 
(*Only OR2 can have caused such a part of a message to appear. We do not 

497 
know anything about X'.*) 

498 
goal thy 

499 
"!!evs. [ B ~: lost; evs : otway lost ] \ 

500 
\ ==> Crypt {NA, NB, Agent A, Agent B} (shrK B) \ 

501 
\ : parts (sees lost Spy evs) > \ 

502 
\ (EX X'. Says B Server \ 

503 
\ {NA, Agent A, Agent B, X', \ 

504 
\ Crypt {NA, NB, Agent A, Agent B} (shrK B)} \ 

505 
\ : set_of_list evs)"; 

2064  506 
by (parts_induct_tac 1); 
507 
by (auto_tac (!claset, !simpset addcongs [conj_cong])); 

2048  508 
qed_spec_mp "Crypt_imp_OR2"; 
509 

510 

511 
(** The Nonce NB uniquely identifies B's message. **) 

512 

513 
goal thy 

514 
"!!evs. [ evs : otway lost; B ~: lost ] \ 

2064  515 
\ ==> EX NA' A'. ALL NA A. \ 
2048  516 
\ Crypt {NA, NB, Agent A, Agent B} (shrK B) : parts(sees lost Spy evs) \ 
517 
\ > NA = NA' & A = A'"; 

2064  518 
by (parts_induct_tac 1); 
519 
by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 

2048  520 
(*OR2: creation of new Nonce. Move assertion into global context*) 
2064  521 
by (expand_case_tac "NB = ?y" 1); 
2048  522 
by (fast_tac (!claset addSEs (nonce_not_seen_now::partsEs)) 1); 
523 
val lemma = result(); 

524 

525 
goal thy 

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

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

528 
\ Crypt {NC, NB, Agent C, Agent B} (shrK B) \ 

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

530 
\ evs : otway lost; B ~: lost ] \ 

531 
\ ==> NC = NA & C = A"; 

532 
by (dtac lemma 1); 

533 
by (assume_tac 1); 

534 
by (REPEAT (etac exE 1)); 

535 
(*Duplicate the assumption*) 

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

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

538 
qed "unique_NB"; 

539 

540 

541 
(*If the encrypted message appears, and B has used Nonce NB, 

542 
then it originated with the Server!*) 

543 
goal thy 

544 
"!!evs. [ B ~: lost; B ~= Spy; evs : otway lost ] \ 

545 
\ ==> Crypt {NB, Key K} (shrK B) : parts (sees lost Spy evs) \ 

546 
\ > (ALL X'. Says B Server \ 

547 
\ {NA, Agent A, Agent B, X', \ 

548 
\ Crypt {NA, NB, Agent A, Agent B} (shrK B)} \ 

549 
\ : set_of_list evs \ 

550 
\ > Says Server B \ 

551 
\ {NA, Crypt {NA, Key K} (shrK A), \ 

552 
\ Crypt {NB, Key K} (shrK B)} \ 

553 
\ : set_of_list evs)"; 

2064  554 
by (parts_induct_tac 1); 
2048  555 
(*OR1: it cannot be a new Nonce, contradiction.*) 
556 
by (fast_tac (!claset addSIs [parts_insertI] 

557 
addSEs partsEs 

558 
addEs [Says_imp_old_nonces RS less_irrefl] 

559 
addss (!simpset)) 1); 

560 
(*OR3 and OR4*) (** LEVEL 5 **) 

561 
(*OR4*) 

562 
by (REPEAT (Safe_step_tac 2)); 

563 
br (Crypt_imp_OR2 RS exE) 2; 

564 
by (REPEAT (fast_tac (!claset addEs partsEs) 2)); 

565 
(*OR3*) (** LEVEL 8 **) 

566 
by (step_tac (!claset delrules [disjCI, impCE]) 1); 

567 
by (fast_tac (!claset delrules [conjI] (*stop splitup*)) 3); 

568 
by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj] 

569 
addSEs [MPair_parts] 

570 
addDs [unique_NB]) 2); 

571 
by (fast_tac (!claset addSEs [MPair_parts] 

572 
addSDs [Says_imp_sees_Spy RS parts.Inj] 

573 
addSEs [no_nonce_OR1_OR2 RSN (2, rev_notE)] 

574 
delrules [conjI, impCE] (*stop splitup*)) 1); 

575 
qed_spec_mp "NB_Crypt_imp_Server_msg"; 

576 

577 

578 
(*Guarantee for B: if it gets a message with matching NB then the Server 

579 
has sent the correct message.*) 

580 
goal thy 

581 
"!!evs. [ B ~: lost; B ~= Spy; evs : otway lost; \ 

582 
\ Says S B {NA, X, Crypt {NB, Key K} (shrK B)} \ 

583 
\ : set_of_list evs; \ 

584 
\ Says B Server {NA, Agent A, Agent B, X', \ 

585 
\ Crypt {NA, NB, Agent A, Agent B} \ 

586 
\ (shrK B)} \ 

587 
\ : set_of_list evs ] \ 

588 
\ ==> Says Server B \ 

589 
\ {NA, \ 

590 
\ Crypt {NA, Key K} (shrK A), \ 

591 
\ Crypt {NB, Key K} (shrK B)} \ 

592 
\ : set_of_list evs"; 

593 
by (fast_tac (!claset addSIs [NB_Crypt_imp_Server_msg] 

594 
addEs partsEs 

595 
addDs [Says_imp_sees_Spy RS parts.Inj]) 1); 

2064  596 
qed "B_trust_OR3"; 
2048  597 

598 

2064  599 
B_trust_OR3 RS Spy_not_see_encrypted_key; 
2048  600 

601 

2026
0df5a96bf77e
Last working version prior to introduction of "lost"
paulson
parents:
2014
diff
changeset

602 
(** A session key uniquely identifies a pair of senders in the message 
2048  603 
encrypted by a good agent C. NEEDED? INTERESTING?**) 
1945  604 
goal thy 
2032  605 
"!!evs. evs : otway lost ==> \ 
2135  606 
\ EX A B. ALL C N. \ 
607 
\ C ~: lost > \ 

608 
\ Crypt {N, Key K} (shrK C) : parts (sees lost Spy evs) > \ 

2026
0df5a96bf77e
Last working version prior to introduction of "lost"
paulson
parents:
2014
diff
changeset

609 
\ C=A  C=B"; 
2032  610 
by (Simp_tac 1); (*Miniscoping*) 
611 
by (etac otway.induct 1); 

2064  612 
by analz_Fake_tac; 
2032  613 
(*spy_analz_tac just does not work here: it is an entirely different proof!*) 
1945  614 
by (ALLGOALS 
2026
0df5a96bf77e
Last working version prior to introduction of "lost"
paulson
parents:
2014
diff
changeset

615 
(asm_simp_tac (!simpset addsimps [all_conj_distrib, ex_disj_distrib, 
2134  616 
imp_conjR, parts_insert_sees, 
2032  617 
parts_insert2]))); 
1945  618 
by (REPEAT_FIRST (etac exE)); 
2026
0df5a96bf77e
Last working version prior to introduction of "lost"
paulson
parents:
2014
diff
changeset

619 
(*OR3: extraction of K = newK evsa to global context...*) (** LEVEL 6 **) 
2064  620 
by (expand_case_tac "K = ?y" 4); 
621 
by (REPEAT (ares_tac [exI] 5)); 

1945  622 
(*...we prove this case by contradiction: the key is too new!*) 
2026
0df5a96bf77e
Last working version prior to introduction of "lost"
paulson
parents:
2014
diff
changeset

623 
by (fast_tac (!claset addSEs partsEs 
2032  624 
addEs [Says_imp_old_keys RS less_irrefl] 
625 
addss (!simpset)) 4); 

2026
0df5a96bf77e
Last working version prior to introduction of "lost"
paulson
parents:
2014
diff
changeset

626 
(*Base, Fake, OR2, OR4*) 
0df5a96bf77e
Last working version prior to introduction of "lost"
paulson
parents:
2014
diff
changeset

627 
by (REPEAT_FIRST ex_strip_tac); 
2032  628 
by (dtac synth.Inj 4); 
629 
by (dtac synth.Inj 3); 

2026
0df5a96bf77e
Last working version prior to introduction of "lost"
paulson
parents:
2014
diff
changeset

630 
(*Now in effect there are three Fake cases*) 
0df5a96bf77e
Last working version prior to introduction of "lost"
paulson
parents:
2014
diff
changeset

631 
by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs Fake_parts_insert] 
2032  632 
delrules [disjCI, disjE] 
633 
addss (!simpset)))); 

2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

634 
qed "key_identifies_senders"; 