author  paulson <lp15@cam.ac.uk> 
Mon, 24 Oct 2016 14:31:05 +0100  
changeset 64364  464420ba7f74 
parent 61956  38b73f7940af 
child 67226  ec32cdaab97b 
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.*) 
64364  29 
 Fake: "\<lbrakk>evsf \<in> yahalom; X \<in> synth (analz (knows Spy evsf))\<rbrakk> 
30 
\<Longrightarrow> 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.*) 

64364  34 
 Reception: "\<lbrakk>evsr \<in> yahalom; Says A B X \<in> set evsr\<rbrakk> 
35 
\<Longrightarrow> 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*) 
64364  38 
 YM1: "\<lbrakk>evs1 \<in> yahalom; Nonce NA \<notin> used evs1\<rbrakk> 
39 
\<Longrightarrow> 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.*) 
64364  42 
 YM2: "\<lbrakk>evs2 \<in> yahalom; Nonce NB \<notin> used evs2; 
43 
Gets B \<lbrace>Agent A, Nonce NA\<rbrace> \<in> set evs2\<rbrakk> 

44 
\<Longrightarrow> 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!*) 
64364  51 
 YM3: "\<lbrakk>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> 

64364  54 
\<in> set evs3\<rbrakk> 
55 
\<Longrightarrow> 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.*) 
64364  63 
 YM4: "\<lbrakk>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; 

64364  66 
Says A B \<lbrace>Agent A, Nonce NA\<rbrace> \<in> set evs4\<rbrakk> 
67 
\<Longrightarrow> 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. *) 

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

64364  75 
X\<rbrace> \<in> set evso\<rbrakk> 
76 
\<Longrightarrow> 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 [] 
64364  86 
\<Longrightarrow> \<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: 

64364  98 
"\<lbrakk>Gets B X \<in> set evs; evs \<in> yahalom\<rbrakk> \<Longrightarrow> \<exists>A. Says A B X \<in> set evs" 
11251  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: 
64364  103 
"\<lbrakk>Gets B X \<in> set evs; evs \<in> yahalom\<rbrakk> \<Longrightarrow> X \<in> knows Spy evs" 
11251  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: 
64364  114 
"\<lbrakk>Gets A \<lbrace>NB, Crypt (shrK A) Y, X\<rbrace> \<in> set evs; evs \<in> yahalom\<rbrakk> 
115 
\<Longrightarrow> X \<in> analz (knows Spy evs)" 

11251  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]: 
64364  127 
"evs \<in> yahalom \<Longrightarrow> (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]: 

64364  132 
"evs \<in> yahalom \<Longrightarrow> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)" 
11251  133 
by auto 
134 

135 
lemma Spy_see_shrK_D [dest!]: 

64364  136 
"\<lbrakk>Key (shrK A) \<in> parts (knows Spy evs); evs \<in> yahalom\<rbrakk> \<Longrightarrow> A \<in> bad" 
11251  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]: 
64364  142 
"\<lbrakk>Key K \<notin> used evs; K \<in> symKeys; evs \<in> yahalom\<rbrakk> 
143 
\<Longrightarrow> K \<notin> keysFor (parts (spies evs))" 

14207
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) 

64364  147 
subgoal \<open>Fake\<close> by (force dest!: keysFor_parts_insert) 
148 
subgoal \<open>YM3 \<close>by blast 

149 
subgoal \<open>YM4\<close> by (fastforce dest!: Gets_imp_knows_Spy [THEN parts.Inj]) 

11251  150 
done 
151 

152 

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

11251  155 
lemma Says_Server_message_form: 
64364  156 
"\<lbrakk>Says Server A \<lbrace>nb', Crypt (shrK A) \<lbrace>Agent B, Key K, na\<rbrace>, X\<rbrace> 
157 
\<in> set evs; evs \<in> yahalom\<rbrakk> 

158 
\<Longrightarrow> K \<notin> range shrK" 

11251  159 
by (erule rev_mp, erule yahalom.induct, simp_all) 
160 

161 

162 
(**** 

163 
The following is to prove theorems of the form 

164 

64364  165 
Key K \<in> analz (insert (Key KAB) (knows Spy evs)) \<Longrightarrow> 
11251  166 
Key K \<in> analz (knows Spy evs) 
167 

168 
A more general formula must be proved inductively. 

169 
****) 

170 

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

172 

173 
lemma analz_image_freshK [rule_format]: 

64364  174 
"evs \<in> yahalom \<Longrightarrow> 
11251  175 
\<forall>K KK. KK <=  (range shrK) > 
176 
(Key K \<in> analz (Key`KK Un (knows Spy evs))) = 

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

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

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

180 
apply (drule_tac [7] YM4_analz_knows_Spy, analz_freshK, spy_analz, blast) 
11251  181 
done 
182 

183 
lemma analz_insert_freshK: 

64364  184 
"\<lbrakk>evs \<in> yahalom; KAB \<notin> range shrK\<rbrakk> \<Longrightarrow> 
11655  185 
(Key K \<in> analz (insert (Key KAB) (knows Spy evs))) = 
11251  186 
(K = KAB  Key K \<in> analz (knows Spy evs))" 
187 
by (simp only: analz_image_freshK analz_image_freshK_simps) 

188 

189 

61830  190 
text\<open>The Key K uniquely identifies the Server's message\<close> 
11251  191 
lemma unique_session_keys: 
64364  192 
"\<lbrakk>Says Server A 
61956  193 
\<lbrace>nb, Crypt (shrK A) \<lbrace>Agent B, Key K, na\<rbrace>, X\<rbrace> \<in> set evs; 
11251  194 
Says Server A' 
61956  195 
\<lbrace>nb', Crypt (shrK A') \<lbrace>Agent B', Key K, na'\<rbrace>, X'\<rbrace> \<in> set evs; 
64364  196 
evs \<in> yahalom\<rbrakk> 
197 
\<Longrightarrow> A=A' & B=B' & na=na' & nb=nb'" 

11251  198 
apply (erule rev_mp, erule rev_mp) 
199 
apply (erule yahalom.induct, simp_all) 

61830  200 
txt\<open>YM3, by freshness\<close> 
11251  201 
apply blast 
202 
done 

203 

204 

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

207 
lemma secrecy_lemma: 

64364  208 
"\<lbrakk>A \<notin> bad; B \<notin> bad; evs \<in> yahalom\<rbrakk> 
209 
\<Longrightarrow> Says Server A 

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

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

216 
drule_tac [6] YM4_analz_knows_Spy) 

13907  217 
apply (simp_all add: pushes analz_insert_eq analz_insert_freshK, spy_analz) 
11251  218 
apply (blast dest: unique_session_keys)+ (*YM3, Oops*) 
219 
done 

220 

221 

61830  222 
text\<open>Final version\<close> 
11251  223 
lemma Spy_not_see_encrypted_key: 
64364  224 
"\<lbrakk>Says Server A 
61956  225 
\<lbrace>nb, Crypt (shrK A) \<lbrace>Agent B, Key K, na\<rbrace>, 
226 
Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, nb\<rbrace>\<rbrace> 

11251  227 
\<in> set evs; 
61956  228 
Notes Spy \<lbrace>na, nb, Key K\<rbrace> \<notin> set evs; 
64364  229 
A \<notin> bad; B \<notin> bad; evs \<in> yahalom\<rbrakk> 
230 
\<Longrightarrow> Key K \<notin> analz (knows Spy evs)" 

11251  231 
by (blast dest: secrecy_lemma Says_Server_message_form) 
232 

233 

13907  234 

61830  235 
text\<open>This form is an immediate consequence of the previous result. It is 
13907  236 
similar to the assertions established by other methods. It is equivalent 
237 
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

238 
@{term synth} at his disposal. However, the conclusion 
13907  239 
@{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

240 
other than Fake are trivial, while Fake requires 
61830  241 
@{term "Key K \<notin> analz (knows Spy evs)"}.\<close> 
13907  242 
lemma Spy_not_know_encrypted_key: 
64364  243 
"\<lbrakk>Says Server A 
61956  244 
\<lbrace>nb, Crypt (shrK A) \<lbrace>Agent B, Key K, na\<rbrace>, 
245 
Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, nb\<rbrace>\<rbrace> 

13907  246 
\<in> set evs; 
61956  247 
Notes Spy \<lbrace>na, nb, Key K\<rbrace> \<notin> set evs; 
64364  248 
A \<notin> bad; B \<notin> bad; evs \<in> yahalom\<rbrakk> 
249 
\<Longrightarrow> Key K \<notin> knows Spy evs" 

13907  250 
by (blast dest: Spy_not_see_encrypted_key) 
251 

252 

61830  253 
subsection\<open>Security Guarantee for A upon receiving YM3\<close> 
11251  254 

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

11251  257 
lemma A_trusts_YM3: 
64364  258 
"\<lbrakk>Crypt (shrK A) \<lbrace>Agent B, Key K, na\<rbrace> \<in> parts (knows Spy evs); 
259 
A \<notin> bad; evs \<in> yahalom\<rbrakk> 

260 
\<Longrightarrow> \<exists>nb. Says Server A 

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

11251  263 
\<in> set evs" 
264 
apply (erule rev_mp) 

265 
apply (erule yahalom.induct, force, 

266 
frule_tac [6] YM4_parts_knows_Spy, simp_all) 

61830  267 
txt\<open>Fake, YM3\<close> 
11251  268 
apply blast+ 
269 
done 

270 

61830  271 
text\<open>The obvious combination of \<open>A_trusts_YM3\<close> with 
272 
\<open>Spy_not_see_encrypted_key\<close>\<close> 

13907  273 
theorem A_gets_good_key: 
64364  274 
"\<lbrakk>Crypt (shrK A) \<lbrace>Agent B, Key K, na\<rbrace> \<in> parts (knows Spy evs); 
61956  275 
\<forall>nb. Notes Spy \<lbrace>na, nb, Key K\<rbrace> \<notin> set evs; 
64364  276 
A \<notin> bad; B \<notin> bad; evs \<in> yahalom\<rbrakk> 
277 
\<Longrightarrow> Key K \<notin> analz (knows Spy evs)" 

11251  278 
by (blast dest!: A_trusts_YM3 Spy_not_see_encrypted_key) 
279 

280 

61830  281 
subsection\<open>Security Guarantee for B upon receiving YM4\<close> 
11251  282 

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

11251  285 
lemma B_trusts_YM4_shrK: 
64364  286 
"\<lbrakk>Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> 
11251  287 
\<in> parts (knows Spy evs); 
64364  288 
B \<notin> bad; evs \<in> yahalom\<rbrakk> 
289 
\<Longrightarrow> \<exists>NA. Says Server A 

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

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

11251  293 
\<in> set evs" 
294 
apply (erule rev_mp) 

295 
apply (erule yahalom.induct, force, 

296 
frule_tac [6] YM4_parts_knows_Spy, simp_all) 

61830  297 
txt\<open>Fake, YM3\<close> 
11251  298 
apply blast+ 
299 
done 

300 

301 

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

11251  304 

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

11251  307 
lemma B_trusts_YM4: 
64364  308 
"\<lbrakk>Gets B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace>, X\<rbrace> 
11251  309 
\<in> set evs; 
64364  310 
A \<notin> bad; B \<notin> bad; evs \<in> yahalom\<rbrakk> 
311 
\<Longrightarrow> \<exists>NA. Says Server A 

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

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

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

317 

318 

61830  319 
text\<open>The obvious combination of \<open>B_trusts_YM4\<close> with 
320 
\<open>Spy_not_see_encrypted_key\<close>\<close> 

13907  321 
theorem B_gets_good_key: 
64364  322 
"\<lbrakk>Gets B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace>, X\<rbrace> 
11251  323 
\<in> set evs; 
61956  324 
\<forall>na. Notes Spy \<lbrace>na, Nonce NB, Key K\<rbrace> \<notin> set evs; 
64364  325 
A \<notin> bad; B \<notin> bad; evs \<in> yahalom\<rbrakk> 
326 
\<Longrightarrow> Key K \<notin> analz (knows Spy evs)" 

11251  327 
by (blast dest!: B_trusts_YM4 Spy_not_see_encrypted_key) 
328 

329 

61830  330 
subsection\<open>Authenticating B to A\<close> 
11251  331 

61830  332 
text\<open>The encryption in message YM2 tells us it cannot be faked.\<close> 
11251  333 
lemma B_Said_YM2: 
64364  334 
"\<lbrakk>Crypt (shrK B) \<lbrace>Agent A, Nonce NA\<rbrace> \<in> parts (knows Spy evs); 
335 
B \<notin> bad; evs \<in> yahalom\<rbrakk> 

336 
\<Longrightarrow> \<exists>NB. Says B Server \<lbrace>Agent B, Nonce NB, 

61956  337 
Crypt (shrK B) \<lbrace>Agent A, Nonce NA\<rbrace>\<rbrace> 
11251  338 
\<in> set evs" 
339 
apply (erule rev_mp) 

340 
apply (erule yahalom.induct, force, 

341 
frule_tac [6] YM4_parts_knows_Spy, simp_all) 

61830  342 
txt\<open>Fake, YM2\<close> 
11251  343 
apply blast+ 
344 
done 

345 

346 

61830  347 
text\<open>If the server sends YM3 then B sent YM2, perhaps with a different NB\<close> 
11251  348 
lemma YM3_auth_B_to_A_lemma: 
64364  349 
"\<lbrakk>Says Server A \<lbrace>nb, Crypt (shrK A) \<lbrace>Agent B, Key K, Nonce NA\<rbrace>, X\<rbrace> 
11251  350 
\<in> set evs; 
64364  351 
B \<notin> bad; evs \<in> yahalom\<rbrakk> 
352 
\<Longrightarrow> \<exists>nb'. Says B Server \<lbrace>Agent B, nb', 

61956  353 
Crypt (shrK B) \<lbrace>Agent A, Nonce NA\<rbrace>\<rbrace> 
11251  354 
\<in> set evs" 
355 
apply (erule rev_mp) 

356 
apply (erule yahalom.induct, simp_all) 

61830  357 
txt\<open>Fake, YM2, YM3\<close> 
11251  358 
apply (blast dest!: B_Said_YM2)+ 
359 
done 

360 

61830  361 
text\<open>If A receives YM3 then B has used nonce NA (and therefore is alive)\<close> 
13907  362 
theorem YM3_auth_B_to_A: 
64364  363 
"\<lbrakk>Gets A \<lbrace>nb, Crypt (shrK A) \<lbrace>Agent B, Key K, Nonce NA\<rbrace>, X\<rbrace> 
11251  364 
\<in> set evs; 
64364  365 
A \<notin> bad; B \<notin> bad; evs \<in> yahalom\<rbrakk> 
366 
\<Longrightarrow> \<exists>nb'. Says B Server 

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

370 

371 

61830  372 
subsection\<open>Authenticating A to B\<close> 
11251  373 

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

61830  376 
text\<open>Assuming the session key is secure, if both certificates are present then 
11251  377 
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

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

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

11251  383 
lemma secure_unique_session_keys: 
64364  384 
"\<lbrakk>Crypt (shrK A) \<lbrace>Agent B, Key K, na\<rbrace> \<in> analz (spies evs); 
61956  385 
Crypt (shrK A') \<lbrace>Agent B', Key K, na'\<rbrace> \<in> analz (spies evs); 
64364  386 
Key K \<notin> analz (knows Spy evs); evs \<in> yahalom\<rbrakk> 
387 
\<Longrightarrow> A=A' & B=B'" 

11251  388 
by (blast dest!: A_trusts_YM3 dest: unique_session_keys Crypt_Spy_analz_bad) 
389 

390 

391 
lemma Auth_A_to_B_lemma [rule_format]: 

392 
"evs \<in> yahalom 

64364  393 
\<Longrightarrow> Key K \<notin> analz (knows Spy evs) > 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

394 
K \<in> symKeys > 
11251  395 
Crypt K (Nonce NB) \<in> parts (knows Spy evs) > 
61956  396 
Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace> 
11251  397 
\<in> parts (knows Spy evs) > 
398 
B \<notin> bad > 

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

402 
apply (analz_mono_contra, simp_all) 

64364  403 
subgoal \<open>Fake\<close> by blast 
404 
subgoal \<open>YM3 because the message @{term "Crypt K (Nonce NB)"} could not exist\<close> 

405 
by (force dest!: Crypt_imp_keysFor) 

406 
subgoal \<open>YM4: was @{term "Crypt K (Nonce NB)"} the very last message? If not, use the induction hypothesis, 

407 
otherwise by unicity of session keys\<close> 

408 
by (blast dest!: B_trusts_YM4_shrK dest: secure_unique_session_keys) 

11251  409 
done 
410 

411 

61830  412 
text\<open>If B receives YM4 then A has used nonce NB (and therefore is alive). 
11251  413 
Moreover, A associates K with NB (thus is talking about the same run). 
61830  414 
Other premises guarantee secrecy of K.\<close> 
13907  415 
theorem YM4_imp_A_Said_YM3 [rule_format]: 
64364  416 
"\<lbrakk>Gets B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Agent B, Key K, Nonce NB\<rbrace>, 
61956  417 
Crypt K (Nonce NB)\<rbrace> \<in> set evs; 
418 
(\<forall>NA. Notes Spy \<lbrace>Nonce NA, Nonce NB, Key K\<rbrace> \<notin> set evs); 

64364  419 
K \<in> symKeys; A \<notin> bad; B \<notin> bad; evs \<in> yahalom\<rbrakk> 
420 
\<Longrightarrow> \<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs" 

11251  421 
by (blast intro: Auth_A_to_B_lemma 
422 
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

423 

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

424 
end 