src/HOL/Auth/NS_Shared.thy
author wenzelm
Mon Aug 31 21:28:08 2015 +0200 (2015-08-31)
changeset 61070 b72a990adfe2
parent 58889 5b7a9633cfa8
child 61830 4f5ab843cf5b
permissions -rw-r--r--
prefer symbols;
     1 (*  Title:      HOL/Auth/NS_Shared.thy
     2     Author:     Lawrence C Paulson and Giampaolo Bella 
     3     Copyright   1996  University of Cambridge
     4 *)
     5 
     6 section{*Needham-Schroeder Shared-Key Protocol and the Issues Property*}
     7 
     8 theory NS_Shared imports Public begin
     9 
    10 text{*
    11 From page 247 of
    12   Burrows, Abadi and Needham (1989).  A Logic of Authentication.
    13   Proc. Royal Soc. 426
    14 *}
    15 
    16 definition
    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] => bool"
    20              ("_ Issues _ with _ on _") where
    21    "A Issues B with X on evs =
    22       (\<exists>Y. Says A B Y \<in> set evs & X \<in> parts {Y} &
    23         X \<notin> parts (spies (takeWhile (% z. z  \<noteq> Says A B Y) (rev evs))))"
    24 
    25 
    26 inductive_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 
    85 declare Says_imp_knows_Spy [THEN parts.Inj, dest]
    86 declare parts.Body  [dest]
    87 declare Fake_parts_insert_in_Un  [dest]
    88 declare analz_into_parts [dest]
    89 
    90 
    91 text{*A "possibility property": there are traces that reach the end*}
    92 lemma "[| 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"
    95 apply (intro exI bexI)
    96 apply (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])
    99 apply (possibility, simp add: used_Cons)
   100 done
   101 
   102 (*This version is similar, while instantiating ?K and ?N to epsilon-terms
   103 lemma "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 
   108 subsection{*Inductive proofs about @{term ns_shared}*}
   109 
   110 subsubsection{*Forwarding lemmas, to aid simplification*}
   111 
   112 text{*For reasoning about the encrypted portion of message NS3*}
   113 lemma 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)"
   115 by blast
   116 
   117 text{*For reasoning about the Oops message*}
   118 lemma 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)"
   121 by blast
   122 
   123 text{*Theorems of the form @{term "X \<notin> parts (spies evs)"} imply that NOBODY
   124     sends messages containing @{term X}*}
   125 
   126 text{*Spy never sees another agent's shared key! (unless it's bad at start)*}
   127 lemma Spy_see_shrK [simp]:
   128      "evs \<in> ns_shared \<Longrightarrow> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)"
   129 apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, simp_all, blast+)
   130 done
   131 
   132 lemma Spy_analz_shrK [simp]:
   133      "evs \<in> ns_shared \<Longrightarrow> (Key (shrK A) \<in> analz (spies evs)) = (A \<in> bad)"
   134 by auto
   135 
   136 
   137 text{*Nobody can have used non-existent keys!*}
   138 lemma 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))"
   141 apply (erule rev_mp)
   142 apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, simp_all)
   143 txt{*Fake, NS2, NS4, NS5*}
   144 apply (force dest!: keysFor_parts_insert, blast+)
   145 done
   146 
   147 
   148 subsubsection{*Lemmas concerning the form of items passed in messages*}
   149 
   150 text{*Describes the form of K, X and K' when the Server sends this message.*}
   151 lemma 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"
   157 by (erule rev_mp, erule ns_shared.induct, auto)
   158 
   159 
   160 text{*If the encrypted message appears then it originated with the Server*}
   161 lemma 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"
   165 apply (erule rev_mp)
   166 apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, auto)
   167 done
   168 
   169 lemma 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>)"
   173 by (blast dest!: A_trusts_NS2 Says_Server_message_form)
   174 
   175 text{*EITHER describes the form of X when the following message is sent,
   176   OR     reduces it to the Fake case.
   177   Use @{text Says_Server_message_form} if applicable.*}
   178 lemma 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)"
   183 by (blast dest: Says_imp_knows_Spy analz_shrK_Decrypt cert_A_form analz.Inj)
   184 
   185 
   186 (*Alternative version also provable
   187 lemma 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)"
   192 apply (case_tac "A \<in> bad")
   193 apply (force dest!: Says_imp_knows_Spy [THEN analz.Inj])
   194 by (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 
   207 text{*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.*}
   210 lemma  "\<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)"
   213 apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, simp_all)
   214 txt{*Fake*}
   215 apply (blast dest: parts_insert_subset_Un)
   216 txt{*Base, NS4 and NS5*}
   217 apply auto
   218 done
   219 
   220 
   221 subsubsection{*Session keys are not used to encrypt other session keys*}
   222 
   223 text{*The equality makes the induction hypothesis easier to apply*}
   224 
   225 lemma 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))"
   230 apply (erule ns_shared.induct)
   231 apply (drule_tac [8] Says_Server_message_form)
   232 apply (erule_tac [5] Says_S_message_form [THEN disjE], analz_freshK, spy_analz)
   233 txt{*NS2, NS3*}
   234 apply blast+ 
   235 done
   236 
   237 
   238 lemma 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))"
   242 by (simp only: analz_image_freshK analz_image_freshK_simps)
   243 
   244 
   245 subsubsection{*The session key K uniquely identifies the message*}
   246 
   247 text{*In messages of this form, the session key uniquely identifies the rest*}
   248 lemma 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'"
   252 by (erule rev_mp, erule rev_mp, erule ns_shared.induct, simp_all, blast+)
   253 
   254 
   255 subsubsection{*Crucial secrecy property: Spy doesn't see the keys sent in NS2*}
   256 
   257 text{*Beware of @{text "[rule_format]"} and the universal quantifier!*}
   258 lemma 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)"
   265 apply (erule rev_mp)
   266 apply (erule ns_shared.induct, force)
   267 apply (frule_tac [7] Says_Server_message_form)
   268 apply (frule_tac [4] Says_S_message_form)
   269 apply (erule_tac [5] disjE)
   270 apply (simp_all add: analz_insert_eq analz_insert_freshK pushes split_ifs, spy_analz)
   271 txt{*NS2*}
   272 apply blast
   273 txt{*NS3*}
   274 apply (blast dest!: Crypt_Spy_analz_bad A_trusts_NS2
   275              dest:  Says_imp_knows_Spy analz.Inj unique_session_keys)
   276 txt{*Oops*}
   277 apply (blast dest: unique_session_keys)
   278 done
   279 
   280 
   281 
   282 text{*Final version: Server's message in the most abstract form*}
   283 lemma 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)"
   288 by (blast dest: Says_Server_message_form secrecy_lemma)
   289 
   290 
   291 subsection{*Guarantees available at various stages of protocol*}
   292 
   293 text{*If the encrypted message appears then it originated with the Server*}
   294 lemma 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"
   301 apply (erule rev_mp)
   302 apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, auto)
   303 done
   304 
   305 
   306 lemma 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"
   312 apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
   313 apply (analz_mono_contra, simp_all, blast)
   314 txt{*NS2: contradiction from the assumptions @{term "Key K \<notin> used evs2"} and
   315     @{term "Crypt K (Nonce NB) \<in> parts (spies evs2)"} *} 
   316 apply (force dest!: Crypt_imp_keysFor)
   317 txt{*NS4*}
   318 apply (metis B_trusts_NS3 Crypt_Spy_analz_bad Says_imp_analz_Spy Says_imp_parts_knows_Spy analz.Fst unique_session_keys)
   319 done
   320 
   321 text{*This version no longer assumes that K is secure*}
   322 lemma 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"
   328 by (blast intro: A_trusts_NS4_lemma
   329           dest: A_trusts_NS2 Spy_not_see_encrypted_key)
   330 
   331 text{*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.*}
   334 theorem 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)"
   340 apply (erule ns_shared.induct, force)
   341 apply (drule_tac [4] NS3_msg_in_parts_spies)
   342 apply analz_mono_contra
   343 apply (simp_all add: ex_disj_distrib, blast)
   344 txt{*NS2*}
   345 apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)
   346 txt{*NS4*}
   347 apply (metis B_trusts_NS3 Crypt_Spy_analz_bad Says_imp_analz_Spy Says_imp_parts_knows_Spy analz.Fst unique_session_keys)
   348 done
   349 
   350 
   351 lemma 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"
   359 apply (erule ns_shared.induct, force)
   360 apply (drule_tac [4] NS3_msg_in_parts_spies)
   361 apply (analz_mono_contra, simp_all, blast)
   362 txt{*NS2*}
   363 apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)
   364 txt{*NS5*}
   365 apply (blast dest!: A_trusts_NS2
   366              dest: Says_imp_knows_Spy [THEN analz.Inj]
   367                    unique_session_keys Crypt_Spy_analz_bad)
   368 done
   369 
   370 
   371 text{*Very strong Oops condition reveals protocol's weakness*}
   372 lemma 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"
   378 by (blast intro: B_trusts_NS5_lemma
   379           dest: B_trusts_NS3 Spy_not_see_encrypted_key)
   380 
   381 text{*Unaltered so far wrt original version*}
   382 
   383 subsection{*Lemmas for reasoning about predicate "Issues"*}
   384 
   385 lemma spies_Says_rev: "spies (evs @ [Says A B X]) = insert X (spies evs)"
   386 apply (induct_tac "evs")
   387 apply (rename_tac [2] a b)
   388 apply (induct_tac [2] "a", auto)
   389 done
   390 
   391 lemma spies_Gets_rev: "spies (evs @ [Gets A X]) = spies evs"
   392 apply (induct_tac "evs")
   393 apply (rename_tac [2] a b)
   394 apply (induct_tac [2] "a", auto)
   395 done
   396 
   397 lemma spies_Notes_rev: "spies (evs @ [Notes A X]) =
   398           (if A:bad then insert X (spies evs) else spies evs)"
   399 apply (induct_tac "evs")
   400 apply (rename_tac [2] a b)
   401 apply (induct_tac [2] "a", auto)
   402 done
   403 
   404 lemma spies_evs_rev: "spies evs = spies (rev evs)"
   405 apply (induct_tac "evs")
   406 apply (rename_tac [2] a b)
   407 apply (induct_tac [2] "a")
   408 apply (simp_all (no_asm_simp) add: spies_Says_rev spies_Gets_rev spies_Notes_rev)
   409 done
   410 
   411 lemmas parts_spies_evs_revD2 = spies_evs_rev [THEN equalityD2, THEN parts_mono]
   412 
   413 lemma spies_takeWhile: "spies (takeWhile P evs) <=  spies evs"
   414 apply (induct_tac "evs")
   415 apply (rename_tac [2] a b)
   416 apply (induct_tac [2] "a", auto)
   417 txt{* Resembles @{text"used_subset_append"} in theory Event.*}
   418 done
   419 
   420 lemmas parts_spies_takeWhile_mono = spies_takeWhile [THEN parts_mono]
   421 
   422 
   423 subsection{*Guarantees of non-injective agreement on the session key, and
   424 of key distribution. They also express forms of freshness of certain messages,
   425 namely that agents were alive after something happened.*}
   426 
   427 lemma 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"
   432 apply (simp (no_asm) add: Issues_def)
   433 apply (rule exI)
   434 apply (rule conjI, assumption)
   435 apply (simp (no_asm))
   436 apply (erule rev_mp)
   437 apply (erule rev_mp)
   438 apply (erule ns_shared.induct, analz_mono_contra)
   439 apply (simp_all)
   440 txt{*fake*}
   441 apply blast
   442 apply (simp_all add: takeWhile_tail)
   443 txt{*NS3 remains by pure coincidence!*}
   444 apply (force dest!: A_trusts_NS2 Says_Server_message_form)
   445 txt{*NS4 would be the non-trivial case can be solved by Nb being used*}
   446 apply (blast dest: parts_spies_takeWhile_mono [THEN subsetD]
   447                    parts_spies_evs_revD2 [THEN subsetD])
   448 done
   449 
   450 text{*Tells A that B was alive after she sent him the session key.  The
   451 session key must be assumed confidential for this deduction to be meaningful,
   452 but that assumption can be relaxed by the appropriate argument.
   453 
   454 Precisely, the theorem guarantees (to A) key distribution of the session key
   455 to B. It also guarantees (to A) non-injective agreement of B with A on the
   456 session key. Both goals are available to A in the sense of Goal Availability.
   457 *}
   458 lemma 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"
   464 by (blast intro: A_trusts_NS4_lemma B_Issues_A dest: A_trusts_NS2)
   465 
   466 lemma 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"
   472 apply (erule rev_mp)
   473 apply (erule rev_mp)
   474 apply (erule rev_mp)
   475 apply (erule ns_shared.induct, analz_mono_contra)
   476 apply (simp_all)
   477 txt{*Fake*}
   478 apply blast
   479 txt{*NS2*}
   480 apply (force dest!: Crypt_imp_keysFor)
   481 txt{*NS3*}
   482 apply (metis NS3_msg_in_parts_spies parts_cut_eq)
   483 txt{*NS5, the most important case, can be solved by unicity*}
   484 apply (metis A_trusts_NS2 Crypt_Spy_analz_bad Says_imp_analz_Spy Says_imp_parts_knows_Spy analz.Fst analz.Snd unique_session_keys)
   485 done
   486 
   487 lemma 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"
   492 apply (simp (no_asm) add: Issues_def)
   493 apply (rule exI)
   494 apply (rule conjI, assumption)
   495 apply (simp (no_asm))
   496 apply (erule rev_mp)
   497 apply (erule rev_mp)
   498 apply (erule ns_shared.induct, analz_mono_contra)
   499 apply (simp_all)
   500 txt{*fake*}
   501 apply blast
   502 apply (simp_all add: takeWhile_tail)
   503 txt{*NS3 remains by pure coincidence!*}
   504 apply (force dest!: A_trusts_NS2 Says_Server_message_form)
   505 txt{*NS5 is the non-trivial case and cannot be solved as in @{term B_Issues_A}! because NB is not fresh. We need @{term A_trusts_NS5}, proved for this very purpose*}
   506 apply (blast dest: A_trusts_NS5 parts_spies_takeWhile_mono [THEN subsetD]
   507         parts_spies_evs_revD2 [THEN subsetD])
   508 done
   509 
   510 text{*Tells B that A was alive after B issued NB.
   511 
   512 Precisely, 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 *}
   514 lemma 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"
   520 by (blast intro: A_Issues_B B_trusts_NS5_lemma dest: B_trusts_NS3)
   521 
   522 end