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