src/HOL/Auth/NS_Shared.thy
author wenzelm
Thu Jul 22 18:08:39 2010 +0200 (2010-07-22)
changeset 37936 1e4c5015a72e
parent 36866 426d5781bb25
child 38617 f7b32911340b
permissions -rw-r--r--
updated some headers;
     1 (*  Title:      HOL/Auth/NS_Shared.thy
     2     Author:     Lawrence C Paulson and Giampaolo Bella 
     3     Copyright   1996  University of Cambridge
     4 *)
     5 
     6 header{*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 declare image_eq_UN [simp]  (*accelerates proofs involving nested images*)
    90 
    91 
    92 text{*A "possibility property": there are traces that reach the end*}
    93 lemma "[| A \<noteq> Server; Key K \<notin> used []; K \<in> symKeys |]
    94        ==> \<exists>N. \<exists>evs \<in> ns_shared.
    95                     Says A B (Crypt K \<lbrace>Nonce N, Nonce N\<rbrace>) \<in> set evs"
    96 apply (intro exI bexI)
    97 apply (rule_tac [2] ns_shared.Nil
    98        [THEN ns_shared.NS1, THEN ns_shared.NS2, THEN ns_shared.NS3,
    99         THEN ns_shared.NS4, THEN ns_shared.NS5])
   100 apply (possibility, simp add: used_Cons)
   101 done
   102 
   103 (*This version is similar, while instantiating ?K and ?N to epsilon-terms
   104 lemma "A \<noteq> Server \<Longrightarrow> \<exists>evs \<in> ns_shared.
   105                 Says A B (Crypt ?K \<lbrace>Nonce ?N, Nonce ?N\<rbrace>) \<in> set evs"
   106 *)
   107 
   108 
   109 subsection{*Inductive proofs about @{term ns_shared}*}
   110 
   111 subsubsection{*Forwarding lemmas, to aid simplification*}
   112 
   113 text{*For reasoning about the encrypted portion of message NS3*}
   114 lemma NS3_msg_in_parts_spies:
   115      "Says S A (Crypt KA \<lbrace>N, B, K, X\<rbrace>) \<in> set evs \<Longrightarrow> X \<in> parts (spies evs)"
   116 by blast
   117 
   118 text{*For reasoning about the Oops message*}
   119 lemma Oops_parts_spies:
   120      "Says Server A (Crypt (shrK A) \<lbrace>NA, B, K, X\<rbrace>) \<in> set evs
   121             \<Longrightarrow> K \<in> parts (spies evs)"
   122 by blast
   123 
   124 text{*Theorems of the form @{term "X \<notin> parts (spies evs)"} imply that NOBODY
   125     sends messages containing @{term X}*}
   126 
   127 text{*Spy never sees another agent's shared key! (unless it's bad at start)*}
   128 lemma Spy_see_shrK [simp]:
   129      "evs \<in> ns_shared \<Longrightarrow> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)"
   130 apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, simp_all, blast+)
   131 done
   132 
   133 lemma Spy_analz_shrK [simp]:
   134      "evs \<in> ns_shared \<Longrightarrow> (Key (shrK A) \<in> analz (spies evs)) = (A \<in> bad)"
   135 by auto
   136 
   137 
   138 text{*Nobody can have used non-existent keys!*}
   139 lemma new_keys_not_used [simp]:
   140     "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> ns_shared|]
   141      ==> K \<notin> keysFor (parts (spies evs))"
   142 apply (erule rev_mp)
   143 apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, simp_all)
   144 txt{*Fake, NS2, NS4, NS5*}
   145 apply (force dest!: keysFor_parts_insert, blast+)
   146 done
   147 
   148 
   149 subsubsection{*Lemmas concerning the form of items passed in messages*}
   150 
   151 text{*Describes the form of K, X and K' when the Server sends this message.*}
   152 lemma Says_Server_message_form:
   153      "\<lbrakk>Says Server A (Crypt K' \<lbrace>N, Agent B, Key K, X\<rbrace>) \<in> set evs;
   154        evs \<in> ns_shared\<rbrakk>
   155       \<Longrightarrow> K \<notin> range shrK \<and>
   156           X = (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>) \<and>
   157           K' = shrK A"
   158 by (erule rev_mp, erule ns_shared.induct, auto)
   159 
   160 
   161 text{*If the encrypted message appears then it originated with the Server*}
   162 lemma A_trusts_NS2:
   163      "\<lbrakk>Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace> \<in> parts (spies evs);
   164        A \<notin> bad;  evs \<in> ns_shared\<rbrakk>
   165       \<Longrightarrow> Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs"
   166 apply (erule rev_mp)
   167 apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, auto)
   168 done
   169 
   170 lemma cert_A_form:
   171      "\<lbrakk>Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace> \<in> parts (spies evs);
   172        A \<notin> bad;  evs \<in> ns_shared\<rbrakk>
   173       \<Longrightarrow> K \<notin> range shrK \<and>  X = (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>)"
   174 by (blast dest!: A_trusts_NS2 Says_Server_message_form)
   175 
   176 text{*EITHER describes the form of X when the following message is sent,
   177   OR     reduces it to the Fake case.
   178   Use @{text Says_Server_message_form} if applicable.*}
   179 lemma Says_S_message_form:
   180      "\<lbrakk>Says S A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
   181        evs \<in> ns_shared\<rbrakk>
   182       \<Longrightarrow> (K \<notin> range shrK \<and> X = (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>))
   183           \<or> X \<in> analz (spies evs)"
   184 by (blast dest: Says_imp_knows_Spy analz_shrK_Decrypt cert_A_form analz.Inj)
   185 
   186 
   187 (*Alternative version also provable
   188 lemma Says_S_message_form2:
   189   "\<lbrakk>Says S A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
   190     evs \<in> ns_shared\<rbrakk>
   191    \<Longrightarrow> Says Server A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs
   192        \<or> X \<in> analz (spies evs)"
   193 apply (case_tac "A \<in> bad")
   194 apply (force dest!: Says_imp_knows_Spy [THEN analz.Inj])
   195 by (blast dest!: A_trusts_NS2 Says_Server_message_form)
   196 *)
   197 
   198 
   199 (****
   200  SESSION KEY COMPROMISE THEOREM.  To prove theorems of the form
   201 
   202   Key K \<in> analz (insert (Key KAB) (spies evs)) \<Longrightarrow>
   203   Key K \<in> analz (spies evs)
   204 
   205  A more general formula must be proved inductively.
   206 ****)
   207 
   208 text{*NOT useful in this form, but it says that session keys are not used
   209   to encrypt messages containing other keys, in the actual protocol.
   210   We require that agents should behave like this subsequently also.*}
   211 lemma  "\<lbrakk>evs \<in> ns_shared;  Kab \<notin> range shrK\<rbrakk> \<Longrightarrow>
   212          (Crypt KAB X) \<in> parts (spies evs) \<and>
   213          Key K \<in> parts {X} \<longrightarrow> Key K \<in> parts (spies evs)"
   214 apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, simp_all)
   215 txt{*Fake*}
   216 apply (blast dest: parts_insert_subset_Un)
   217 txt{*Base, NS4 and NS5*}
   218 apply auto
   219 done
   220 
   221 
   222 subsubsection{*Session keys are not used to encrypt other session keys*}
   223 
   224 text{*The equality makes the induction hypothesis easier to apply*}
   225 
   226 lemma analz_image_freshK [rule_format]:
   227  "evs \<in> ns_shared \<Longrightarrow>
   228    \<forall>K KK. KK \<subseteq> - (range shrK) \<longrightarrow>
   229              (Key K \<in> analz (Key`KK \<union> (spies evs))) =
   230              (K \<in> KK \<or> Key K \<in> analz (spies evs))"
   231 apply (erule ns_shared.induct)
   232 apply (drule_tac [8] Says_Server_message_form)
   233 apply (erule_tac [5] Says_S_message_form [THEN disjE], analz_freshK, spy_analz)
   234 txt{*NS2, NS3*}
   235 apply blast+; 
   236 done
   237 
   238 
   239 lemma analz_insert_freshK:
   240      "\<lbrakk>evs \<in> ns_shared;  KAB \<notin> range shrK\<rbrakk> \<Longrightarrow>
   241        (Key K \<in> analz (insert (Key KAB) (spies evs))) =
   242        (K = KAB \<or> Key K \<in> analz (spies evs))"
   243 by (simp only: analz_image_freshK analz_image_freshK_simps)
   244 
   245 
   246 subsubsection{*The session key K uniquely identifies the message*}
   247 
   248 text{*In messages of this form, the session key uniquely identifies the rest*}
   249 lemma unique_session_keys:
   250      "\<lbrakk>Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
   251        Says Server A' (Crypt (shrK A') \<lbrace>NA', Agent B', Key K, X'\<rbrace>) \<in> set evs;
   252        evs \<in> ns_shared\<rbrakk> \<Longrightarrow> A=A' \<and> NA=NA' \<and> B=B' \<and> X = X'"
   253 by (erule rev_mp, erule rev_mp, erule ns_shared.induct, simp_all, blast+)
   254 
   255 
   256 subsubsection{*Crucial secrecy property: Spy doesn't see the keys sent in NS2*}
   257 
   258 text{*Beware of @{text "[rule_format]"} and the universal quantifier!*}
   259 lemma secrecy_lemma:
   260      "\<lbrakk>Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K,
   261                                       Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>)
   262               \<in> set evs;
   263          A \<notin> bad;  B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
   264       \<Longrightarrow> (\<forall>NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs) \<longrightarrow>
   265          Key K \<notin> analz (spies evs)"
   266 apply (erule rev_mp)
   267 apply (erule ns_shared.induct, force)
   268 apply (frule_tac [7] Says_Server_message_form)
   269 apply (frule_tac [4] Says_S_message_form)
   270 apply (erule_tac [5] disjE)
   271 apply (simp_all add: analz_insert_eq analz_insert_freshK pushes split_ifs, spy_analz)
   272 txt{*NS2*}
   273 apply blast
   274 txt{*NS3*}
   275 apply (blast dest!: Crypt_Spy_analz_bad A_trusts_NS2
   276              dest:  Says_imp_knows_Spy analz.Inj unique_session_keys)
   277 txt{*Oops*}
   278 apply (blast dest: unique_session_keys)
   279 done
   280 
   281 
   282 
   283 text{*Final version: Server's message in the most abstract form*}
   284 lemma Spy_not_see_encrypted_key:
   285      "\<lbrakk>Says Server A (Crypt K' \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
   286        \<forall>NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
   287        A \<notin> bad;  B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
   288       \<Longrightarrow> Key K \<notin> analz (spies evs)"
   289 by (blast dest: Says_Server_message_form secrecy_lemma)
   290 
   291 
   292 subsection{*Guarantees available at various stages of protocol*}
   293 
   294 text{*If the encrypted message appears then it originated with the Server*}
   295 lemma B_trusts_NS3:
   296      "\<lbrakk>Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace> \<in> parts (spies evs);
   297        B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
   298       \<Longrightarrow> \<exists>NA. Says Server A
   299                (Crypt (shrK A) \<lbrace>NA, Agent B, Key K,
   300                                  Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>)
   301               \<in> set evs"
   302 apply (erule rev_mp)
   303 apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, auto)
   304 done
   305 
   306 
   307 lemma A_trusts_NS4_lemma [rule_format]:
   308    "evs \<in> ns_shared \<Longrightarrow>
   309       Key K \<notin> analz (spies evs) \<longrightarrow>
   310       Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs \<longrightarrow>
   311       Crypt K (Nonce NB) \<in> parts (spies evs) \<longrightarrow>
   312       Says B A (Crypt K (Nonce NB)) \<in> set evs"
   313 apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
   314 apply (analz_mono_contra, simp_all, blast)
   315 txt{*NS2: contradiction from the assumptions @{term "Key K \<notin> used evs2"} and
   316     @{term "Crypt K (Nonce NB) \<in> parts (spies evs2)"} *} 
   317 apply (force dest!: Crypt_imp_keysFor)
   318 txt{*NS4*}
   319 apply (metis B_trusts_NS3 Crypt_Spy_analz_bad Says_imp_analz_Spy Says_imp_parts_knows_Spy analz.Fst unique_session_keys)
   320 done
   321 
   322 text{*This version no longer assumes that K is secure*}
   323 lemma A_trusts_NS4:
   324      "\<lbrakk>Crypt K (Nonce NB) \<in> parts (spies evs);
   325        Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace> \<in> parts (spies evs);
   326        \<forall>NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
   327        A \<notin> bad;  B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
   328       \<Longrightarrow> Says B A (Crypt K (Nonce NB)) \<in> set evs"
   329 by (blast intro: A_trusts_NS4_lemma
   330           dest: A_trusts_NS2 Spy_not_see_encrypted_key)
   331 
   332 text{*If the session key has been used in NS4 then somebody has forwarded
   333   component X in some instance of NS4.  Perhaps an interesting property,
   334   but not needed (after all) for the proofs below.*}
   335 theorem NS4_implies_NS3 [rule_format]:
   336   "evs \<in> ns_shared \<Longrightarrow>
   337      Key K \<notin> analz (spies evs) \<longrightarrow>
   338      Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs \<longrightarrow>
   339      Crypt K (Nonce NB) \<in> parts (spies evs) \<longrightarrow>
   340      (\<exists>A'. Says A' B X \<in> set evs)"
   341 apply (erule ns_shared.induct, force)
   342 apply (drule_tac [4] NS3_msg_in_parts_spies)
   343 apply analz_mono_contra
   344 apply (simp_all add: ex_disj_distrib, blast)
   345 txt{*NS2*}
   346 apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)
   347 txt{*NS4*}
   348 apply (metis B_trusts_NS3 Crypt_Spy_analz_bad Says_imp_analz_Spy Says_imp_parts_knows_Spy analz.Fst unique_session_keys)
   349 done
   350 
   351 
   352 lemma B_trusts_NS5_lemma [rule_format]:
   353   "\<lbrakk>B \<notin> bad;  evs \<in> ns_shared\<rbrakk> \<Longrightarrow>
   354      Key K \<notin> analz (spies evs) \<longrightarrow>
   355      Says Server A
   356           (Crypt (shrK A) \<lbrace>NA, Agent B, Key K,
   357                             Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>) \<in> set evs \<longrightarrow>
   358      Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace> \<in> parts (spies evs) \<longrightarrow>
   359      Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) \<in> set evs"
   360 apply (erule ns_shared.induct, force)
   361 apply (drule_tac [4] NS3_msg_in_parts_spies)
   362 apply (analz_mono_contra, simp_all, blast)
   363 txt{*NS2*}
   364 apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)
   365 txt{*NS5*}
   366 apply (blast dest!: A_trusts_NS2
   367              dest: Says_imp_knows_Spy [THEN analz.Inj]
   368                    unique_session_keys Crypt_Spy_analz_bad)
   369 done
   370 
   371 
   372 text{*Very strong Oops condition reveals protocol's weakness*}
   373 lemma B_trusts_NS5:
   374      "\<lbrakk>Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace> \<in> parts (spies evs);
   375        Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace> \<in> parts (spies evs);
   376        \<forall>NA NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
   377        A \<notin> bad;  B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
   378       \<Longrightarrow> Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) \<in> set evs"
   379 by (blast intro: B_trusts_NS5_lemma
   380           dest: B_trusts_NS3 Spy_not_see_encrypted_key)
   381 
   382 text{*Unaltered so far wrt original version*}
   383 
   384 subsection{*Lemmas for reasoning about predicate "Issues"*}
   385 
   386 lemma spies_Says_rev: "spies (evs @ [Says A B X]) = insert X (spies evs)"
   387 apply (induct_tac "evs")
   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 (induct_tac [2] "a", auto)
   394 done
   395 
   396 lemma spies_Notes_rev: "spies (evs @ [Notes A X]) =
   397           (if A:bad then insert X (spies evs) else spies evs)"
   398 apply (induct_tac "evs")
   399 apply (induct_tac [2] "a", auto)
   400 done
   401 
   402 lemma spies_evs_rev: "spies evs = spies (rev evs)"
   403 apply (induct_tac "evs")
   404 apply (induct_tac [2] "a")
   405 apply (simp_all (no_asm_simp) add: spies_Says_rev spies_Gets_rev spies_Notes_rev)
   406 done
   407 
   408 lemmas parts_spies_evs_revD2 = spies_evs_rev [THEN equalityD2, THEN parts_mono]
   409 
   410 lemma spies_takeWhile: "spies (takeWhile P evs) <=  spies evs"
   411 apply (induct_tac "evs")
   412 apply (induct_tac [2] "a", auto)
   413 txt{* Resembles @{text"used_subset_append"} in theory Event.*}
   414 done
   415 
   416 lemmas parts_spies_takeWhile_mono = spies_takeWhile [THEN parts_mono]
   417 
   418 
   419 subsection{*Guarantees of non-injective agreement on the session key, and
   420 of key distribution. They also express forms of freshness of certain messages,
   421 namely that agents were alive after something happened.*}
   422 
   423 lemma B_Issues_A:
   424      "\<lbrakk> Says B A (Crypt K (Nonce Nb)) \<in> set evs;
   425          Key K \<notin> analz (spies evs);
   426          A \<notin> bad;  B \<notin> bad; evs \<in> ns_shared \<rbrakk>
   427       \<Longrightarrow> B Issues A with (Crypt K (Nonce Nb)) on evs"
   428 apply (simp (no_asm) add: Issues_def)
   429 apply (rule exI)
   430 apply (rule conjI, assumption)
   431 apply (simp (no_asm))
   432 apply (erule rev_mp)
   433 apply (erule rev_mp)
   434 apply (erule ns_shared.induct, analz_mono_contra)
   435 apply (simp_all)
   436 txt{*fake*}
   437 apply blast
   438 apply (simp_all add: takeWhile_tail)
   439 txt{*NS3 remains by pure coincidence!*}
   440 apply (force dest!: A_trusts_NS2 Says_Server_message_form)
   441 txt{*NS4 would be the non-trivial case can be solved by Nb being used*}
   442 apply (blast dest: parts_spies_takeWhile_mono [THEN subsetD]
   443                    parts_spies_evs_revD2 [THEN subsetD])
   444 done
   445 
   446 text{*Tells A that B was alive after she sent him the session key.  The
   447 session key must be assumed confidential for this deduction to be meaningful,
   448 but that assumption can be relaxed by the appropriate argument.
   449 
   450 Precisely, the theorem guarantees (to A) key distribution of the session key
   451 to B. It also guarantees (to A) non-injective agreement of B with A on the
   452 session key. Both goals are available to A in the sense of Goal Availability.
   453 *}
   454 lemma A_authenticates_and_keydist_to_B:
   455      "\<lbrakk>Crypt K (Nonce NB) \<in> parts (spies evs);
   456        Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace> \<in> parts (spies evs);
   457        Key K \<notin> analz(knows Spy evs);
   458        A \<notin> bad;  B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
   459       \<Longrightarrow> B Issues A with (Crypt K (Nonce NB)) on evs"
   460 by (blast intro: A_trusts_NS4_lemma B_Issues_A dest: A_trusts_NS2)
   461 
   462 lemma A_trusts_NS5:
   463   "\<lbrakk> Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace> \<in> parts(spies evs);
   464      Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace> \<in> parts(spies evs);
   465      Key K \<notin> analz (spies evs);
   466      A \<notin> bad; B \<notin> bad; evs \<in> ns_shared \<rbrakk>
   467  \<Longrightarrow> Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) \<in> set evs";
   468 apply (erule rev_mp)
   469 apply (erule rev_mp)
   470 apply (erule rev_mp)
   471 apply (erule ns_shared.induct, analz_mono_contra)
   472 apply (simp_all)
   473 txt{*Fake*}
   474 apply blast
   475 txt{*NS2*}
   476 apply (force dest!: Crypt_imp_keysFor)
   477 txt{*NS3*}
   478 apply (metis NS3_msg_in_parts_spies parts_cut_eq)
   479 txt{*NS5, the most important case, can be solved by unicity*}
   480 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)
   481 done
   482 
   483 lemma A_Issues_B:
   484      "\<lbrakk> Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) \<in> set evs;
   485         Key K \<notin> analz (spies evs);
   486         A \<notin> bad;  B \<notin> bad; evs \<in> ns_shared \<rbrakk>
   487     \<Longrightarrow> A Issues B with (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) on evs"
   488 apply (simp (no_asm) add: Issues_def)
   489 apply (rule exI)
   490 apply (rule conjI, assumption)
   491 apply (simp (no_asm))
   492 apply (erule rev_mp)
   493 apply (erule rev_mp)
   494 apply (erule ns_shared.induct, analz_mono_contra)
   495 apply (simp_all)
   496 txt{*fake*}
   497 apply blast
   498 apply (simp_all add: takeWhile_tail)
   499 txt{*NS3 remains by pure coincidence!*}
   500 apply (force dest!: A_trusts_NS2 Says_Server_message_form)
   501 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*}
   502 apply (blast dest: A_trusts_NS5 parts_spies_takeWhile_mono [THEN subsetD]
   503         parts_spies_evs_revD2 [THEN subsetD])
   504 done
   505 
   506 text{*Tells B that A was alive after B issued NB.
   507 
   508 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.
   509 *}
   510 lemma B_authenticates_and_keydist_to_A:
   511      "\<lbrakk>Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace> \<in> parts (spies evs);
   512        Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace> \<in> parts (spies evs);
   513        Key K \<notin> analz (spies evs);
   514        A \<notin> bad;  B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
   515    \<Longrightarrow> A Issues B with (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) on evs"
   516 by (blast intro: A_Issues_B B_trusts_NS5_lemma dest: B_trusts_NS3)
   517 
   518 end