src/HOL/Auth/Yahalom.thy
author webertj
Mon Mar 07 19:30:53 2005 +0100 (2005-03-07)
changeset 15584 3478bb4f93ff
parent 14207 f20fbb141673
child 16417 9bc16273c2d4
permissions -rw-r--r--
refute_params: default value itself=1 added (for type classes)
     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 = Public:
    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_knows_Spy [THEN analz.Inj, 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 declare Gets_imp_knows_Spy [THEN analz.Inj, dest]
   117 
   118 
   119 text{*Lets us treat YM4 using a similar argument as for the Fake case.*}
   120 lemma YM4_analz_knows_Spy:
   121      "[| Gets A {|Crypt (shrK A) Y, X|} \<in> set evs;  evs \<in> yahalom |]
   122       ==> X \<in> analz (knows Spy evs)"
   123 by blast
   124 
   125 lemmas YM4_parts_knows_Spy =
   126        YM4_analz_knows_Spy [THEN analz_into_parts, standard]
   127 
   128 text{*For Oops*}
   129 lemma YM4_Key_parts_knows_Spy:
   130      "Says Server A {|Crypt (shrK A) {|B,K,NA,NB|}, X|} \<in> set evs
   131       ==> K \<in> parts (knows Spy evs)"
   132 by (blast dest!: parts.Body Says_imp_knows_Spy [THEN parts.Inj])
   133 
   134 
   135 text{*Theorems of the form @{term "X \<notin> parts (knows Spy evs)"} imply 
   136 that NOBODY sends messages containing X! *}
   137 
   138 text{*Spy never sees a good agent's shared key!*}
   139 lemma Spy_see_shrK [simp]:
   140      "evs \<in> yahalom ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"
   141 by (erule yahalom.induct, force,
   142     drule_tac [6] YM4_parts_knows_Spy, simp_all, blast+)
   143 
   144 lemma Spy_analz_shrK [simp]:
   145      "evs \<in> yahalom ==> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)"
   146 by auto
   147 
   148 lemma Spy_see_shrK_D [dest!]:
   149      "[|Key (shrK A) \<in> parts (knows Spy evs);  evs \<in> yahalom|] ==> A \<in> bad"
   150 by (blast dest: Spy_see_shrK)
   151 
   152 text{*Nobody can have used non-existent keys!
   153     Needed to apply @{text analz_insert_Key}*}
   154 lemma new_keys_not_used [simp]:
   155     "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> yahalom|]
   156      ==> K \<notin> keysFor (parts (spies evs))"
   157 apply (erule rev_mp)
   158 apply (erule yahalom.induct, force,
   159        frule_tac [6] YM4_parts_knows_Spy, simp_all)
   160 txt{*Fake*}
   161 apply (force dest!: keysFor_parts_insert, auto)
   162 done
   163 
   164 
   165 text{*Earlier, all protocol proofs declared this theorem.
   166   But only a few proofs need it, e.g. Yahalom and Kerberos IV.*}
   167 lemma new_keys_not_analzd:
   168  "[|K \<in> symKeys; evs \<in> yahalom; Key K \<notin> used evs|]
   169   ==> K \<notin> keysFor (analz (knows Spy evs))"
   170 by (blast dest: new_keys_not_used intro: keysFor_mono [THEN subsetD])
   171 
   172 
   173 text{*Describes the form of K when the Server sends this message.  Useful for
   174   Oops as well as main secrecy property.*}
   175 lemma Says_Server_not_range [simp]:
   176      "[| Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|}
   177            \<in> set evs;   evs \<in> yahalom |]
   178       ==> K \<notin> range shrK"
   179 by (erule rev_mp, erule yahalom.induct, simp_all, blast)
   180 
   181 
   182 subsection{*Secrecy Theorems*}
   183 
   184 (****
   185  The following is to prove theorems of the form
   186 
   187   Key K \<in> analz (insert (Key KAB) (knows Spy evs)) ==>
   188   Key K \<in> analz (knows Spy evs)
   189 
   190  A more general formula must be proved inductively.
   191 ****)
   192 
   193 text{* Session keys are not used to encrypt other session keys *}
   194 
   195 lemma analz_image_freshK [rule_format]:
   196  "evs \<in> yahalom ==>
   197    \<forall>K KK. KK <= - (range shrK) -->
   198           (Key K \<in> analz (Key`KK Un (knows Spy evs))) =
   199           (K \<in> KK | Key K \<in> analz (knows Spy evs))"
   200 apply (erule yahalom.induct,
   201        drule_tac [7] YM4_analz_knows_Spy, analz_freshK, spy_analz, blast)
   202 apply (simp only: Says_Server_not_range analz_image_freshK_simps)
   203 done
   204 
   205 lemma analz_insert_freshK:
   206      "[| evs \<in> yahalom;  KAB \<notin> range shrK |] ==>
   207       (Key K \<in> analz (insert (Key KAB) (knows Spy evs))) =
   208       (K = KAB | Key K \<in> analz (knows Spy evs))"
   209 by (simp only: analz_image_freshK analz_image_freshK_simps)
   210 
   211 
   212 text{*The Key K uniquely identifies the Server's  message.*}
   213 lemma unique_session_keys:
   214      "[| Says Server A
   215           {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} \<in> set evs;
   216         Says Server A'
   217           {|Crypt (shrK A') {|Agent B', Key K, na', nb'|}, X'|} \<in> set evs;
   218         evs \<in> yahalom |]
   219      ==> A=A' & B=B' & na=na' & nb=nb'"
   220 apply (erule rev_mp, erule rev_mp)
   221 apply (erule yahalom.induct, simp_all)
   222 txt{*YM3, by freshness, and YM4*}
   223 apply blast+
   224 done
   225 
   226 
   227 text{*Crucial secrecy property: Spy does not see the keys sent in msg YM3*}
   228 lemma secrecy_lemma:
   229      "[| A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   230       ==> Says Server A
   231             {|Crypt (shrK A) {|Agent B, Key K, na, nb|},
   232               Crypt (shrK B) {|Agent A, Key K|}|}
   233            \<in> set evs -->
   234           Notes Spy {|na, nb, Key K|} \<notin> set evs -->
   235           Key K \<notin> analz (knows Spy evs)"
   236 apply (erule yahalom.induct, force,
   237        drule_tac [6] YM4_analz_knows_Spy)
   238 apply (simp_all add: pushes analz_insert_eq analz_insert_freshK, spy_analz)   --{*Fake*}
   239 apply (blast dest: unique_session_keys)+  --{*YM3, Oops*}
   240 done
   241 
   242 text{*Final version*}
   243 lemma Spy_not_see_encrypted_key:
   244      "[| Says Server A
   245             {|Crypt (shrK A) {|Agent B, Key K, na, nb|},
   246               Crypt (shrK B) {|Agent A, Key K|}|}
   247            \<in> set evs;
   248          Notes Spy {|na, nb, Key K|} \<notin> set evs;
   249          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   250       ==> Key K \<notin> analz (knows Spy evs)"
   251 by (blast dest: secrecy_lemma)
   252 
   253 
   254 subsubsection{* Security Guarantee for A upon receiving YM3 *}
   255 
   256 text{*If the encrypted message appears then it originated with the Server*}
   257 lemma A_trusts_YM3:
   258      "[| Crypt (shrK A) {|Agent B, Key K, na, nb|} \<in> parts (knows Spy evs);
   259          A \<notin> bad;  evs \<in> yahalom |]
   260        ==> Says Server A
   261             {|Crypt (shrK A) {|Agent B, Key K, na, nb|},
   262               Crypt (shrK B) {|Agent A, Key K|}|}
   263            \<in> set evs"
   264 apply (erule rev_mp)
   265 apply (erule yahalom.induct, force,
   266        frule_tac [6] YM4_parts_knows_Spy, simp_all)
   267 txt{*Fake, YM3*}
   268 apply blast+
   269 done
   270 
   271 text{*The obvious combination of @{text A_trusts_YM3} with
   272   @{text Spy_not_see_encrypted_key}*}
   273 lemma A_gets_good_key:
   274      "[| Crypt (shrK A) {|Agent B, Key K, na, nb|} \<in> parts (knows Spy evs);
   275          Notes Spy {|na, nb, Key K|} \<notin> set evs;
   276          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   277       ==> Key K \<notin> analz (knows Spy evs)"
   278 by (blast dest!: A_trusts_YM3 Spy_not_see_encrypted_key)
   279 
   280 
   281 subsubsection{* Security Guarantees for B upon receiving YM4 *}
   282 
   283 text{*B knows, by the first part of A's message, that the Server distributed
   284   the key for A and B.  But this part says nothing about nonces.*}
   285 lemma B_trusts_YM4_shrK:
   286      "[| Crypt (shrK B) {|Agent A, Key K|} \<in> parts (knows Spy evs);
   287          B \<notin> bad;  evs \<in> yahalom |]
   288       ==> \<exists>NA NB. Says Server A
   289                       {|Crypt (shrK A) {|Agent B, Key K,
   290                                          Nonce NA, Nonce NB|},
   291                         Crypt (shrK B) {|Agent A, Key K|}|}
   292                      \<in> set evs"
   293 apply (erule rev_mp)
   294 apply (erule yahalom.induct, force,
   295        frule_tac [6] YM4_parts_knows_Spy, simp_all)
   296 txt{*Fake, YM3*}
   297 apply blast+
   298 done
   299 
   300 text{*B knows, by the second part of A's message, that the Server distributed
   301   the key quoting nonce NB.  This part says nothing about agent names.
   302   Secrecy of NB is crucial.  Note that  Nonce NB \<notin> analz(knows Spy evs)  must
   303   be the FIRST antecedent of the induction formula.*}
   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                       {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|},
   309                         Crypt (shrK B) {|Agent A, Key K|}|}
   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{*Fake, YM3*}
   316 apply blast
   317 apply blast
   318 txt{*YM4.  A is uncompromised because NB is secure
   319   A's certificate guarantees the existence of the Server message*}
   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{* Towards proving secrecy of Nonce NB *}
   327 
   328 text{*Lemmas about the predicate KeyWithNonce*}
   329 
   330 lemma KeyWithNonceI:
   331  "Says Server A
   332           {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|}
   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 = {|Crypt (shrK A) {|Agent B, Key K, n, Nonce NB|}, X'|})
   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{*A fresh key cannot be associated with any nonce
   353   (with respect to a given trace). *}
   354 lemma fresh_not_KeyWithNonce:
   355      "Key K \<notin> used evs ==> ~ KeyWithNonce K NB evs"
   356 by (unfold KeyWithNonce_def, blast)
   357 
   358 text{*The Server message associates K with NB' and therefore not with any
   359   other nonce NB.*}
   360 lemma Says_Server_KeyWithNonce:
   361  "[| Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB'|}, X|}
   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{*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 @{text analz_image_freshK}, but it is much more complicated.*}
   371 
   372 
   373 text{*As with @{text analz_image_freshK}, we take some pains to express the 
   374   property as a logical equivalence so that the simplifier can apply it.*}
   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{*For Oops, simplification proves NBa\<noteq>NB.  By Says_Server_KeyWithNonce,
   396   we get (~ KeyWithNonce K NB evs); then simplification can apply the
   397   induction hypothesis with KK = {K}.*}
   398 txt{*Fake*}
   399 apply spy_analz
   400 txt{*YM2*}
   401 apply blast
   402 txt{*YM3*}
   403 apply blast
   404 txt{*YM4*}
   405 apply (erule_tac V = "\<forall>KK. ?P KK" in thin_rl, clarify)
   406 txt{*If A \<in> bad then NBa is known, therefore NBa \<noteq> NB.  Previous two steps 
   407    make the next step faster.*}
   408 apply (blast dest!: Gets_imp_Says Says_imp_spies Crypt_Spy_analz_bad
   409          dest: analz.Inj
   410            parts.Inj [THEN parts.Fst, THEN A_trusts_YM3, THEN KeyWithNonceI])
   411 done
   412 
   413 
   414 text{*Version required below: if NB can be decrypted using a session key then
   415    it was distributed with that key.  The more general form above is required
   416    for the induction to carry through.*}
   417 lemma single_Nonce_secrecy:
   418      "[| Says Server A
   419           {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB'|}, X|}
   420          \<in> set evs;
   421          NB \<noteq> NB';  KAB \<notin> range shrK;  evs \<in> yahalom |]
   422       ==> (Nonce NB \<in> analz (insert (Key KAB) (knows Spy evs))) =
   423           (Nonce NB \<in> analz (knows Spy evs))"
   424 by (simp_all del: image_insert image_Un imp_disjL
   425              add: analz_image_freshK_simps split_ifs
   426                   Nonce_secrecy Says_Server_KeyWithNonce)
   427 
   428 
   429 subsubsection{* The Nonce NB uniquely identifies B's message. *}
   430 
   431 lemma unique_NB:
   432      "[| Crypt (shrK B) {|Agent A, Nonce NA, nb|} \<in> parts (knows Spy evs);
   433          Crypt (shrK B') {|Agent A', Nonce NA', nb|} \<in> parts (knows Spy evs);
   434         evs \<in> yahalom;  B \<notin> bad;  B' \<notin> bad |]
   435       ==> NA' = NA & A' = A & B' = B"
   436 apply (erule rev_mp, erule rev_mp)
   437 apply (erule yahalom.induct, force,
   438        frule_tac [6] YM4_parts_knows_Spy, simp_all)
   439 txt{*Fake, and YM2 by freshness*}
   440 apply blast+
   441 done
   442 
   443 
   444 text{*Variant useful for proving secrecy of NB.  Because nb is assumed to be
   445   secret, we no longer must assume B, B' not bad.*}
   446 lemma Says_unique_NB:
   447      "[| Says C S   {|X,  Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}
   448            \<in> set evs;
   449          Gets S' {|X', Crypt (shrK B') {|Agent A', Nonce NA', nb|}|}
   450            \<in> set evs;
   451          nb \<notin> analz (knows Spy evs);  evs \<in> yahalom |]
   452       ==> NA' = NA & A' = A & B' = B"
   453 by (blast dest!: Gets_imp_Says Crypt_Spy_analz_bad
   454           dest: Says_imp_spies unique_NB parts.Inj analz.Inj)
   455 
   456 
   457 subsubsection{* A nonce value is never used both as NA and as NB *}
   458 
   459 lemma no_nonce_YM1_YM2:
   460      "[|Crypt (shrK B') {|Agent A', Nonce NB, nb'|} \<in> parts(knows Spy evs);
   461         Nonce NB \<notin> analz (knows Spy evs);  evs \<in> yahalom|]
   462   ==> Crypt (shrK B)  {|Agent A, na, Nonce NB|} \<notin> parts(knows Spy evs)"
   463 apply (erule rev_mp, erule rev_mp)
   464 apply (erule yahalom.induct, force,
   465        frule_tac [6] YM4_parts_knows_Spy)
   466 apply (analz_mono_contra, simp_all)
   467 txt{*Fake, YM2*}
   468 apply blast+
   469 done
   470 
   471 text{*The Server sends YM3 only in response to YM2.*}
   472 lemma Says_Server_imp_YM2:
   473      "[| Says Server A {|Crypt (shrK A) {|Agent B, k, na, nb|}, X|} \<in> set evs;
   474          evs \<in> yahalom |]
   475       ==> Gets Server {| Agent B, Crypt (shrK B) {|Agent A, na, nb|} |}
   476              \<in> set evs"
   477 by (erule rev_mp, erule yahalom.induct, auto)
   478 
   479 text{*A vital theorem for B, that nonce NB remains secure from the Spy.*}
   480 lemma Spy_not_see_NB :
   481      "[| Says B Server
   482 	        {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
   483 	   \<in> set evs;
   484 	 (\<forall>k. Notes Spy {|Nonce NA, Nonce NB, k|} \<notin> set evs);
   485          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   486       ==> Nonce NB \<notin> analz (knows Spy evs)"
   487 apply (erule rev_mp, erule rev_mp)
   488 apply (erule yahalom.induct, force,
   489        frule_tac [6] YM4_analz_knows_Spy)
   490 apply (simp_all add: split_ifs pushes new_keys_not_analzd analz_insert_eq
   491                      analz_insert_freshK)
   492 txt{*Fake*}
   493 apply spy_analz
   494 txt{*YM1: NB=NA is impossible anyway, but NA is secret because it is fresh!*}
   495 apply blast
   496 txt{*YM2*}
   497 apply blast
   498 txt{*Prove YM3 by showing that no NB can also be an NA*}
   499 apply (blast dest!: no_nonce_YM1_YM2 dest: Gets_imp_Says Says_unique_NB)
   500 txt{*LEVEL 7: YM4 and Oops remain*}
   501 apply (clarify, simp add: all_conj_distrib)
   502 txt{*YM4: key K is visible to Spy, contradicting session key secrecy theorem*}
   503 txt{*Case analysis on Aa:bad; PROOF FAILED problems
   504   use Says_unique_NB to identify message components: Aa=A, Ba=B*}
   505 apply (blast dest!: Says_unique_NB analz_shrK_Decrypt
   506                     parts.Inj [THEN parts.Fst, THEN A_trusts_YM3]
   507              dest: Gets_imp_Says Says_imp_spies Says_Server_imp_YM2
   508                    Spy_not_see_encrypted_key)
   509 txt{*Oops case: if the nonce is betrayed now, show that the Oops event is
   510   covered by the quantified Oops assumption.*}
   511 apply (clarify, simp add: all_conj_distrib)
   512 apply (frule Says_Server_imp_YM2, assumption)
   513 apply (case_tac "NB = NBa")
   514 txt{*If NB=NBa then all other components of the Oops message agree*}
   515 apply (blast dest: Says_unique_NB)
   516 txt{*case NB \<noteq> NBa*}
   517 apply (simp add: single_Nonce_secrecy)
   518 apply (blast dest!: no_nonce_YM1_YM2 (*to prove NB\<noteq>NAa*))
   519 done
   520 
   521 
   522 text{*B's session key guarantee from YM4.  The two certificates contribute to a
   523   single conclusion about the Server's message.  Note that the "Notes Spy"
   524   assumption must quantify over \<forall>POSSIBLE keys instead of our particular K.
   525   If this run is broken and the spy substitutes a certificate containing an
   526   old key, B has no means of telling.*}
   527 lemma B_trusts_YM4:
   528      "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|},
   529                   Crypt K (Nonce NB)|} \<in> set evs;
   530          Says B Server
   531            {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
   532            \<in> set evs;
   533          \<forall>k. Notes Spy {|Nonce NA, Nonce NB, k|} \<notin> set evs;
   534          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   535        ==> Says Server A
   536                    {|Crypt (shrK A) {|Agent B, Key K,
   537                              Nonce NA, Nonce NB|},
   538                      Crypt (shrK B) {|Agent A, Key K|}|}
   539              \<in> set evs"
   540 by (blast dest: Spy_not_see_NB Says_unique_NB
   541                 Says_Server_imp_YM2 B_trusts_YM4_newK)
   542 
   543 
   544 
   545 text{*The obvious combination of @{text B_trusts_YM4} with 
   546   @{text Spy_not_see_encrypted_key}*}
   547 lemma B_gets_good_key:
   548      "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|},
   549                   Crypt K (Nonce NB)|} \<in> set evs;
   550          Says B Server
   551            {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
   552            \<in> set evs;
   553          \<forall>k. Notes Spy {|Nonce NA, Nonce NB, k|} \<notin> set evs;
   554          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   555       ==> Key K \<notin> analz (knows Spy evs)"
   556 by (blast dest!: B_trusts_YM4 Spy_not_see_encrypted_key)
   557 
   558 
   559 subsection{*Authenticating B to A*}
   560 
   561 text{*The encryption in message YM2 tells us it cannot be faked.*}
   562 lemma B_Said_YM2 [rule_format]:
   563      "[|Crypt (shrK B) {|Agent A, Nonce NA, nb|} \<in> parts (knows Spy evs);
   564         evs \<in> yahalom|]
   565       ==> B \<notin> bad -->
   566           Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}
   567             \<in> set evs"
   568 apply (erule rev_mp, erule yahalom.induct, force,
   569        frule_tac [6] YM4_parts_knows_Spy, simp_all)
   570 txt{*Fake*}
   571 apply blast
   572 done
   573 
   574 text{*If the server sends YM3 then B sent YM2*}
   575 lemma YM3_auth_B_to_A_lemma:
   576      "[|Says Server A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|}
   577        \<in> set evs;  evs \<in> yahalom|]
   578       ==> B \<notin> bad -->
   579           Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}
   580             \<in> set evs"
   581 apply (erule rev_mp, erule yahalom.induct, simp_all)
   582 txt{*YM3, YM4*}
   583 apply (blast dest!: B_Said_YM2)+
   584 done
   585 
   586 text{*If A receives YM3 then B has used nonce NA (and therefore is alive)*}
   587 lemma YM3_auth_B_to_A:
   588      "[| Gets A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|}
   589            \<in> set evs;
   590          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   591       ==> Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}
   592        \<in> set evs"
   593 by (blast dest!: A_trusts_YM3 YM3_auth_B_to_A_lemma elim: knows_Spy_partsEs)
   594 
   595 
   596 subsection{*Authenticating A to B using the certificate 
   597   @{term "Crypt K (Nonce NB)"}*}
   598 
   599 text{*Assuming the session key is secure, if both certificates are present then
   600   A has said NB.  We can't be sure about the rest of A's message, but only
   601   NB matters for freshness.*}
   602 lemma A_Said_YM3_lemma [rule_format]:
   603      "evs \<in> yahalom
   604       ==> Key K \<notin> analz (knows Spy evs) -->
   605           Crypt K (Nonce NB) \<in> parts (knows Spy evs) -->
   606           Crypt (shrK B) {|Agent A, Key K|} \<in> parts (knows Spy evs) -->
   607           B \<notin> bad -->
   608           (\<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs)"
   609 apply (erule yahalom.induct, force,
   610        frule_tac [6] YM4_parts_knows_Spy)
   611 apply (analz_mono_contra, simp_all)
   612 txt{*Fake*}
   613 apply blast
   614 txt{*YM3: by @{text new_keys_not_used}, the message
   615    @{term "Crypt K (Nonce NB)"} could not exist*}
   616 apply (force dest!: Crypt_imp_keysFor)
   617 txt{*YM4: was @{term "Crypt K (Nonce NB)"} the very last message?
   618     If not, use the induction hypothesis*}
   619 apply (simp add: ex_disj_distrib)
   620 txt{*yes: apply unicity of session keys*}
   621 apply (blast dest!: Gets_imp_Says A_trusts_YM3 B_trusts_YM4_shrK
   622                     Crypt_Spy_analz_bad
   623              dest: Says_imp_knows_Spy [THEN parts.Inj] unique_session_keys)
   624 done
   625 
   626 text{*If B receives YM4 then A has used nonce NB (and therefore is alive).
   627   Moreover, A associates K with NB (thus is talking about the same run).
   628   Other premises guarantee secrecy of K.*}
   629 lemma YM4_imp_A_Said_YM3 [rule_format]:
   630      "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|},
   631                   Crypt K (Nonce NB)|} \<in> set evs;
   632          Says B Server
   633            {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
   634            \<in> set evs;
   635          (\<forall>NA k. Notes Spy {|Nonce NA, Nonce NB, k|} \<notin> set evs);
   636          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   637       ==> \<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs"
   638 by (blast intro!: A_Said_YM3_lemma
   639           dest: Spy_not_see_encrypted_key B_trusts_YM4 Gets_imp_Says)
   640 
   641 end