# Theory OtwayRees_AN

Up to index of Isabelle/HOL/Auth

theory OtwayRees_AN
imports Public
begin

    (*  Title:      HOL/Auth/OtwayRees
        ID:         $Id: OtwayRees_AN.thy,v 1.26 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 as Modified by Abadi and Needham*}

    theory OtwayRees_AN imports Public begin

    text{*
    This simplified version has minimal encryption and explicit messages.

    Note that the formalization does not even assume that nonces are fresh.
    This is because the protocol does not rely on uniqueness of nonces for
    security, only for freshness, and the proof script does not prove freshness
    properties.

    From page 11 of
      Abadi and Needham (1996).
      Prudent Engineering Practice for Cryptographic Protocols.
      IEEE Trans. SE 22 (1)
    *}

    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
              ==> Says A B {|Agent A, Agent B, Nonce NA|} # evs1 ∈ otway"

       OR2:  --{*Bob's response to Alice's message.*}
             "[| evs2 ∈ otway;
                 Gets B {|Agent A, Agent B, Nonce NA|} ∈set evs2 |]
              ==> Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
                     # evs2 ∈ otway"

       OR3:  --{*The Server receives Bob's message.  Then he sends a new
               session key to Bob with a packet for forwarding to Alice.*}
             "[| evs3 ∈ otway;  Key KAB ∉ used evs3;
                 Gets Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
                   ∈set evs3 |]
              ==> Says Server B
                   {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key KAB|},
                     Crypt (shrK B) {|Nonce NB, Agent A, Agent B, 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 {|Agent A, Agent B, Nonce NA, Nonce NB|} ∈set evs4;
                 Gets B {|X, Crypt(shrK B){|Nonce NB,Agent A,Agent B,Key K|}|}
                   ∈set evs4 |]
              ==> Says B A X # evs4 ∈ otway"

       Oops: --{*This message models possible leaks of session keys.  The nonces
                 identify the protocol run.*}
             "[| evso ∈ otway;
                 Says Server B
                          {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|},
                            Crypt (shrK B) {|Nonce NB, Agent A, Agent B, 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 [] |]
          ==> ∃evs ∈ otway.
               Says B A (Crypt (shrK A) {|Nonce NA, Agent A, Agent B, 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"
    by (erule rev_mp, erule otway.induct, auto)

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

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

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

    subsection{*Authenticity properties relating to NA*}

    text{*If the encrypted message appears then it originated with the Server!*}
    lemma NA_Crypt_imp_Server_msg [rule_format]:
        "[| A ∉ bad;  A ≠ B;  evs ∈ otway |]
         ==> Crypt (shrK A) {|NA, Agent A, Agent B, Key K|} ∈ parts (knows Spy evs)
           --> (∃NB. Says Server B
                        {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},
                          Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}
                        ∈ set evs)"
    apply (erule otway.induct, force)
    apply (simp_all add: ex_disj_distrib)
    apply blast+  --{*Fake, OR3*}
    done

    text{*Corollary: if A receives B's OR4 message then it originated with the
          Server. Freshness may be inferred from nonce NA.*}
    lemma A_trusts_OR4:
         "[| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}) ∈ set evs;
             A ∉ bad;  A ≠ B;  evs ∈ otway |]
          ==> ∃NB. Says Server B
                      {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},
                        Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}
                     ∈ set evs"
    by (blast intro!: NA_Crypt_imp_Server_msg)

    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
               {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},
                 Crypt (shrK B) {|NB, Agent A, Agent B, 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 (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
                {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},
                  Crypt (shrK B) {|NB, Agent A, Agent B, 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)

    text{*A's guarantee.  The Oops premise quantifies over NB because A cannot know
      what it is.*}
    lemma A_gets_good_key:
         "[| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}) ∈ set evs;
             ∀NB. Notes Spy {|NA, NB, Key K|} ∉ set evs;
             A ∉ bad;  B ∉ bad;  A ≠ B;  evs ∈ otway |]
          ==> Key K ∉ analz (knows Spy evs)"
    by (blast dest!: A_trusts_OR4 Spy_not_see_encrypted_key)

    subsection{*Authenticity properties relating to NB*}

    text{*If the encrypted message appears then it originated with the Server!*}
    lemma NB_Crypt_imp_Server_msg [rule_format]:
     "[| B ∉ bad;  A ≠ B;  evs ∈ otway |]
      ==> Crypt (shrK B) {|NB, Agent A, Agent B, Key K|} ∈ parts (knows Spy evs)
          --> (∃NA. Says Server B
                       {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},
                         Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}
                       ∈ set evs)"
    apply (erule otway.induct, force, simp_all add: ex_disj_distrib)
    apply blast+  --{*Fake, OR3*}
    done

    text{*Guarantee for B: if it gets a well-formed certificate then the Server
      has sent the correct message in round 3.*}
    lemma B_trusts_OR3:
         "[| Says S B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}
               ∈ set evs;
             B ∉ bad;  A ≠ B;  evs ∈ otway |]
          ==> ∃NA. Says Server B
                       {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},
                         Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}
                       ∈ set evs"
    by (blast intro!: NB_Crypt_imp_Server_msg)

    text{*The obvious combination of @{text B_trusts_OR3} with
          @{text Spy_not_see_encrypted_key}*}
    lemma B_gets_good_key:
         "[| Gets B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}
              ∈ set evs;
             ∀NA. Notes Spy {|NA, NB, Key K|} ∉ set evs;
             A ∉ bad;  B ∉ bad;  A ≠ B;  evs ∈ otway |]
          ==> Key K ∉ analz (knows Spy evs)"
    by (blast dest: B_trusts_OR3 Spy_not_see_encrypted_key)

    end

lemma

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

lemma Gets_imp_Says:

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

lemma OR4_analz_knows_Spy:

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

### Authenticity properties relating to NA

lemma NA_Crypt_imp_Server_msg:

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

lemma A_trusts_OR4:

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

lemma secrecy_lemma:

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

lemma A_gets_good_key:

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

### Authenticity properties relating to NB

lemma NB_Crypt_imp_Server_msg:

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

lemma B_trusts_OR3:

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

lemma B_gets_good_key:

      [| Gets B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} ∈ set evs;
         ∀NA. Notes Spy {|NA, NB, Key K|} ∉ set evs; A ∉ bad; B ∉ bad; A ≠ B;
         evs ∈ otway |]
      ==> Key K ∉ analz (knows Spy evs)