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