Theory Yahalom

(*  Title:      HOL/Auth/Yahalom.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1996  University of Cambridge
*)

sectionThe Yahalom Protocol

theory Yahalom imports Public begin

textFrom page 257 of
  Burrows, Abadi and Needham (1989).  A Logic of Authentication.
  Proc. Royal Soc. 426

This theory has the prototypical example of a secrecy relation, KeyCryptNonce.


inductive_set yahalom :: "event list set"
  where
         (*Initial trace is empty*)
   Nil:  "[]  yahalom"

         (*The spy MAY say anything he CAN say.  We do not expect him to
           invent new nonces here, but he can also use NS1.  Common to
           all similar protocols.*)
 | Fake: "evsf  yahalom;  X  synth (analz (knows Spy evsf))
           Says Spy B X  # evsf  yahalom"

         (*A message that has been sent can be received by the
           intended recipient.*)
 | Reception: "evsr  yahalom;  Says A B X  set evsr
                Gets B X # evsr  yahalom"

         (*Alice initiates a protocol run*)
 | YM1:  "evs1  yahalom;  Nonce NA  used evs1
           Says A B Agent A, Nonce NA # evs1  yahalom"

         (*Bob's response to Alice's message.*)
 | YM2:  "evs2  yahalom;  Nonce NB  used evs2;
             Gets B Agent A, Nonce NA  set evs2
           Says B Server 
                  Agent B, Crypt (shrK B) Agent A, Nonce NA, Nonce NB
                # evs2  yahalom"

         (*The Server receives Bob's message.  He responds by sending a
            new session key to Alice, with a packet for forwarding to Bob.*)
 | YM3:  "evs3  yahalom;  Key KAB  used evs3;  KAB  symKeys;
             Gets Server 
                  Agent B, Crypt (shrK B) Agent A, Nonce NA, Nonce NB
                set evs3
           Says Server A
                   Crypt (shrK A) Agent B, Key KAB, Nonce NA, Nonce NB,
                     Crypt (shrK B) Agent A, Key KAB
                # evs3  yahalom"

 | YM4:  
       ― ‹Alice receives the Server's (?) message, checks her Nonce, and
           uses the new session key to send Bob his Nonce.  The premise
           termA  Server is needed for Says_Server_not_range›.
           Alice can check that K is symmetric by its length.
         "evs4  yahalom;  A  Server;  K  symKeys;
             Gets A Crypt(shrK A) Agent B, Key K, Nonce NA, Nonce NB, X
                 set evs4;
             Says A B Agent A, Nonce NA  set evs4
           Says A B X, Crypt K (Nonce NB) # evs4  yahalom"

         (*This message models possible leaks of session keys.  The Nonces
           identify the protocol run.  Quoting Server here ensures they are
           correct.*)
 | Oops: "evso  yahalom;  
             Says Server A Crypt (shrK A)
                                   Agent B, Key K, Nonce NA, Nonce NB,
                             X   set evso
           Notes Spy Nonce NA, Nonce NB, Key K # evso  yahalom"


definition KeyWithNonce :: "[key, nat, event list]  bool" where
  "KeyWithNonce K NB evs ==
     A B na X. 
       Says Server A Crypt (shrK A) Agent B, Key K, na, Nonce NB, X
          set evs"


declare Says_imp_analz_Spy [dest]
declare parts.Body  [dest]
declare Fake_parts_insert_in_Un  [dest]
declare analz_into_parts [dest]

textA "possibility property": there are traces that reach the end
lemma "A  Server; K  symKeys; Key K  used []
       X NB. evs  yahalom.
             Says A B X, Crypt K (Nonce NB)  set evs"
apply (intro exI bexI)
apply (rule_tac [2] yahalom.Nil
                    [THEN yahalom.YM1, THEN yahalom.Reception,
                     THEN yahalom.YM2, THEN yahalom.Reception,
                     THEN yahalom.YM3, THEN yahalom.Reception,
                     THEN yahalom.YM4])
apply (possibility, simp add: used_Cons)
done


subsectionRegularity Lemmas for Yahalom

lemma Gets_imp_Says:
     "Gets B X  set evs; evs  yahalom  A. Says A B X  set evs"
by (erule rev_mp, erule yahalom.induct, auto)

textMust be proved separately for each protocol
lemma Gets_imp_knows_Spy:
     "Gets B X  set evs; evs  yahalom   X  knows Spy evs"
by (blast dest!: Gets_imp_Says Says_imp_knows_Spy)

lemmas Gets_imp_analz_Spy = Gets_imp_knows_Spy [THEN analz.Inj]
declare Gets_imp_analz_Spy [dest]


textLets us treat YM4 using a similar argument as for the Fake case.
lemma YM4_analz_knows_Spy:
     "Gets A Crypt (shrK A) Y, X  set evs;  evs  yahalom
       X  analz (knows Spy evs)"
by blast

lemmas YM4_parts_knows_Spy =
       YM4_analz_knows_Spy [THEN analz_into_parts]

textFor Oops
lemma YM4_Key_parts_knows_Spy:
     "Says Server A Crypt (shrK A) B,K,NA,NB, X  set evs
       K  parts (knows Spy evs)"
  by (metis parts.Body parts.Fst parts.Snd  Says_imp_knows_Spy parts.Inj)

textTheorems of the form termX  parts (knows Spy evs) imply 
that NOBODY sends messages containing X!

textSpy never sees a good agent's shared key!
lemma Spy_see_shrK [simp]:
     "evs  yahalom  (Key (shrK A)  parts (knows Spy evs)) = (A  bad)"
by (erule yahalom.induct, force,
    drule_tac [6] YM4_parts_knows_Spy, simp_all, blast+)

lemma Spy_analz_shrK [simp]:
     "evs  yahalom  (Key (shrK A)  analz (knows Spy evs)) = (A  bad)"
by auto

lemma Spy_see_shrK_D [dest!]:
     "Key (shrK A)  parts (knows Spy evs);  evs  yahalom  A  bad"
by (blast dest: Spy_see_shrK)

textNobody can have used non-existent keys!
    Needed to apply analz_insert_Key›
lemma new_keys_not_used [simp]:
    "Key K  used evs; K  symKeys; evs  yahalom
      K  keysFor (parts (spies evs))"
apply (erule rev_mp)
apply (erule yahalom.induct, force,
       frule_tac [6] YM4_parts_knows_Spy, simp_all)
txtFake
apply (force dest!: keysFor_parts_insert, auto)
done


textEarlier, all protocol proofs declared this theorem.
  But only a few proofs need it, e.g. Yahalom and Kerberos IV.
lemma new_keys_not_analzd:
 "K  symKeys; evs  yahalom; Key K  used evs
   K  keysFor (analz (knows Spy evs))"
by (blast dest: new_keys_not_used intro: keysFor_mono [THEN subsetD])


textDescribes the form of K when the Server sends this message.  Useful for
  Oops as well as main secrecy property.
lemma Says_Server_not_range [simp]:
     "Says Server A Crypt (shrK A) Agent B, Key K, na, nb, X
            set evs;   evs  yahalom
       K  range shrK"
by (erule rev_mp, erule yahalom.induct, simp_all)


subsectionSecrecy Theorems

(****
 The following is to prove theorems of the form

  Key K ∈ analz (insert (Key KAB) (knows Spy evs)) ⟹
  Key K ∈ analz (knows Spy evs)

 A more general formula must be proved inductively.
****)

textSession keys are not used to encrypt other session keys

lemma analz_image_freshK [rule_format]:
 "evs  yahalom 
   K KK. KK  - (range shrK) 
          (Key K  analz (Key`KK  (knows Spy evs))) =
          (K  KK | Key K  analz (knows Spy evs))"
apply (erule yahalom.induct,
       drule_tac [7] YM4_analz_knows_Spy, analz_freshK, spy_analz, blast)
apply (simp only: Says_Server_not_range analz_image_freshK_simps)
apply safe
done

lemma analz_insert_freshK:
     "evs  yahalom;  KAB  range shrK 
      (Key K  analz (insert (Key KAB) (knows Spy evs))) =
      (K = KAB | Key K  analz (knows Spy evs))"
by (simp only: analz_image_freshK analz_image_freshK_simps)


textThe Key K uniquely identifies the Server's  message.
lemma unique_session_keys:
     "Says Server A
          Crypt (shrK A) Agent B, Key K, na, nb, X  set evs;
        Says Server A'
          Crypt (shrK A') Agent B', Key K, na', nb', X'  set evs;
        evs  yahalom
      A=A'  B=B'  na=na'  nb=nb'"
apply (erule rev_mp, erule rev_mp)
apply (erule yahalom.induct, simp_all)
txtYM3, by freshness, and YM4
apply blast+
done


textCrucial secrecy property: Spy does not see the keys sent in msg YM3
lemma secrecy_lemma:
     "A  bad;  B  bad;  evs  yahalom
       Says Server A
            Crypt (shrK A) Agent B, Key K, na, nb,
              Crypt (shrK B) Agent A, Key K
            set evs 
          Notes Spy na, nb, Key K  set evs 
          Key K  analz (knows Spy evs)"
apply (erule yahalom.induct, force,
       drule_tac [6] YM4_analz_knows_Spy)
apply (simp_all add: pushes analz_insert_eq analz_insert_freshK) 
  subgoal ― ‹Fake by spy_analz
  subgoal ― ‹YM3 by blast   
  subgoal ― ‹Oops by  (blast dest: unique_session_keys)   
done

textFinal version
lemma Spy_not_see_encrypted_key:
     "Says Server A
            Crypt (shrK A) Agent B, Key K, na, nb,
              Crypt (shrK B) Agent A, Key K
            set evs;
         Notes Spy na, nb, Key K  set evs;
         A  bad;  B  bad;  evs  yahalom
       Key K  analz (knows Spy evs)"
by (blast dest: secrecy_lemma)


subsubsectionSecurity Guarantee for A upon receiving YM3

textIf the encrypted message appears then it originated with the Server
lemma A_trusts_YM3:
     "Crypt (shrK A) Agent B, Key K, na, nb  parts (knows Spy evs);
         A  bad;  evs  yahalom
        Says Server A
            Crypt (shrK A) Agent B, Key K, na, nb,
              Crypt (shrK B) Agent A, Key K
            set evs"
apply (erule rev_mp)
apply (erule yahalom.induct, force,
       frule_tac [6] YM4_parts_knows_Spy, simp_all)
txtFake, YM3
apply blast+
done

textThe obvious combination of A_trusts_YM3› with
  Spy_not_see_encrypted_key›
lemma A_gets_good_key:
     "Crypt (shrK A) Agent B, Key K, na, nb  parts (knows Spy evs);
         Notes Spy na, nb, Key K  set evs;
         A  bad;  B  bad;  evs  yahalom
       Key K  analz (knows Spy evs)"
  by (metis A_trusts_YM3 secrecy_lemma)


subsubsectionSecurity Guarantees for B upon receiving YM4

textB knows, by the first part of A's message, that the Server distributed
  the key for A and B.  But this part says nothing about nonces.
lemma B_trusts_YM4_shrK:
     "Crypt (shrK B) Agent A, Key K  parts (knows Spy evs);
         B  bad;  evs  yahalom
       NA NB. Says Server A
                      Crypt (shrK A) Agent B, Key K,
                                         Nonce NA, Nonce NB,
                        Crypt (shrK B) Agent A, Key K
                      set evs"
apply (erule rev_mp)
apply (erule yahalom.induct, force,
       frule_tac [6] YM4_parts_knows_Spy, simp_all)
txtFake, YM3
apply blast+
done

textB knows, by the second part of A's message, that the Server
  distributed the key quoting nonce NB.  This part says nothing about
  agent names.  Secrecy of NB is crucial.  Note that termNonce NB
   analz(knows Spy evs) must be the FIRST antecedent of the
  induction formula.

lemma B_trusts_YM4_newK [rule_format]:
     "Crypt K (Nonce NB)  parts (knows Spy evs);
        Nonce NB  analz (knows Spy evs);  evs  yahalom
       A B NA. Says Server A
                      Crypt (shrK A) Agent B, Key K, Nonce NA, Nonce NB,
                        Crypt (shrK B) Agent A, Key K
                      set evs"
apply (erule rev_mp, erule rev_mp)
apply (erule yahalom.induct, force,
       frule_tac [6] YM4_parts_knows_Spy)
         apply (analz_mono_contra, simp_all)
  subgoal ― ‹Fake by blast
  subgoal ― ‹YM3 by blast   
txtYM4.  A is uncompromised because NB is secure
  A's certificate guarantees the existence of the Server message
apply (blast dest!: Gets_imp_Says Crypt_Spy_analz_bad
             dest: Says_imp_spies
                   parts.Inj [THEN parts.Fst, THEN A_trusts_YM3])
done


subsubsectionTowards proving secrecy of Nonce NB

textLemmas about the predicate KeyWithNonce

lemma KeyWithNonceI:
 "Says Server A
          Crypt (shrK A) Agent B, Key K, na, Nonce NB, X
         set evs  KeyWithNonce K NB evs"
by (unfold KeyWithNonce_def, blast)

lemma KeyWithNonce_Says [simp]:
   "KeyWithNonce K NB (Says S A X # evs) =
      (Server = S 
       (B n X'. X = Crypt (shrK A) Agent B, Key K, n, Nonce NB, X')
      | KeyWithNonce K NB evs)"
by (simp add: KeyWithNonce_def, blast)


lemma KeyWithNonce_Notes [simp]:
   "KeyWithNonce K NB (Notes A X # evs) = KeyWithNonce K NB evs"
by (simp add: KeyWithNonce_def)

lemma KeyWithNonce_Gets [simp]:
   "KeyWithNonce K NB (Gets A X # evs) = KeyWithNonce K NB evs"
by (simp add: KeyWithNonce_def)

textA fresh key cannot be associated with any nonce
  (with respect to a given trace).
lemma fresh_not_KeyWithNonce:
     "Key K  used evs  ¬ KeyWithNonce K NB evs"
by (unfold KeyWithNonce_def, blast)

textThe Server message associates K with NB' and therefore not with any
  other nonce NB.
lemma Says_Server_KeyWithNonce:
 "Says Server A Crypt (shrK A) Agent B, Key K, na, Nonce NB', X
        set evs;
     NB  NB';  evs  yahalom
   ¬ KeyWithNonce K NB evs"
by (unfold KeyWithNonce_def, blast dest: unique_session_keys)


textThe only nonces that can be found with the help of session keys are
  those distributed as nonce NB by the Server.  The form of the theorem
  recalls analz_image_freshK›, but it is much more complicated.


textAs with analz_image_freshK›, we take some pains to express the 
  property as a logical equivalence so that the simplifier can apply it.
lemma Nonce_secrecy_lemma:
     "P  (X  analz (G  H))  (X  analz H)  
      P  (X  analz (G  H)) = (X  analz H)"
by (blast intro: analz_mono [THEN subsetD])

lemma Nonce_secrecy:
     "evs  yahalom 
      (KK. KK  - (range shrK) 
           (K  KK. K  symKeys  ¬ KeyWithNonce K NB evs)   
           (Nonce NB  analz (Key`KK  (knows Spy evs))) =
           (Nonce NB  analz (knows Spy evs)))"
apply (erule yahalom.induct,
       frule_tac [7] YM4_analz_knows_Spy)
apply (safe del: allI impI intro!: Nonce_secrecy_lemma [THEN impI, THEN allI])
apply (simp_all del: image_insert image_Un
       add: analz_image_freshK_simps split_ifs
            all_conj_distrib ball_conj_distrib
            analz_image_freshK fresh_not_KeyWithNonce
            imp_disj_not1               (*Moves NBa≠NB to the front*)
            Says_Server_KeyWithNonce)
txtFor Oops, simplification proves propNBaNB.  By
  termSays_Server_KeyWithNonce, we get prop¬ KeyWithNonce K NB
  evs; then simplification can apply the induction hypothesis with
  termKK = {K}.
  subgoal ― ‹Fake by spy_analz
  subgoal ― ‹YM2 by blast
  subgoal ― ‹YM3 by blast
  subgoal ― ‹YM4: If propA  bad then termNBa is known, therefore propNBa  NB.
    by (metis A_trusts_YM3 Gets_imp_analz_Spy Gets_imp_knows_Spy KeyWithNonce_def
        Spy_analz_shrK analz.Fst analz.Snd analz_shrK_Decrypt parts.Fst parts.Inj)
done


textVersion required below: if NB can be decrypted using a session key then
   it was distributed with that key.  The more general form above is required
   for the induction to carry through.
lemma single_Nonce_secrecy:
     "Says Server A
          Crypt (shrK A) Agent B, Key KAB, na, Nonce NB', X
          set evs;
         NB  NB';  KAB  range shrK;  evs  yahalom
       (Nonce NB  analz (insert (Key KAB) (knows Spy evs))) =
          (Nonce NB  analz (knows Spy evs))"
by (simp_all del: image_insert image_Un imp_disjL
             add: analz_image_freshK_simps split_ifs
                  Nonce_secrecy Says_Server_KeyWithNonce)


subsubsectionThe Nonce NB uniquely identifies B's message.

lemma unique_NB:
     "Crypt (shrK B) Agent A, Nonce NA, nb  parts (knows Spy evs);
         Crypt (shrK B') Agent A', Nonce NA', nb  parts (knows Spy evs);
        evs  yahalom;  B  bad;  B'  bad
       NA' = NA  A' = A  B' = B"
apply (erule rev_mp, erule rev_mp)
apply (erule yahalom.induct, force,
       frule_tac [6] YM4_parts_knows_Spy, simp_all)
txtFake, and YM2 by freshness
apply blast+
done


textVariant useful for proving secrecy of NB.  Because nb is assumed to be
  secret, we no longer must assume B, B' not bad.
lemma Says_unique_NB:
     "Says C S   X,  Crypt (shrK B) Agent A, Nonce NA, nb
            set evs;
         Gets S' X', Crypt (shrK B') Agent A', Nonce NA', nb
            set evs;
         nb  analz (knows Spy evs);  evs  yahalom
       NA' = NA  A' = A  B' = B"
by (blast dest!: Gets_imp_Says Crypt_Spy_analz_bad
          dest: Says_imp_spies unique_NB parts.Inj analz.Inj)


subsubsectionA nonce value is never used both as NA and as NB

lemma no_nonce_YM1_YM2:
     "Crypt (shrK B') Agent A', Nonce NB, nb'  parts(knows Spy evs);
        Nonce NB  analz (knows Spy evs);  evs  yahalom
   Crypt (shrK B)  Agent A, na, Nonce NB  parts(knows Spy evs)"
apply (erule rev_mp, erule rev_mp)
apply (erule yahalom.induct, force,
       frule_tac [6] YM4_parts_knows_Spy)
apply (analz_mono_contra, simp_all)
txtFake, YM2
apply blast+
done

textThe Server sends YM3 only in response to YM2.
lemma Says_Server_imp_YM2:
     "Says Server A Crypt (shrK A) Agent B, k, na, nb, X  set evs;
         evs  yahalom
       Gets Server Agent B, Crypt (shrK B) Agent A, na, nb
              set evs"
by (erule rev_mp, erule yahalom.induct, auto)

textA vital theorem for B, that nonce NB remains secure from the Spy.
theorem Spy_not_see_NB :
     "Says B Server
                Agent B, Crypt (shrK B) Agent A, Nonce NA, Nonce NB
            set evs;
         (k. Notes Spy Nonce NA, Nonce NB, k  set evs);
         A  bad;  B  bad;  evs  yahalom
       Nonce NB  analz (knows Spy evs)"
apply (erule rev_mp, erule rev_mp)
apply (erule yahalom.induct, force,
       frule_tac [6] YM4_analz_knows_Spy)
apply (simp_all add: split_ifs pushes new_keys_not_analzd analz_insert_eq
                     analz_insert_freshK)
  subgoal ― ‹Fake by spy_analz
  subgoal ― ‹YM1: NB=NA is impossible anyway, but NA is secret because it is fresh! by blast
  subgoal ― ‹YM2 by blast
  subgoal ― ‹YM3: because no NB can also be an NA 
    by (blast dest!: no_nonce_YM1_YM2 dest: Gets_imp_Says Says_unique_NB)
  subgoal ― ‹YM4: key K is visible to Spy, contradicting session key secrecy theorem
    ― ‹Case analysis on whether Aa is bad;
            use Says_unique_NB› to identify message components: termAa=A, termBa=B
    apply clarify
    apply (blast dest!: Says_unique_NB analz_shrK_Decrypt
                        parts.Inj [THEN parts.Fst, THEN A_trusts_YM3]
                 dest: Gets_imp_Says Says_imp_spies Says_Server_imp_YM2
                       Spy_not_see_encrypted_key)
    done
  subgoal ― ‹Oops case: if the nonce is betrayed now, show that the Oops event is
    covered by the quantified Oops assumption.
    apply clarsimp
    apply (metis Says_Server_imp_YM2 Gets_imp_Says Says_Server_not_range Says_unique_NB no_nonce_YM1_YM2 parts.Snd single_Nonce_secrecy spies_partsEs(1))
    done
done

textB's session key guarantee from YM4.  The two certificates contribute to a
  single conclusion about the Server's message.  Note that the "Notes Spy"
  assumption must quantify over ∀› POSSIBLE keys instead of our particular K.
  If this run is broken and the spy substitutes a certificate containing an
  old key, B has no means of telling.
lemma B_trusts_YM4:
     "Gets B Crypt (shrK B) Agent A, Key K,
                  Crypt K (Nonce NB)  set evs;
         Says B Server
           Agent B, Crypt (shrK B) Agent A, Nonce NA, Nonce NB
            set evs;
         k. Notes Spy Nonce NA, Nonce NB, k  set evs;
         A  bad;  B  bad;  evs  yahalom
        Says Server A
                   Crypt (shrK A) Agent B, Key K,
                             Nonce NA, Nonce NB,
                     Crypt (shrK B) Agent A, Key K
              set evs"
by (blast dest: Spy_not_see_NB Says_unique_NB
                Says_Server_imp_YM2 B_trusts_YM4_newK)



textThe obvious combination of B_trusts_YM4› with 
  Spy_not_see_encrypted_key›
lemma B_gets_good_key:
     "Gets B Crypt (shrK B) Agent A, Key K,
                  Crypt K (Nonce NB)  set evs;
         Says B Server
           Agent B, Crypt (shrK B) Agent A, Nonce NA, Nonce NB
            set evs;
         k. Notes Spy Nonce NA, Nonce NB, k  set evs;
         A  bad;  B  bad;  evs  yahalom
       Key K  analz (knows Spy evs)"
  by (metis B_trusts_YM4 Spy_not_see_encrypted_key)


subsectionAuthenticating B to A

textThe encryption in message YM2 tells us it cannot be faked.
lemma B_Said_YM2 [rule_format]:
     "Crypt (shrK B) Agent A, Nonce NA, nb  parts (knows Spy evs);
        evs  yahalom
       B  bad 
          Says B Server Agent B, Crypt (shrK B) Agent A, Nonce NA, nb
             set evs"
apply (erule rev_mp, erule yahalom.induct, force,
       frule_tac [6] YM4_parts_knows_Spy, simp_all)
txtFake
apply blast
done

textIf the server sends YM3 then B sent YM2
lemma YM3_auth_B_to_A_lemma:
     "Says Server A Crypt (shrK A) Agent B, Key K, Nonce NA, nb, X
        set evs;  evs  yahalom
       B  bad 
          Says B Server Agent B, Crypt (shrK B) Agent A, Nonce NA, nb
             set evs"
apply (erule rev_mp, erule yahalom.induct, simp_all)
txtYM3, YM4
apply (blast dest!: B_Said_YM2)+
done

textIf A receives YM3 then B has used nonce NA (and therefore is alive)
theorem YM3_auth_B_to_A:
     "Gets A Crypt (shrK A) Agent B, Key K, Nonce NA, nb, X
            set evs;
         A  bad;  B  bad;  evs  yahalom
       Says B Server Agent B, Crypt (shrK B) Agent A, Nonce NA, nb
        set evs"
  by (metis A_trusts_YM3 Gets_imp_analz_Spy YM3_auth_B_to_A_lemma analz.Fst
         not_parts_not_analz)


subsectionAuthenticating A to B using the certificate 
  termCrypt K (Nonce NB)

textAssuming the session key is secure, if both certificates are present then
  A has said NB.  We can't be sure about the rest of A's message, but only
  NB matters for freshness.
theorem A_Said_YM3_lemma [rule_format]:
     "evs  yahalom
       Key K  analz (knows Spy evs) 
          Crypt K (Nonce NB)  parts (knows Spy evs) 
          Crypt (shrK B) Agent A, Key K  parts (knows Spy evs) 
          B  bad 
          (X. Says A B X, Crypt K (Nonce NB)  set evs)"
apply (erule yahalom.induct, force,
       frule_tac [6] YM4_parts_knows_Spy)
apply (analz_mono_contra, simp_all)
  subgoal ― ‹Fake by blast
  subgoal ― ‹YM3 because the message termCrypt K (Nonce NB) could not exist
     by (force dest!: Crypt_imp_keysFor)
   subgoal ― ‹YM4: was termCrypt K (Nonce NB) the very last message? If not, use the induction hypothesis,
               otherwise by unicity of session keys
     by (blast dest!: Gets_imp_Says A_trusts_YM3 B_trusts_YM4_shrK Crypt_Spy_analz_bad
             dest: Says_imp_knows_Spy [THEN parts.Inj] unique_session_keys)
done

textIf B receives YM4 then A has used nonce NB (and therefore is alive).
  Moreover, A associates K with NB (thus is talking about the same run).
  Other premises guarantee secrecy of K.
theorem YM4_imp_A_Said_YM3 [rule_format]:
     "Gets B Crypt (shrK B) Agent A, Key K,
                  Crypt K (Nonce NB)  set evs;
         Says B Server
           Agent B, Crypt (shrK B) Agent A, Nonce NA, Nonce NB
            set evs;
         (NA k. Notes Spy Nonce NA, Nonce NB, k  set evs);
         A  bad;  B  bad;  evs  yahalom
       X. Says A B X, Crypt K (Nonce NB)  set evs"
by (metis A_Said_YM3_lemma B_gets_good_key Gets_imp_analz_Spy YM4_parts_knows_Spy analz.Fst not_parts_not_analz)

end