author  paulson 
Fri, 17 Jan 1997 12:49:31 +0100  
changeset 2516  4d68fbe6378b 
parent 2451  ce85a2aafc7a 
child 2637  e9b203f854ae 
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; 

19 

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

20 

2328  21 
(*A "possibility property": 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

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

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

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

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

27 
by (REPEAT (resolve_tac [exI,bexI] 1)); 
2032  28 
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

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

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

31 

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

32 

1941  33 
(**** Inductive proofs about otway ****) 
34 

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

35 
(*Monotonicity*) 
2032  36 
goal thy "!!evs. lost' <= lost ==> otway lost' <= otway lost"; 
37 
by (rtac subsetI 1); 

38 
by (etac otway.induct 1); 

39 
by (REPEAT_FIRST 

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

41 
:: otway.intrs)))); 

42 
qed "otway_mono"; 

43 

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

1941  47 
by (Auto_tac()); 
48 
qed_spec_mp "not_Says_to_self"; 

49 
Addsimps [not_Says_to_self]; 

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

51 

52 

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

54 

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

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

1941  59 

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

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

1941  64 

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

65 
goal thy "!!evs. Says Server B {NA, X, Crypt K' {NB,K}} : set_of_list evs \ 
2135  66 
\ ==> 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

67 
by (fast_tac (!claset addSEs sees_Spy_partsEs) 1); 
2135  68 
qed "Oops_parts_sees_Spy"; 
1941  69 

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

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

2032  73 
messages originate from the Spy. *) 
1964  74 

2032  75 
bind_thm ("OR2_parts_sees_Spy", 
76 
OR2_analz_sees_Spy RS (impOfSubs analz_subset_parts)); 

77 
bind_thm ("OR4_parts_sees_Spy", 

78 
OR4_analz_sees_Spy RS (impOfSubs analz_subset_parts)); 

79 

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

81 
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

82 
val parts_Fake_tac = 
2032  83 
let val tac = forw_inst_tac [("lost","lost")] 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

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

86 
tac Oops_parts_sees_Spy 7 
2032  87 
end; 
1941  88 

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

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

2171  92 
(*Fake message*) 
93 
TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts, 

94 
impOfSubs Fake_parts_insert] 

2064  95 
addss (!simpset)) 2)) THEN 
96 
(*Base case*) 

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

98 
ALLGOALS Asm_simp_tac) i; 

1941  99 

2032  100 
(** 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

101 
sends messages containing X! **) 
1941  102 

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

2064  107 
by (parts_induct_tac 1); 
1941  108 
by (Auto_tac()); 
2135  109 
qed "Spy_see_shrK"; 
110 
Addsimps [Spy_see_shrK]; 

1941  111 

2135  112 
goal thy 
113 
"!!evs. evs : otway lost \ 

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

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

116 
qed "Spy_analz_shrK"; 

117 
Addsimps [Spy_analz_shrK]; 

1941  118 

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

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

122 
qed "Spy_see_shrK_D"; 

1941  123 

2135  124 
bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D); 
125 
AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D]; 

1941  126 

127 

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

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

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

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

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

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

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

135 
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

136 
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

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

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

139 
by (REPEAT (fast_tac (!claset addss (!simpset)) 1)); 
2160  140 
qed_spec_mp "new_keys_not_used"; 
1941  141 

142 
bind_thm ("new_keys_not_analzd", 

2032  143 
[analz_subset_parts RS keysFor_mono, 
144 
new_keys_not_used] MRS contra_subsetD); 

1941  145 

146 
Addsimps [new_keys_not_used, new_keys_not_analzd]; 

147 

148 

2064  149 

150 
(*** Proofs involving analz ***) 

151 

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

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

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

156 
\ {NA, X, Crypt (shrK B) {NB, Key K}} : set_of_list evs; \ 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2417
diff
changeset

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

158 
\ ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)"; 
2135  159 
by (etac rev_mp 1); 
160 
by (etac otway.induct 1); 

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

162 
qed "Says_Server_message_form"; 

2064  163 

164 

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

166 
val analz_Fake_tac = 

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

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

2135  169 
forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

171 
REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7); 
1941  172 

173 

174 
(**** 

175 
The following is to prove theorems of the form 

176 

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

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

178 
Key K : analz (sees lost Spy evs) 
1941  179 

180 
A more general formula must be proved inductively. 

181 
****) 

182 

183 

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

185 

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

186 
(*The equality makes the induction hypothesis easier to apply*) 
1941  187 
goal thy 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

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

190 
\ (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

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

194 
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

195 
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

196 
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

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

198 
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

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

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

201 
qed_spec_mp "analz_image_freshK"; 
1941  202 

203 

204 
goal thy 

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

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

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

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

208 
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

209 
qed "analz_insert_freshK"; 
1941  210 

211 

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

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

213 

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

214 
goal thy 
2135  215 
"!!evs. evs : otway lost ==> \ 
216 
\ 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

217 
\ Says Server B {NA, X, Crypt (shrK B) {NB, K}} : set_of_list evs > \ 
2135  218 
\ B=B' & NA=NA' & NB=NB' & X=X'"; 
2032  219 
by (etac otway.induct 1); 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

220 
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

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

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

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

224 
by (Fast_tac 2); 
2064  225 
by (expand_case_tac "K = ?y" 1); 
226 
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

227 
(*...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

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

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

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

232 

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

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

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

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

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

237 
\ : set_of_list evs; \ 
2135  238 
\ evs : otway lost ] ==> X=X' & B=B' & NA=NA' & NB=NB'"; 
2417  239 
by (prove_unique_tac lemma 1); 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

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

241 

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

242 

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

243 

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

245 

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

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

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

249 
\ ==> Crypt (shrK A) {NA, Agent A, Agent B} \ 
2064  250 
\ : parts (sees lost Spy evs) > \ 
251 
\ 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

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

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

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

256 

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

257 

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

259 

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

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

262 
\ ==> EX B'. ALL B. \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

263 
\ Crypt (shrK A) {NA, Agent A, Agent B} : parts (sees lost Spy evs) \ 
2048  264 
\ > B = B'"; 
2064  265 
by (parts_induct_tac 1); 
266 
by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 

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

267 
(*OR1: creation of new Nonce. Move assertion into global context*) 
2064  268 
by (expand_case_tac "NA = ?y" 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

269 
by (best_tac (!claset addSEs sees_Spy_partsEs) 1); 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

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

271 

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

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

273 
"!!evs.[ Crypt (shrK A) {NA, Agent A, Agent B}: parts(sees lost Spy evs); \ 
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

274 
\ Crypt (shrK A) {NA, Agent A, Agent C}: parts(sees lost Spy evs); \ 
2048  275 
\ evs : otway lost; A ~: lost ] \ 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

276 
\ ==> B = C"; 
2417  277 
by (prove_unique_tac lemma 1); 
2048  278 
qed "unique_NA"; 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

279 

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

280 

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

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

282 
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

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

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

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

288 
\ Crypt (shrK A) {NA', NA, Agent A', Agent A} \ 
2032  289 
\ ~: 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

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

291 
by (REPEAT (fast_tac (!claset addSEs sees_Spy_partsEs 
2026
0df5a96bf77e
Last working version prior to introduction of "lost"
paulson
parents:
2014
diff
changeset

292 
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

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

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

295 

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

296 

2053  297 
(*Crucial property: If the encrypted message appears, and A has used NA 
298 
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

299 
goal thy 
2048  300 
"!!evs. [ A ~: lost; A ~= Spy; evs : otway lost ] \ 
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} : parts (sees lost Spy evs) \ 
2048  302 
\ > 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

303 
\ Crypt (shrK A) {NA, Agent A, Agent B}} \ 
2048  304 
\ : set_of_list evs > \ 
305 
\ (EX NB. Says Server B \ 

306 
\ {NA, \ 

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

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

308 
\ Crypt (shrK B) {NB, Key K}} \ 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

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

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

312 
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

313 
addSEs sees_Spy_partsEs 
2032  314 
addss (!simpset)) 1); 
2064  315 
(*OR3 and OR4*) 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

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

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

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

319 
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

320 
addEs sees_Spy_partsEs) 2); 
2064  321 
(*OR3*) (** LEVEL 5 **) 
322 
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

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

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

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

329 
addSEs [MPair_parts] 

330 
addEs [unique_NA]) 1); 

331 
qed_spec_mp "NA_Crypt_imp_Server_msg"; 

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

332 

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

333 

2053  334 
(*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

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

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

339 
"!!evs. [ Says B' A {NA, Crypt (shrK A) {NA, Key K}} \ 
2053  340 
\ : set_of_list evs; \ 
341 
\ 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

342 
\ Crypt (shrK A) {NA, Agent A, Agent B}} \ 
2053  343 
\ : set_of_list evs; \ 
344 
\ A ~: lost; A ~= Spy; evs : otway lost ] \ 

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

2048  346 
\ {NA, \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

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

348 
\ Crypt (shrK B) {NB, Key K}} \ 
2053  349 
\ : set_of_list evs"; 
2048  350 
by (fast_tac (!claset addSIs [NA_Crypt_imp_Server_msg] 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

351 
addEs sees_Spy_partsEs) 1); 
2328  352 
qed "A_trusts_OR4"; 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

353 

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

354 

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

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

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

358 

1941  359 
goal thy 
2166  360 
"!!evs. [ A ~: lost; B ~: lost; evs : otway lost ] \ 
2048  361 
\ ==> Says Server B \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

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

363 
\ Crypt (shrK B) {NB, Key K}} : set_of_list evs > \ 
2135  364 
\ Says B Spy {NA, NB, Key K} ~: set_of_list evs > \ 
2048  365 
\ Key K ~: analz (sees lost Spy evs)"; 
2032  366 
by (etac otway.induct 1); 
2064  367 
by analz_Fake_tac; 
1964  368 
by (ALLGOALS 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

370 
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

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

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

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

375 
addIs [impOfSubs analz_subset_parts] 
2048  376 
addss (!simpset addsimps [parts_insert2])) 3); 
2135  377 
(*OR4, OR2, Fake*) 
2375  378 
by (REPEAT_FIRST spy_analz_tac); 
2135  379 
(*Oops*) (** LEVEL 5 **) 
380 
by (fast_tac (!claset delrules [disjE] 

2171  381 
addDs [unique_session_keys] addss (!simpset)) 1); 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

382 
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

383 

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

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

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

386 
\ {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

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

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

390 
\ ==> Key K ~: analz (sees lost Spy evs)"; 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

391 
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

392 
by (fast_tac (!claset addSEs [lemma]) 1); 
2032  393 
qed "Spy_not_see_encrypted_key"; 
394 

1945  395 

2032  396 
goal thy 
2048  397 
"!!evs. [ C ~: {A,B,Server}; \ 
398 
\ Says Server B \ 

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

399 
\ {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

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

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

403 
\ ==> Key K ~: analz (sees lost C evs)"; 
2032  404 
by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1); 
405 
by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1); 

406 
by (FIRSTGOAL (rtac Spy_not_see_encrypted_key)); 

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

408 
qed "Agent_not_see_encrypted_key"; 

1945  409 

410 

2048  411 
(**** Authenticity properties relating to NB ****) 
412 

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

2194
63a68a3a8a76
Removal of an obsolete result, and authentication of
paulson
parents:
2171
diff
changeset

414 
know anything about X: it does NOT have to have the right form.*) 
2048  415 
goal thy 
416 
"!!evs. [ B ~: lost; evs : otway lost ] \ 

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

417 
\ ==> Crypt (shrK B) {NA, NB, Agent A, Agent B} \ 
2048  418 
\ : parts (sees lost Spy evs) > \ 
2194
63a68a3a8a76
Removal of an obsolete result, and authentication of
paulson
parents:
2171
diff
changeset

419 
\ (EX X. Says B Server \ 
63a68a3a8a76
Removal of an obsolete result, and authentication of
paulson
parents:
2171
diff
changeset

420 
\ {NA, Agent A, Agent B, X, \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

421 
\ Crypt (shrK B) {NA, NB, Agent A, Agent B}} \ 
2048  422 
\ : set_of_list evs)"; 
2064  423 
by (parts_induct_tac 1); 
424 
by (auto_tac (!claset, !simpset addcongs [conj_cong])); 

2194
63a68a3a8a76
Removal of an obsolete result, and authentication of
paulson
parents:
2171
diff
changeset

425 
bind_thm ("Crypt_imp_OR2", result() RSN (2,rev_mp) RS exE); 
2048  426 

427 

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

429 

430 
goal thy 

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

2064  432 
\ ==> EX NA' A'. ALL NA A. \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

433 
\ Crypt (shrK B) {NA, NB, Agent A, Agent B} : parts(sees lost Spy evs) \ 
2048  434 
\ > NA = NA' & A = A'"; 
2064  435 
by (parts_induct_tac 1); 
436 
by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 

2048  437 
(*OR2: creation of new Nonce. Move assertion into global context*) 
2064  438 
by (expand_case_tac "NB = ?y" 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

439 
by (deepen_tac (!claset addSEs sees_Spy_partsEs) 3 1); 
2048  440 
val lemma = result(); 
441 

442 
goal thy 

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

443 
"!!evs.[ Crypt (shrK B) {NA, NB, Agent A, Agent B} \ 
2048  444 
\ : parts(sees lost Spy evs); \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

445 
\ Crypt (shrK B) {NC, NB, Agent C, Agent B} \ 
2048  446 
\ : parts(sees lost Spy evs); \ 
447 
\ evs : otway lost; B ~: lost ] \ 

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

2417  449 
by (prove_unique_tac lemma 1); 
2048  450 
qed "unique_NB"; 
451 

452 

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

454 
then it originated with the Server!*) 

455 
goal thy 

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

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

457 
\ ==> Crypt (shrK B) {NB, Key K} : parts (sees lost Spy evs) \ 
2048  458 
\ > (ALL X'. Says B Server \ 
459 
\ {NA, Agent A, Agent B, X', \ 

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

460 
\ Crypt (shrK B) {NA, NB, Agent A, Agent B}} \ 
2048  461 
\ : set_of_list evs \ 
462 
\ > Says Server B \ 

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

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

464 
\ Crypt (shrK B) {NB, Key K}} \ 
2048  465 
\ : set_of_list evs)"; 
2064  466 
by (parts_induct_tac 1); 
2048  467 
(*OR1: it cannot be a new Nonce, contradiction.*) 
468 
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

469 
addSEs sees_Spy_partsEs 
2048  470 
addss (!simpset)) 1); 
471 
(*OR4*) 

2194
63a68a3a8a76
Removal of an obsolete result, and authentication of
paulson
parents:
2171
diff
changeset

472 
by (fast_tac (!claset addSEs [MPair_parts, Crypt_imp_OR2]) 2); 
63a68a3a8a76
Removal of an obsolete result, and authentication of
paulson
parents:
2171
diff
changeset

473 
(*OR3*) 
2048  474 
by (step_tac (!claset delrules [disjCI, impCE]) 1); 
475 
by (fast_tac (!claset delrules [conjI] (*stop splitup*)) 3); 

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

477 
addSEs [MPair_parts] 

478 
addDs [unique_NB]) 2); 

479 
by (fast_tac (!claset addSEs [MPair_parts] 

480 
addSDs [Says_imp_sees_Spy RS parts.Inj] 

481 
addSEs [no_nonce_OR1_OR2 RSN (2, rev_notE)] 

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

483 
qed_spec_mp "NB_Crypt_imp_Server_msg"; 

484 

485 

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

487 
has sent the correct message.*) 

488 
goal thy 

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

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

490 
\ Says S B {NA, X, Crypt (shrK B) {NB, Key K}} \ 
2048  491 
\ : set_of_list evs; \ 
492 
\ Says B Server {NA, Agent A, Agent B, X', \ 

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

493 
\ Crypt (shrK B) {NA, NB, Agent A, Agent B} } \ 
2048  494 
\ : set_of_list evs ] \ 
495 
\ ==> Says Server B \ 

496 
\ {NA, \ 

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

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

498 
\ Crypt (shrK B) {NB, Key K}} \ 
2048  499 
\ : set_of_list evs"; 
500 
by (fast_tac (!claset addSIs [NB_Crypt_imp_Server_msg] 

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

501 
addEs sees_Spy_partsEs) 1); 
2328  502 
qed "B_trusts_OR3"; 
2048  503 

504 

2328  505 
B_trusts_OR3 RS Spy_not_see_encrypted_key; 
2048  506 

507 

1945  508 
goal thy 
2214  509 
"!!evs. [ B ~: lost; evs : otway lost ] \ 
510 
\ ==> Says Server B \ 

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

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

512 
\ Crypt (shrK B) {NB, Key K}} : set_of_list evs > \ 
2214  513 
\ (EX X. Says B Server {NA, Agent A, Agent B, X, \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

514 
\ Crypt (shrK B) {NA, NB, Agent A, Agent B} } \ 
2194
63a68a3a8a76
Removal of an obsolete result, and authentication of
paulson
parents:
2171
diff
changeset

515 
\ : set_of_list evs)"; 
2032  516 
by (etac otway.induct 1); 
2194
63a68a3a8a76
Removal of an obsolete result, and authentication of
paulson
parents:
2171
diff
changeset

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

518 
by (dtac (Says_imp_sees_Spy RS parts.Inj) 1); 
2194
63a68a3a8a76
Removal of an obsolete result, and authentication of
paulson
parents:
2171
diff
changeset

519 
by (fast_tac (!claset addSEs [MPair_parts, Crypt_imp_OR2]) 1); 
63a68a3a8a76
Removal of an obsolete result, and authentication of
paulson
parents:
2171
diff
changeset

520 
bind_thm ("OR3_imp_OR2", result() RSN (2,rev_mp) RS exE); 
63a68a3a8a76
Removal of an obsolete result, and authentication of
paulson
parents:
2171
diff
changeset

521 

63a68a3a8a76
Removal of an obsolete result, and authentication of
paulson
parents:
2171
diff
changeset

522 

63a68a3a8a76
Removal of an obsolete result, and authentication of
paulson
parents:
2171
diff
changeset

523 
(*After getting and checking OR4, agent A can trust that B has been active. 
63a68a3a8a76
Removal of an obsolete result, and authentication of
paulson
parents:
2171
diff
changeset

524 
We could probably prove that X has the expected form, but that is not 
63a68a3a8a76
Removal of an obsolete result, and authentication of
paulson
parents:
2171
diff
changeset

525 
strictly necessary for authentication.*) 
63a68a3a8a76
Removal of an obsolete result, and authentication of
paulson
parents:
2171
diff
changeset

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

527 
"!!evs. [ Says B' A {NA, Crypt (shrK A) {NA, Key K}} \ 
2194
63a68a3a8a76
Removal of an obsolete result, and authentication of
paulson
parents:
2171
diff
changeset

528 
\ : set_of_list evs; \ 
63a68a3a8a76
Removal of an obsolete result, and authentication of
paulson
parents:
2171
diff
changeset

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

530 
\ Crypt (shrK A) {NA, Agent A, Agent B}} \ 
2194
63a68a3a8a76
Removal of an obsolete result, and authentication of
paulson
parents:
2171
diff
changeset

531 
\ : set_of_list evs; \ 
63a68a3a8a76
Removal of an obsolete result, and authentication of
paulson
parents:
2171
diff
changeset

532 
\ A ~: lost; A ~= Spy; B ~: lost; evs : otway lost ] \ 
63a68a3a8a76
Removal of an obsolete result, and authentication of
paulson
parents:
2171
diff
changeset

533 
\ ==> EX NB X. Says B Server {NA, Agent A, Agent B, X, \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

534 
\ Crypt (shrK B) {NA, NB, Agent A, Agent B} }\ 
2194
63a68a3a8a76
Removal of an obsolete result, and authentication of
paulson
parents:
2171
diff
changeset

535 
\ : set_of_list evs"; 
2328  536 
by (fast_tac (!claset addSDs [A_trusts_OR4] 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

537 
addSEs [OR3_imp_OR2]) 1); 
2194
63a68a3a8a76
Removal of an obsolete result, and authentication of
paulson
parents:
2171
diff
changeset

538 
qed "A_auths_B"; 