src/HOL/Auth/Yahalom.thy
author haftmann
Fri Jan 02 08:12:46 2009 +0100 (2009-01-02)
changeset 29332 edc1e2a56398
parent 23746 a455e69c31cc
child 32367 a508148f7c25
permissions -rw-r--r--
named code theorem for Fract_norm
     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 inductive_set yahalom :: "event list set"
    19   where
    20          (*Initial trace is empty*)
    21    Nil:  "[] \<in> yahalom"
    22 
    23          (*The spy MAY say anything he CAN say.  We do not expect him to
    24            invent new nonces here, but he can also use NS1.  Common to
    25            all similar protocols.*)
    26  | Fake: "[| evsf \<in> yahalom;  X \<in> synth (analz (knows Spy evsf)) |]
    27           ==> Says Spy B X  # evsf \<in> yahalom"
    28 
    29          (*A message that has been sent can be received by the
    30            intended recipient.*)
    31  | Reception: "[| evsr \<in> yahalom;  Says A B X \<in> set evsr |]
    32                ==> Gets B X # evsr \<in> yahalom"
    33 
    34          (*Alice initiates a protocol run*)
    35  | YM1:  "[| evs1 \<in> yahalom;  Nonce NA \<notin> used evs1 |]
    36           ==> Says A B {|Agent A, Nonce NA|} # evs1 \<in> yahalom"
    37 
    38          (*Bob's response to Alice's message.*)
    39  | YM2:  "[| evs2 \<in> yahalom;  Nonce NB \<notin> used evs2;
    40              Gets B {|Agent A, Nonce NA|} \<in> set evs2 |]
    41           ==> Says B Server 
    42                   {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
    43                 # evs2 \<in> yahalom"
    44 
    45          (*The Server receives Bob's message.  He responds by sending a
    46             new session key to Alice, with a packet for forwarding to Bob.*)
    47  | YM3:  "[| evs3 \<in> yahalom;  Key KAB \<notin> used evs3;  KAB \<in> symKeys;
    48              Gets Server 
    49                   {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
    50                \<in> set evs3 |]
    51           ==> Says Server A
    52                    {|Crypt (shrK A) {|Agent B, Key KAB, Nonce NA, Nonce NB|},
    53                      Crypt (shrK B) {|Agent A, Key KAB|}|}
    54                 # evs3 \<in> yahalom"
    55 
    56  | YM4:  
    57        --{*Alice receives the Server's (?) message, checks her Nonce, and
    58            uses the new session key to send Bob his Nonce.  The premise
    59            @{term "A \<noteq> Server"} is needed for @{text Says_Server_not_range}.
    60            Alice can check that K is symmetric by its length.*}
    61 	 "[| evs4 \<in> yahalom;  A \<noteq> Server;  K \<in> symKeys;
    62              Gets A {|Crypt(shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|}, X|}
    63                 \<in> set evs4;
    64              Says A B {|Agent A, Nonce NA|} \<in> set evs4 |]
    65           ==> Says A B {|X, Crypt K (Nonce NB)|} # evs4 \<in> yahalom"
    66 
    67          (*This message models possible leaks of session keys.  The Nonces
    68            identify the protocol run.  Quoting Server here ensures they are
    69            correct.*)
    70  | Oops: "[| evso \<in> yahalom;  
    71              Says Server A {|Crypt (shrK A)
    72                                    {|Agent B, Key K, Nonce NA, Nonce NB|},
    73                              X|}  \<in> set evso |]
    74           ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso \<in> yahalom"
    75 
    76 
    77 constdefs 
    78   KeyWithNonce :: "[key, nat, event list] => bool"
    79   "KeyWithNonce K NB evs ==
    80      \<exists>A B na X. 
    81        Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|} 
    82          \<in> set evs"
    83 
    84 
    85 declare Says_imp_analz_Spy [dest]
    86 declare parts.Body  [dest]
    87 declare Fake_parts_insert_in_Un  [dest]
    88 declare analz_into_parts [dest]
    89 
    90 text{*A "possibility property": there are traces that reach the end*}
    91 lemma "[| A \<noteq> Server; K \<in> symKeys; Key K \<notin> used [] |]
    92       ==> \<exists>X NB. \<exists>evs \<in> yahalom.
    93              Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs"
    94 apply (intro exI bexI)
    95 apply (rule_tac [2] yahalom.Nil
    96                     [THEN yahalom.YM1, THEN yahalom.Reception,
    97                      THEN yahalom.YM2, THEN yahalom.Reception,
    98                      THEN yahalom.YM3, THEN yahalom.Reception,
    99                      THEN yahalom.YM4])
   100 apply (possibility, simp add: used_Cons)
   101 done
   102 
   103 
   104 subsection{*Regularity Lemmas for Yahalom*}
   105 
   106 lemma Gets_imp_Says:
   107      "[| Gets B X \<in> set evs; evs \<in> yahalom |] ==> \<exists>A. Says A B X \<in> set evs"
   108 by (erule rev_mp, erule yahalom.induct, auto)
   109 
   110 text{*Must be proved separately for each protocol*}
   111 lemma Gets_imp_knows_Spy:
   112      "[| Gets B X \<in> set evs; evs \<in> yahalom |]  ==> X \<in> knows Spy evs"
   113 by (blast dest!: Gets_imp_Says Says_imp_knows_Spy)
   114 
   115 lemmas Gets_imp_analz_Spy = Gets_imp_knows_Spy [THEN analz.Inj]
   116 declare Gets_imp_analz_Spy [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)
   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
   301   distributed the key quoting nonce NB.  This part says nothing about
   302   agent names.  Secrecy of NB is crucial.  Note that @{term "Nonce NB
   303   \<notin> analz(knows Spy evs)"} must be the FIRST antecedent of the
   304   induction formula.*}
   305 
   306 lemma B_trusts_YM4_newK [rule_format]:
   307      "[|Crypt K (Nonce NB) \<in> parts (knows Spy evs);
   308         Nonce NB \<notin> analz (knows Spy evs);  evs \<in> yahalom|]
   309       ==> \<exists>A B NA. Says Server A
   310                       {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|},
   311                         Crypt (shrK B) {|Agent A, Key K|}|}
   312                      \<in> set evs"
   313 apply (erule rev_mp, erule rev_mp)
   314 apply (erule yahalom.induct, force,
   315        frule_tac [6] YM4_parts_knows_Spy)
   316 apply (analz_mono_contra, simp_all)
   317 txt{*Fake, YM3*}
   318 apply blast
   319 apply blast
   320 txt{*YM4.  A is uncompromised because NB is secure
   321   A's certificate guarantees the existence of the Server message*}
   322 apply (blast dest!: Gets_imp_Says Crypt_Spy_analz_bad
   323              dest: Says_imp_spies
   324                    parts.Inj [THEN parts.Fst, THEN A_trusts_YM3])
   325 done
   326 
   327 
   328 subsubsection{* Towards proving secrecy of Nonce NB *}
   329 
   330 text{*Lemmas about the predicate KeyWithNonce*}
   331 
   332 lemma KeyWithNonceI:
   333  "Says Server A
   334           {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|}
   335         \<in> set evs ==> KeyWithNonce K NB evs"
   336 by (unfold KeyWithNonce_def, blast)
   337 
   338 lemma KeyWithNonce_Says [simp]:
   339    "KeyWithNonce K NB (Says S A X # evs) =
   340       (Server = S &
   341        (\<exists>B n X'. X = {|Crypt (shrK A) {|Agent B, Key K, n, Nonce NB|}, X'|})
   342       | KeyWithNonce K NB evs)"
   343 by (simp add: KeyWithNonce_def, blast)
   344 
   345 
   346 lemma KeyWithNonce_Notes [simp]:
   347    "KeyWithNonce K NB (Notes A X # evs) = KeyWithNonce K NB evs"
   348 by (simp add: KeyWithNonce_def)
   349 
   350 lemma KeyWithNonce_Gets [simp]:
   351    "KeyWithNonce K NB (Gets A X # evs) = KeyWithNonce K NB evs"
   352 by (simp add: KeyWithNonce_def)
   353 
   354 text{*A fresh key cannot be associated with any nonce
   355   (with respect to a given trace). *}
   356 lemma fresh_not_KeyWithNonce:
   357      "Key K \<notin> used evs ==> ~ KeyWithNonce K NB evs"
   358 by (unfold KeyWithNonce_def, blast)
   359 
   360 text{*The Server message associates K with NB' and therefore not with any
   361   other nonce NB.*}
   362 lemma Says_Server_KeyWithNonce:
   363  "[| Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB'|}, X|}
   364        \<in> set evs;
   365      NB \<noteq> NB';  evs \<in> yahalom |]
   366   ==> ~ KeyWithNonce K NB evs"
   367 by (unfold KeyWithNonce_def, blast dest: unique_session_keys)
   368 
   369 
   370 text{*The only nonces that can be found with the help of session keys are
   371   those distributed as nonce NB by the Server.  The form of the theorem
   372   recalls @{text analz_image_freshK}, but it is much more complicated.*}
   373 
   374 
   375 text{*As with @{text analz_image_freshK}, we take some pains to express the 
   376   property as a logical equivalence so that the simplifier can apply it.*}
   377 lemma Nonce_secrecy_lemma:
   378      "P --> (X \<in> analz (G Un H)) --> (X \<in> analz H)  ==>
   379       P --> (X \<in> analz (G Un H)) = (X \<in> analz H)"
   380 by (blast intro: analz_mono [THEN subsetD])
   381 
   382 lemma Nonce_secrecy:
   383      "evs \<in> yahalom ==>
   384       (\<forall>KK. KK <= - (range shrK) -->
   385            (\<forall>K \<in> KK. K \<in> symKeys --> ~ KeyWithNonce K NB evs)   -->
   386            (Nonce NB \<in> analz (Key`KK Un (knows Spy evs))) =
   387            (Nonce NB \<in> analz (knows Spy evs)))"
   388 apply (erule yahalom.induct,
   389        frule_tac [7] YM4_analz_knows_Spy)
   390 apply (safe del: allI impI intro!: Nonce_secrecy_lemma [THEN impI, THEN allI])
   391 apply (simp_all del: image_insert image_Un
   392        add: analz_image_freshK_simps split_ifs
   393             all_conj_distrib ball_conj_distrib
   394             analz_image_freshK fresh_not_KeyWithNonce
   395             imp_disj_not1               (*Moves NBa\<noteq>NB to the front*)
   396             Says_Server_KeyWithNonce)
   397 txt{*For Oops, simplification proves @{prop "NBa\<noteq>NB"}.  By
   398   @{term Says_Server_KeyWithNonce}, we get @{prop "~ KeyWithNonce K NB
   399   evs"}; then simplification can apply the induction hypothesis with
   400   @{term "KK = {K}"}.*}
   401 txt{*Fake*}
   402 apply spy_analz
   403 txt{*YM2*}
   404 apply blast
   405 txt{*YM3*}
   406 apply blast
   407 txt{*YM4*}
   408 apply (erule_tac V = "\<forall>KK. ?P KK" in thin_rl, clarify)
   409 txt{*If @{prop "A \<in> bad"} then @{term NBa} is known, therefore
   410   @{prop "NBa \<noteq> NB"}.  Previous two steps make the next step
   411   faster.*}
   412 apply (blast dest!: Gets_imp_Says Says_imp_spies Crypt_Spy_analz_bad
   413          dest: analz.Inj
   414            parts.Inj [THEN parts.Fst, THEN A_trusts_YM3, THEN KeyWithNonceI])
   415 done
   416 
   417 
   418 text{*Version required below: if NB can be decrypted using a session key then
   419    it was distributed with that key.  The more general form above is required
   420    for the induction to carry through.*}
   421 lemma single_Nonce_secrecy:
   422      "[| Says Server A
   423           {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB'|}, X|}
   424          \<in> set evs;
   425          NB \<noteq> NB';  KAB \<notin> range shrK;  evs \<in> yahalom |]
   426       ==> (Nonce NB \<in> analz (insert (Key KAB) (knows Spy evs))) =
   427           (Nonce NB \<in> analz (knows Spy evs))"
   428 by (simp_all del: image_insert image_Un imp_disjL
   429              add: analz_image_freshK_simps split_ifs
   430                   Nonce_secrecy Says_Server_KeyWithNonce)
   431 
   432 
   433 subsubsection{* The Nonce NB uniquely identifies B's message. *}
   434 
   435 lemma unique_NB:
   436      "[| Crypt (shrK B) {|Agent A, Nonce NA, nb|} \<in> parts (knows Spy evs);
   437          Crypt (shrK B') {|Agent A', Nonce NA', nb|} \<in> parts (knows Spy evs);
   438         evs \<in> yahalom;  B \<notin> bad;  B' \<notin> bad |]
   439       ==> NA' = NA & A' = A & B' = B"
   440 apply (erule rev_mp, erule rev_mp)
   441 apply (erule yahalom.induct, force,
   442        frule_tac [6] YM4_parts_knows_Spy, simp_all)
   443 txt{*Fake, and YM2 by freshness*}
   444 apply blast+
   445 done
   446 
   447 
   448 text{*Variant useful for proving secrecy of NB.  Because nb is assumed to be
   449   secret, we no longer must assume B, B' not bad.*}
   450 lemma Says_unique_NB:
   451      "[| Says C S   {|X,  Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}
   452            \<in> set evs;
   453          Gets S' {|X', Crypt (shrK B') {|Agent A', Nonce NA', nb|}|}
   454            \<in> set evs;
   455          nb \<notin> analz (knows Spy evs);  evs \<in> yahalom |]
   456       ==> NA' = NA & A' = A & B' = B"
   457 by (blast dest!: Gets_imp_Says Crypt_Spy_analz_bad
   458           dest: Says_imp_spies unique_NB parts.Inj analz.Inj)
   459 
   460 
   461 subsubsection{* A nonce value is never used both as NA and as NB *}
   462 
   463 lemma no_nonce_YM1_YM2:
   464      "[|Crypt (shrK B') {|Agent A', Nonce NB, nb'|} \<in> parts(knows Spy evs);
   465         Nonce NB \<notin> analz (knows Spy evs);  evs \<in> yahalom|]
   466   ==> Crypt (shrK B)  {|Agent A, na, Nonce NB|} \<notin> parts(knows Spy evs)"
   467 apply (erule rev_mp, erule rev_mp)
   468 apply (erule yahalom.induct, force,
   469        frule_tac [6] YM4_parts_knows_Spy)
   470 apply (analz_mono_contra, simp_all)
   471 txt{*Fake, YM2*}
   472 apply blast+
   473 done
   474 
   475 text{*The Server sends YM3 only in response to YM2.*}
   476 lemma Says_Server_imp_YM2:
   477      "[| Says Server A {|Crypt (shrK A) {|Agent B, k, na, nb|}, X|} \<in> set evs;
   478          evs \<in> yahalom |]
   479       ==> Gets Server {| Agent B, Crypt (shrK B) {|Agent A, na, nb|} |}
   480              \<in> set evs"
   481 by (erule rev_mp, erule yahalom.induct, auto)
   482 
   483 text{*A vital theorem for B, that nonce NB remains secure from the Spy.*}
   484 lemma Spy_not_see_NB :
   485      "[| Says B Server
   486 	        {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
   487 	   \<in> set evs;
   488 	 (\<forall>k. Notes Spy {|Nonce NA, Nonce NB, k|} \<notin> set evs);
   489          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   490       ==> Nonce NB \<notin> analz (knows Spy evs)"
   491 apply (erule rev_mp, erule rev_mp)
   492 apply (erule yahalom.induct, force,
   493        frule_tac [6] YM4_analz_knows_Spy)
   494 apply (simp_all add: split_ifs pushes new_keys_not_analzd analz_insert_eq
   495                      analz_insert_freshK)
   496 txt{*Fake*}
   497 apply spy_analz
   498 txt{*YM1: NB=NA is impossible anyway, but NA is secret because it is fresh!*}
   499 apply blast
   500 txt{*YM2*}
   501 apply blast
   502 txt{*Prove YM3 by showing that no NB can also be an NA*}
   503 apply (blast dest!: no_nonce_YM1_YM2 dest: Gets_imp_Says Says_unique_NB)
   504 txt{*LEVEL 7: YM4 and Oops remain*}
   505 apply (clarify, simp add: all_conj_distrib)
   506 txt{*YM4: key K is visible to Spy, contradicting session key secrecy theorem*}
   507 txt{*Case analysis on Aa:bad; PROOF FAILED problems
   508   use @{text Says_unique_NB} to identify message components: @{term "Aa=A"}, @{term "Ba=B"}*}
   509 apply (blast dest!: Says_unique_NB analz_shrK_Decrypt
   510                     parts.Inj [THEN parts.Fst, THEN A_trusts_YM3]
   511              dest: Gets_imp_Says Says_imp_spies Says_Server_imp_YM2
   512                    Spy_not_see_encrypted_key)
   513 txt{*Oops case: if the nonce is betrayed now, show that the Oops event is
   514   covered by the quantified Oops assumption.*}
   515 apply (clarify, simp add: all_conj_distrib)
   516 apply (frule Says_Server_imp_YM2, assumption)
   517 apply (case_tac "NB = NBa")
   518 txt{*If NB=NBa then all other components of the Oops message agree*}
   519 apply (blast dest: Says_unique_NB)
   520 txt{*case @{prop "NB \<noteq> NBa"}*}
   521 apply (simp add: single_Nonce_secrecy)
   522 apply (blast dest!: no_nonce_YM1_YM2 (*to prove NB\<noteq>NAa*))
   523 done
   524 
   525 
   526 text{*B's session key guarantee from YM4.  The two certificates contribute to a
   527   single conclusion about the Server's message.  Note that the "Notes Spy"
   528   assumption must quantify over @{text \<forall>} POSSIBLE keys instead of our particular K.
   529   If this run is broken and the spy substitutes a certificate containing an
   530   old key, B has no means of telling.*}
   531 lemma B_trusts_YM4:
   532      "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|},
   533                   Crypt K (Nonce NB)|} \<in> set evs;
   534          Says B Server
   535            {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
   536            \<in> set evs;
   537          \<forall>k. Notes Spy {|Nonce NA, Nonce NB, k|} \<notin> set evs;
   538          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   539        ==> Says Server A
   540                    {|Crypt (shrK A) {|Agent B, Key K,
   541                              Nonce NA, Nonce NB|},
   542                      Crypt (shrK B) {|Agent A, Key K|}|}
   543              \<in> set evs"
   544 by (blast dest: Spy_not_see_NB Says_unique_NB
   545                 Says_Server_imp_YM2 B_trusts_YM4_newK)
   546 
   547 
   548 
   549 text{*The obvious combination of @{text B_trusts_YM4} with 
   550   @{text Spy_not_see_encrypted_key}*}
   551 lemma B_gets_good_key:
   552      "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|},
   553                   Crypt K (Nonce NB)|} \<in> set evs;
   554          Says B Server
   555            {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
   556            \<in> set evs;
   557          \<forall>k. Notes Spy {|Nonce NA, Nonce NB, k|} \<notin> set evs;
   558          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   559       ==> Key K \<notin> analz (knows Spy evs)"
   560 by (blast dest!: B_trusts_YM4 Spy_not_see_encrypted_key)
   561 
   562 
   563 subsection{*Authenticating B to A*}
   564 
   565 text{*The encryption in message YM2 tells us it cannot be faked.*}
   566 lemma B_Said_YM2 [rule_format]:
   567      "[|Crypt (shrK B) {|Agent A, Nonce NA, nb|} \<in> parts (knows Spy evs);
   568         evs \<in> yahalom|]
   569       ==> B \<notin> bad -->
   570           Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}
   571             \<in> set evs"
   572 apply (erule rev_mp, erule yahalom.induct, force,
   573        frule_tac [6] YM4_parts_knows_Spy, simp_all)
   574 txt{*Fake*}
   575 apply blast
   576 done
   577 
   578 text{*If the server sends YM3 then B sent YM2*}
   579 lemma YM3_auth_B_to_A_lemma:
   580      "[|Says Server A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|}
   581        \<in> set evs;  evs \<in> yahalom|]
   582       ==> B \<notin> bad -->
   583           Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}
   584             \<in> set evs"
   585 apply (erule rev_mp, erule yahalom.induct, simp_all)
   586 txt{*YM3, YM4*}
   587 apply (blast dest!: B_Said_YM2)+
   588 done
   589 
   590 text{*If A receives YM3 then B has used nonce NA (and therefore is alive)*}
   591 lemma YM3_auth_B_to_A:
   592      "[| Gets A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|}
   593            \<in> set evs;
   594          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   595       ==> Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}
   596        \<in> set evs"
   597 by (blast dest!: A_trusts_YM3 YM3_auth_B_to_A_lemma elim: knows_Spy_partsEs)
   598 
   599 
   600 subsection{*Authenticating A to B using the certificate 
   601   @{term "Crypt K (Nonce NB)"}*}
   602 
   603 text{*Assuming the session key is secure, if both certificates are present then
   604   A has said NB.  We can't be sure about the rest of A's message, but only
   605   NB matters for freshness.*}
   606 lemma A_Said_YM3_lemma [rule_format]:
   607      "evs \<in> yahalom
   608       ==> Key K \<notin> analz (knows Spy evs) -->
   609           Crypt K (Nonce NB) \<in> parts (knows Spy evs) -->
   610           Crypt (shrK B) {|Agent A, Key K|} \<in> parts (knows Spy evs) -->
   611           B \<notin> bad -->
   612           (\<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs)"
   613 apply (erule yahalom.induct, force,
   614        frule_tac [6] YM4_parts_knows_Spy)
   615 apply (analz_mono_contra, simp_all)
   616 txt{*Fake*}
   617 apply blast
   618 txt{*YM3: by @{text new_keys_not_used}, the message
   619    @{term "Crypt K (Nonce NB)"} could not exist*}
   620 apply (force dest!: Crypt_imp_keysFor)
   621 txt{*YM4: was @{term "Crypt K (Nonce NB)"} the very last message?
   622     If not, use the induction hypothesis*}
   623 apply (simp add: ex_disj_distrib)
   624 txt{*yes: apply unicity of session keys*}
   625 apply (blast dest!: Gets_imp_Says A_trusts_YM3 B_trusts_YM4_shrK
   626                     Crypt_Spy_analz_bad
   627              dest: Says_imp_knows_Spy [THEN parts.Inj] unique_session_keys)
   628 done
   629 
   630 text{*If B receives YM4 then A has used nonce NB (and therefore is alive).
   631   Moreover, A associates K with NB (thus is talking about the same run).
   632   Other premises guarantee secrecy of K.*}
   633 lemma YM4_imp_A_Said_YM3 [rule_format]:
   634      "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|},
   635                   Crypt K (Nonce NB)|} \<in> set evs;
   636          Says B Server
   637            {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
   638            \<in> set evs;
   639          (\<forall>NA k. Notes Spy {|Nonce NA, Nonce NB, k|} \<notin> set evs);
   640          A \<notin> bad;  B \<notin> bad;  evs \<in> yahalom |]
   641       ==> \<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs"
   642 by (blast intro!: A_Said_YM3_lemma
   643           dest: Spy_not_see_encrypted_key B_trusts_YM4 Gets_imp_Says)
   644 
   645 end