1(*  Title:      HOL/Auth/Yahalom.thy
2    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3    Copyright   1996  University of Cambridge
4*)
5
6section\<open>The Yahalom Protocol\<close>
7
8theory Yahalom imports Public begin
9
10text\<open>From page 257 of
11  Burrows, Abadi and Needham (1989).  A Logic of Authentication.
12  Proc. Royal Soc. 426
13
14This theory has the prototypical example of a secrecy relation, KeyCryptNonce.
15\<close>
16
17inductive_set yahalom :: "event list set"
18  where
19         (*Initial trace is empty*)
20   Nil:  "[] \<in> yahalom"
21
22         (*The spy MAY say anything he CAN say.  We do not expect him to
23           invent new nonces here, but he can also use NS1.  Common to
24           all similar protocols.*)
25 | Fake: "\<lbrakk>evsf \<in> yahalom;  X \<in> synth (analz (knows Spy evsf))\<rbrakk>
26          \<Longrightarrow> Says Spy B X  # evsf \<in> yahalom"
27
28         (*A message that has been sent can be received by the
29           intended recipient.*)
30 | Reception: "\<lbrakk>evsr \<in> yahalom;  Says A B X \<in> set evsr\<rbrakk>
31               \<Longrightarrow> Gets B X # evsr \<in> yahalom"
32
33         (*Alice initiates a protocol run*)
34 | YM1:  "\<lbrakk>evs1 \<in> yahalom;  Nonce NA \<notin> used evs1\<rbrakk>
35          \<Longrightarrow> Says A B \<lbrace>Agent A, Nonce NA\<rbrace> # evs1 \<in> yahalom"
36
37         (*Bob's response to Alice's message.*)
38 | YM2:  "\<lbrakk>evs2 \<in> yahalom;  Nonce NB \<notin> used evs2;
39             Gets B \<lbrace>Agent A, Nonce NA\<rbrace> \<in> set evs2\<rbrakk>
40          \<Longrightarrow> Says B Server 
41                  \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>\<rbrace>
42                # evs2 \<in> yahalom"
43
44         (*The Server receives Bob's message.  He responds by sending a
45            new session key to Alice, with a packet for forwarding to Bob.*)
46 | YM3:  "\<lbrakk>evs3 \<in> yahalom;  Key KAB \<notin> used evs3;  KAB \<in> symKeys;
47             Gets Server 
48                  \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>\<rbrace>
49               \<in> set evs3\<rbrakk>
50          \<Longrightarrow> Says Server A
51                   \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key KAB, Nonce NA, Nonce NB\<rbrace>,
52                     Crypt (shrK B) \<lbrace>Agent A, Key KAB\<rbrace>\<rbrace>
53                # evs3 \<in> yahalom"
54
55 | YM4:  
56       \<comment> \<open>Alice receives the Server's (?) message, checks her Nonce, and
57           uses the new session key to send Bob his Nonce.  The premise
58           \<^term>\<open>A \<noteq> Server\<close> is needed for \<open>Says_Server_not_range\<close>.
59           Alice can check that K is symmetric by its length.\<close>
60         "\<lbrakk>evs4 \<in> yahalom;  A \<noteq> Server;  K \<in> symKeys;
61             Gets A \<lbrace>Crypt(shrK A) \<lbrace>Agent B, Key K, Nonce NA, Nonce NB\<rbrace>, X\<rbrace>
62                \<in> set evs4;
63             Says A B \<lbrace>Agent A, Nonce NA\<rbrace> \<in> set evs4\<rbrakk>
64          \<Longrightarrow> Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> # evs4 \<in> yahalom"
65
66         (*This message models possible leaks of session keys.  The Nonces
67           identify the protocol run.  Quoting Server here ensures they are
68           correct.*)
69 | Oops: "\<lbrakk>evso \<in> yahalom;  
70             Says Server A \<lbrace>Crypt (shrK A)
71                                   \<lbrace>Agent B, Key K, Nonce NA, Nonce NB\<rbrace>,
72                             X\<rbrace>  \<in> set evso\<rbrakk>
73          \<Longrightarrow> Notes Spy \<lbrace>Nonce NA, Nonce NB, Key K\<rbrace> # evso \<in> yahalom"
74
75
76definition KeyWithNonce :: "[key, nat, event list] \<Rightarrow> bool" where
77  "KeyWithNonce K NB evs ==
78     \<exists>A B na X. 
79       Says Server A \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, Nonce NB\<rbrace>, X\<rbrace>
80         \<in> set evs"
81
82
83declare Says_imp_analz_Spy [dest]
84declare parts.Body  [dest]
85declare Fake_parts_insert_in_Un  [dest]
86declare analz_into_parts [dest]
87
88text\<open>A "possibility property": there are traces that reach the end\<close>
89lemma "\<lbrakk>A \<noteq> Server; K \<in> symKeys; Key K \<notin> used []\<rbrakk>
90      \<Longrightarrow> \<exists>X NB. \<exists>evs \<in> yahalom.
91             Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs"
92apply (intro exI bexI)
93apply (rule_tac [2] yahalom.Nil
94                    [THEN yahalom.YM1, THEN yahalom.Reception,
95                     THEN yahalom.YM2, THEN yahalom.Reception,
96                     THEN yahalom.YM3, THEN yahalom.Reception,
97                     THEN yahalom.YM4])
98apply (possibility, simp add: used_Cons)
99done
100
101
102subsection\<open>Regularity Lemmas for Yahalom\<close>
103
104lemma Gets_imp_Says:
105     "\<lbrakk>Gets B X \<in> set evs; evs \<in> yahalom\<rbrakk> \<Longrightarrow> \<exists>A. Says A B X \<in> set evs"
106by (erule rev_mp, erule yahalom.induct, auto)
107
108text\<open>Must be proved separately for each protocol\<close>
109lemma Gets_imp_knows_Spy:
110     "\<lbrakk>Gets B X \<in> set evs; evs \<in> yahalom\<rbrakk>  \<Longrightarrow> X \<in> knows Spy evs"
111by (blast dest!: Gets_imp_Says Says_imp_knows_Spy)
112
113lemmas Gets_imp_analz_Spy = Gets_imp_knows_Spy [THEN analz.Inj]
114declare Gets_imp_analz_Spy [dest]
115
116
117text\<open>Lets us treat YM4 using a similar argument as for the Fake case.\<close>
118lemma YM4_analz_knows_Spy:
119     "\<lbrakk>Gets A \<lbrace>Crypt (shrK A) Y, X\<rbrace> \<in> set evs;  evs \<in> yahalom\<rbrakk>
120      \<Longrightarrow> X \<in> analz (knows Spy evs)"
121by blast
122
123lemmas YM4_parts_knows_Spy =
124       YM4_analz_knows_Spy [THEN analz_into_parts]
125
126text\<open>For Oops\<close>
127lemma YM4_Key_parts_knows_Spy:
128     "Says Server A \<lbrace>Crypt (shrK A) \<lbrace>B,K,NA,NB\<rbrace>, X\<rbrace> \<in> set evs
129      \<Longrightarrow> K \<in> parts (knows Spy evs)"
130  by (metis parts.Body parts.Fst parts.Snd  Says_imp_knows_Spy parts.Inj)
131
132text\<open>Theorems of the form \<^term>\<open>X \<notin> parts (knows Spy evs)\<close> imply 
133that NOBODY sends messages containing X!\<close>
134
135text\<open>Spy never sees a good agent's shared key!\<close>
136lemma Spy_see_shrK [simp]:
137     "evs \<in> yahalom \<Longrightarrow> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"
138by (erule yahalom.induct, force,
139    drule_tac [6] YM4_parts_knows_Spy, simp_all, blast+)
140
141lemma Spy_analz_shrK [simp]:
142     "evs \<in> yahalom \<Longrightarrow> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)"
143by auto
144
145lemma Spy_see_shrK_D [dest!]:
146     "\<lbrakk>Key (shrK A) \<in> parts (knows Spy evs);  evs \<in> yahalom\<rbrakk> \<Longrightarrow> A \<in> bad"
147by (blast dest: Spy_see_shrK)
148
149text\<open>Nobody can have used non-existent keys!
150    Needed to apply \<open>analz_insert_Key\<close>\<close>
151lemma new_keys_not_used [simp]:
152    "\<lbrakk>Key K \<notin> used evs; K \<in> symKeys; evs \<in> yahalom\<rbrakk>
153     \<Longrightarrow> K \<notin> keysFor (parts (spies evs))"
154apply (erule rev_mp)
155apply (erule yahalom.induct, force,
156       frule_tac [6] YM4_parts_knows_Spy, simp_all)
157txt\<open>Fake\<close>
158apply (force dest!: keysFor_parts_insert, auto)
159done
160
161
162text\<open>Earlier, all protocol proofs declared this theorem.
163  But only a few proofs need it, e.g. Yahalom and Kerberos IV.\<close>
164lemma new_keys_not_analzd:
165 "\<lbrakk>K \<in> symKeys; evs \<in> yahalom; Key K \<notin> used evs\<rbrakk>
166  \<Longrightarrow> K \<notin> keysFor (analz (knows Spy evs))"
167by (blast dest: new_keys_not_used intro: keysFor_mono [THEN subsetD])
168
169
170text\<open>Describes the form of K when the Server sends this message.  Useful for
171  Oops as well as main secrecy property.\<close>
172lemma Says_Server_not_range [simp]:
173     "\<lbrakk>Says Server A \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace>, X\<rbrace>
174           \<in> set evs;   evs \<in> yahalom\<rbrakk>
175      \<Longrightarrow> K \<notin> range shrK"
176by (erule rev_mp, erule yahalom.induct, simp_all)
177
178
179subsection\<open>Secrecy Theorems\<close>
180
181(****
182 The following is to prove theorems of the form
183
184  Key K \<in> analz (insert (Key KAB) (knows Spy evs)) \<Longrightarrow>
185  Key K \<in> analz (knows Spy evs)
186
187 A more general formula must be proved inductively.
188****)
189
190text\<open>Session keys are not used to encrypt other session keys\<close>
191
192lemma analz_image_freshK [rule_format]:
193 "evs \<in> yahalom \<Longrightarrow>
194   \<forall>K KK. KK \<subseteq> - (range shrK) \<longrightarrow>
195          (Key K \<in> analz (Key`KK \<union> (knows Spy evs))) =
196          (K \<in> KK | Key K \<in> analz (knows Spy evs))"
197apply (erule yahalom.induct,
198       drule_tac [7] YM4_analz_knows_Spy, analz_freshK, spy_analz, blast)
199apply (simp only: Says_Server_not_range analz_image_freshK_simps)
200apply safe
201done
202
203lemma analz_insert_freshK:
204     "\<lbrakk>evs \<in> yahalom;  KAB \<notin> range shrK\<rbrakk> \<Longrightarrow>
205      (Key K \<in> analz (insert (Key KAB) (knows Spy evs))) =
206      (K = KAB | Key K \<in> analz (knows Spy evs))"
207by (simp only: analz_image_freshK analz_image_freshK_simps)
208
209
210text\<open>The Key K uniquely identifies the Server's  message.\<close>
211lemma unique_session_keys:
212     "\<lbrakk>Says Server A
213          \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace>, X\<rbrace> \<in> set evs;
214        Says Server A'
215          \<lbrace>Crypt (shrK A') \<lbrace>Agent B', Key K, na', nb'\<rbrace>, X'\<rbrace> \<in> set evs;
216        evs \<in> yahalom\<rbrakk>
217     \<Longrightarrow> A=A' \<and> B=B' \<and> na=na' \<and> nb=nb'"
218apply (erule rev_mp, erule rev_mp)
219apply (erule yahalom.induct, simp_all)
220txt\<open>YM3, by freshness, and YM4\<close>
221apply blast+
222done
223
224
225text\<open>Crucial secrecy property: Spy does not see the keys sent in msg YM3\<close>
226lemma secrecy_lemma:
227     "\<lbrakk>A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom\<rbrakk>
228      \<Longrightarrow> Says Server A
229            \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace>,
230              Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace>
231           \<in> set evs \<longrightarrow>
232          Notes Spy \<lbrace>na, nb, Key K\<rbrace> \<notin> set evs \<longrightarrow>
233          Key K \<notin> analz (knows Spy evs)"
234apply (erule yahalom.induct, force,
235       drule_tac [6] YM4_analz_knows_Spy)
236apply (simp_all add: pushes analz_insert_eq analz_insert_freshK) 
237  subgoal \<comment> \<open>Fake\<close> by spy_analz
238  subgoal \<comment> \<open>YM3\<close> by blast   
239  subgoal \<comment> \<open>Oops\<close> by  (blast dest: unique_session_keys)   
240done
241
242text\<open>Final version\<close>
243lemma Spy_not_see_encrypted_key:
244     "\<lbrakk>Says Server A
245            \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace>,
246              Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace>
247           \<in> set evs;
248         Notes Spy \<lbrace>na, nb, Key K\<rbrace> \<notin> set evs;
249         A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom\<rbrakk>
250      \<Longrightarrow> Key K \<notin> analz (knows Spy evs)"
251by (blast dest: secrecy_lemma)
252
253
254subsubsection\<open>Security Guarantee for A upon receiving YM3\<close>
255
256text\<open>If the encrypted message appears then it originated with the Server\<close>
257lemma A_trusts_YM3:
258     "\<lbrakk>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace> \<in> parts (knows Spy evs);
259         A \<notin> bad;  evs \<in> yahalom\<rbrakk>
260       \<Longrightarrow> Says Server A
261            \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace>,
262              Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace>
263           \<in> set evs"
264apply (erule rev_mp)
265apply (erule yahalom.induct, force,
266       frule_tac [6] YM4_parts_knows_Spy, simp_all)
267txt\<open>Fake, YM3\<close>
268apply blast+
269done
270
271text\<open>The obvious combination of \<open>A_trusts_YM3\<close> with
272  \<open>Spy_not_see_encrypted_key\<close>\<close>
273lemma A_gets_good_key:
274     "\<lbrakk>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace> \<in> parts (knows Spy evs);
275         Notes Spy \<lbrace>na, nb, Key K\<rbrace> \<notin> set evs;
276         A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom\<rbrakk>
277      \<Longrightarrow> Key K \<notin> analz (knows Spy evs)"
278  by (metis A_trusts_YM3 secrecy_lemma)
279
280
281subsubsection\<open>Security Guarantees for B upon receiving YM4\<close>
282
283text\<open>B knows, by the first part of A's message, that the Server distributed
284  the key for A and B.  But this part says nothing about nonces.\<close>
285lemma B_trusts_YM4_shrK:
286     "\<lbrakk>Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace> \<in> parts (knows Spy evs);
287         B \<notin> bad;  evs \<in> yahalom\<rbrakk>
288      \<Longrightarrow> \<exists>NA NB. Says Server A
289                      \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K,
290                                         Nonce NA, Nonce NB\<rbrace>,
291                        Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace>
292                     \<in> set evs"
293apply (erule rev_mp)
294apply (erule yahalom.induct, force,
295       frule_tac [6] YM4_parts_knows_Spy, simp_all)
296txt\<open>Fake, YM3\<close>
297apply blast+
298done
299
300text\<open>B knows, by the second part of A's message, that the Server
301  distributed the key quoting nonce NB.  This part says nothing about
302  agent names.  Secrecy of NB is crucial.  Note that \<^term>\<open>Nonce NB
303  \<notin> analz(knows Spy evs)\<close> must be the FIRST antecedent of the
304  induction formula.\<close>
305
306lemma B_trusts_YM4_newK [rule_format]:
307     "\<lbrakk>Crypt K (Nonce NB) \<in> parts (knows Spy evs);
308        Nonce NB \<notin> analz (knows Spy evs);  evs \<in> yahalom\<rbrakk>
309      \<Longrightarrow> \<exists>A B NA. Says Server A
310                      \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, Nonce NA, Nonce NB\<rbrace>,
311                        Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace>
312                     \<in> set evs"
313apply (erule rev_mp, erule rev_mp)
314apply (erule yahalom.induct, force,
315       frule_tac [6] YM4_parts_knows_Spy)
316         apply (analz_mono_contra, simp_all)
317  subgoal \<comment> \<open>Fake\<close> by blast
318  subgoal \<comment> \<open>YM3\<close> by blast   
319txt\<open>YM4.  A is uncompromised because NB is secure
320  A's certificate guarantees the existence of the Server message\<close>
321apply (blast dest!: Gets_imp_Says Crypt_Spy_analz_bad
322             dest: Says_imp_spies
323                   parts.Inj [THEN parts.Fst, THEN A_trusts_YM3])
324done
325
326
327subsubsection\<open>Towards proving secrecy of Nonce NB\<close>
328
329text\<open>Lemmas about the predicate KeyWithNonce\<close>
330
331lemma KeyWithNonceI:
332 "Says Server A
333          \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, Nonce NB\<rbrace>, X\<rbrace>
334        \<in> set evs \<Longrightarrow> KeyWithNonce K NB evs"
335by (unfold KeyWithNonce_def, blast)
336
337lemma KeyWithNonce_Says [simp]:
338   "KeyWithNonce K NB (Says S A X # evs) =
339      (Server = S \<and>
340       (\<exists>B n X'. X = \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, n, Nonce NB\<rbrace>, X'\<rbrace>)
341      | KeyWithNonce K NB evs)"
342by (simp add: KeyWithNonce_def, blast)
343
344
345lemma KeyWithNonce_Notes [simp]:
346   "KeyWithNonce K NB (Notes A X # evs) = KeyWithNonce K NB evs"
347by (simp add: KeyWithNonce_def)
348
349lemma KeyWithNonce_Gets [simp]:
350   "KeyWithNonce K NB (Gets A X # evs) = KeyWithNonce K NB evs"
351by (simp add: KeyWithNonce_def)
352
353text\<open>A fresh key cannot be associated with any nonce
354  (with respect to a given trace).\<close>
355lemma fresh_not_KeyWithNonce:
356     "Key K \<notin> used evs \<Longrightarrow> \<not> KeyWithNonce K NB evs"
357by (unfold KeyWithNonce_def, blast)
358
359text\<open>The Server message associates K with NB' and therefore not with any
360  other nonce NB.\<close>
361lemma Says_Server_KeyWithNonce:
362 "\<lbrakk>Says Server A \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, Nonce NB'\<rbrace>, X\<rbrace>
363       \<in> set evs;
364     NB \<noteq> NB';  evs \<in> yahalom\<rbrakk>
365  \<Longrightarrow> \<not> KeyWithNonce K NB evs"
366by (unfold KeyWithNonce_def, blast dest: unique_session_keys)
367
368
369text\<open>The only nonces that can be found with the help of session keys are
370  those distributed as nonce NB by the Server.  The form of the theorem
371  recalls \<open>analz_image_freshK\<close>, but it is much more complicated.\<close>
372
373
374text\<open>As with \<open>analz_image_freshK\<close>, we take some pains to express the 
375  property as a logical equivalence so that the simplifier can apply it.\<close>
376lemma Nonce_secrecy_lemma:
377     "P \<longrightarrow> (X \<in> analz (G \<union> H)) \<longrightarrow> (X \<in> analz H)  \<Longrightarrow>
378      P \<longrightarrow> (X \<in> analz (G \<union> H)) = (X \<in> analz H)"
379by (blast intro: analz_mono [THEN subsetD])
380
381lemma Nonce_secrecy:
382     "evs \<in> yahalom \<Longrightarrow>
383      (\<forall>KK. KK \<subseteq> - (range shrK) \<longrightarrow>
384           (\<forall>K \<in> KK. K \<in> symKeys \<longrightarrow> \<not> KeyWithNonce K NB evs)   \<longrightarrow>
385           (Nonce NB \<in> analz (Key`KK \<union> (knows Spy evs))) =
386           (Nonce NB \<in> analz (knows Spy evs)))"
387apply (erule yahalom.induct,
388       frule_tac [7] YM4_analz_knows_Spy)
389apply (safe del: allI impI intro!: Nonce_secrecy_lemma [THEN impI, THEN allI])
390apply (simp_all del: image_insert image_Un
391       add: analz_image_freshK_simps split_ifs
392            all_conj_distrib ball_conj_distrib
393            analz_image_freshK fresh_not_KeyWithNonce
394            imp_disj_not1               (*Moves NBa\<noteq>NB to the front*)
395            Says_Server_KeyWithNonce)
396txt\<open>For Oops, simplification proves \<^prop>\<open>NBa\<noteq>NB\<close>.  By
397  \<^term>\<open>Says_Server_KeyWithNonce\<close>, we get \<^prop>\<open>\<not> KeyWithNonce K NB
398  evs\<close>; then simplification can apply the induction hypothesis with
399  \<^term>\<open>KK = {K}\<close>.\<close>
400  subgoal \<comment> \<open>Fake\<close> by spy_analz
401  subgoal \<comment> \<open>YM2\<close> by blast
402  subgoal \<comment> \<open>YM3\<close> by blast
403  subgoal \<comment> \<open>YM4: If \<^prop>\<open>A \<in> bad\<close> then \<^term>\<open>NBa\<close> is known, therefore \<^prop>\<open>NBa \<noteq> NB\<close>.\<close>
404    by (metis A_trusts_YM3 Gets_imp_analz_Spy Gets_imp_knows_Spy KeyWithNonce_def
405        Spy_analz_shrK analz.Fst analz.Snd analz_shrK_Decrypt parts.Fst parts.Inj)
406done
407
408
409text\<open>Version required below: if NB can be decrypted using a session key then
410   it was distributed with that key.  The more general form above is required
411   for the induction to carry through.\<close>
412lemma single_Nonce_secrecy:
413     "\<lbrakk>Says Server A
414          \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key KAB, na, Nonce NB'\<rbrace>, X\<rbrace>
415         \<in> set evs;
416         NB \<noteq> NB';  KAB \<notin> range shrK;  evs \<in> yahalom\<rbrakk>
417      \<Longrightarrow> (Nonce NB \<in> analz (insert (Key KAB) (knows Spy evs))) =
418          (Nonce NB \<in> analz (knows Spy evs))"
419by (simp_all del: image_insert image_Un imp_disjL
420             add: analz_image_freshK_simps split_ifs
421                  Nonce_secrecy Says_Server_KeyWithNonce)
422
423
424subsubsection\<open>The Nonce NB uniquely identifies B's message.\<close>
425
426lemma unique_NB:
427     "\<lbrakk>Crypt (shrK B) \<lbrace>Agent A, Nonce NA, nb\<rbrace> \<in> parts (knows Spy evs);
428         Crypt (shrK B') \<lbrace>Agent A', Nonce NA', nb\<rbrace> \<in> parts (knows Spy evs);
429        evs \<in> yahalom;  B \<notin> bad;  B' \<notin> bad\<rbrakk>
430      \<Longrightarrow> NA' = NA \<and> A' = A \<and> B' = B"
431apply (erule rev_mp, erule rev_mp)
432apply (erule yahalom.induct, force,
433       frule_tac [6] YM4_parts_knows_Spy, simp_all)
434txt\<open>Fake, and YM2 by freshness\<close>
435apply blast+
436done
437
438
439text\<open>Variant useful for proving secrecy of NB.  Because nb is assumed to be
440  secret, we no longer must assume B, B' not bad.\<close>
441lemma Says_unique_NB:
442     "\<lbrakk>Says C S   \<lbrace>X,  Crypt (shrK B) \<lbrace>Agent A, Nonce NA, nb\<rbrace>\<rbrace>
443           \<in> set evs;
444         Gets S' \<lbrace>X', Crypt (shrK B') \<lbrace>Agent A', Nonce NA', nb\<rbrace>\<rbrace>
445           \<in> set evs;
446         nb \<notin> analz (knows Spy evs);  evs \<in> yahalom\<rbrakk>
447      \<Longrightarrow> NA' = NA \<and> A' = A \<and> B' = B"
448by (blast dest!: Gets_imp_Says Crypt_Spy_analz_bad
449          dest: Says_imp_spies unique_NB parts.Inj analz.Inj)
450
451
452subsubsection\<open>A nonce value is never used both as NA and as NB\<close>
453
454lemma no_nonce_YM1_YM2:
455     "\<lbrakk>Crypt (shrK B') \<lbrace>Agent A', Nonce NB, nb'\<rbrace> \<in> parts(knows Spy evs);
456        Nonce NB \<notin> analz (knows Spy evs);  evs \<in> yahalom\<rbrakk>
457  \<Longrightarrow> Crypt (shrK B)  \<lbrace>Agent A, na, Nonce NB\<rbrace> \<notin> parts(knows Spy evs)"
458apply (erule rev_mp, erule rev_mp)
459apply (erule yahalom.induct, force,
460       frule_tac [6] YM4_parts_knows_Spy)
461apply (analz_mono_contra, simp_all)
462txt\<open>Fake, YM2\<close>
463apply blast+
464done
465
466text\<open>The Server sends YM3 only in response to YM2.\<close>
467lemma Says_Server_imp_YM2:
468     "\<lbrakk>Says Server A \<lbrace>Crypt (shrK A) \<lbrace>Agent B, k, na, nb\<rbrace>, X\<rbrace> \<in> set evs;
469         evs \<in> yahalom\<rbrakk>
470      \<Longrightarrow> Gets Server \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, na, nb\<rbrace>\<rbrace>
471             \<in> set evs"
472by (erule rev_mp, erule yahalom.induct, auto)
473
474text\<open>A vital theorem for B, that nonce NB remains secure from the Spy.\<close>
475theorem Spy_not_see_NB :
476     "\<lbrakk>Says B Server
477                \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>\<rbrace>
478           \<in> set evs;
479         (\<forall>k. Notes Spy \<lbrace>Nonce NA, Nonce NB, k\<rbrace> \<notin> set evs);
480         A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom\<rbrakk>
481      \<Longrightarrow> Nonce NB \<notin> analz (knows Spy evs)"
482apply (erule rev_mp, erule rev_mp)
483apply (erule yahalom.induct, force,
484       frule_tac [6] YM4_analz_knows_Spy)
485apply (simp_all add: split_ifs pushes new_keys_not_analzd analz_insert_eq
486                     analz_insert_freshK)
487  subgoal \<comment> \<open>Fake\<close> by spy_analz
488  subgoal \<comment> \<open>YM1: NB=NA is impossible anyway, but NA is secret because it is fresh!\<close> by blast
489  subgoal \<comment> \<open>YM2\<close> by blast
490  subgoal \<comment> \<open>YM3: because no NB can also be an NA\<close> 
491    by (blast dest!: no_nonce_YM1_YM2 dest: Gets_imp_Says Says_unique_NB)
492  subgoal \<comment> \<open>YM4: key K is visible to Spy, contradicting session key secrecy theorem\<close>
493    \<comment> \<open>Case analysis on whether Aa is bad;
494            use \<open>Says_unique_NB\<close> to identify message components: \<^term>\<open>Aa=A\<close>, \<^term>\<open>Ba=B\<close>\<close>
495    apply clarify
496    apply (blast dest!: Says_unique_NB analz_shrK_Decrypt
497                        parts.Inj [THEN parts.Fst, THEN A_trusts_YM3]
498                 dest: Gets_imp_Says Says_imp_spies Says_Server_imp_YM2
499                       Spy_not_see_encrypted_key)
500    done
501  subgoal \<comment> \<open>Oops case: if the nonce is betrayed now, show that the Oops event is
502    covered by the quantified Oops assumption.\<close>
503    apply clarsimp
504    apply (metis Says_Server_imp_YM2 Gets_imp_Says Says_Server_not_range Says_unique_NB no_nonce_YM1_YM2 parts.Snd single_Nonce_secrecy spies_partsEs(1))
505    done
506done
507
508text\<open>B's session key guarantee from YM4.  The two certificates contribute to a
509  single conclusion about the Server's message.  Note that the "Notes Spy"
510  assumption must quantify over \<open>\<forall>\<close> POSSIBLE keys instead of our particular K.
511  If this run is broken and the spy substitutes a certificate containing an
512  old key, B has no means of telling.\<close>
513lemma B_trusts_YM4:
514     "\<lbrakk>Gets B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>,
515                  Crypt K (Nonce NB)\<rbrace> \<in> set evs;
516         Says B Server
517           \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>\<rbrace>
518           \<in> set evs;
519         \<forall>k. Notes Spy \<lbrace>Nonce NA, Nonce NB, k\<rbrace> \<notin> set evs;
520         A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom\<rbrakk>
521       \<Longrightarrow> Says Server A
522                   \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K,
523                             Nonce NA, Nonce NB\<rbrace>,
524                     Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace>
525             \<in> set evs"
526by (blast dest: Spy_not_see_NB Says_unique_NB
527                Says_Server_imp_YM2 B_trusts_YM4_newK)
528
529
530
531text\<open>The obvious combination of \<open>B_trusts_YM4\<close> with 
532  \<open>Spy_not_see_encrypted_key\<close>\<close>
533lemma B_gets_good_key:
534     "\<lbrakk>Gets B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>,
535                  Crypt K (Nonce NB)\<rbrace> \<in> set evs;
536         Says B Server
537           \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>\<rbrace>
538           \<in> set evs;
539         \<forall>k. Notes Spy \<lbrace>Nonce NA, Nonce NB, k\<rbrace> \<notin> set evs;
540         A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom\<rbrakk>
541      \<Longrightarrow> Key K \<notin> analz (knows Spy evs)"
542  by (metis B_trusts_YM4 Spy_not_see_encrypted_key)
543
544
545subsection\<open>Authenticating B to A\<close>
546
547text\<open>The encryption in message YM2 tells us it cannot be faked.\<close>
548lemma B_Said_YM2 [rule_format]:
549     "\<lbrakk>Crypt (shrK B) \<lbrace>Agent A, Nonce NA, nb\<rbrace> \<in> parts (knows Spy evs);
550        evs \<in> yahalom\<rbrakk>
551      \<Longrightarrow> B \<notin> bad \<longrightarrow>
552          Says B Server \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, nb\<rbrace>\<rbrace>
553            \<in> set evs"
554apply (erule rev_mp, erule yahalom.induct, force,
555       frule_tac [6] YM4_parts_knows_Spy, simp_all)
556txt\<open>Fake\<close>
557apply blast
558done
559
560text\<open>If the server sends YM3 then B sent YM2\<close>
561lemma YM3_auth_B_to_A_lemma:
562     "\<lbrakk>Says Server A \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, Nonce NA, nb\<rbrace>, X\<rbrace>
563       \<in> set evs;  evs \<in> yahalom\<rbrakk>
564      \<Longrightarrow> B \<notin> bad \<longrightarrow>
565          Says B Server \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, nb\<rbrace>\<rbrace>
566            \<in> set evs"
567apply (erule rev_mp, erule yahalom.induct, simp_all)
568txt\<open>YM3, YM4\<close>
569apply (blast dest!: B_Said_YM2)+
570done
571
572text\<open>If A receives YM3 then B has used nonce NA (and therefore is alive)\<close>
573theorem YM3_auth_B_to_A:
574     "\<lbrakk>Gets A \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, Nonce NA, nb\<rbrace>, X\<rbrace>
575           \<in> set evs;
576         A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom\<rbrakk>
577      \<Longrightarrow> Says B Server \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, nb\<rbrace>\<rbrace>
578       \<in> set evs"
579  by (metis A_trusts_YM3 Gets_imp_analz_Spy YM3_auth_B_to_A_lemma analz.Fst
580         not_parts_not_analz)
581
582
583subsection\<open>Authenticating A to B using the certificate 
584  \<^term>\<open>Crypt K (Nonce NB)\<close>\<close>
585
586text\<open>Assuming the session key is secure, if both certificates are present then
587  A has said NB.  We can't be sure about the rest of A's message, but only
588  NB matters for freshness.\<close>
589theorem A_Said_YM3_lemma [rule_format]:
590     "evs \<in> yahalom
591      \<Longrightarrow> Key K \<notin> analz (knows Spy evs) \<longrightarrow>
592          Crypt K (Nonce NB) \<in> parts (knows Spy evs) \<longrightarrow>
593          Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace> \<in> parts (knows Spy evs) \<longrightarrow>
594          B \<notin> bad \<longrightarrow>
595          (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs)"
596apply (erule yahalom.induct, force,
597       frule_tac [6] YM4_parts_knows_Spy)
598apply (analz_mono_contra, simp_all)
599  subgoal \<comment> \<open>Fake\<close> by blast
600  subgoal \<comment> \<open>YM3 because the message \<^term>\<open>Crypt K (Nonce NB)\<close> could not exist\<close>
601     by (force dest!: Crypt_imp_keysFor)
602   subgoal \<comment> \<open>YM4: was \<^term>\<open>Crypt K (Nonce NB)\<close> the very last message? If not, use the induction hypothesis,
603               otherwise by unicity of session keys\<close>
604     by (blast dest!: Gets_imp_Says A_trusts_YM3 B_trusts_YM4_shrK Crypt_Spy_analz_bad
605             dest: Says_imp_knows_Spy [THEN parts.Inj] unique_session_keys)
606done
607
608text\<open>If B receives YM4 then A has used nonce NB (and therefore is alive).
609  Moreover, A associates K with NB (thus is talking about the same run).
610  Other premises guarantee secrecy of K.\<close>
611theorem YM4_imp_A_Said_YM3 [rule_format]:
612     "\<lbrakk>Gets B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>,
613                  Crypt K (Nonce NB)\<rbrace> \<in> set evs;
614         Says B Server
615           \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>\<rbrace>
616           \<in> set evs;
617         (\<forall>NA k. Notes Spy \<lbrace>Nonce NA, Nonce NB, k\<rbrace> \<notin> set evs);
618         A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom\<rbrakk>
619      \<Longrightarrow> \<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs"
620by (metis A_Said_YM3_lemma B_gets_good_key Gets_imp_analz_Spy YM4_parts_knows_Spy analz.Fst not_parts_not_analz)
621
622end
623