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