author  wenzelm 
Mon, 28 Dec 2015 23:13:33 +0100  
changeset 61956  38b73f7940af 
parent 61830  4f5ab843cf5b 
child 64364  464420ba7f74 
permissions  rwrr 
37936  1 
(* Title: HOL/Auth/Yahalom2.thy 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

2 
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

3 
Copyright 1996 University of Cambridge 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

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

5 

61830  6 
section\<open>The Yahalom Protocol, Variant 2\<close> 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

7 

16417  8 
theory Yahalom2 imports Public begin 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

9 

61830  10 
text\<open> 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

11 
This version trades encryption of NB for additional explicitness in YM3. 
3432  12 
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

13 

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

14 
From page 259 of 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

15 
Burrows, Abadi and Needham (1989). A Logic of Authentication. 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

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

17 

14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

18 
This theory has the prototypical example of a secrecy relation, KeyCryptNonce. 
61830  19 
\<close> 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

20 

23746  21 
inductive_set yahalom :: "event list set" 
22 
where 

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

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

25 

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

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

27 
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

28 
all similar protocols.*) 
23746  29 
 Fake: "[ evsf \<in> yahalom; X \<in> synth (analz (knows Spy evsf)) ] 
11251  30 
==> 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

31 

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

23746  34 
 Reception: "[ evsr \<in> yahalom; Says A B X \<in> set evsr ] 
11251  35 
==> Gets B X # evsr \<in> yahalom" 
6335  36 

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

37 
(*Alice initiates a protocol run*) 
23746  38 
 YM1: "[ evs1 \<in> yahalom; Nonce NA \<notin> used evs1 ] 
61956  39 
==> Says A B \<lbrace>Agent A, Nonce NA\<rbrace> # evs1 \<in> yahalom" 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

40 

6335  41 
(*Bob's response to Alice's message.*) 
23746  42 
 YM2: "[ evs2 \<in> yahalom; Nonce NB \<notin> used evs2; 
61956  43 
Gets B \<lbrace>Agent A, Nonce NA\<rbrace> \<in> set evs2 ] 
11251  44 
==> Says B Server 
61956  45 
\<lbrace>Agent B, Nonce NB, Crypt (shrK B) \<lbrace>Agent A, Nonce NA\<rbrace>\<rbrace> 
11251  46 
# evs2 \<in> yahalom" 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

47 

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

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

49 
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

50 
Both agents are quoted in the 2nd certificate to prevent attacks!*) 
23746  51 
 YM3: "[ evs3 \<in> yahalom; Key KAB \<notin> used evs3; 
61956  52 
Gets Server \<lbrace>Agent B, Nonce NB, 
53 
Crypt (shrK B) \<lbrace>Agent A, Nonce NA\<rbrace>\<rbrace> 

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

55 
==> Says Server A 
61956  56 
\<lbrace>Nonce NB, 
57 
Crypt (shrK A) \<lbrace>Agent B, Key KAB, Nonce NA\<rbrace>, 

58 
Crypt (shrK B) \<lbrace>Agent A, Agent B, Key KAB, Nonce NB\<rbrace>\<rbrace> 

11251  59 
# evs3 \<in> yahalom" 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

60 

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

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

62 
uses the new session key to send Bob his Nonce.*) 
23746  63 
 YM4: "[ evs4 \<in> yahalom; 
61956  64 
Gets A \<lbrace>Nonce NB, Crypt (shrK A) \<lbrace>Agent B, Key K, Nonce NA\<rbrace>, 
65 
X\<rbrace> \<in> set evs4; 

66 
Says A B \<lbrace>Agent A, Nonce NA\<rbrace> \<in> set evs4 ] 

67 
==> Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> # evs4 \<in> yahalom" 

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

68 

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

71 
correct. *) 

23746  72 
 Oops: "[ evso \<in> yahalom; 
61956  73 
Says Server A \<lbrace>Nonce NB, 
74 
Crypt (shrK A) \<lbrace>Agent B, Key K, Nonce NA\<rbrace>, 

75 
X\<rbrace> \<in> set evso ] 

76 
==> Notes Spy \<lbrace>Nonce NA, Nonce NB, Key K\<rbrace> # evso \<in> yahalom" 

11251  77 

78 

79 
declare Says_imp_knows_Spy [THEN analz.Inj, dest] 

80 
declare parts.Body [dest] 

81 
declare Fake_parts_insert_in_Un [dest] 

82 
declare analz_into_parts [dest] 

83 

61830  84 
text\<open>A "possibility property": there are traces that reach the end\<close> 
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
13956
diff
changeset

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

86 
==> \<exists>X NB. \<exists>evs \<in> yahalom. 
61956  87 
Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs" 
11251  88 
apply (intro exI bexI) 
89 
apply (rule_tac [2] yahalom.Nil 

90 
[THEN yahalom.YM1, THEN yahalom.Reception, 

91 
THEN yahalom.YM2, THEN yahalom.Reception, 

92 
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

93 
THEN yahalom.YM4]) 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

94 
apply (possibility, simp add: used_Cons) 
11251  95 
done 
96 

97 
lemma Gets_imp_Says: 

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

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

100 

61830  101 
text\<open>Must be proved separately for each protocol\<close> 
11251  102 
lemma Gets_imp_knows_Spy: 
103 
"[ Gets B X \<in> set evs; evs \<in> yahalom ] ==> X \<in> knows Spy evs" 

104 
by (blast dest!: Gets_imp_Says Says_imp_knows_Spy) 

105 

106 
declare Gets_imp_knows_Spy [THEN analz.Inj, dest] 

107 

108 

61830  109 
subsection\<open>Inductive Proofs\<close> 
11251  110 

61830  111 
text\<open>Result for reasoning about the encrypted portion of messages. 
112 
Lets us treat YM4 using a similar argument as for the Fake case.\<close> 

11251  113 
lemma YM4_analz_knows_Spy: 
61956  114 
"[ Gets A \<lbrace>NB, Crypt (shrK A) Y, X\<rbrace> \<in> set evs; evs \<in> yahalom ] 
11251  115 
==> X \<in> analz (knows Spy evs)" 
116 
by blast 

117 

118 
lemmas YM4_parts_knows_Spy = 

45605  119 
YM4_analz_knows_Spy [THEN analz_into_parts] 
11251  120 

121 

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

123 
sends messages containing X! **) 

124 

61830  125 
text\<open>Spy never sees a good agent's shared key!\<close> 
11251  126 
lemma Spy_see_shrK [simp]: 
127 
"evs \<in> yahalom ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)" 

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

11251  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 

61830  139 
text\<open>Nobody can have used nonexistent keys! 
140 
Needed to apply \<open>analz_insert_Key\<close>\<close> 

14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

141 
lemma new_keys_not_used [simp]: 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

142 
"[Key K \<notin> used evs; K \<in> symKeys; evs \<in> yahalom] 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

143 
==> K \<notin> keysFor (parts (spies evs))" 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

144 
apply (erule rev_mp) 
11251  145 
apply (erule yahalom.induct, force, 
146 
frule_tac [6] YM4_parts_knows_Spy, simp_all) 

61830  147 
txt\<open>Fake\<close> 
13926  148 
apply (force dest!: keysFor_parts_insert) 
61830  149 
txt\<open>YM3\<close> 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

150 
apply blast 
61830  151 
txt\<open>YM4\<close> 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

152 
apply auto 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

153 
apply (blast dest!: Gets_imp_knows_Spy [THEN parts.Inj]) 
11251  154 
done 
155 

156 

61830  157 
text\<open>Describes the form of K when the Server sends this message. Useful for 
158 
Oops as well as main secrecy property.\<close> 

11251  159 
lemma Says_Server_message_form: 
61956  160 
"[ Says Server A \<lbrace>nb', Crypt (shrK A) \<lbrace>Agent B, Key K, na\<rbrace>, X\<rbrace> 
11251  161 
\<in> set evs; evs \<in> yahalom ] 
162 
==> K \<notin> range shrK" 

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

164 

165 

166 
(**** 

167 
The following is to prove theorems of the form 

168 

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

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

171 

172 
A more general formula must be proved inductively. 

173 
****) 

174 

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

176 

177 
lemma analz_image_freshK [rule_format]: 

178 
"evs \<in> yahalom ==> 

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

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

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

14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

182 
apply (erule yahalom.induct) 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

183 
apply (frule_tac [8] Says_Server_message_form) 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

184 
apply (drule_tac [7] YM4_analz_knows_Spy, analz_freshK, spy_analz, blast) 
11251  185 
done 
186 

187 
lemma analz_insert_freshK: 

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

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

192 

193 

61830  194 
text\<open>The Key K uniquely identifies the Server's message\<close> 
11251  195 
lemma unique_session_keys: 
196 
"[ Says Server A 

61956  197 
\<lbrace>nb, Crypt (shrK A) \<lbrace>Agent B, Key K, na\<rbrace>, X\<rbrace> \<in> set evs; 
11251  198 
Says Server A' 
61956  199 
\<lbrace>nb', Crypt (shrK A') \<lbrace>Agent B', Key K, na'\<rbrace>, X'\<rbrace> \<in> set evs; 
11251  200 
evs \<in> yahalom ] 
201 
==> A=A' & B=B' & na=na' & nb=nb'" 

202 
apply (erule rev_mp, erule rev_mp) 

203 
apply (erule yahalom.induct, simp_all) 

61830  204 
txt\<open>YM3, by freshness\<close> 
11251  205 
apply blast 
206 
done 

207 

208 

61830  209 
subsection\<open>Crucial Secrecy Property: Spy Does Not See Key @{term KAB}\<close> 
11251  210 

211 
lemma secrecy_lemma: 

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

213 
==> Says Server A 

61956  214 
\<lbrace>nb, Crypt (shrK A) \<lbrace>Agent B, Key K, na\<rbrace>, 
215 
Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, nb\<rbrace>\<rbrace> 

11251  216 
\<in> set evs > 
61956  217 
Notes Spy \<lbrace>na, nb, Key K\<rbrace> \<notin> set evs > 
11251  218 
Key K \<notin> analz (knows Spy evs)" 
219 
apply (erule yahalom.induct, force, frule_tac [7] Says_Server_message_form, 

220 
drule_tac [6] YM4_analz_knows_Spy) 

13907  221 
apply (simp_all add: pushes analz_insert_eq analz_insert_freshK, spy_analz) 
11251  222 
apply (blast dest: unique_session_keys)+ (*YM3, Oops*) 
223 
done 

224 

225 

61830  226 
text\<open>Final version\<close> 
11251  227 
lemma Spy_not_see_encrypted_key: 
228 
"[ Says Server A 

61956  229 
\<lbrace>nb, Crypt (shrK A) \<lbrace>Agent B, Key K, na\<rbrace>, 
230 
Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, nb\<rbrace>\<rbrace> 

11251  231 
\<in> set evs; 
61956  232 
Notes Spy \<lbrace>na, nb, Key K\<rbrace> \<notin> set evs; 
11251  233 
A \<notin> bad; B \<notin> bad; evs \<in> yahalom ] 
234 
==> Key K \<notin> analz (knows Spy evs)" 

235 
by (blast dest: secrecy_lemma Says_Server_message_form) 

236 

237 

13907  238 

61830  239 
text\<open>This form is an immediate consequence of the previous result. It is 
13907  240 
similar to the assertions established by other methods. It is equivalent 
241 
to the previous result in that the Spy already has @{term analz} and 

14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

242 
@{term synth} at his disposal. However, the conclusion 
13907  243 
@{term "Key K \<notin> knows Spy evs"} appears not to be inductive: all the cases 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

244 
other than Fake are trivial, while Fake requires 
61830  245 
@{term "Key K \<notin> analz (knows Spy evs)"}.\<close> 
13907  246 
lemma Spy_not_know_encrypted_key: 
247 
"[ Says Server A 

61956  248 
\<lbrace>nb, Crypt (shrK A) \<lbrace>Agent B, Key K, na\<rbrace>, 
249 
Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, nb\<rbrace>\<rbrace> 

13907  250 
\<in> set evs; 
61956  251 
Notes Spy \<lbrace>na, nb, Key K\<rbrace> \<notin> set evs; 
13907  252 
A \<notin> bad; B \<notin> bad; evs \<in> yahalom ] 
253 
==> Key K \<notin> knows Spy evs" 

254 
by (blast dest: Spy_not_see_encrypted_key) 

255 

256 

61830  257 
subsection\<open>Security Guarantee for A upon receiving YM3\<close> 
11251  258 

61830  259 
text\<open>If the encrypted message appears then it originated with the Server. 
260 
May now apply \<open>Spy_not_see_encrypted_key\<close>, subject to its conditions.\<close> 

11251  261 
lemma A_trusts_YM3: 
61956  262 
"[ Crypt (shrK A) \<lbrace>Agent B, Key K, na\<rbrace> \<in> parts (knows Spy evs); 
11251  263 
A \<notin> bad; evs \<in> yahalom ] 
264 
==> \<exists>nb. Says Server A 

61956  265 
\<lbrace>nb, Crypt (shrK A) \<lbrace>Agent B, Key K, na\<rbrace>, 
266 
Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, nb\<rbrace>\<rbrace> 

11251  267 
\<in> set evs" 
268 
apply (erule rev_mp) 

269 
apply (erule yahalom.induct, force, 

270 
frule_tac [6] YM4_parts_knows_Spy, simp_all) 

61830  271 
txt\<open>Fake, YM3\<close> 
11251  272 
apply blast+ 
273 
done 

274 

61830  275 
text\<open>The obvious combination of \<open>A_trusts_YM3\<close> with 
276 
\<open>Spy_not_see_encrypted_key\<close>\<close> 

13907  277 
theorem A_gets_good_key: 
61956  278 
"[ Crypt (shrK A) \<lbrace>Agent B, Key K, na\<rbrace> \<in> parts (knows Spy evs); 
279 
\<forall>nb. Notes Spy \<lbrace>na, nb, Key K\<rbrace> \<notin> set evs; 

11251  280 
A \<notin> bad; B \<notin> bad; evs \<in> yahalom ] 
281 
==> Key K \<notin> analz (knows Spy evs)" 

282 
by (blast dest!: A_trusts_YM3 Spy_not_see_encrypted_key) 

283 

284 

61830  285 
subsection\<open>Security Guarantee for B upon receiving YM4\<close> 
11251  286 

61830  287 
text\<open>B knows, by the first part of A's message, that the Server distributed 
288 
the key for A and B, and has associated it with NB.\<close> 

11251  289 
lemma B_trusts_YM4_shrK: 
61956  290 
"[ Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> 
11251  291 
\<in> parts (knows Spy evs); 
292 
B \<notin> bad; evs \<in> yahalom ] 

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

61956  294 
\<lbrace>Nonce NB, 
295 
Crypt (shrK A) \<lbrace>Agent B, Key K, Nonce NA\<rbrace>, 

296 
Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace>\<rbrace> 

11251  297 
\<in> set evs" 
298 
apply (erule rev_mp) 

299 
apply (erule yahalom.induct, force, 

300 
frule_tac [6] YM4_parts_knows_Spy, simp_all) 

61830  301 
txt\<open>Fake, YM3\<close> 
11251  302 
apply blast+ 
303 
done 

304 

305 

61830  306 
text\<open>With this protocol variant, we don't need the 2nd part of YM4 at all: 
307 
Nonce NB is available in the first part.\<close> 

11251  308 

61830  309 
text\<open>What can B deduce from receipt of YM4? Stronger and simpler than Yahalom 
310 
because we do not have to show that NB is secret.\<close> 

11251  311 
lemma B_trusts_YM4: 
61956  312 
"[ Gets B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace>, X\<rbrace> 
11251  313 
\<in> set evs; 
314 
A \<notin> bad; B \<notin> bad; evs \<in> yahalom ] 

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

61956  316 
\<lbrace>Nonce NB, 
317 
Crypt (shrK A) \<lbrace>Agent B, Key K, Nonce NA\<rbrace>, 

318 
Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace>\<rbrace> 

11251  319 
\<in> set evs" 
320 
by (blast dest!: B_trusts_YM4_shrK) 

321 

322 

61830  323 
text\<open>The obvious combination of \<open>B_trusts_YM4\<close> with 
324 
\<open>Spy_not_see_encrypted_key\<close>\<close> 

13907  325 
theorem B_gets_good_key: 
61956  326 
"[ Gets B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace>, X\<rbrace> 
11251  327 
\<in> set evs; 
61956  328 
\<forall>na. Notes Spy \<lbrace>na, Nonce NB, Key K\<rbrace> \<notin> set evs; 
11251  329 
A \<notin> bad; B \<notin> bad; evs \<in> yahalom ] 
330 
==> Key K \<notin> analz (knows Spy evs)" 

331 
by (blast dest!: B_trusts_YM4 Spy_not_see_encrypted_key) 

332 

333 

61830  334 
subsection\<open>Authenticating B to A\<close> 
11251  335 

61830  336 
text\<open>The encryption in message YM2 tells us it cannot be faked.\<close> 
11251  337 
lemma B_Said_YM2: 
61956  338 
"[ Crypt (shrK B) \<lbrace>Agent A, Nonce NA\<rbrace> \<in> parts (knows Spy evs); 
11251  339 
B \<notin> bad; evs \<in> yahalom ] 
61956  340 
==> \<exists>NB. Says B Server \<lbrace>Agent B, Nonce NB, 
341 
Crypt (shrK B) \<lbrace>Agent A, Nonce NA\<rbrace>\<rbrace> 

11251  342 
\<in> set evs" 
343 
apply (erule rev_mp) 

344 
apply (erule yahalom.induct, force, 

345 
frule_tac [6] YM4_parts_knows_Spy, simp_all) 

61830  346 
txt\<open>Fake, YM2\<close> 
11251  347 
apply blast+ 
348 
done 

349 

350 

61830  351 
text\<open>If the server sends YM3 then B sent YM2, perhaps with a different NB\<close> 
11251  352 
lemma YM3_auth_B_to_A_lemma: 
61956  353 
"[ Says Server A \<lbrace>nb, Crypt (shrK A) \<lbrace>Agent B, Key K, Nonce NA\<rbrace>, X\<rbrace> 
11251  354 
\<in> set evs; 
355 
B \<notin> bad; evs \<in> yahalom ] 

61956  356 
==> \<exists>nb'. Says B Server \<lbrace>Agent B, nb', 
357 
Crypt (shrK B) \<lbrace>Agent A, Nonce NA\<rbrace>\<rbrace> 

11251  358 
\<in> set evs" 
359 
apply (erule rev_mp) 

360 
apply (erule yahalom.induct, simp_all) 

61830  361 
txt\<open>Fake, YM2, YM3\<close> 
11251  362 
apply (blast dest!: B_Said_YM2)+ 
363 
done 

364 

61830  365 
text\<open>If A receives YM3 then B has used nonce NA (and therefore is alive)\<close> 
13907  366 
theorem YM3_auth_B_to_A: 
61956  367 
"[ Gets A \<lbrace>nb, Crypt (shrK A) \<lbrace>Agent B, Key K, Nonce NA\<rbrace>, X\<rbrace> 
11251  368 
\<in> set evs; 
369 
A \<notin> bad; B \<notin> bad; evs \<in> yahalom ] 

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

61956  371 
\<lbrace>Agent B, nb', Crypt (shrK B) \<lbrace>Agent A, Nonce NA\<rbrace>\<rbrace> 
11251  372 
\<in> set evs" 
373 
by (blast dest!: A_trusts_YM3 YM3_auth_B_to_A_lemma) 

374 

375 

61830  376 
subsection\<open>Authenticating A to B\<close> 
11251  377 

61830  378 
text\<open>using the certificate @{term "Crypt K (Nonce NB)"}\<close> 
11251  379 

61830  380 
text\<open>Assuming the session key is secure, if both certificates are present then 
11251  381 
A has said NB. We can't be sure about the rest of A's message, but only 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

382 
NB matters for freshness. Note that @{term "Key K \<notin> analz (knows Spy evs)"} 
61830  383 
must be the FIRST antecedent of the induction formula.\<close> 
11251  384 

61830  385 
text\<open>This lemma allows a use of \<open>unique_session_keys\<close> in the next proof, 
386 
which otherwise is extremely slow.\<close> 

11251  387 
lemma secure_unique_session_keys: 
61956  388 
"[ Crypt (shrK A) \<lbrace>Agent B, Key K, na\<rbrace> \<in> analz (spies evs); 
389 
Crypt (shrK A') \<lbrace>Agent B', Key K, na'\<rbrace> \<in> analz (spies evs); 

11251  390 
Key K \<notin> analz (knows Spy evs); evs \<in> yahalom ] 
391 
==> A=A' & B=B'" 

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

393 

394 

395 
lemma Auth_A_to_B_lemma [rule_format]: 

396 
"evs \<in> yahalom 

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

14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

398 
K \<in> symKeys > 
11251  399 
Crypt K (Nonce NB) \<in> parts (knows Spy evs) > 
61956  400 
Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> 
11251  401 
\<in> parts (knows Spy evs) > 
402 
B \<notin> bad > 

61956  403 
(\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs)" 
11251  404 
apply (erule yahalom.induct, force, 
405 
frule_tac [6] YM4_parts_knows_Spy) 

406 
apply (analz_mono_contra, simp_all) 

61830  407 
txt\<open>Fake\<close> 
11251  408 
apply blast 
61830  409 
txt\<open>YM3: by \<open>new_keys_not_used\<close>, the message 
410 
@{term "Crypt K (Nonce NB)"} could not exist\<close> 

11251  411 
apply (force dest!: Crypt_imp_keysFor) 
61830  412 
txt\<open>YM4: was @{term "Crypt K (Nonce NB)"} the very last message? If so, 
413 
apply unicity of session keys; if not, use the induction hypothesis\<close> 

14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

414 
apply (blast dest!: B_trusts_YM4_shrK dest: secure_unique_session_keys) 
11251  415 
done 
416 

417 

61830  418 
text\<open>If B receives YM4 then A has used nonce NB (and therefore is alive). 
11251  419 
Moreover, A associates K with NB (thus is talking about the same run). 
61830  420 
Other premises guarantee secrecy of K.\<close> 
13907  421 
theorem YM4_imp_A_Said_YM3 [rule_format]: 
61956  422 
"[ Gets B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace>, 
423 
Crypt K (Nonce NB)\<rbrace> \<in> set evs; 

424 
(\<forall>NA. Notes Spy \<lbrace>Nonce NA, Nonce NB, Key K\<rbrace> \<notin> set evs); 

14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

425 
K \<in> symKeys; A \<notin> bad; B \<notin> bad; evs \<in> yahalom ] 
61956  426 
==> \<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs" 
11251  427 
by (blast intro: Auth_A_to_B_lemma 
428 
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

429 

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

430 
end 