author  paulson 
Tue, 23 Sep 2003 15:41:33 +0200  
changeset 14200  d8598e24f8fa 
parent 13956  8fe7e12290e1 
child 14207  f20fbb141673 
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 
This version trades encryption of NB for additional explicitness in YM3. 
3432  7 
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

8 

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

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

10 
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

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

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

13 

13956  14 
header{*The Yahalom Protocol, Variant 2*} 
13907  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 

13907  82 
text{*A "possibility property": there are traces that reach the end*} 
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
13956
diff
changeset

83 
lemma "Key K \<notin> used [] 
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
13956
diff
changeset

84 
==> \<exists>X NB. \<exists>evs \<in> yahalom. 
11251  85 
Says A B {X, Crypt K (Nonce NB)} \<in> set evs" 
86 
apply (intro exI bexI) 

87 
apply (rule_tac [2] yahalom.Nil 

88 
[THEN yahalom.YM1, THEN yahalom.Reception, 

89 
THEN yahalom.YM2, THEN yahalom.Reception, 

90 
THEN yahalom.YM3, THEN yahalom.Reception, 

14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
13956
diff
changeset

91 
THEN yahalom.YM4]) 
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
13956
diff
changeset

92 
apply (possibility, simp add: used_Cons) 
11251  93 
done 
94 

95 
lemma Gets_imp_Says: 

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

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

98 

13907  99 
text{*Must be proved separately for each protocol*} 
11251  100 
lemma Gets_imp_knows_Spy: 
101 
"[ Gets B X \<in> set evs; evs \<in> yahalom ] ==> X \<in> knows Spy evs" 

102 
by (blast dest!: Gets_imp_Says Says_imp_knows_Spy) 

103 

104 
declare Gets_imp_knows_Spy [THEN analz.Inj, dest] 

105 

106 

13907  107 
subsection{*Inductive Proofs*} 
11251  108 

13907  109 
text{*Result for reasoning about the encrypted portion of messages. 
110 
Lets us treat YM4 using a similar argument as for the Fake case.*} 

11251  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 

13907  123 
text{*Spy never sees a good agent's shared key!*} 
11251  124 
lemma Spy_see_shrK [simp]: 
125 
"evs \<in> yahalom ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)" 

13907  126 
by (erule yahalom.induct, force, 
127 
drule_tac [6] YM4_parts_knows_Spy, simp_all, blast+) 

11251  128 

129 
lemma Spy_analz_shrK [simp]: 

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

131 
by auto 

132 

133 
lemma Spy_see_shrK_D [dest!]: 

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

135 
by (blast dest: Spy_see_shrK) 

136 

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

138 
lemma new_keys_not_used [rule_format, simp]: 

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

140 
apply (erule yahalom.induct, force, 

141 
frule_tac [6] YM4_parts_knows_Spy, simp_all) 

13926  142 
txt{*Fake*} 
143 
apply (force dest!: keysFor_parts_insert) 

144 
txt{*YM3, YM4*} 

145 
apply blast+ 

11251  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, 

13507  175 
drule_tac [6] YM4_analz_knows_Spy, analz_freshK, spy_analz) 
11251  176 
done 
177 

178 
lemma analz_insert_freshK: 

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

11655  180 
(Key K \<in> analz (insert (Key KAB) (knows Spy evs))) = 
11251  181 
(K = KAB  Key K \<in> analz (knows Spy evs))" 
182 
by (simp only: analz_image_freshK analz_image_freshK_simps) 

183 

184 

13907  185 
text{*The Key K uniquely identifies the Server's message*} 
11251  186 
lemma unique_session_keys: 
187 
"[ Says Server A 

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

189 
Says Server A' 

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

191 
evs \<in> yahalom ] 

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

193 
apply (erule rev_mp, erule rev_mp) 

194 
apply (erule yahalom.induct, simp_all) 

13907  195 
txt{*YM3, by freshness*} 
11251  196 
apply blast 
197 
done 

198 

199 

13907  200 
subsection{*Crucial Secrecy Property: Spy Does Not See Key @{term KAB}*} 
11251  201 

202 
lemma secrecy_lemma: 

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

204 
==> Says Server A 

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

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

207 
\<in> set evs > 

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

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

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

211 
drule_tac [6] YM4_analz_knows_Spy) 

13907  212 
apply (simp_all add: pushes analz_insert_eq analz_insert_freshK, spy_analz) 
11251  213 
apply (blast dest: unique_session_keys)+ (*YM3, Oops*) 
214 
done 

215 

216 

217 
(*Final version*) 

218 
lemma Spy_not_see_encrypted_key: 

219 
"[ Says Server A 

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

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

222 
\<in> set evs; 

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

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

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

226 
by (blast dest: secrecy_lemma Says_Server_message_form) 

227 

228 

13907  229 

230 
text{*This form is an immediate consequence of the previous result. It is 

231 
similar to the assertions established by other methods. It is equivalent 

232 
to the previous result in that the Spy already has @{term analz} and 

233 
@{term synth} at his disposal. However, the conclusion 

234 
@{term "Key K \<notin> knows Spy evs"} appears not to be inductive: all the cases 

235 
other than Fake are trivial, while Fake requires 

236 
@{term "Key K \<notin> analz (knows Spy evs)"}. *} 

237 
lemma Spy_not_know_encrypted_key: 

238 
"[ Says Server A 

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

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

241 
\<in> set evs; 

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

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

244 
==> Key K \<notin> knows Spy evs" 

245 
by (blast dest: Spy_not_see_encrypted_key) 

246 

247 

248 
subsection{*Security Guarantee for A upon receiving YM3*} 

11251  249 

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

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

252 
lemma A_trusts_YM3: 

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

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

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

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

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

258 
\<in> set evs" 

259 
apply (erule rev_mp) 

260 
apply (erule yahalom.induct, force, 

261 
frule_tac [6] YM4_parts_knows_Spy, simp_all) 

13907  262 
txt{*Fake, YM3*} 
11251  263 
apply blast+ 
264 
done 

265 

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

13907  267 
theorem A_gets_good_key: 
11251  268 
"[ Crypt (shrK A) {Agent B, Key K, na} \<in> parts (knows Spy evs); 
269 
\<forall>nb. Notes Spy {na, nb, Key K} \<notin> set evs; 

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

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

272 
by (blast dest!: A_trusts_YM3 Spy_not_see_encrypted_key) 

273 

274 

13907  275 
subsection{*Security Guarantee for B upon receiving YM4*} 
11251  276 

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

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

279 
lemma B_trusts_YM4_shrK: 

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

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

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

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

284 
{Nonce NB, 

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

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

287 
\<in> set evs" 

288 
apply (erule rev_mp) 

289 
apply (erule yahalom.induct, force, 

290 
frule_tac [6] YM4_parts_knows_Spy, simp_all) 

291 
(*Fake, YM3*) 

292 
apply blast+ 

293 
done 

294 

295 

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

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

298 

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

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

301 
lemma B_trusts_YM4: 

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

303 
\<in> set evs; 

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

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

306 
{Nonce NB, 

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

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

309 
\<in> set evs" 

310 
by (blast dest!: B_trusts_YM4_shrK) 

311 

312 

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

13907  314 
theorem B_gets_good_key: 
11251  315 
"[ Gets B {Crypt (shrK B) {Agent A, Agent B, Key K, Nonce NB}, X} 
316 
\<in> set evs; 

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

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

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

320 
by (blast dest!: B_trusts_YM4 Spy_not_see_encrypted_key) 

321 

322 

13907  323 
subsection{*Authenticating B to A*} 
11251  324 

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

326 
lemma B_Said_YM2: 

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

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

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

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

331 
\<in> set evs" 

332 
apply (erule rev_mp) 

333 
apply (erule yahalom.induct, force, 

334 
frule_tac [6] YM4_parts_knows_Spy, simp_all) 

335 
(*Fake, YM2*) 

336 
apply blast+ 

337 
done 

338 

339 

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

341 
lemma YM3_auth_B_to_A_lemma: 

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

343 
\<in> set evs; 

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

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

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

347 
\<in> set evs" 

348 
apply (erule rev_mp) 

349 
apply (erule yahalom.induct, simp_all) 

350 
(*Fake, YM2, YM3*) 

351 
apply (blast dest!: B_Said_YM2)+ 

352 
done 

353 

13907  354 
text{*If A receives YM3 then B has used nonce NA (and therefore is alive)*} 
355 
theorem YM3_auth_B_to_A: 

11251  356 
"[ Gets A {nb, Crypt (shrK A) {Agent B, Key K, Nonce NA}, X} 
357 
\<in> set evs; 

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

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

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

361 
\<in> set evs" 

362 
by (blast dest!: A_trusts_YM3 YM3_auth_B_to_A_lemma) 

363 

364 

13907  365 
subsection{*Authenticating A to B*} 
11251  366 

13907  367 
text{*using the certificate @{term "Crypt K (Nonce NB)"}*} 
11251  368 

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

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

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

372 
the FIRST antecedent of the induction formula.*) 

373 

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

375 
which otherwise is extremely slow.*) 

376 
lemma secure_unique_session_keys: 

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

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

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

380 
==> A=A' & B=B'" 

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

382 

383 

384 
lemma Auth_A_to_B_lemma [rule_format]: 

385 
"evs \<in> yahalom 

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

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

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

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

390 
B \<notin> bad > 

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

392 
apply (erule yahalom.induct, force, 

393 
frule_tac [6] YM4_parts_knows_Spy) 

394 
apply (analz_mono_contra, simp_all) 

395 
(*Fake*) 

396 
apply blast 

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

398 
apply (force dest!: Crypt_imp_keysFor) 

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

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

13926  401 
apply (blast dest!: B_trusts_YM4_shrK dest: secure_unique_session_keys ) 
11251  402 
done 
403 

404 

13907  405 
text{*If B receives YM4 then A has used nonce NB (and therefore is alive). 
11251  406 
Moreover, A associates K with NB (thus is talking about the same run). 
13907  407 
Other premises guarantee secrecy of K.*} 
408 
theorem YM4_imp_A_Said_YM3 [rule_format]: 

11251  409 
"[ Gets B {Crypt (shrK B) {Agent A, Agent B, Key K, Nonce NB}, 
410 
Crypt K (Nonce NB)} \<in> set evs; 

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

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

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

414 
by (blast intro: Auth_A_to_B_lemma 

415 
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

416 

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

417 
end 