Theory Yahalom_Bad

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

sectionThe Yahalom Protocol: A Flawed Version

theory Yahalom_Bad imports Public begin

text
Demonstrates of why Oops is necessary.  This protocol can be attacked because
it doesn't keep NB secret, but without Oops it can be "verified" anyway.
The issues are discussed in lcp's LICS 2000 invited lecture.


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, Nonce NB, Crypt (shrK B) Agent A, Nonce NA
                # 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, Nonce NB, Crypt (shrK B) Agent A, Nonce NA
                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"

         (*Alice receives the Server's (?) message, checks her Nonce, and
           uses the new session key to send Bob his Nonce.  The premise
           A ≠ Server is needed to prove Says_Server_not_range.*)
 | YM4:  "[| 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"


declare Says_imp_knows_Spy [THEN analz.Inj, 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; Key K  used []; K  symKeys |] 
       ==> 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)

(*Must 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)

declare Gets_imp_knows_Spy [THEN analz.Inj, dest]


subsectionFor reasoning about the encrypted portion of messages

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]


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)"
apply (erule yahalom.induct, force,
       drule_tac [6] YM4_parts_knows_Spy, simp_all, blast+)
done

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


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.
****)

subsectionSession 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))"
by (erule yahalom.induct, 
    drule_tac [7] YM4_analz_knows_Spy, analz_freshK, spy_analz, blast) 

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 
          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, spy_analz)  (*Fake*)
apply (blast dest: unique_session_keys)  (*YM3*)
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;
         A  bad;  B  bad;  evs  yahalom |]
      ==> Key K  analz (knows Spy evs)"
by (blast dest: secrecy_lemma)


subsectionSecurity 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);
         A  bad;  B  bad;  evs  yahalom |]
      ==> Key K  analz (knows Spy evs)"
by (blast dest!: A_trusts_YM3 Spy_not_see_encrypted_key)

subsectionSecurity 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

subsectionThe Flaw in the Model

textUp to now, the reasoning is similar to standard Yahalom.  Now the
    doubtful reasoning occurs.  We should not be assuming that an unknown
    key is secure, but the model allows us to: there is no Oops rule to
    let session keys become compromised.

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 K is assumed; the valid Yahalom proof uses (and later proves)
  the secrecy of NB.
lemma B_trusts_YM4_newK [rule_format]:
     "[|Key K  analz (knows Spy evs);  evs  yahalom|]
      ==> Crypt K (Nonce NB)  parts (knows Spy evs) 
          (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)
apply (erule yahalom.induct, force,
       frule_tac [6] YM4_parts_knows_Spy)
apply (analz_mono_contra, simp_all)
txtFake
apply blast
txtYM3
apply blast
txtA 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


textB's session key guarantee from YM4.  The two certificates contribute to a
  single conclusion about the Server's message.
lemma B_trusts_YM4:
     "[| Gets B Crypt (shrK B) Agent A, Key K,
                  Crypt K (Nonce NB)  set evs;
         Says B Server
           Agent B, Nonce NB, Crypt (shrK B) Agent A, Nonce NA
            set evs;
         A  bad;  B  bad;  evs  yahalom |]
       ==> na nb. Says Server A
                   Crypt (shrK A) Agent B, Key K, na, nb,
                     Crypt (shrK B) Agent A, Key K
              set evs"
by (blast dest: B_trusts_YM4_newK B_trusts_YM4_shrK Spy_not_see_encrypted_key
                unique_session_keys)


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, Nonce NB, Crypt (shrK B) Agent A, Nonce NA
            set evs;
         A  bad;  B  bad;  evs  yahalom |]
      ==> Key K  analz (knows Spy evs)"
by (blast dest!: B_trusts_YM4 Spy_not_see_encrypted_key)


(*** Authenticating B to A: these proofs are not considered.
     They are irrelevant to showing the need for Oops. ***)


(*** Authenticating A to B using the certificate Crypt 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.
lemma 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)
txtFake
apply blast
txtYM3: by new_keys_not_used›, the message
   termCrypt K (Nonce NB) could not exist
apply (force dest!: Crypt_imp_keysFor)
txtYM4: was termCrypt K (Nonce NB) the very last message?
    If not, use the induction hypothesis
apply (simp add: ex_disj_distrib)
txtyes: apply unicity of session keys
apply (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.
lemma 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, Nonce NB, Crypt (shrK B) Agent A, Nonce NA
            set evs;
         A  bad;  B  bad;  evs  yahalom |]
      ==> X. Says A B X, Crypt K (Nonce NB)  set evs"
by (blast intro!: A_Said_YM3_lemma
          dest: Spy_not_see_encrypted_key B_trusts_YM4 Gets_imp_Says)

end