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