author  paulson 
Thu, 12 Apr 2001 12:45:05 +0200  
changeset 11251  a6816d47f41d 
parent 11185  1b737b4c2108 
child 11655  923e4d0d36d5 
permissions  rwrr 
3445  1 
(* Title: HOL/Auth/Yahalom2 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

2 
ID: $Id$ 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

4 
Copyright 1996 University of Cambridge 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

5 

81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

6 
Inductive relation "yahalom" for the Yahalom protocol, Variant 2. 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

7 

81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

8 
This version trades encryption of NB for additional explicitness in YM3. 
3432  9 
Also in YM3, care is taken to make the two certificates distinct. 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

10 

81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

11 
From page 259 of 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

12 
Burrows, Abadi and Needham. A Logic of Authentication. 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

13 
Proc. Royal Soc. 426 (1989) 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

14 
*) 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

15 

11251  16 
theory Yahalom2 = Shared: 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

17 

11251  18 
consts yahalom :: "event list set" 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3481
diff
changeset

19 
inductive "yahalom" 
11251  20 
intros 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

21 
(*Initial trace is empty*) 
11251  22 
Nil: "[] \<in> yahalom" 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

23 

81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

24 
(*The spy MAY say anything he CAN say. We do not expect him to 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

25 
invent new nonces here, but he can also use NS1. Common to 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

26 
all similar protocols.*) 
11251  27 
Fake: "[ evsf \<in> yahalom; X \<in> synth (analz (knows Spy evsf)) ] 
28 
==> Says Spy B X # evsf \<in> yahalom" 

2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

29 

6335  30 
(*A message that has been sent can be received by the 
31 
intended recipient.*) 

11251  32 
Reception: "[ evsr \<in> yahalom; Says A B X \<in> set evsr ] 
33 
==> Gets B X # evsr \<in> yahalom" 

6335  34 

2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

35 
(*Alice initiates a protocol run*) 
11251  36 
YM1: "[ evs1 \<in> yahalom; Nonce NA \<notin> used evs1 ] 
37 
==> Says A B {Agent A, Nonce NA} # evs1 \<in> yahalom" 

2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

38 

6335  39 
(*Bob's response to Alice's message.*) 
11251  40 
YM2: "[ evs2 \<in> yahalom; Nonce NB \<notin> used evs2; 
41 
Gets B {Agent A, Nonce NA} \<in> set evs2 ] 

42 
==> Says B Server 

3432  43 
{Agent B, Nonce NB, Crypt (shrK B) {Agent A, Nonce NA}} 
11251  44 
# evs2 \<in> yahalom" 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

45 

81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

46 
(*The Server receives Bob's message. He responds by sending a 
3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

47 
new session key to Alice, with a certificate for forwarding to Bob. 
5066
30271d90644f
Changed format of Bob's certificate from Nb,K,A to A,B,K,Nb.
paulson
parents:
4537
diff
changeset

48 
Both agents are quoted in the 2nd certificate to prevent attacks!*) 
11251  49 
YM3: "[ evs3 \<in> yahalom; Key KAB \<notin> used evs3; 
6335  50 
Gets Server {Agent B, Nonce NB, 
51 
Crypt (shrK B) {Agent A, Nonce NA}} 

11251  52 
\<in> set evs3 ] 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

53 
==> Says Server A 
11251  54 
{Nonce NB, 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

55 
Crypt (shrK A) {Agent B, Key KAB, Nonce NA}, 
5066
30271d90644f
Changed format of Bob's certificate from Nb,K,A to A,B,K,Nb.
paulson
parents:
4537
diff
changeset

56 
Crypt (shrK B) {Agent A, Agent B, Key KAB, Nonce NB}} 
11251  57 
# evs3 \<in> yahalom" 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

58 

81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

59 
(*Alice receives the Server's (?) message, checks her Nonce, and 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

60 
uses the new session key to send Bob his Nonce.*) 
11251  61 
YM4: "[ evs4 \<in> yahalom; 
6335  62 
Gets A {Nonce NB, Crypt (shrK A) {Agent B, Key K, Nonce NA}, 
11251  63 
X} \<in> set evs4; 
64 
Says A B {Agent A, Nonce NA} \<in> set evs4 ] 

65 
==> Says A B {X, Crypt K (Nonce NB)} # evs4 \<in> yahalom" 

2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

66 

2155  67 
(*This message models possible leaks of session keys. The nonces 
68 
identify the protocol run. Quoting Server here ensures they are 

69 
correct. *) 

11251  70 
Oops: "[ evso \<in> yahalom; 
71 
Says Server A {Nonce NB, 

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

72 
Crypt (shrK A) {Agent B, Key K, Nonce NA}, 
11251  73 
X} \<in> set evso ] 
74 
==> Notes Spy {Nonce NA, Nonce NB, Key K} # evso \<in> yahalom" 

75 

76 

77 
declare Says_imp_knows_Spy [THEN analz.Inj, dest] 

78 
declare parts.Body [dest] 

79 
declare Fake_parts_insert_in_Un [dest] 

80 
declare analz_into_parts [dest] 

81 

82 
(*A "possibility property": there are traces that reach the end*) 

83 
lemma "\<exists>X NB K. \<exists>evs \<in> yahalom. 

84 
Says A B {X, Crypt K (Nonce NB)} \<in> set evs" 

85 
apply (intro exI bexI) 

86 
apply (rule_tac [2] yahalom.Nil 

87 
[THEN yahalom.YM1, THEN yahalom.Reception, 

88 
THEN yahalom.YM2, THEN yahalom.Reception, 

89 
THEN yahalom.YM3, THEN yahalom.Reception, 

90 
THEN yahalom.YM4]) 

91 
apply possibility 

92 
done 

93 

94 
lemma Gets_imp_Says: 

95 
"[ Gets B X \<in> set evs; evs \<in> yahalom ] ==> \<exists>A. Says A B X \<in> set evs" 

96 
by (erule rev_mp, erule yahalom.induct, auto) 

97 

98 
(*Must be proved separately for each protocol*) 

99 
lemma Gets_imp_knows_Spy: 

100 
"[ Gets B X \<in> set evs; evs \<in> yahalom ] ==> X \<in> knows Spy evs" 

101 
by (blast dest!: Gets_imp_Says Says_imp_knows_Spy) 

102 

103 
declare Gets_imp_knows_Spy [THEN analz.Inj, dest] 

104 

105 

106 
(**** Inductive proofs about yahalom ****) 

107 

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

109 

110 
(*Lets us treat YM4 using a similar argument as for the Fake case.*) 

111 
lemma YM4_analz_knows_Spy: 

112 
"[ Gets A {NB, Crypt (shrK A) Y, X} \<in> set evs; evs \<in> yahalom ] 

113 
==> X \<in> analz (knows Spy evs)" 

114 
by blast 

115 

116 
lemmas YM4_parts_knows_Spy = 

117 
YM4_analz_knows_Spy [THEN analz_into_parts, standard] 

118 

119 

120 
(** Theorems of the form X \<notin> parts (knows Spy evs) imply that NOBODY 

121 
sends messages containing X! **) 

122 

123 
(*Spy never sees a good agent's shared key!*) 

124 
lemma Spy_see_shrK [simp]: 

125 
"evs \<in> yahalom ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)" 

126 
apply (erule yahalom.induct, force, 

127 
drule_tac [6] YM4_parts_knows_Spy, simp_all) 

128 
apply blast+ 

129 
done 

130 

131 
lemma Spy_analz_shrK [simp]: 

132 
"evs \<in> yahalom ==> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)" 

133 
by auto 

134 

135 
lemma Spy_see_shrK_D [dest!]: 

136 
"[Key (shrK A) \<in> parts (knows Spy evs); evs \<in> yahalom] ==> A \<in> bad" 

137 
by (blast dest: Spy_see_shrK) 

138 

139 
(*Nobody can have used nonexistent keys! Needed to apply analz_insert_Key*) 

140 
lemma new_keys_not_used [rule_format, simp]: 

141 
"evs \<in> yahalom ==> Key K \<notin> used evs > K \<notin> keysFor (parts (knows Spy evs))" 

142 
apply (erule yahalom.induct, force, 

143 
frule_tac [6] YM4_parts_knows_Spy, simp_all) 

144 
(*Fake, YM3, YM4*) 

145 
apply (blast dest!: keysFor_parts_insert)+ 

146 
done 

147 

148 

149 
(*Describes the form of K when the Server sends this message. Useful for 

150 
Oops as well as main secrecy property.*) 

151 
lemma Says_Server_message_form: 

152 
"[ Says Server A {nb', Crypt (shrK A) {Agent B, Key K, na}, X} 

153 
\<in> set evs; evs \<in> yahalom ] 

154 
==> K \<notin> range shrK" 

155 
by (erule rev_mp, erule yahalom.induct, simp_all) 

156 

157 

158 
(**** 

159 
The following is to prove theorems of the form 

160 

161 
Key K \<in> analz (insert (Key KAB) (knows Spy evs)) ==> 

162 
Key K \<in> analz (knows Spy evs) 

163 

164 
A more general formula must be proved inductively. 

165 
****) 

166 

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

168 

169 
lemma analz_image_freshK [rule_format]: 

170 
"evs \<in> yahalom ==> 

171 
\<forall>K KK. KK <=  (range shrK) > 

172 
(Key K \<in> analz (Key`KK Un (knows Spy evs))) = 

173 
(K \<in> KK  Key K \<in> analz (knows Spy evs))" 

174 
apply (erule yahalom.induct, force, frule_tac [7] Says_Server_message_form, 

175 
drule_tac [6] YM4_analz_knows_Spy) 

176 
apply analz_freshK 

177 
apply spy_analz 

178 
done 

179 

180 
lemma analz_insert_freshK: 

181 
"[ evs \<in> yahalom; KAB \<notin> range shrK ] ==> 

182 
Key K \<in> analz (insert (Key KAB) (knows Spy evs)) = 

183 
(K = KAB  Key K \<in> analz (knows Spy evs))" 

184 
by (simp only: analz_image_freshK analz_image_freshK_simps) 

185 

186 

187 
(*** The Key K uniquely identifies the Server's message. **) 

188 

189 
lemma unique_session_keys: 

190 
"[ Says Server A 

191 
{nb, Crypt (shrK A) {Agent B, Key K, na}, X} \<in> set evs; 

192 
Says Server A' 

193 
{nb', Crypt (shrK A') {Agent B', Key K, na'}, X'} \<in> set evs; 

194 
evs \<in> yahalom ] 

195 
==> A=A' & B=B' & na=na' & nb=nb'" 

196 
apply (erule rev_mp, erule rev_mp) 

197 
apply (erule yahalom.induct, simp_all) 

198 
(*YM3, by freshness*) 

199 
apply blast 

200 
done 

201 

202 

203 
(** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **) 

204 

205 
lemma secrecy_lemma: 

206 
"[ A \<notin> bad; B \<notin> bad; evs \<in> yahalom ] 

207 
==> Says Server A 

208 
{nb, Crypt (shrK A) {Agent B, Key K, na}, 

209 
Crypt (shrK B) {Agent A, Agent B, Key K, nb}} 

210 
\<in> set evs > 

211 
Notes Spy {na, nb, Key K} \<notin> set evs > 

212 
Key K \<notin> analz (knows Spy evs)" 

213 
apply (erule yahalom.induct, force, frule_tac [7] Says_Server_message_form, 

214 
drule_tac [6] YM4_analz_knows_Spy) 

215 
apply (simp_all add: pushes analz_insert_eq analz_insert_freshK) 

216 
apply spy_analz (*Fake*) 

217 
apply (blast dest: unique_session_keys)+ (*YM3, Oops*) 

218 
done 

219 

220 

221 
(*Final version*) 

222 
lemma Spy_not_see_encrypted_key: 

223 
"[ Says Server A 

224 
{nb, Crypt (shrK A) {Agent B, Key K, na}, 

225 
Crypt (shrK B) {Agent A, Agent B, Key K, nb}} 

226 
\<in> set evs; 

227 
Notes Spy {na, nb, Key K} \<notin> set evs; 

228 
A \<notin> bad; B \<notin> bad; evs \<in> yahalom ] 

229 
==> Key K \<notin> analz (knows Spy evs)" 

230 
by (blast dest: secrecy_lemma Says_Server_message_form) 

231 

232 

233 
(** Security Guarantee for A upon receiving YM3 **) 

234 

235 
(*If the encrypted message appears then it originated with the Server. 

236 
May now apply Spy_not_see_encrypted_key, subject to its conditions.*) 

237 
lemma A_trusts_YM3: 

238 
"[ Crypt (shrK A) {Agent B, Key K, na} \<in> parts (knows Spy evs); 

239 
A \<notin> bad; evs \<in> yahalom ] 

240 
==> \<exists>nb. Says Server A 

241 
{nb, Crypt (shrK A) {Agent B, Key K, na}, 

242 
Crypt (shrK B) {Agent A, Agent B, Key K, nb}} 

243 
\<in> set evs" 

244 
apply (erule rev_mp) 

245 
apply (erule yahalom.induct, force, 

246 
frule_tac [6] YM4_parts_knows_Spy, simp_all) 

247 
(*Fake, YM3*) 

248 
apply blast+ 

249 
done 

250 

251 
(*The obvious combination of A_trusts_YM3 with Spy_not_see_encrypted_key*) 

252 
lemma A_gets_good_key: 

253 
"[ Crypt (shrK A) {Agent B, Key K, na} \<in> parts (knows Spy evs); 

254 
\<forall>nb. Notes Spy {na, nb, Key K} \<notin> set evs; 

255 
A \<notin> bad; B \<notin> bad; evs \<in> yahalom ] 

256 
==> Key K \<notin> analz (knows Spy evs)" 

257 
by (blast dest!: A_trusts_YM3 Spy_not_see_encrypted_key) 

258 

259 

260 
(** Security Guarantee for B upon receiving YM4 **) 

261 

262 
(*B knows, by the first part of A's message, that the Server distributed 

263 
the key for A and B, and has associated it with NB.*) 

264 
lemma B_trusts_YM4_shrK: 

265 
"[ Crypt (shrK B) {Agent A, Agent B, Key K, Nonce NB} 

266 
\<in> parts (knows Spy evs); 

267 
B \<notin> bad; evs \<in> yahalom ] 

268 
==> \<exists>NA. Says Server A 

269 
{Nonce NB, 

270 
Crypt (shrK A) {Agent B, Key K, Nonce NA}, 

271 
Crypt (shrK B) {Agent A, Agent B, Key K, Nonce NB}} 

272 
\<in> set evs" 

273 
apply (erule rev_mp) 

274 
apply (erule yahalom.induct, force, 

275 
frule_tac [6] YM4_parts_knows_Spy, simp_all) 

276 
(*Fake, YM3*) 

277 
apply blast+ 

278 
done 

279 

280 

281 
(*With this protocol variant, we don't need the 2nd part of YM4 at all: 

282 
Nonce NB is available in the first part.*) 

283 

284 
(*What can B deduce from receipt of YM4? Stronger and simpler than Yahalom 

285 
because we do not have to show that NB is secret. *) 

286 
lemma B_trusts_YM4: 

287 
"[ Gets B {Crypt (shrK B) {Agent A, Agent B, Key K, Nonce NB}, X} 

288 
\<in> set evs; 

289 
A \<notin> bad; B \<notin> bad; evs \<in> yahalom ] 

290 
==> \<exists>NA. Says Server A 

291 
{Nonce NB, 

292 
Crypt (shrK A) {Agent B, Key K, Nonce NA}, 

293 
Crypt (shrK B) {Agent A, Agent B, Key K, Nonce NB}} 

294 
\<in> set evs" 

295 
by (blast dest!: B_trusts_YM4_shrK) 

296 

297 

298 
(*The obvious combination of B_trusts_YM4 with Spy_not_see_encrypted_key*) 

299 
lemma B_gets_good_key: 

300 
"[ Gets B {Crypt (shrK B) {Agent A, Agent B, Key K, Nonce NB}, X} 

301 
\<in> set evs; 

302 
\<forall>na. Notes Spy {na, Nonce NB, Key K} \<notin> set evs; 

303 
A \<notin> bad; B \<notin> bad; evs \<in> yahalom ] 

304 
==> Key K \<notin> analz (knows Spy evs)" 

305 
by (blast dest!: B_trusts_YM4 Spy_not_see_encrypted_key) 

306 

307 

308 
(*** Authenticating B to A ***) 

309 

310 
(*The encryption in message YM2 tells us it cannot be faked.*) 

311 
lemma B_Said_YM2: 

312 
"[ Crypt (shrK B) {Agent A, Nonce NA} \<in> parts (knows Spy evs); 

313 
B \<notin> bad; evs \<in> yahalom ] 

314 
==> \<exists>NB. Says B Server {Agent B, Nonce NB, 

315 
Crypt (shrK B) {Agent A, Nonce NA}} 

316 
\<in> set evs" 

317 
apply (erule rev_mp) 

318 
apply (erule yahalom.induct, force, 

319 
frule_tac [6] YM4_parts_knows_Spy, simp_all) 

320 
(*Fake, YM2*) 

321 
apply blast+ 

322 
done 

323 

324 

325 
(*If the server sends YM3 then B sent YM2, perhaps with a different NB*) 

326 
lemma YM3_auth_B_to_A_lemma: 

327 
"[ Says Server A {nb, Crypt (shrK A) {Agent B, Key K, Nonce NA}, X} 

328 
\<in> set evs; 

329 
B \<notin> bad; evs \<in> yahalom ] 

330 
==> \<exists>nb'. Says B Server {Agent B, nb', 

331 
Crypt (shrK B) {Agent A, Nonce NA}} 

332 
\<in> set evs" 

333 
apply (erule rev_mp) 

334 
apply (erule yahalom.induct, simp_all) 

335 
(*Fake, YM2, YM3*) 

336 
apply (blast dest!: B_Said_YM2)+ 

337 
done 

338 

339 
(*If A receives YM3 then B has used nonce NA (and therefore is alive)*) 

340 
lemma YM3_auth_B_to_A: 

341 
"[ Gets A {nb, Crypt (shrK A) {Agent B, Key K, Nonce NA}, X} 

342 
\<in> set evs; 

343 
A \<notin> bad; B \<notin> bad; evs \<in> yahalom ] 

344 
==> \<exists>nb'. Says B Server 

345 
{Agent B, nb', Crypt (shrK B) {Agent A, Nonce NA}} 

346 
\<in> set evs" 

347 
by (blast dest!: A_trusts_YM3 YM3_auth_B_to_A_lemma) 

348 

349 

350 

351 
(*** Authenticating A to B using the certificate Crypt K (Nonce NB) ***) 

352 

353 
(*Assuming the session key is secure, if both certificates are present then 

354 
A has said NB. We can't be sure about the rest of A's message, but only 

355 
NB matters for freshness. Note that Key K \<notin> analz (knows Spy evs) must be 

356 
the FIRST antecedent of the induction formula.*) 

357 

358 
(*This lemma allows a use of unique_session_keys in the next proof, 

359 
which otherwise is extremely slow.*) 

360 
lemma secure_unique_session_keys: 

361 
"[ Crypt (shrK A) {Agent B, Key K, na} \<in> analz (spies evs); 

362 
Crypt (shrK A') {Agent B', Key K, na'} \<in> analz (spies evs); 

363 
Key K \<notin> analz (knows Spy evs); evs \<in> yahalom ] 

364 
==> A=A' & B=B'" 

365 
by (blast dest!: A_trusts_YM3 dest: unique_session_keys Crypt_Spy_analz_bad) 

366 

367 

368 
lemma Auth_A_to_B_lemma [rule_format]: 

369 
"evs \<in> yahalom 

370 
==> Key K \<notin> analz (knows Spy evs) > 

371 
Crypt K (Nonce NB) \<in> parts (knows Spy evs) > 

372 
Crypt (shrK B) {Agent A, Agent B, Key K, Nonce NB} 

373 
\<in> parts (knows Spy evs) > 

374 
B \<notin> bad > 

375 
(\<exists>X. Says A B {X, Crypt K (Nonce NB)} \<in> set evs)" 

376 
apply (erule yahalom.induct, force, 

377 
frule_tac [6] YM4_parts_knows_Spy) 

378 
apply (analz_mono_contra, simp_all) 

379 
(*Fake*) 

380 
apply blast 

381 
(*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*) 

382 
apply (force dest!: Crypt_imp_keysFor) 

383 
(*YM4: was Crypt K (Nonce NB) the very last message? If so, apply unicity 

384 
of session keys; if not, use ind. hyp.*) 

385 
apply (blast dest!: B_trusts_YM4_shrK dest: secure_unique_session_keys ) 

386 
done 

387 

388 

389 
(*If B receives YM4 then A has used nonce NB (and therefore is alive). 

390 
Moreover, A associates K with NB (thus is talking about the same run). 

391 
Other premises guarantee secrecy of K.*) 

392 
lemma YM4_imp_A_Said_YM3 [rule_format]: 

393 
"[ Gets B {Crypt (shrK B) {Agent A, Agent B, Key K, Nonce NB}, 

394 
Crypt K (Nonce NB)} \<in> set evs; 

395 
(\<forall>NA. Notes Spy {Nonce NA, Nonce NB, Key K} \<notin> set evs); 

396 
A \<notin> bad; B \<notin> bad; evs \<in> yahalom ] 

397 
==> \<exists>X. Says A B {X, Crypt K (Nonce NB)} \<in> set evs" 

398 
by (blast intro: Auth_A_to_B_lemma 

399 
dest: Spy_not_see_encrypted_key B_trusts_YM4_shrK) 

2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

400 

81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

401 
end 