src/HOL/Auth/Yahalom.thy
author wenzelm
Mon Jan 11 21:21:02 2016 +0100 (2016-01-11)
changeset 62145 5b946c81dfbf
parent 61956 38b73f7940af
child 64364 464420ba7f74
permissions -rw-r--r--
eliminated old defs;
     1 (*  Title:      HOL/Auth/Yahalom.thy
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Copyright   1996  University of Cambridge
     4 *)
     5 
     6 section\<open>The Yahalom Protocol\<close>
     7 
     8 theory Yahalom imports Public begin
     9 
    10 text\<open>From page 257 of
    11   Burrows, Abadi and Needham (1989).  A Logic of Authentication.
    12   Proc. Royal Soc. 426
    13 
    14 This theory has the prototypical example of a secrecy relation, KeyCryptNonce.
    15 \<close>
    16 
    17 inductive_set yahalom :: "event list set"
    18   where
    19          (*Initial trace is empty*)
    20    Nil:  "[] \<in> yahalom"
    21 
    22          (*The spy MAY say anything he CAN say.  We do not expect him to
    23            invent new nonces here, but he can also use NS1.  Common to
    24            all similar protocols.*)
    25  | Fake: "[| evsf \<in> yahalom;  X \<in> synth (analz (knows Spy evsf)) |]
    26           ==> Says Spy B X  # evsf \<in> yahalom"
    27 
    28          (*A message that has been sent can be received by the
    29            intended recipient.*)
    30  | Reception: "[| evsr \<in> yahalom;  Says A B X \<in> set evsr |]
    31                ==> Gets B X # evsr \<in> yahalom"
    32 
    33          (*Alice initiates a protocol run*)
    34  | YM1:  "[| evs1 \<in> yahalom;  Nonce NA \<notin> used evs1 |]
    35           ==> Says A B \<lbrace>Agent A, Nonce NA\<rbrace> # evs1 \<in> yahalom"
    36 
    37          (*Bob's response to Alice's message.*)
    38  | YM2:  "[| evs2 \<in> yahalom;  Nonce NB \<notin> used evs2;
    39              Gets B \<lbrace>Agent A, Nonce NA\<rbrace> \<in> set evs2 |]
    40           ==> Says B Server 
    41                   \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>\<rbrace>
    42                 # evs2 \<in> yahalom"
    43 
    44          (*The Server receives Bob's message.  He responds by sending a
    45             new session key to Alice, with a packet for forwarding to Bob.*)
    46  | YM3:  "[| evs3 \<in> yahalom;  Key KAB \<notin> used evs3;  KAB \<in> symKeys;
    47              Gets Server 
    48                   \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>\<rbrace>
    49                \<in> set evs3 |]
    50           ==> Says Server A
    51                    \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key KAB, Nonce NA, Nonce NB\<rbrace>,
    52                      Crypt (shrK B) \<lbrace>Agent A, Key KAB\<rbrace>\<rbrace>
    53                 # evs3 \<in> yahalom"
    54 
    55  | YM4:  
    56        \<comment>\<open>Alice receives the Server's (?) message, checks her Nonce, and
    57            uses the new session key to send Bob his Nonce.  The premise
    58            @{term "A \<noteq> Server"} is needed for \<open>Says_Server_not_range\<close>.
    59            Alice can check that K is symmetric by its length.\<close>
    60          "[| evs4 \<in> yahalom;  A \<noteq> Server;  K \<in> symKeys;
    61              Gets A \<lbrace>Crypt(shrK A) \<lbrace>Agent B, Key K, Nonce NA, Nonce NB\<rbrace>, X\<rbrace>
    62                 \<in> set evs4;
    63              Says A B \<lbrace>Agent A, Nonce NA\<rbrace> \<in> set evs4 |]
    64           ==> Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> # evs4 \<in> yahalom"
    65 
    66          (*This message models possible leaks of session keys.  The Nonces
    67            identify the protocol run.  Quoting Server here ensures they are
    68            correct.*)
    69  | Oops: "[| evso \<in> yahalom;  
    70              Says Server A \<lbrace>Crypt (shrK A)
    71                                    \<lbrace>Agent B, Key K, Nonce NA, Nonce NB\<rbrace>,
    72                              X\<rbrace>  \<in> set evso |]
    73           ==> Notes Spy \<lbrace>Nonce NA, Nonce NB, Key K\<rbrace> # evso \<in> yahalom"
    74 
    75 
    76 definition KeyWithNonce :: "[key, nat, event list] => bool" where
    77   "KeyWithNonce K NB evs ==
    78      \<exists>A B na X. 
    79        Says Server A \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, Nonce NB\<rbrace>, X\<rbrace>
    80          \<in> set evs"
    81 
    82 
    83 declare Says_imp_analz_Spy [dest]
    84 declare parts.Body  [dest]
    85 declare Fake_parts_insert_in_Un  [dest]
    86 declare analz_into_parts [dest]
    87 
    88 text\<open>A "possibility property": there are traces that reach the end\<close>
    89 lemma "[| A \<noteq> Server; K \<in> symKeys; Key K \<notin> used [] |]
    90       ==> \<exists>X NB. \<exists>evs \<in> yahalom.
    91              Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs"
    92 apply (intro exI bexI)
    93 apply (rule_tac [2] yahalom.Nil
    94                     [THEN yahalom.YM1, THEN yahalom.Reception,
    95                      THEN yahalom.YM2, THEN yahalom.Reception,
    96                      THEN yahalom.YM3, THEN yahalom.Reception,
    97                      THEN yahalom.YM4])
    98 apply (possibility, simp add: used_Cons)
    99 done
   100 
   101 
   102 subsection\<open>Regularity Lemmas for Yahalom\<close>
   103 
   104 lemma Gets_imp_Says:
   105      "[| Gets B X \<in> set evs; evs \<in> yahalom |] ==> \<exists>A. Says A B X \<in> set evs"
   106 by (erule rev_mp, erule yahalom.induct, auto)
   107 
   108 text\<open>Must be proved separately for each protocol\<close>
   109 lemma Gets_imp_knows_Spy:
   110      "[| Gets B X \<in> set evs; evs \<in> yahalom |]  ==> X \<in> knows Spy evs"
   111 by (blast dest!: Gets_imp_Says Says_imp_knows_Spy)
   112 
   113 lemmas Gets_imp_analz_Spy = Gets_imp_knows_Spy [THEN analz.Inj]
   114 declare Gets_imp_analz_Spy [dest]
   115 
   116 
   117 text\<open>Lets us treat YM4 using a similar argument as for the Fake case.\<close>
   118 lemma YM4_analz_knows_Spy:
   119      "[| Gets A \<lbrace>Crypt (shrK A) Y, X\<rbrace> \<in> set evs;  evs \<in> yahalom |]
   120       ==> X \<in> analz (knows Spy evs)"
   121 by blast
   122 
   123 lemmas YM4_parts_knows_Spy =
   124        YM4_analz_knows_Spy [THEN analz_into_parts]
   125 
   126 text\<open>For Oops\<close>
   127 lemma YM4_Key_parts_knows_Spy:
   128      "Says Server A \<lbrace>Crypt (shrK A) \<lbrace>B,K,NA,NB\<rbrace>, X\<rbrace> \<in> set evs
   129       ==> K \<in> parts (knows Spy evs)"
   130   by (metis parts.Body parts.Fst parts.Snd  Says_imp_knows_Spy parts.Inj)
   131 
   132 text\<open>Theorems of the form @{term "X \<notin> parts (knows Spy evs)"} imply 
   133 that NOBODY sends messages containing X!\<close>
   134 
   135 text\<open>Spy never sees a good agent's shared key!\<close>
   136 lemma Spy_see_shrK [simp]:
   137      "evs \<in> yahalom ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"
   138 by (erule yahalom.induct, force,
   139     drule_tac [6] YM4_parts_knows_Spy, simp_all, blast+)
   140 
   141 lemma Spy_analz_shrK [simp]:
   142      "evs \<in> yahalom ==> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)"
   143 by auto
   144 
   145 lemma Spy_see_shrK_D [dest!]:
   146      "[|Key (shrK A) \<in> parts (knows Spy evs);  evs \<in> yahalom|] ==> A \<in> bad"
   147 by (blast dest: Spy_see_shrK)
   148 
   149 text\<open>Nobody can have used non-existent keys!
   150     Needed to apply \<open>analz_insert_Key\<close>\<close>
   151 lemma new_keys_not_used [simp]:
   152     "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> yahalom|]
   153      ==> K \<notin> keysFor (parts (spies evs))"
   154 apply (erule rev_mp)
   155 apply (erule yahalom.induct, force,
   156        frule_tac [6] YM4_parts_knows_Spy, simp_all)
   157 txt\<open>Fake\<close>
   158 apply (force dest!: keysFor_parts_insert, auto)
   159 done
   160 
   161 
   162 text\<open>Earlier, all protocol proofs declared this theorem.
   163   But only a few proofs need it, e.g. Yahalom and Kerberos IV.\<close>
   164 lemma new_keys_not_analzd:
   165  "[|K \<in> symKeys; evs \<in> yahalom; Key K \<notin> used evs|]
   166   ==> K \<notin> keysFor (analz (knows Spy evs))"
   167 by (blast dest: new_keys_not_used intro: keysFor_mono [THEN subsetD])
   168 
   169 
   170 text\<open>Describes the form of K when the Server sends this message.  Useful for
   171   Oops as well as main secrecy property.\<close>
   172 lemma Says_Server_not_range [simp]:
   173      "[| Says Server A \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace>, X\<rbrace>
   174            \<in> set evs;   evs \<in> yahalom |]
   175       ==> K \<notin> range shrK"
   176 by (erule rev_mp, erule yahalom.induct, simp_all)
   177 
   178 
   179 subsection\<open>Secrecy Theorems\<close>
   180 
   181 (****
   182  The following is to prove theorems of the form
   183 
   184   Key K \<in> analz (insert (Key KAB) (knows Spy evs)) ==>
   185   Key K \<in> analz (knows Spy evs)
   186 
   187  A more general formula must be proved inductively.
   188 ****)
   189 
   190 text\<open>Session keys are not used to encrypt other session keys\<close>
   191 
   192 lemma analz_image_freshK [rule_format]:
   193  "evs \<in> yahalom ==>
   194    \<forall>K KK. KK <= - (range shrK) -->
   195           (Key K \<in> analz (Key`KK Un (knows Spy evs))) =
   196           (K \<in> KK | Key K \<in> analz (knows Spy evs))"
   197 apply (erule yahalom.induct,
   198        drule_tac [7] YM4_analz_knows_Spy, analz_freshK, spy_analz, blast)
   199 apply (simp only: Says_Server_not_range analz_image_freshK_simps)
   200 apply safe
   201 done
   202 
   203 lemma analz_insert_freshK:
   204      "[| evs \<in> yahalom;  KAB \<notin> range shrK |] ==>
   205       (Key K \<in> analz (insert (Key KAB) (knows Spy evs))) =
   206       (K = KAB | Key K \<in> analz (knows Spy evs))"
   207 by (simp only: analz_image_freshK analz_image_freshK_simps)
   208 
   209 
   210 text\<open>The Key K uniquely identifies the Server's  message.\<close>
   211 lemma unique_session_keys:
   212      "[| Says Server A
   213           \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace>, X\<rbrace> \<in> set evs;
   214         Says Server A'
   215           \<lbrace>Crypt (shrK A') \<lbrace>Agent B', Key K, na', nb'\<rbrace>, X'\<rbrace> \<in> set evs;
   216         evs \<in> yahalom |]
   217      ==> A=A' & B=B' & na=na' & nb=nb'"
   218 apply (erule rev_mp, erule rev_mp)
   219 apply (erule yahalom.induct, simp_all)
   220 txt\<open>YM3, by freshness, and YM4\<close>
   221 apply blast+
   222 done
   223 
   224 
   225 text\<open>Crucial secrecy property: Spy does not see the keys sent in msg YM3\<close>
   226 lemma secrecy_lemma:
   227      "[| A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   228       ==> Says Server A
   229             \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace>,
   230               Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace>
   231            \<in> set evs -->
   232           Notes Spy \<lbrace>na, nb, Key K\<rbrace> \<notin> set evs -->
   233           Key K \<notin> analz (knows Spy evs)"
   234 apply (erule yahalom.induct, force,
   235        drule_tac [6] YM4_analz_knows_Spy)
   236 apply (simp_all add: pushes analz_insert_eq analz_insert_freshK, spy_analz)   \<comment>\<open>Fake\<close>
   237 apply (blast dest: unique_session_keys)+  \<comment>\<open>YM3, Oops\<close>
   238 done
   239 
   240 text\<open>Final version\<close>
   241 lemma Spy_not_see_encrypted_key:
   242      "[| Says Server A
   243             \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace>,
   244               Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace>
   245            \<in> set evs;
   246          Notes Spy \<lbrace>na, nb, Key K\<rbrace> \<notin> set evs;
   247          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   248       ==> Key K \<notin> analz (knows Spy evs)"
   249 by (blast dest: secrecy_lemma)
   250 
   251 
   252 subsubsection\<open>Security Guarantee for A upon receiving YM3\<close>
   253 
   254 text\<open>If the encrypted message appears then it originated with the Server\<close>
   255 lemma A_trusts_YM3:
   256      "[| Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace> \<in> parts (knows Spy evs);
   257          A \<notin> bad;  evs \<in> yahalom |]
   258        ==> Says Server A
   259             \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace>,
   260               Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace>
   261            \<in> set evs"
   262 apply (erule rev_mp)
   263 apply (erule yahalom.induct, force,
   264        frule_tac [6] YM4_parts_knows_Spy, simp_all)
   265 txt\<open>Fake, YM3\<close>
   266 apply blast+
   267 done
   268 
   269 text\<open>The obvious combination of \<open>A_trusts_YM3\<close> with
   270   \<open>Spy_not_see_encrypted_key\<close>\<close>
   271 lemma A_gets_good_key:
   272      "[| Crypt (shrK A) \<lbrace>Agent B, Key K, na, nb\<rbrace> \<in> parts (knows Spy evs);
   273          Notes Spy \<lbrace>na, nb, Key K\<rbrace> \<notin> set evs;
   274          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   275       ==> Key K \<notin> analz (knows Spy evs)"
   276   by (metis A_trusts_YM3 secrecy_lemma)
   277 
   278 
   279 subsubsection\<open>Security Guarantees for B upon receiving YM4\<close>
   280 
   281 text\<open>B knows, by the first part of A's message, that the Server distributed
   282   the key for A and B.  But this part says nothing about nonces.\<close>
   283 lemma B_trusts_YM4_shrK:
   284      "[| Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace> \<in> parts (knows Spy evs);
   285          B \<notin> bad;  evs \<in> yahalom |]
   286       ==> \<exists>NA NB. Says Server A
   287                       \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K,
   288                                          Nonce NA, Nonce NB\<rbrace>,
   289                         Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace>
   290                      \<in> set evs"
   291 apply (erule rev_mp)
   292 apply (erule yahalom.induct, force,
   293        frule_tac [6] YM4_parts_knows_Spy, simp_all)
   294 txt\<open>Fake, YM3\<close>
   295 apply blast+
   296 done
   297 
   298 text\<open>B knows, by the second part of A's message, that the Server
   299   distributed the key quoting nonce NB.  This part says nothing about
   300   agent names.  Secrecy of NB is crucial.  Note that @{term "Nonce NB
   301   \<notin> analz(knows Spy evs)"} must be the FIRST antecedent of the
   302   induction formula.\<close>
   303 
   304 lemma B_trusts_YM4_newK [rule_format]:
   305      "[|Crypt K (Nonce NB) \<in> parts (knows Spy evs);
   306         Nonce NB \<notin> analz (knows Spy evs);  evs \<in> yahalom|]
   307       ==> \<exists>A B NA. Says Server A
   308                       \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, Nonce NA, Nonce NB\<rbrace>,
   309                         Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace>
   310                      \<in> set evs"
   311 apply (erule rev_mp, erule rev_mp)
   312 apply (erule yahalom.induct, force,
   313        frule_tac [6] YM4_parts_knows_Spy)
   314 apply (analz_mono_contra, simp_all)
   315 txt\<open>Fake, YM3\<close>
   316 apply blast
   317 apply blast
   318 txt\<open>YM4.  A is uncompromised because NB is secure
   319   A's certificate guarantees the existence of the Server message\<close>
   320 apply (blast dest!: Gets_imp_Says Crypt_Spy_analz_bad
   321              dest: Says_imp_spies
   322                    parts.Inj [THEN parts.Fst, THEN A_trusts_YM3])
   323 done
   324 
   325 
   326 subsubsection\<open>Towards proving secrecy of Nonce NB\<close>
   327 
   328 text\<open>Lemmas about the predicate KeyWithNonce\<close>
   329 
   330 lemma KeyWithNonceI:
   331  "Says Server A
   332           \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, Nonce NB\<rbrace>, X\<rbrace>
   333         \<in> set evs ==> KeyWithNonce K NB evs"
   334 by (unfold KeyWithNonce_def, blast)
   335 
   336 lemma KeyWithNonce_Says [simp]:
   337    "KeyWithNonce K NB (Says S A X # evs) =
   338       (Server = S &
   339        (\<exists>B n X'. X = \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, n, Nonce NB\<rbrace>, X'\<rbrace>)
   340       | KeyWithNonce K NB evs)"
   341 by (simp add: KeyWithNonce_def, blast)
   342 
   343 
   344 lemma KeyWithNonce_Notes [simp]:
   345    "KeyWithNonce K NB (Notes A X # evs) = KeyWithNonce K NB evs"
   346 by (simp add: KeyWithNonce_def)
   347 
   348 lemma KeyWithNonce_Gets [simp]:
   349    "KeyWithNonce K NB (Gets A X # evs) = KeyWithNonce K NB evs"
   350 by (simp add: KeyWithNonce_def)
   351 
   352 text\<open>A fresh key cannot be associated with any nonce
   353   (with respect to a given trace).\<close>
   354 lemma fresh_not_KeyWithNonce:
   355      "Key K \<notin> used evs ==> ~ KeyWithNonce K NB evs"
   356 by (unfold KeyWithNonce_def, blast)
   357 
   358 text\<open>The Server message associates K with NB' and therefore not with any
   359   other nonce NB.\<close>
   360 lemma Says_Server_KeyWithNonce:
   361  "[| Says Server A \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, Nonce NB'\<rbrace>, X\<rbrace>
   362        \<in> set evs;
   363      NB \<noteq> NB';  evs \<in> yahalom |]
   364   ==> ~ KeyWithNonce K NB evs"
   365 by (unfold KeyWithNonce_def, blast dest: unique_session_keys)
   366 
   367 
   368 text\<open>The only nonces that can be found with the help of session keys are
   369   those distributed as nonce NB by the Server.  The form of the theorem
   370   recalls \<open>analz_image_freshK\<close>, but it is much more complicated.\<close>
   371 
   372 
   373 text\<open>As with \<open>analz_image_freshK\<close>, we take some pains to express the 
   374   property as a logical equivalence so that the simplifier can apply it.\<close>
   375 lemma Nonce_secrecy_lemma:
   376      "P --> (X \<in> analz (G Un H)) --> (X \<in> analz H)  ==>
   377       P --> (X \<in> analz (G Un H)) = (X \<in> analz H)"
   378 by (blast intro: analz_mono [THEN subsetD])
   379 
   380 lemma Nonce_secrecy:
   381      "evs \<in> yahalom ==>
   382       (\<forall>KK. KK <= - (range shrK) -->
   383            (\<forall>K \<in> KK. K \<in> symKeys --> ~ KeyWithNonce K NB evs)   -->
   384            (Nonce NB \<in> analz (Key`KK Un (knows Spy evs))) =
   385            (Nonce NB \<in> analz (knows Spy evs)))"
   386 apply (erule yahalom.induct,
   387        frule_tac [7] YM4_analz_knows_Spy)
   388 apply (safe del: allI impI intro!: Nonce_secrecy_lemma [THEN impI, THEN allI])
   389 apply (simp_all del: image_insert image_Un
   390        add: analz_image_freshK_simps split_ifs
   391             all_conj_distrib ball_conj_distrib
   392             analz_image_freshK fresh_not_KeyWithNonce
   393             imp_disj_not1               (*Moves NBa\<noteq>NB to the front*)
   394             Says_Server_KeyWithNonce)
   395 txt\<open>For Oops, simplification proves @{prop "NBa\<noteq>NB"}.  By
   396   @{term Says_Server_KeyWithNonce}, we get @{prop "~ KeyWithNonce K NB
   397   evs"}; then simplification can apply the induction hypothesis with
   398   @{term "KK = {K}"}.\<close>
   399 txt\<open>Fake\<close>
   400 apply spy_analz
   401 txt\<open>YM2\<close>
   402 apply blast
   403 txt\<open>YM3\<close>
   404 apply blast
   405 txt\<open>YM4\<close>
   406 apply (erule_tac V = "\<forall>KK. P KK" for P in thin_rl, clarify)
   407 txt\<open>If @{prop "A \<in> bad"} then @{term NBa} is known, therefore
   408   @{prop "NBa \<noteq> NB"}.  Previous two steps make the next step
   409   faster.\<close>
   410 apply (metis A_trusts_YM3 Gets_imp_analz_Spy Gets_imp_knows_Spy KeyWithNonce_def
   411       Spy_analz_shrK analz.Fst analz.Snd analz_shrK_Decrypt parts.Fst parts.Inj)
   412 done
   413 
   414 
   415 text\<open>Version required below: if NB can be decrypted using a session key then
   416    it was distributed with that key.  The more general form above is required
   417    for the induction to carry through.\<close>
   418 lemma single_Nonce_secrecy:
   419      "[| Says Server A
   420           \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key KAB, na, Nonce NB'\<rbrace>, X\<rbrace>
   421          \<in> set evs;
   422          NB \<noteq> NB';  KAB \<notin> range shrK;  evs \<in> yahalom |]
   423       ==> (Nonce NB \<in> analz (insert (Key KAB) (knows Spy evs))) =
   424           (Nonce NB \<in> analz (knows Spy evs))"
   425 by (simp_all del: image_insert image_Un imp_disjL
   426              add: analz_image_freshK_simps split_ifs
   427                   Nonce_secrecy Says_Server_KeyWithNonce)
   428 
   429 
   430 subsubsection\<open>The Nonce NB uniquely identifies B's message.\<close>
   431 
   432 lemma unique_NB:
   433      "[| Crypt (shrK B) \<lbrace>Agent A, Nonce NA, nb\<rbrace> \<in> parts (knows Spy evs);
   434          Crypt (shrK B') \<lbrace>Agent A', Nonce NA', nb\<rbrace> \<in> parts (knows Spy evs);
   435         evs \<in> yahalom;  B \<notin> bad;  B' \<notin> bad |]
   436       ==> NA' = NA & A' = A & B' = B"
   437 apply (erule rev_mp, erule rev_mp)
   438 apply (erule yahalom.induct, force,
   439        frule_tac [6] YM4_parts_knows_Spy, simp_all)
   440 txt\<open>Fake, and YM2 by freshness\<close>
   441 apply blast+
   442 done
   443 
   444 
   445 text\<open>Variant useful for proving secrecy of NB.  Because nb is assumed to be
   446   secret, we no longer must assume B, B' not bad.\<close>
   447 lemma Says_unique_NB:
   448      "[| Says C S   \<lbrace>X,  Crypt (shrK B) \<lbrace>Agent A, Nonce NA, nb\<rbrace>\<rbrace>
   449            \<in> set evs;
   450          Gets S' \<lbrace>X', Crypt (shrK B') \<lbrace>Agent A', Nonce NA', nb\<rbrace>\<rbrace>
   451            \<in> set evs;
   452          nb \<notin> analz (knows Spy evs);  evs \<in> yahalom |]
   453       ==> NA' = NA & A' = A & B' = B"
   454 by (blast dest!: Gets_imp_Says Crypt_Spy_analz_bad
   455           dest: Says_imp_spies unique_NB parts.Inj analz.Inj)
   456 
   457 
   458 subsubsection\<open>A nonce value is never used both as NA and as NB\<close>
   459 
   460 lemma no_nonce_YM1_YM2:
   461      "[|Crypt (shrK B') \<lbrace>Agent A', Nonce NB, nb'\<rbrace> \<in> parts(knows Spy evs);
   462         Nonce NB \<notin> analz (knows Spy evs);  evs \<in> yahalom|]
   463   ==> Crypt (shrK B)  \<lbrace>Agent A, na, Nonce NB\<rbrace> \<notin> parts(knows Spy evs)"
   464 apply (erule rev_mp, erule rev_mp)
   465 apply (erule yahalom.induct, force,
   466        frule_tac [6] YM4_parts_knows_Spy)
   467 apply (analz_mono_contra, simp_all)
   468 txt\<open>Fake, YM2\<close>
   469 apply blast+
   470 done
   471 
   472 text\<open>The Server sends YM3 only in response to YM2.\<close>
   473 lemma Says_Server_imp_YM2:
   474      "[| Says Server A \<lbrace>Crypt (shrK A) \<lbrace>Agent B, k, na, nb\<rbrace>, X\<rbrace> \<in> set evs;
   475          evs \<in> yahalom |]
   476       ==> Gets Server \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, na, nb\<rbrace>\<rbrace>
   477              \<in> set evs"
   478 by (erule rev_mp, erule yahalom.induct, auto)
   479 
   480 text\<open>A vital theorem for B, that nonce NB remains secure from the Spy.\<close>
   481 lemma Spy_not_see_NB :
   482      "[| Says B Server
   483                 \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>\<rbrace>
   484            \<in> set evs;
   485          (\<forall>k. Notes Spy \<lbrace>Nonce NA, Nonce NB, k\<rbrace> \<notin> set evs);
   486          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   487       ==> Nonce NB \<notin> analz (knows Spy evs)"
   488 apply (erule rev_mp, erule rev_mp)
   489 apply (erule yahalom.induct, force,
   490        frule_tac [6] YM4_analz_knows_Spy)
   491 apply (simp_all add: split_ifs pushes new_keys_not_analzd analz_insert_eq
   492                      analz_insert_freshK)
   493 txt\<open>Fake\<close>
   494 apply spy_analz
   495 txt\<open>YM1: NB=NA is impossible anyway, but NA is secret because it is fresh!\<close>
   496 apply blast
   497 txt\<open>YM2\<close>
   498 apply blast
   499 txt\<open>Prove YM3 by showing that no NB can also be an NA\<close>
   500 apply (blast dest!: no_nonce_YM1_YM2 dest: Gets_imp_Says Says_unique_NB)
   501 txt\<open>LEVEL 7: YM4 and Oops remain\<close>
   502 apply (clarify, simp add: all_conj_distrib)
   503 txt\<open>YM4: key K is visible to Spy, contradicting session key secrecy theorem\<close>
   504 txt\<open>Case analysis on Aa:bad; PROOF FAILED problems
   505   use \<open>Says_unique_NB\<close> to identify message components: @{term "Aa=A"}, @{term "Ba=B"}\<close>
   506 apply (blast dest!: Says_unique_NB analz_shrK_Decrypt
   507                     parts.Inj [THEN parts.Fst, THEN A_trusts_YM3]
   508              dest: Gets_imp_Says Says_imp_spies Says_Server_imp_YM2
   509                    Spy_not_see_encrypted_key)
   510 txt\<open>Oops case: if the nonce is betrayed now, show that the Oops event is
   511   covered by the quantified Oops assumption.\<close>
   512 apply (clarify, simp add: all_conj_distrib)
   513 apply (frule Says_Server_imp_YM2, assumption)
   514 apply (metis Gets_imp_Says Says_Server_not_range Says_unique_NB no_nonce_YM1_YM2 parts.Snd single_Nonce_secrecy spies_partsEs(1))
   515 done
   516 
   517 
   518 text\<open>B's session key guarantee from YM4.  The two certificates contribute to a
   519   single conclusion about the Server's message.  Note that the "Notes Spy"
   520   assumption must quantify over \<open>\<forall>\<close> POSSIBLE keys instead of our particular K.
   521   If this run is broken and the spy substitutes a certificate containing an
   522   old key, B has no means of telling.\<close>
   523 lemma B_trusts_YM4:
   524      "[| Gets B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>,
   525                   Crypt K (Nonce NB)\<rbrace> \<in> set evs;
   526          Says B Server
   527            \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>\<rbrace>
   528            \<in> set evs;
   529          \<forall>k. Notes Spy \<lbrace>Nonce NA, Nonce NB, k\<rbrace> \<notin> set evs;
   530          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   531        ==> Says Server A
   532                    \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K,
   533                              Nonce NA, Nonce NB\<rbrace>,
   534                      Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>\<rbrace>
   535              \<in> set evs"
   536 by (blast dest: Spy_not_see_NB Says_unique_NB
   537                 Says_Server_imp_YM2 B_trusts_YM4_newK)
   538 
   539 
   540 
   541 text\<open>The obvious combination of \<open>B_trusts_YM4\<close> with 
   542   \<open>Spy_not_see_encrypted_key\<close>\<close>
   543 lemma B_gets_good_key:
   544      "[| Gets B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>,
   545                   Crypt K (Nonce NB)\<rbrace> \<in> set evs;
   546          Says B Server
   547            \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>\<rbrace>
   548            \<in> set evs;
   549          \<forall>k. Notes Spy \<lbrace>Nonce NA, Nonce NB, k\<rbrace> \<notin> set evs;
   550          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   551       ==> Key K \<notin> analz (knows Spy evs)"
   552   by (metis B_trusts_YM4 Spy_not_see_encrypted_key)
   553 
   554 
   555 subsection\<open>Authenticating B to A\<close>
   556 
   557 text\<open>The encryption in message YM2 tells us it cannot be faked.\<close>
   558 lemma B_Said_YM2 [rule_format]:
   559      "[|Crypt (shrK B) \<lbrace>Agent A, Nonce NA, nb\<rbrace> \<in> parts (knows Spy evs);
   560         evs \<in> yahalom|]
   561       ==> B \<notin> bad -->
   562           Says B Server \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, nb\<rbrace>\<rbrace>
   563             \<in> set evs"
   564 apply (erule rev_mp, erule yahalom.induct, force,
   565        frule_tac [6] YM4_parts_knows_Spy, simp_all)
   566 txt\<open>Fake\<close>
   567 apply blast
   568 done
   569 
   570 text\<open>If the server sends YM3 then B sent YM2\<close>
   571 lemma YM3_auth_B_to_A_lemma:
   572      "[|Says Server A \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, Nonce NA, nb\<rbrace>, X\<rbrace>
   573        \<in> set evs;  evs \<in> yahalom|]
   574       ==> B \<notin> bad -->
   575           Says B Server \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, nb\<rbrace>\<rbrace>
   576             \<in> set evs"
   577 apply (erule rev_mp, erule yahalom.induct, simp_all)
   578 txt\<open>YM3, YM4\<close>
   579 apply (blast dest!: B_Said_YM2)+
   580 done
   581 
   582 text\<open>If A receives YM3 then B has used nonce NA (and therefore is alive)\<close>
   583 lemma YM3_auth_B_to_A:
   584      "[| Gets A \<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, Nonce NA, nb\<rbrace>, X\<rbrace>
   585            \<in> set evs;
   586          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   587       ==> Says B Server \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, nb\<rbrace>\<rbrace>
   588        \<in> set evs"
   589   by (metis A_trusts_YM3 Gets_imp_analz_Spy YM3_auth_B_to_A_lemma analz.Fst
   590          not_parts_not_analz)
   591 
   592 
   593 subsection\<open>Authenticating A to B using the certificate 
   594   @{term "Crypt K (Nonce NB)"}\<close>
   595 
   596 text\<open>Assuming the session key is secure, if both certificates are present then
   597   A has said NB.  We can't be sure about the rest of A's message, but only
   598   NB matters for freshness.\<close>
   599 lemma A_Said_YM3_lemma [rule_format]:
   600      "evs \<in> yahalom
   601       ==> Key K \<notin> analz (knows Spy evs) -->
   602           Crypt K (Nonce NB) \<in> parts (knows Spy evs) -->
   603           Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace> \<in> parts (knows Spy evs) -->
   604           B \<notin> bad -->
   605           (\<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs)"
   606 apply (erule yahalom.induct, force,
   607        frule_tac [6] YM4_parts_knows_Spy)
   608 apply (analz_mono_contra, simp_all)
   609 txt\<open>Fake\<close>
   610 apply blast
   611 txt\<open>YM3: by \<open>new_keys_not_used\<close>, the message
   612    @{term "Crypt K (Nonce NB)"} could not exist\<close>
   613 apply (force dest!: Crypt_imp_keysFor)
   614 txt\<open>YM4: was @{term "Crypt K (Nonce NB)"} the very last message?
   615     If not, use the induction hypothesis\<close>
   616 apply (simp add: ex_disj_distrib)
   617 txt\<open>yes: apply unicity of session keys\<close>
   618 apply (blast dest!: Gets_imp_Says A_trusts_YM3 B_trusts_YM4_shrK
   619                     Crypt_Spy_analz_bad
   620              dest: Says_imp_knows_Spy [THEN parts.Inj] unique_session_keys)
   621 done
   622 
   623 text\<open>If B receives YM4 then A has used nonce NB (and therefore is alive).
   624   Moreover, A associates K with NB (thus is talking about the same run).
   625   Other premises guarantee secrecy of K.\<close>
   626 lemma YM4_imp_A_Said_YM3 [rule_format]:
   627      "[| Gets B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Key K\<rbrace>,
   628                   Crypt K (Nonce NB)\<rbrace> \<in> set evs;
   629          Says B Server
   630            \<lbrace>Agent B, Crypt (shrK B) \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>\<rbrace>
   631            \<in> set evs;
   632          (\<forall>NA k. Notes Spy \<lbrace>Nonce NA, Nonce NB, k\<rbrace> \<notin> set evs);
   633          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   634       ==> \<exists>X. Says A B \<lbrace>X, Crypt K (Nonce NB)\<rbrace> \<in> set evs"
   635 by (metis A_Said_YM3_lemma B_gets_good_key Gets_imp_analz_Spy YM4_parts_knows_Spy analz.Fst not_parts_not_analz)
   636 end