# Theory Yahalom_Bad

Up to index of Isabelle/HOL/Auth

theory Yahalom_Bad
imports Public
begin

    (*  Title:      HOL/Auth/Yahalom
        ID:         $Id: Yahalom_Bad.thy,v 1.10 2005/06/17 14:13:06 haftmann Exp $
        Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
        Copyright   1996  University of Cambridge
    *)

    header{*The 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.
    *}

    consts  yahalom   :: "event list set"
    inductive "yahalom"
      intros
             (*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]

    text{*A "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

    subsection{*Regularity 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]

    subsection{* For reasoning about the encrypted portion of messages *}

    text{*Lets 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, standard]

    text{*Theorems of the form @{term "X ∉ parts (knows Spy evs)"} imply
                that NOBODY sends messages containing X!*}

    text{*Spy 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)

    text{*Nobody can have used non-existent keys!
        Needed to apply @{text 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)
    txt{*Fake*}
    apply (force dest!: keysFor_parts_insert, auto)
    done

    subsection{*Secrecy 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.
    ****)

    subsection{* Session 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 Un (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)

    text{*The 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)
    txt{*YM3, by freshness, and YM4*}
    apply blast+
    done

    text{* Crucial 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

    text{*Final 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)

    subsection{* Security Guarantee for A upon receiving YM3 *}

    text{*If 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)
    txt{*Fake, YM3*}
    apply blast+
    done

    text{*The obvious combination of @{text A_trusts_YM3} with
      @{text 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)

    subsection{* Security Guarantees for B upon receiving YM4 *}

    text{*B 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)
    txt{*Fake, YM3*}
    apply blast+
    done

    subsection{*The Flaw in the Model*}

    text{* Up 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.*}

    text{*B 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)
    txt{*Fake*}
    apply blast
    txt{*YM3*}
    apply blast
    txt{*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

    text{*B'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)

    text{*The obvious combination of @{text B_trusts_YM4} with
      @{text 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) ***)

    text{*Assuming 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)
    txt{*Fake*}
    apply blast
    txt{*YM3: by @{text new_keys_not_used}, the message
       @{term "Crypt K (Nonce NB)"} could not exist*}
    apply (force dest!: Crypt_imp_keysFor)
    txt{*YM4: was @{term "Crypt K (Nonce NB)"} the very last message?
        If not, use the induction hypothesis*}
    apply (simp add: ex_disj_distrib)
    txt{*yes: 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

    text{*If 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

lemma

      [| A ≠ Server; Key K ∉ used []; K ∈ symKeys |]
      ==> ∃X NB. ∃evs∈yahalom. Says A B {|X, Crypt K (Nonce NB)|} ∈ set evs

### Regularity Lemmas for Yahalom

lemma Gets_imp_Says:

      [| Gets B X ∈ set evs; evs ∈ yahalom |] ==> ∃A. Says A B X ∈ set evs

lemma Gets_imp_knows_Spy:

      [| Gets B X ∈ set evs; evs ∈ yahalom |] ==> X ∈ knows Spy evs

### For reasoning about the encrypted portion of messages

lemma YM4_analz_knows_Spy:

      [| Gets A {|Crypt (shrK A) Y, X|} ∈ set evs; evs ∈ yahalom |]
      ==> X ∈ analz (knows Spy evs)

lemmas YM4_parts_knows_Spy:

      [| Gets A {|Crypt (shrK A) Y, c|} ∈ set evs; evs ∈ yahalom |]
      ==> c ∈ parts (knows Spy evs)

lemmas YM4_parts_knows_Spy:

      [| Gets A {|Crypt (shrK A) Y, c|} ∈ set evs; evs ∈ yahalom |]
      ==> c ∈ parts (knows Spy evs)

lemma Spy_see_shrK:

      evs ∈ yahalom ==> (Key (shrK A) ∈ parts (knows Spy evs)) = (A ∈ bad)

lemma Spy_analz_shrK:

      evs ∈ yahalom ==> (Key (shrK A) ∈ analz (knows Spy evs)) = (A ∈ bad)

lemma Spy_see_shrK_D:

      [| Key (shrK A) ∈ parts (knows Spy evs); evs ∈ yahalom |] ==> A ∈ bad

lemma new_keys_not_used:

      [| Key K ∉ used evs; K ∈ symKeys; evs ∈ yahalom |]
      ==> K ∉ keysFor (parts (knows Spy evs))

### Secrecy Theorems

### Session keys are not used to encrypt other session keys

lemma analz_image_freshK:

      [| evs ∈ yahalom; KK ⊆ - range shrK |]
      ==> (Key K ∈ analz (Key ` KK ∪ knows Spy evs)) =
          (K ∈ KK ∨ Key K ∈ analz (knows Spy evs))

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

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'

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)

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)

### Security Guarantee for A upon receiving YM3

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

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)

### Security Guarantees for B upon receiving YM4

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

### The Flaw in the Model

lemma B_trusts_YM4_newK:

      [| 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

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

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)

lemma A_Said_YM3_lemma:

      [| 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

lemma YM4_imp_A_Said_YM3:

      [| 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