# Theory OtwayRees_Bad

Up to index of Isabelle/HOL/Auth

theory OtwayRees_Bad
imports Public
begin

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

    header{*The Otway-Rees Protocol: The Faulty BAN Version*}

    theory OtwayRees_Bad imports Public begin

    text{*The FAULTY version omitting encryption of Nonce NB, as suggested on
    page 247 of
      Burrows, Abadi and Needham (1988).  A Logic of Authentication.
      Proc. Royal Soc. 426

    This file illustrates the consequences of such errors.  We can still prove
    impressive-looking properties such as @{text Spy_not_see_encrypted_key}, yet
    the protocol is open to a middleperson attack.  Attempting to prove some key
    lemmas indicates the possibility of this attack.*}

    consts  otway   :: "event list set"
    inductive "otway"
      intros
       Nil: --{*The empty trace*}
            "[] ∈ otway"

       Fake: --{*The Spy may say anything he can say.  The sender field is correct,
                but agents don't use that information.*}
             "[| evsf ∈ otway;  X ∈ synth (analz (knows Spy evsf)) |]
              ==> Says Spy B X  # evsf ∈ otway"

       Reception: --{*A message that has been sent can be received by the
                      intended recipient.*}
                  "[| evsr ∈ otway;  Says A B X ∈set evsr |]
                   ==> Gets B X # evsr ∈ otway"

       OR1:  --{*Alice initiates a protocol run*}
             "[| evs1 ∈ otway;  Nonce NA ∉ used evs1 |]
              ==> Says A B {|Nonce NA, Agent A, Agent B,
                             Crypt (shrK A) {|Nonce NA, Agent A, Agent B|} |}
                     # evs1 ∈ otway"

       OR2:  --{*Bob's response to Alice's message.
                 This variant of the protocol does NOT encrypt NB.*}
             "[| evs2 ∈ otway;  Nonce NB ∉ used evs2;
                 Gets B {|Nonce NA, Agent A, Agent B, X|} ∈ set evs2 |]
              ==> Says B Server
                      {|Nonce NA, Agent A, Agent B, X, Nonce NB,
                        Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|}
                     # evs2 ∈ otway"

       OR3:  --{*The Server receives Bob's message and checks that the three NAs
               match.  Then he sends a new session key to Bob with a packet for
               forwarding to Alice.*}
             "[| evs3 ∈ otway;  Key KAB ∉ used evs3;
                 Gets Server
                      {|Nonce NA, Agent A, Agent B,
                        Crypt (shrK A) {|Nonce NA, Agent A, Agent B|},
                        Nonce NB,
                        Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|}
                   ∈ set evs3 |]
              ==> Says Server B
                      {|Nonce NA,
                        Crypt (shrK A) {|Nonce NA, Key KAB|},
                        Crypt (shrK B) {|Nonce NB, Key KAB|}|}
                     # evs3 ∈ otway"

       OR4:  --{*Bob receives the Server's (?) message and compares the Nonces with
                 those in the message he previously sent the Server.
                 Need @{term "B ≠ Server"} because we allow messages to self.*}
             "[| evs4 ∈ otway;  B ≠ Server;
                 Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB,
                                 Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|}
                   ∈ set evs4;
                 Gets B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
                   ∈ set evs4 |]
              ==> Says B A {|Nonce NA, X|} # evs4 ∈ otway"

       Oops: --{*This message models possible leaks of session keys.  The nonces
                 identify the protocol run.*}
             "[| evso ∈ otway;
                 Says Server B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
                   ∈ set evso |]
              ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso ∈ otway"

    declare Says_imp_knows_Spy [THEN analz.Inj, dest]
    declare parts.Body  [dest]
    declare analz_into_parts [dest]
    declare Fake_parts_insert_in_Un  [dest]

    text{*A "possibility property": there are traces that reach the end*}
    lemma "[| B ≠ Server; Key K ∉ used [] |]
          ==> ∃NA. ∃evs ∈ otway.
                Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|}
                  ∈ set evs"
    apply (intro exI bexI)
    apply (rule_tac [2] otway.Nil
                        [THEN otway.OR1, THEN otway.Reception,
                         THEN otway.OR2, THEN otway.Reception,
                         THEN otway.OR3, THEN otway.Reception, THEN otway.OR4])
    apply (possibility, simp add: used_Cons)
    done

    lemma Gets_imp_Says [dest!]:
         "[| Gets B X ∈ set evs; evs ∈ otway |] ==> ∃A. Says A B X ∈ set evs"
    apply (erule rev_mp)
    apply (erule otway.induct, auto)
    done

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

    lemma OR2_analz_knows_Spy:
         "[| Gets B {|N, Agent A, Agent B, X|} ∈ set evs;  evs ∈ otway |]
          ==> X ∈ analz (knows Spy evs)"
    by blast

    lemma OR4_analz_knows_Spy:
         "[| Gets B {|N, X, Crypt (shrK B) X'|} ∈ set evs;  evs ∈ otway |]
          ==> X ∈ analz (knows Spy evs)"
    by blast

    lemma Oops_parts_knows_Spy:
         "Says Server B {|NA, X, Crypt K' {|NB,K|}|} ∈ set evs
          ==> K ∈ parts (knows Spy evs)"
    by blast

    text{*Forwarding lemma: see comments in OtwayRees.thy*}
    lemmas OR2_parts_knows_Spy =
        OR2_analz_knows_Spy [THEN analz_into_parts, standard]

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

    text{*Spy never sees a good agent's shared key!*}
    lemma Spy_see_shrK [simp]:
         "evs ∈ otway ==> (Key (shrK A) ∈ parts (knows Spy evs)) = (A ∈ bad)"
    by (erule otway.induct, force,
        drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)

    lemma Spy_analz_shrK [simp]:
         "evs ∈ otway ==> (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 ∈ otway|] ==> A ∈ bad"
    by (blast dest: Spy_see_shrK)

    subsection{*Proofs involving analz *}

    text{*Describes the form of K and NA when the Server sends this message.  Also
      for Oops case.*}
    lemma Says_Server_message_form:
         "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} ∈ set evs;
             evs ∈ otway |]
          ==> K ∉ range shrK & (∃i. NA = Nonce i) & (∃j. NB = Nonce j)"
    apply (erule rev_mp)
    apply (erule otway.induct, simp_all, blast)
    done

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

    text{*Session keys are not used to encrypt other session keys*}

    text{*The equality makes the induction hypothesis easier to apply*}
    lemma analz_image_freshK [rule_format]:
     "evs ∈ otway ==>
       ∀K KK. KK <= -(range shrK) -->
              (Key K ∈ analz (Key`KK Un (knows Spy evs))) =
              (K ∈ KK | Key K ∈ analz (knows Spy evs))"
    apply (erule otway.induct)
    apply (frule_tac [8] Says_Server_message_form)
    apply (drule_tac [7] OR4_analz_knows_Spy)
    apply (drule_tac [5] OR2_analz_knows_Spy, analz_freshK, spy_analz, auto)
    done

    lemma analz_insert_freshK:
      "[| evs ∈ otway;  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 B {|NA, X, Crypt (shrK B) {|NB, K|}|}   ∈ set evs;
             Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|} ∈ set evs;
             evs ∈ otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'"
    apply (erule rev_mp)
    apply (erule rev_mp)
    apply (erule otway.induct, simp_all)
    apply blast+  --{*OR3 and OR4*}
    done

    text{*Crucial secrecy property: Spy does not see the keys sent in msg OR3
        Does not in itself guarantee security: an attack could violate
        the premises, e.g. by having @{term "A=Spy"} *}
    lemma secrecy_lemma:
     "[| A ∉ bad;  B ∉ bad;  evs ∈ otway |]
      ==> Says Server B
            {|NA, Crypt (shrK A) {|NA, Key K|},
              Crypt (shrK B) {|NB, Key K|}|} ∈ set evs -->
          Notes Spy {|NA, NB, Key K|} ∉ set evs -->
          Key K ∉ analz (knows Spy evs)"
    apply (erule otway.induct, force)
    apply (frule_tac [7] Says_Server_message_form)
    apply (drule_tac [6] OR4_analz_knows_Spy)
    apply (drule_tac [4] OR2_analz_knows_Spy)
    apply (simp_all add: analz_insert_eq analz_insert_freshK pushes)
    apply spy_analz  --{*Fake*}
    apply (blast dest: unique_session_keys)+  --{*OR3, OR4, Oops*}
    done

    lemma Spy_not_see_encrypted_key:
         "[| Says Server B
              {|NA, Crypt (shrK A) {|NA, Key K|},
                    Crypt (shrK B) {|NB, Key K|}|} ∈ set evs;
             Notes Spy {|NA, NB, Key K|} ∉ set evs;
             A ∉ bad;  B ∉ bad;  evs ∈ otway |]
          ==> Key K ∉ analz (knows Spy evs)"
    by (blast dest: Says_Server_message_form secrecy_lemma)

    subsection{*Attempting to prove stronger properties *}

    text{*Only OR1 can have caused such a part of a message to appear. The premise
      @{term "A ≠ B"} prevents OR2's similar-looking cryptogram from being picked
      up. Original Otway-Rees doesn't need it.*}
    lemma Crypt_imp_OR1 [rule_format]:
         "[| A ∉ bad;  A ≠ B;  evs ∈ otway |]
          ==> Crypt (shrK A) {|NA, Agent A, Agent B|} ∈ parts (knows Spy evs) -->
              Says A B {|NA, Agent A, Agent B,
                         Crypt (shrK A) {|NA, Agent A, Agent B|}|}  ∈ set evs"
    by (erule otway.induct, force,
        drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)

    text{*Crucial property: If the encrypted message appears, and A has used NA
      to start a run, then it originated with the Server!
      The premise @{term "A ≠ B"} allows use of @{text Crypt_imp_OR1}*}
    text{*Only it is FALSE.  Somebody could make a fake message to Server
              substituting some other nonce NA' for NB.*}
    lemma "[| A ∉ bad;  A ≠ B;  evs ∈ otway |]
           ==> Crypt (shrK A) {|NA, Key K|} ∈ parts (knows Spy evs) -->
               Says A B {|NA, Agent A, Agent B,
                          Crypt (shrK A) {|NA, Agent A, Agent B|}|}
                ∈ set evs -->
               (∃B NB. Says Server B
                    {|NA,
                      Crypt (shrK A) {|NA, Key K|},
                      Crypt (shrK B) {|NB, Key K|}|}  ∈ set evs)"
    apply (erule otway.induct, force,
           drule_tac [4] OR2_parts_knows_Spy, simp_all)
    apply blast  --{*Fake*}
    apply blast  --{*OR1: it cannot be a new Nonce, contradiction.*}
    txt{*OR3 and OR4*}
    apply (simp_all add: ex_disj_distrib)
     prefer 2 apply (blast intro!: Crypt_imp_OR1)  --{*OR4*}
    txt{*OR3*}
    apply clarify
    (*The hypotheses at this point suggest an attack in which nonce NB is used
      in two different roles:
              Gets Server
               {|Nonce NA, Agent Aa, Agent A,
                 Crypt (shrK Aa) {|Nonce NA, Agent Aa, Agent A|}, Nonce NB,
                 Crypt (shrK A) {|Nonce NA, Agent Aa, Agent A|}|}
              ∈ set evs3
              Says A B
               {|Nonce NB, Agent A, Agent B,
                 Crypt (shrK A) {|Nonce NB, Agent A, Agent B|}|}
              ∈ set evs3;
    *)

    (*Thus the key property A_can_trust probably fails too.*)
    oops

    end

lemma

      [| B ≠ Server; Key K ∉ used [] |]
      ==> ∃NA. ∃evs∈otway.
                  Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} ∈ set evs

lemma Gets_imp_Says:

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

### For reasoning about the encrypted portion of messages

lemma OR2_analz_knows_Spy:

      [| Gets B {|N, Agent A, Agent B, X|} ∈ set evs; evs ∈ otway |]
      ==> X ∈ analz (knows Spy evs)

lemma OR4_analz_knows_Spy:

      [| Gets B {|N, X, Crypt (shrK B) X'|} ∈ set evs; evs ∈ otway |]
      ==> X ∈ analz (knows Spy evs)

lemma Oops_parts_knows_Spy:

      Says Server B {|NA, X, Crypt K' {|NB, K|}|} ∈ set evs
      ==> K ∈ parts (knows Spy evs)

lemmas OR2_parts_knows_Spy:

      [| Gets B {|N, Agent A, Agent B, c|} ∈ set evs; evs ∈ otway |]
      ==> c ∈ parts (knows Spy evs)

lemmas OR2_parts_knows_Spy:

      [| Gets B {|N, Agent A, Agent B, c|} ∈ set evs; evs ∈ otway |]
      ==> c ∈ parts (knows Spy evs)

lemma Spy_see_shrK:

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

lemma Spy_analz_shrK:

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

lemma Spy_see_shrK_D:

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

### Proofs involving analz

lemma Says_Server_message_form:

      [| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} ∈ set evs;
         evs ∈ otway |]
      ==> K ∉ range shrK ∧ (∃i. NA = Nonce i) ∧ (∃j. NB = Nonce j)

lemma analz_image_freshK:

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

lemma analz_insert_freshK:

      [| evs ∈ otway; 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 B {|NA, X, Crypt (shrK B) {|NB, K|}|} ∈ set evs;
         Says Server B' {|NA', X', Crypt (shrK B') {|NB', K|}|} ∈ set evs;
         evs ∈ otway |]
      ==> X = X' ∧ B = B' ∧ NA = NA' ∧ NB = NB'

lemma secrecy_lemma:

      [| A ∉ bad; B ∉ bad; evs ∈ otway |]
      ==> Says Server B
           {|NA, Crypt (shrK A) {|NA, Key K|}, Crypt (shrK B) {|NB, Key K|}|}
          ∈ set evs -->
          Notes Spy {|NA, NB, Key K|} ∉ set evs --> Key K ∉ analz (knows Spy evs)

lemma Spy_not_see_encrypted_key:

      [| Says Server B
          {|NA, Crypt (shrK A) {|NA, Key K|}, Crypt (shrK B) {|NB, Key K|}|}
         ∈ set evs;
         Notes Spy {|NA, NB, Key K|} ∉ set evs; A ∉ bad; B ∉ bad; evs ∈ otway |]
      ==> Key K ∉ analz (knows Spy evs)

### Attempting to prove stronger properties

lemma Crypt_imp_OR1:

      [| A ∉ bad; A ≠ B; evs ∈ otway;
         Crypt (shrK A) {|NA, Agent A, Agent B|} ∈ parts (knows Spy evs) |]
      ==> Says A B {|NA, Agent A, Agent B, Crypt (shrK A) {|NA, Agent A, Agent B|}|}
          ∈ set evs