1(*  Title:      HOL/Auth/NS_Shared.thy
2    Author:     Lawrence C Paulson and Giampaolo Bella 
3    Copyright   1996  University of Cambridge
4*)
5
6section\<open>Needham-Schroeder Shared-Key Protocol and the Issues Property\<close>
7
8theory NS_Shared imports Public begin
9
10text\<open>
11From page 247 of
12  Burrows, Abadi and Needham (1989).  A Logic of Authentication.
13  Proc. Royal Soc. 426
14\<close>
15
16definition
17 (* A is the true creator of X if she has sent X and X never appeared on
18    the trace before this event. Recall that traces grow from head. *)
19  Issues :: "[agent, agent, msg, event list] \<Rightarrow> bool"
20             ("_ Issues _ with _ on _") where
21   "A Issues B with X on evs =
22      (\<exists>Y. Says A B Y \<in> set evs \<and> X \<in> parts {Y} \<and>
23        X \<notin> parts (spies (takeWhile (\<lambda>z. z  \<noteq> Says A B Y) (rev evs))))"
24
25
26inductive_set ns_shared :: "event list set"
27 where
28        (*Initial trace is empty*)
29  Nil:  "[] \<in> ns_shared"
30        (*The spy MAY say anything he CAN say.  We do not expect him to
31          invent new nonces here, but he can also use NS1.  Common to
32          all similar protocols.*)
33| Fake: "\<lbrakk>evsf \<in> ns_shared;  X \<in> synth (analz (spies evsf))\<rbrakk>
34         \<Longrightarrow> Says Spy B X # evsf \<in> ns_shared"
35
36        (*Alice initiates a protocol run, requesting to talk to any B*)
37| NS1:  "\<lbrakk>evs1 \<in> ns_shared;  Nonce NA \<notin> used evs1\<rbrakk>
38         \<Longrightarrow> Says A Server \<lbrace>Agent A, Agent B, Nonce NA\<rbrace> # evs1  \<in>  ns_shared"
39
40        (*Server's response to Alice's message.
41          !! It may respond more than once to A's request !!
42          Server doesn't know who the true sender is, hence the A' in
43              the sender field.*)
44| NS2:  "\<lbrakk>evs2 \<in> ns_shared;  Key KAB \<notin> used evs2;  KAB \<in> symKeys;
45          Says A' Server \<lbrace>Agent A, Agent B, Nonce NA\<rbrace> \<in> set evs2\<rbrakk>
46         \<Longrightarrow> Says Server A
47               (Crypt (shrK A)
48                  \<lbrace>Nonce NA, Agent B, Key KAB,
49                    (Crypt (shrK B) \<lbrace>Key KAB, Agent A\<rbrace>)\<rbrace>)
50               # evs2 \<in> ns_shared"
51
52         (*We can't assume S=Server.  Agent A "remembers" her nonce.
53           Need A \<noteq> Server because we allow messages to self.*)
54| NS3:  "\<lbrakk>evs3 \<in> ns_shared;  A \<noteq> Server;
55          Says S A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs3;
56          Says A Server \<lbrace>Agent A, Agent B, Nonce NA\<rbrace> \<in> set evs3\<rbrakk>
57         \<Longrightarrow> Says A B X # evs3 \<in> ns_shared"
58
59        (*Bob's nonce exchange.  He does not know who the message came
60          from, but responds to A because she is mentioned inside.*)
61| NS4:  "\<lbrakk>evs4 \<in> ns_shared;  Nonce NB \<notin> used evs4;  K \<in> symKeys;
62          Says A' B (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>) \<in> set evs4\<rbrakk>
63         \<Longrightarrow> Says B A (Crypt K (Nonce NB)) # evs4 \<in> ns_shared"
64
65        (*Alice responds with Nonce NB if she has seen the key before.
66          Maybe should somehow check Nonce NA again.
67          We do NOT send NB-1 or similar as the Spy cannot spoof such things.
68          Letting the Spy add or subtract 1 lets him send all nonces.
69          Instead we distinguish the messages by sending the nonce twice.*)
70| NS5:  "\<lbrakk>evs5 \<in> ns_shared;  K \<in> symKeys;
71          Says B' A (Crypt K (Nonce NB)) \<in> set evs5;
72          Says S  A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>)
73            \<in> set evs5\<rbrakk>
74         \<Longrightarrow> Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) # evs5 \<in> ns_shared"
75
76        (*This message models possible leaks of session keys.
77          The two Nonces identify the protocol run: the rule insists upon
78          the true senders in order to make them accurate.*)
79| Oops: "\<lbrakk>evso \<in> ns_shared;  Says B A (Crypt K (Nonce NB)) \<in> set evso;
80          Says Server A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>)
81              \<in> set evso\<rbrakk>
82         \<Longrightarrow> Notes Spy \<lbrace>Nonce NA, Nonce NB, Key K\<rbrace> # evso \<in> ns_shared"
83
84
85declare Says_imp_knows_Spy [THEN parts.Inj, dest]
86declare parts.Body  [dest]
87declare Fake_parts_insert_in_Un  [dest]
88declare analz_into_parts [dest]
89
90
91text\<open>A "possibility property": there are traces that reach the end\<close>
92lemma "[| A \<noteq> Server; Key K \<notin> used []; K \<in> symKeys |]
93       ==> \<exists>N. \<exists>evs \<in> ns_shared.
94                    Says A B (Crypt K \<lbrace>Nonce N, Nonce N\<rbrace>) \<in> set evs"
95apply (intro exI bexI)
96apply (rule_tac [2] ns_shared.Nil
97       [THEN ns_shared.NS1, THEN ns_shared.NS2, THEN ns_shared.NS3,
98        THEN ns_shared.NS4, THEN ns_shared.NS5])
99apply (possibility, simp add: used_Cons)
100done
101
102(*This version is similar, while instantiating ?K and ?N to epsilon-terms
103lemma "A \<noteq> Server \<Longrightarrow> \<exists>evs \<in> ns_shared.
104                Says A B (Crypt ?K \<lbrace>Nonce ?N, Nonce ?N\<rbrace>) \<in> set evs"
105*)
106
107
108subsection\<open>Inductive proofs about \<^term>\<open>ns_shared\<close>\<close>
109
110subsubsection\<open>Forwarding lemmas, to aid simplification\<close>
111
112text\<open>For reasoning about the encrypted portion of message NS3\<close>
113lemma NS3_msg_in_parts_spies:
114     "Says S A (Crypt KA \<lbrace>N, B, K, X\<rbrace>) \<in> set evs \<Longrightarrow> X \<in> parts (spies evs)"
115by blast
116
117text\<open>For reasoning about the Oops message\<close>
118lemma Oops_parts_spies:
119     "Says Server A (Crypt (shrK A) \<lbrace>NA, B, K, X\<rbrace>) \<in> set evs
120            \<Longrightarrow> K \<in> parts (spies evs)"
121by blast
122
123text\<open>Theorems of the form \<^term>\<open>X \<notin> parts (spies evs)\<close> imply that NOBODY
124    sends messages containing \<^term>\<open>X\<close>\<close>
125
126text\<open>Spy never sees another agent's shared key! (unless it's bad at start)\<close>
127lemma Spy_see_shrK [simp]:
128     "evs \<in> ns_shared \<Longrightarrow> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)"
129apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, simp_all, blast+)
130done
131
132lemma Spy_analz_shrK [simp]:
133     "evs \<in> ns_shared \<Longrightarrow> (Key (shrK A) \<in> analz (spies evs)) = (A \<in> bad)"
134by auto
135
136
137text\<open>Nobody can have used non-existent keys!\<close>
138lemma new_keys_not_used [simp]:
139    "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> ns_shared|]
140     ==> K \<notin> keysFor (parts (spies evs))"
141apply (erule rev_mp)
142apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, simp_all)
143txt\<open>Fake, NS2, NS4, NS5\<close>
144apply (force dest!: keysFor_parts_insert, blast+)
145done
146
147
148subsubsection\<open>Lemmas concerning the form of items passed in messages\<close>
149
150text\<open>Describes the form of K, X and K' when the Server sends this message.\<close>
151lemma Says_Server_message_form:
152     "\<lbrakk>Says Server A (Crypt K' \<lbrace>N, Agent B, Key K, X\<rbrace>) \<in> set evs;
153       evs \<in> ns_shared\<rbrakk>
154      \<Longrightarrow> K \<notin> range shrK \<and>
155          X = (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>) \<and>
156          K' = shrK A"
157by (erule rev_mp, erule ns_shared.induct, auto)
158
159
160text\<open>If the encrypted message appears then it originated with the Server\<close>
161lemma A_trusts_NS2:
162     "\<lbrakk>Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace> \<in> parts (spies evs);
163       A \<notin> bad;  evs \<in> ns_shared\<rbrakk>
164      \<Longrightarrow> Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs"
165apply (erule rev_mp)
166apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, auto)
167done
168
169lemma cert_A_form:
170     "\<lbrakk>Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace> \<in> parts (spies evs);
171       A \<notin> bad;  evs \<in> ns_shared\<rbrakk>
172      \<Longrightarrow> K \<notin> range shrK \<and>  X = (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>)"
173by (blast dest!: A_trusts_NS2 Says_Server_message_form)
174
175text\<open>EITHER describes the form of X when the following message is sent,
176  OR     reduces it to the Fake case.
177  Use \<open>Says_Server_message_form\<close> if applicable.\<close>
178lemma Says_S_message_form:
179     "\<lbrakk>Says S A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
180       evs \<in> ns_shared\<rbrakk>
181      \<Longrightarrow> (K \<notin> range shrK \<and> X = (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>))
182          \<or> X \<in> analz (spies evs)"
183by (blast dest: Says_imp_knows_Spy analz_shrK_Decrypt cert_A_form analz.Inj)
184
185
186(*Alternative version also provable
187lemma Says_S_message_form2:
188  "\<lbrakk>Says S A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
189    evs \<in> ns_shared\<rbrakk>
190   \<Longrightarrow> Says Server A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs
191       \<or> X \<in> analz (spies evs)"
192apply (case_tac "A \<in> bad")
193apply (force dest!: Says_imp_knows_Spy [THEN analz.Inj])
194by (blast dest!: A_trusts_NS2 Says_Server_message_form)
195*)
196
197
198(****
199 SESSION KEY COMPROMISE THEOREM.  To prove theorems of the form
200
201  Key K \<in> analz (insert (Key KAB) (spies evs)) \<Longrightarrow>
202  Key K \<in> analz (spies evs)
203
204 A more general formula must be proved inductively.
205****)
206
207text\<open>NOT useful in this form, but it says that session keys are not used
208  to encrypt messages containing other keys, in the actual protocol.
209  We require that agents should behave like this subsequently also.\<close>
210lemma  "\<lbrakk>evs \<in> ns_shared;  Kab \<notin> range shrK\<rbrakk> \<Longrightarrow>
211         (Crypt KAB X) \<in> parts (spies evs) \<and>
212         Key K \<in> parts {X} \<longrightarrow> Key K \<in> parts (spies evs)"
213apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, simp_all)
214txt\<open>Fake\<close>
215apply (blast dest: parts_insert_subset_Un)
216txt\<open>Base, NS4 and NS5\<close>
217apply auto
218done
219
220
221subsubsection\<open>Session keys are not used to encrypt other session keys\<close>
222
223text\<open>The equality makes the induction hypothesis easier to apply\<close>
224
225lemma analz_image_freshK [rule_format]:
226 "evs \<in> ns_shared \<Longrightarrow>
227   \<forall>K KK. KK \<subseteq> - (range shrK) \<longrightarrow>
228             (Key K \<in> analz (Key`KK \<union> (spies evs))) =
229             (K \<in> KK \<or> Key K \<in> analz (spies evs))"
230apply (erule ns_shared.induct)
231apply (drule_tac [8] Says_Server_message_form)
232apply (erule_tac [5] Says_S_message_form [THEN disjE], analz_freshK, spy_analz)
233txt\<open>NS2, NS3\<close>
234apply blast+ 
235done
236
237
238lemma analz_insert_freshK:
239     "\<lbrakk>evs \<in> ns_shared;  KAB \<notin> range shrK\<rbrakk> \<Longrightarrow>
240       (Key K \<in> analz (insert (Key KAB) (spies evs))) =
241       (K = KAB \<or> Key K \<in> analz (spies evs))"
242by (simp only: analz_image_freshK analz_image_freshK_simps)
243
244
245subsubsection\<open>The session key K uniquely identifies the message\<close>
246
247text\<open>In messages of this form, the session key uniquely identifies the rest\<close>
248lemma unique_session_keys:
249     "\<lbrakk>Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
250       Says Server A' (Crypt (shrK A') \<lbrace>NA', Agent B', Key K, X'\<rbrace>) \<in> set evs;
251       evs \<in> ns_shared\<rbrakk> \<Longrightarrow> A=A' \<and> NA=NA' \<and> B=B' \<and> X = X'"
252by (erule rev_mp, erule rev_mp, erule ns_shared.induct, simp_all, blast+)
253
254
255subsubsection\<open>Crucial secrecy property: Spy doesn't see the keys sent in NS2\<close>
256
257text\<open>Beware of \<open>[rule_format]\<close> and the universal quantifier!\<close>
258lemma secrecy_lemma:
259     "\<lbrakk>Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K,
260                                      Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>)
261              \<in> set evs;
262         A \<notin> bad;  B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
263      \<Longrightarrow> (\<forall>NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs) \<longrightarrow>
264         Key K \<notin> analz (spies evs)"
265apply (erule rev_mp)
266apply (erule ns_shared.induct, force)
267apply (frule_tac [7] Says_Server_message_form)
268apply (frule_tac [4] Says_S_message_form)
269apply (erule_tac [5] disjE)
270apply (simp_all add: analz_insert_eq analz_insert_freshK pushes split_ifs, spy_analz)
271txt\<open>NS2\<close>
272apply blast
273txt\<open>NS3\<close>
274apply (blast dest!: Crypt_Spy_analz_bad A_trusts_NS2
275             dest:  Says_imp_knows_Spy analz.Inj unique_session_keys)
276txt\<open>Oops\<close>
277apply (blast dest: unique_session_keys)
278done
279
280
281
282text\<open>Final version: Server's message in the most abstract form\<close>
283lemma Spy_not_see_encrypted_key:
284     "\<lbrakk>Says Server A (Crypt K' \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
285       \<forall>NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
286       A \<notin> bad;  B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
287      \<Longrightarrow> Key K \<notin> analz (spies evs)"
288by (blast dest: Says_Server_message_form secrecy_lemma)
289
290
291subsection\<open>Guarantees available at various stages of protocol\<close>
292
293text\<open>If the encrypted message appears then it originated with the Server\<close>
294lemma B_trusts_NS3:
295     "\<lbrakk>Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace> \<in> parts (spies evs);
296       B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
297      \<Longrightarrow> \<exists>NA. Says Server A
298               (Crypt (shrK A) \<lbrace>NA, Agent B, Key K,
299                                 Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>)
300              \<in> set evs"
301apply (erule rev_mp)
302apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, auto)
303done
304
305
306lemma A_trusts_NS4_lemma [rule_format]:
307   "evs \<in> ns_shared \<Longrightarrow>
308      Key K \<notin> analz (spies evs) \<longrightarrow>
309      Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs \<longrightarrow>
310      Crypt K (Nonce NB) \<in> parts (spies evs) \<longrightarrow>
311      Says B A (Crypt K (Nonce NB)) \<in> set evs"
312apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
313apply (analz_mono_contra, simp_all, blast)
314txt\<open>NS2: contradiction from the assumptions \<^term>\<open>Key K \<notin> used evs2\<close> and
315    \<^term>\<open>Crypt K (Nonce NB) \<in> parts (spies evs2)\<close>\<close> 
316apply (force dest!: Crypt_imp_keysFor)
317txt\<open>NS4\<close>
318apply (metis B_trusts_NS3 Crypt_Spy_analz_bad Says_imp_analz_Spy Says_imp_parts_knows_Spy analz.Fst unique_session_keys)
319done
320
321text\<open>This version no longer assumes that K is secure\<close>
322lemma A_trusts_NS4:
323     "\<lbrakk>Crypt K (Nonce NB) \<in> parts (spies evs);
324       Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace> \<in> parts (spies evs);
325       \<forall>NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
326       A \<notin> bad;  B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
327      \<Longrightarrow> Says B A (Crypt K (Nonce NB)) \<in> set evs"
328by (blast intro: A_trusts_NS4_lemma
329          dest: A_trusts_NS2 Spy_not_see_encrypted_key)
330
331text\<open>If the session key has been used in NS4 then somebody has forwarded
332  component X in some instance of NS4.  Perhaps an interesting property,
333  but not needed (after all) for the proofs below.\<close>
334theorem NS4_implies_NS3 [rule_format]:
335  "evs \<in> ns_shared \<Longrightarrow>
336     Key K \<notin> analz (spies evs) \<longrightarrow>
337     Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs \<longrightarrow>
338     Crypt K (Nonce NB) \<in> parts (spies evs) \<longrightarrow>
339     (\<exists>A'. Says A' B X \<in> set evs)"
340apply (erule ns_shared.induct, force)
341apply (drule_tac [4] NS3_msg_in_parts_spies)
342apply analz_mono_contra
343apply (simp_all add: ex_disj_distrib, blast)
344txt\<open>NS2\<close>
345apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)
346txt\<open>NS4\<close>
347apply (metis B_trusts_NS3 Crypt_Spy_analz_bad Says_imp_analz_Spy Says_imp_parts_knows_Spy analz.Fst unique_session_keys)
348done
349
350
351lemma B_trusts_NS5_lemma [rule_format]:
352  "\<lbrakk>B \<notin> bad;  evs \<in> ns_shared\<rbrakk> \<Longrightarrow>
353     Key K \<notin> analz (spies evs) \<longrightarrow>
354     Says Server A
355          (Crypt (shrK A) \<lbrace>NA, Agent B, Key K,
356                            Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>) \<in> set evs \<longrightarrow>
357     Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace> \<in> parts (spies evs) \<longrightarrow>
358     Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) \<in> set evs"
359apply (erule ns_shared.induct, force)
360apply (drule_tac [4] NS3_msg_in_parts_spies)
361apply (analz_mono_contra, simp_all, blast)
362txt\<open>NS2\<close>
363apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)
364txt\<open>NS5\<close>
365apply (blast dest!: A_trusts_NS2
366             dest: Says_imp_knows_Spy [THEN analz.Inj]
367                   unique_session_keys Crypt_Spy_analz_bad)
368done
369
370
371text\<open>Very strong Oops condition reveals protocol's weakness\<close>
372lemma B_trusts_NS5:
373     "\<lbrakk>Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace> \<in> parts (spies evs);
374       Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace> \<in> parts (spies evs);
375       \<forall>NA NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
376       A \<notin> bad;  B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
377      \<Longrightarrow> Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) \<in> set evs"
378by (blast intro: B_trusts_NS5_lemma
379          dest: B_trusts_NS3 Spy_not_see_encrypted_key)
380
381text\<open>Unaltered so far wrt original version\<close>
382
383subsection\<open>Lemmas for reasoning about predicate "Issues"\<close>
384
385lemma spies_Says_rev: "spies (evs @ [Says A B X]) = insert X (spies evs)"
386apply (induct_tac "evs")
387apply (rename_tac [2] a b)
388apply (induct_tac [2] "a", auto)
389done
390
391lemma spies_Gets_rev: "spies (evs @ [Gets A X]) = spies evs"
392apply (induct_tac "evs")
393apply (rename_tac [2] a b)
394apply (induct_tac [2] "a", auto)
395done
396
397lemma spies_Notes_rev: "spies (evs @ [Notes A X]) =
398          (if A\<in>bad then insert X (spies evs) else spies evs)"
399apply (induct_tac "evs")
400apply (rename_tac [2] a b)
401apply (induct_tac [2] "a", auto)
402done
403
404lemma spies_evs_rev: "spies evs = spies (rev evs)"
405apply (induct_tac "evs")
406apply (rename_tac [2] a b)
407apply (induct_tac [2] "a")
408apply (simp_all (no_asm_simp) add: spies_Says_rev spies_Gets_rev spies_Notes_rev)
409done
410
411lemmas parts_spies_evs_revD2 = spies_evs_rev [THEN equalityD2, THEN parts_mono]
412
413lemma spies_takeWhile: "spies (takeWhile P evs) \<subseteq> spies evs"
414apply (induct_tac "evs")
415apply (rename_tac [2] a b)
416apply (induct_tac [2] "a", auto)
417txt\<open>Resembles \<open>used_subset_append\<close> in theory Event.\<close>
418done
419
420lemmas parts_spies_takeWhile_mono = spies_takeWhile [THEN parts_mono]
421
422
423subsection\<open>Guarantees of non-injective agreement on the session key, and
424of key distribution. They also express forms of freshness of certain messages,
425namely that agents were alive after something happened.\<close>
426
427lemma B_Issues_A:
428     "\<lbrakk> Says B A (Crypt K (Nonce Nb)) \<in> set evs;
429         Key K \<notin> analz (spies evs);
430         A \<notin> bad;  B \<notin> bad; evs \<in> ns_shared \<rbrakk>
431      \<Longrightarrow> B Issues A with (Crypt K (Nonce Nb)) on evs"
432apply (simp (no_asm) add: Issues_def)
433apply (rule exI)
434apply (rule conjI, assumption)
435apply (simp (no_asm))
436apply (erule rev_mp)
437apply (erule rev_mp)
438apply (erule ns_shared.induct, analz_mono_contra)
439apply (simp_all)
440txt\<open>fake\<close>
441apply blast
442apply (simp_all add: takeWhile_tail)
443txt\<open>NS3 remains by pure coincidence!\<close>
444apply (force dest!: A_trusts_NS2 Says_Server_message_form)
445txt\<open>NS4 would be the non-trivial case can be solved by Nb being used\<close>
446apply (blast dest: parts_spies_takeWhile_mono [THEN subsetD]
447                   parts_spies_evs_revD2 [THEN subsetD])
448done
449
450text\<open>Tells A that B was alive after she sent him the session key.  The
451session key must be assumed confidential for this deduction to be meaningful,
452but that assumption can be relaxed by the appropriate argument.
453
454Precisely, the theorem guarantees (to A) key distribution of the session key
455to B. It also guarantees (to A) non-injective agreement of B with A on the
456session key. Both goals are available to A in the sense of Goal Availability.
457\<close>
458lemma A_authenticates_and_keydist_to_B:
459     "\<lbrakk>Crypt K (Nonce NB) \<in> parts (spies evs);
460       Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace> \<in> parts (spies evs);
461       Key K \<notin> analz(knows Spy evs);
462       A \<notin> bad;  B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
463      \<Longrightarrow> B Issues A with (Crypt K (Nonce NB)) on evs"
464by (blast intro: A_trusts_NS4_lemma B_Issues_A dest: A_trusts_NS2)
465
466lemma A_trusts_NS5:
467  "\<lbrakk> Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace> \<in> parts(spies evs);
468     Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace> \<in> parts(spies evs);
469     Key K \<notin> analz (spies evs);
470     A \<notin> bad; B \<notin> bad; evs \<in> ns_shared \<rbrakk>
471 \<Longrightarrow> Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) \<in> set evs"
472apply (erule rev_mp)
473apply (erule rev_mp)
474apply (erule rev_mp)
475apply (erule ns_shared.induct, analz_mono_contra)
476apply (simp_all)
477txt\<open>Fake\<close>
478apply blast
479txt\<open>NS2\<close>
480apply (force dest!: Crypt_imp_keysFor)
481txt\<open>NS3\<close>
482apply (metis NS3_msg_in_parts_spies parts_cut_eq)
483txt\<open>NS5, the most important case, can be solved by unicity\<close>
484apply (metis A_trusts_NS2 Crypt_Spy_analz_bad Says_imp_analz_Spy Says_imp_parts_knows_Spy analz.Fst analz.Snd unique_session_keys)
485done
486
487lemma A_Issues_B:
488     "\<lbrakk> Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) \<in> set evs;
489        Key K \<notin> analz (spies evs);
490        A \<notin> bad;  B \<notin> bad; evs \<in> ns_shared \<rbrakk>
491    \<Longrightarrow> A Issues B with (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) on evs"
492apply (simp (no_asm) add: Issues_def)
493apply (rule exI)
494apply (rule conjI, assumption)
495apply (simp (no_asm))
496apply (erule rev_mp)
497apply (erule rev_mp)
498apply (erule ns_shared.induct, analz_mono_contra)
499apply (simp_all)
500txt\<open>fake\<close>
501apply blast
502apply (simp_all add: takeWhile_tail)
503txt\<open>NS3 remains by pure coincidence!\<close>
504apply (force dest!: A_trusts_NS2 Says_Server_message_form)
505txt\<open>NS5 is the non-trivial case and cannot be solved as in \<^term>\<open>B_Issues_A\<close>! because NB is not fresh. We need \<^term>\<open>A_trusts_NS5\<close>, proved for this very purpose\<close>
506apply (blast dest: A_trusts_NS5 parts_spies_takeWhile_mono [THEN subsetD]
507        parts_spies_evs_revD2 [THEN subsetD])
508done
509
510text\<open>Tells B that A was alive after B issued NB.
511
512Precisely, the theorem guarantees (to B) key distribution of the session key to A. It also guarantees (to B) non-injective agreement of A with B on the session key. Both goals are available to B in the sense of Goal Availability.
513\<close>
514lemma B_authenticates_and_keydist_to_A:
515     "\<lbrakk>Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace> \<in> parts (spies evs);
516       Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace> \<in> parts (spies evs);
517       Key K \<notin> analz (spies evs);
518       A \<notin> bad;  B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
519   \<Longrightarrow> A Issues B with (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) on evs"
520by (blast intro: A_Issues_B B_trusts_NS5_lemma dest: B_trusts_NS3)
521
522end
523