author  paulson 
Thu, 08 Jan 1998 18:10:34 +0100  
changeset 4537  4e835bd9fada 
parent 4509  828148415197 
child 4598  649bf14debe7 
permissions  rwrr 
2090  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 

8 
Simplified version with minimal encryption but explicit messages 

9 

10 
From page 11 of 

11 
Abadi and Needham. Prudent Engineering Practice for Cryptographic Protocols. 

12 
IEEE Trans. SE 22 (1), 1996 

13 
*) 

14 

15 
open OtwayRees_AN; 

16 

4449  17 
set proof_timing; 
2090  18 
HOL_quantifiers := false; 
19 

4470  20 
AddEs spies_partsEs; 
21 
AddDs [impOfSubs analz_subset_parts]; 

22 
AddDs [impOfSubs Fake_parts_insert]; 

23 

2090  24 

2331  25 
(*A "possibility property": there are traces that reach the end*) 
2090  26 
goal thy 
2331  27 
"!!A B. [ A ~= B; A ~= Server; B ~= Server ] \ 
3543  28 
\ ==> 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

29 
\ Says B A (Crypt (shrK A) {Nonce NA, Agent A, Agent B, Key K}) \ 
3465  30 
\ : set evs"; 
2090  31 
by (REPEAT (resolve_tac [exI,bexI] 1)); 
32 
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:
2454
diff
changeset

33 
by possibility_tac; 
2090  34 
result(); 
35 

36 

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

38 

39 
(*Nobody sends themselves messages*) 

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

40 
goal thy "!!evs. evs : otway ==> ALL A X. Says A A X ~: set evs"; 
2090  41 
by (etac otway.induct 1); 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4470
diff
changeset

42 
by Auto_tac; 
2090  43 
qed_spec_mp "not_Says_to_self"; 
44 
Addsimps [not_Says_to_self]; 

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

46 

47 

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

49 

3465  50 
goal thy "!!evs. Says S' B {X, Crypt(shrK B) X'} : set evs ==> \ 
3683  51 
\ X : analz (spies evs)"; 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4470
diff
changeset

52 
by (dtac (Says_imp_spies RS analz.Inj) 1); 
4470  53 
by (Blast_tac 1); 
3683  54 
qed "OR4_analz_spies"; 
2090  55 

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

56 
goal thy "!!evs. Says Server B {X, Crypt K' {NB, a, Agent B, K}} \ 
3683  57 
\ : set evs ==> K : parts (spies evs)"; 
4470  58 
by (Blast_tac 1); 
3683  59 
qed "Oops_parts_spies"; 
2090  60 

3683  61 
bind_thm ("OR4_parts_spies", 
62 
OR4_analz_spies RS (impOfSubs analz_subset_parts)); 

2090  63 

3683  64 
(*For proving the easier theorems about X ~: parts (spies evs).*) 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

65 
fun parts_induct_tac i = 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

66 
etac otway.induct i THEN 
3683  67 
forward_tac [Oops_parts_spies] (i+6) THEN 
68 
forward_tac [OR4_parts_spies] (i+5) THEN 

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

69 
prove_simple_subgoals_tac i; 
2090  70 

71 

3683  72 
(** Theorems of the form X ~: parts (spies evs) imply that NOBODY 
2090  73 
sends messages containing X! **) 
74 

4537
4e835bd9fada
Expressed most Oops rules using Notes instead of Says, and other tidying
paulson
parents:
4509
diff
changeset

75 
(*Spy never sees a good agent's shared key!*) 
2090  76 
goal thy 
3683  77 
"!!evs. evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)"; 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

78 
by (parts_induct_tac 1); 
3961  79 
by (ALLGOALS Blast_tac); 
2131  80 
qed "Spy_see_shrK"; 
81 
Addsimps [Spy_see_shrK]; 

2090  82 

2131  83 
goal thy 
3683  84 
"!!evs. evs : otway ==> (Key (shrK A) : analz (spies evs)) = (A : bad)"; 
4091  85 
by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset())); 
2131  86 
qed "Spy_analz_shrK"; 
87 
Addsimps [Spy_analz_shrK]; 

2090  88 

4470  89 
AddSDs [Spy_see_shrK RSN (2, rev_iffD1), 
90 
Spy_analz_shrK RSN (2, rev_iffD1)]; 

2090  91 

92 

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

93 
(*Nobody can have used nonexistent keys!*) 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

94 
goal thy "!!evs. evs : otway ==> \ 
3683  95 
\ Key K ~: used evs > K ~: keysFor (parts (spies evs))"; 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

97 
(*Fake*) 
4509
828148415197
Making proofs faster, especially using keysFor_parts_insert
paulson
parents:
4477
diff
changeset

98 
by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

99 
(*OR3*) 
3102  100 
by (Blast_tac 1); 
2160  101 
qed_spec_mp "new_keys_not_used"; 
2090  102 

103 
bind_thm ("new_keys_not_analzd", 

104 
[analz_subset_parts RS keysFor_mono, 

105 
new_keys_not_used] MRS contra_subsetD); 

106 

107 
Addsimps [new_keys_not_used, new_keys_not_analzd]; 

108 

109 

110 

111 
(*** Proofs involving analz ***) 

112 

2131  113 
(*Describes the form of K and NA when the Server sends this message.*) 
2090  114 
goal thy 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

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

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

117 
\ Crypt (shrK B) {NB, Agent A, Agent B, Key K}} \ 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

118 
\ : set evs; \ 
3543  119 
\ evs : otway ] \ 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

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

3102  123 
by (ALLGOALS Asm_simp_tac); 
124 
by (Blast_tac 1); 

2131  125 
qed "Says_Server_message_form"; 
2090  126 

127 

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

128 
(*For proofs involving analz.*) 
3683  129 
val analz_spies_tac = 
130 
dtac OR4_analz_spies 6 THEN 

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

131 
forward_tac [Says_Server_message_form] 7 THEN 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

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

133 
REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7); 
2090  134 

135 

136 
(**** 

137 
The following is to prove theorems of the form 

138 

3683  139 
Key K : analz (insert (Key KAB) (spies evs)) ==> 
140 
Key K : analz (spies evs) 

2090  141 

142 
A more general formula must be proved inductively. 

143 
****) 

144 

145 

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

147 

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

149 
goal thy 

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

150 
"!!evs. evs : otway ==> \ 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

151 
\ ALL K KK. KK <= Compl (range shrK) > \ 
3683  152 
\ (Key K : analz (Key``KK Un (spies evs))) = \ 
153 
\ (K : KK  Key K : analz (spies evs))"; 

2090  154 
by (etac otway.induct 1); 
3683  155 
by analz_spies_tac; 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

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

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

158 
by (ALLGOALS (asm_simp_tac analz_image_freshK_ss)); 
3451
d10f100676d8
Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents:
3207
diff
changeset

159 
(*Fake*) 
4422
21238c9d363e
Simplified proofs using rewrites for f``A where f is injective
paulson
parents:
4155
diff
changeset

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

161 
qed_spec_mp "analz_image_freshK"; 
2090  162 

163 

164 
goal thy 

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

165 
"!!evs. [ evs : otway; KAB ~: range shrK ] ==> \ 
3683  166 
\ Key K : analz (insert (Key KAB) (spies evs)) = \ 
167 
\ (K = KAB  Key K : analz (spies evs))"; 

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

168 
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:
2454
diff
changeset

169 
qed "analz_insert_freshK"; 
2090  170 

171 

4155  172 
(*** The Key K uniquely identifies the Server's message. **) 
2090  173 

174 
goal thy 

3543  175 
"!!evs. evs : otway ==> \ 
176 
\ EX A' B' NA' NB'. ALL A B NA NB. \ 

177 
\ Says Server B \ 

3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

178 
\ {Crypt (shrK A) {NA, Agent A, Agent B, K}, \ 
3465  179 
\ Crypt (shrK B) {NB, Agent A, Agent B, K}} : set evs \ 
2090  180 
\ > A=A' & B=B' & NA=NA' & NB=NB'"; 
181 
by (etac otway.induct 1); 

4091  182 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); 
3730  183 
by (ALLGOALS Clarify_tac); 
2090  184 
(*Remaining cases: OR3 and OR4*) 
185 
by (ex_strip_tac 2); 

3102  186 
by (Blast_tac 2); 
2090  187 
by (expand_case_tac "K = ?y" 1); 
188 
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:
2454
diff
changeset

189 
(*...we assume X is a recent message and handle this case by contradiction*) 
4509
828148415197
Making proofs faster, especially using keysFor_parts_insert
paulson
parents:
4477
diff
changeset

190 
by (blast_tac (claset() addSEs spies_partsEs) 1); 
2090  191 
val lemma = result(); 
192 

193 

194 
goal thy 

195 
"!!evs. [ Says Server B \ 

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

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

197 
\ Crypt (shrK B) {NB, Agent A, Agent B, K}} \ 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

198 
\ : set evs; \ 
2090  199 
\ Says Server B' \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

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

201 
\ Crypt (shrK B') {NB', Agent A', Agent B', K}} \ 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

202 
\ : set evs; \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

203 
\ evs : otway ] \ 
2090  204 
\ ==> A=A' & B=B' & NA=NA' & NB=NB'"; 
2417  205 
by (prove_unique_tac lemma 1); 
2090  206 
qed "unique_session_keys"; 
207 

208 

209 

210 
(**** Authenticity properties relating to NA ****) 

211 

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

213 
goal thy 

3683  214 
"!!evs. [ A ~: bad; evs : otway ] \ 
215 
\ ==> Crypt (shrK A) {NA, Agent A, Agent B, Key K} : parts (spies evs) \ 

2331  216 
\ > (EX NB. Says Server B \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

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

218 
\ Crypt (shrK B) {NB, Agent A, Agent B, Key K}} \ 
3465  219 
\ : set evs)"; 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

220 
by (parts_induct_tac 1); 
4470  221 
by (Blast_tac 1); 
4091  222 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib]))); 
2090  223 
(*OR3*) 
3102  224 
by (Blast_tac 1); 
2090  225 
qed_spec_mp "NA_Crypt_imp_Server_msg"; 
226 

227 

2454  228 
(*Corollary: if A receives B's OR4 message then it originated with the Server. 
229 
Freshness may be inferred from nonce NA.*) 

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

231 
"!!evs. [ Says B' A (Crypt (shrK A) {NA, Agent A, Agent B, Key K}) \ 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

232 
\ : set evs; \ 
3683  233 
\ A ~: bad; evs : otway ] \ 
2090  234 
\ ==> EX NB. Says Server B \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

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

236 
\ Crypt (shrK B) {NB, Agent A, Agent B, Key K}} \ 
3465  237 
\ : set evs"; 
4470  238 
by (blast_tac (claset() addSIs [NA_Crypt_imp_Server_msg]) 1); 
2331  239 
qed "A_trusts_OR4"; 
2090  240 

241 

242 
(** Crucial secrecy property: Spy does not see the keys sent in msg OR3 

243 
Does not in itself guarantee security: an attack could violate 

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

245 

246 
goal thy 

4537
4e835bd9fada
Expressed most Oops rules using Notes instead of Says, and other tidying
paulson
parents:
4509
diff
changeset

247 
"!!evs. [ A ~: bad; B ~: bad; evs : otway ] \ 
3543  248 
\ ==> Says Server B \ 
249 
\ {Crypt (shrK A) {NA, Agent A, Agent B, Key K}, \ 

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

251 
\ : set evs > \ 

4537
4e835bd9fada
Expressed most Oops rules using Notes instead of Says, and other tidying
paulson
parents:
4509
diff
changeset

252 
\ Notes Spy {NA, NB, Key K} ~: set evs > \ 
3683  253 
\ Key K ~: analz (spies evs)"; 
2090  254 
by (etac otway.induct 1); 
3683  255 
by analz_spies_tac; 
2090  256 
by (ALLGOALS 
4091  257 
(asm_simp_tac (simpset() addcongs [conj_cong, if_weak_cong] 
4509
828148415197
Making proofs faster, especially using keysFor_parts_insert
paulson
parents:
4477
diff
changeset

258 
addsimps [analz_insert_eq, analz_insert_freshK] 
828148415197
Making proofs faster, especially using keysFor_parts_insert
paulson
parents:
4477
diff
changeset

259 
addsimps (pushes@expand_ifs)))); 
3451
d10f100676d8
Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents:
3207
diff
changeset

260 
(*Oops*) 
4091  261 
by (blast_tac (claset() addSDs [unique_session_keys]) 4); 
3451
d10f100676d8
Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents:
3207
diff
changeset

262 
(*OR4*) 
d10f100676d8
Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents:
3207
diff
changeset

263 
by (Blast_tac 3); 
2090  264 
(*OR3*) 
4470  265 
by (Blast_tac 2); 
3451
d10f100676d8
Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents:
3207
diff
changeset

266 
(*Fake*) 
d10f100676d8
Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents:
3207
diff
changeset

267 
by (spy_analz_tac 1); 
2090  268 
val lemma = result() RS mp RS mp RSN(2,rev_notE); 
269 

270 
goal thy 

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

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

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

273 
\ Crypt (shrK B) {NB, Agent A, Agent B, Key K}} \ 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

274 
\ : set evs; \ 
4537
4e835bd9fada
Expressed most Oops rules using Notes instead of Says, and other tidying
paulson
parents:
4509
diff
changeset

275 
\ Notes Spy {NA, NB, Key K} ~: set evs; \ 
4e835bd9fada
Expressed most Oops rules using Notes instead of Says, and other tidying
paulson
parents:
4509
diff
changeset

276 
\ A ~: bad; B ~: bad; evs : otway ] \ 
3683  277 
\ ==> Key K ~: analz (spies evs)"; 
2090  278 
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); 
4091  279 
by (blast_tac (claset() addSEs [lemma]) 1); 
2090  280 
qed "Spy_not_see_encrypted_key"; 
281 

282 

283 
(**** Authenticity properties relating to NB ****) 

284 

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

286 
goal thy 

3683  287 
"!!evs. [ B ~: bad; evs : otway ] \ 
288 
\ ==> Crypt (shrK B) {NB, Agent A, Agent B, Key K} : parts (spies evs) \ 

2090  289 
\ > (EX NA. Says Server B \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

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

291 
\ Crypt (shrK B) {NB, Agent A, Agent B, Key K}} \ 
3465  292 
\ : set evs)"; 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

293 
by (parts_induct_tac 1); 
4470  294 
by (Blast_tac 1); 
4091  295 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib]))); 
2090  296 
(*OR3*) 
3102  297 
by (Blast_tac 1); 
2090  298 
qed_spec_mp "NB_Crypt_imp_Server_msg"; 
299 

300 

2454  301 
(*Guarantee for B: if it gets a wellformed certificate then the Server 
302 
has sent the correct message in round 3.*) 

2090  303 
goal thy 
3683  304 
"!!evs. [ B ~: bad; evs : otway; \ 
2837
dee1c7f1f576
Trivial renamings (for consistency with CSFW papers)
paulson
parents:
2637
diff
changeset

305 
\ Says S' B {X, Crypt (shrK B) {NB, Agent A, Agent B, Key K}} \ 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

306 
\ : set evs ] \ 
2106  307 
\ ==> EX NA. Says Server B \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

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

309 
\ Crypt (shrK B) {NB, Agent A, Agent B, Key K}} \ 
3465  310 
\ : set evs"; 
4470  311 
by (blast_tac (claset() addSIs [NB_Crypt_imp_Server_msg]) 1); 
2331  312 
qed "B_trusts_OR3"; 