# Theory WooLam

Up to index of Isabelle/HOL/Auth

theory WooLam
imports Public
begin

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

    header{*The Woo-Lam Protocol*}

    theory WooLam imports Public begin

    text{*Simplified version from page 11 of
      Abadi and Needham (1996).
      Prudent Engineering Practice for Cryptographic Protocols.
      IEEE Trans. S.E. 22(1), pages 6-15.

    Note: this differs from the Woo-Lam protocol discussed by Lowe (1996):
      Some New Attacks upon Security Protocols.
      Computer Security Foundations Workshop
    *}

    consts  woolam  :: "event list set"
    inductive woolam
      intros
             (*Initial trace is empty*)
       Nil:  "[] ∈ woolam"

             (** These rules allow agents to send messages to themselves **)

             (*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 ∈ woolam;  X ∈ synth (analz (spies evsf)) |]
              ==> Says Spy B X  # evsf ∈ woolam"

             (*Alice initiates a protocol run*)
       WL1:  "evs1 ∈ woolam ==> Says A B (Agent A) # evs1 ∈ woolam"

             (*Bob responds to Alice's message with a challenge.*)
       WL2:  "[| evs2 ∈ woolam;  Says A' B (Agent A) ∈ set evs2 |]
              ==> Says B A (Nonce NB) # evs2 ∈ woolam"

             (*Alice responds to Bob's challenge by encrypting NB with her key.
               B is *not* properly determined -- Alice essentially broadcasts
               her reply.*)
       WL3:  "[| evs3 ∈ woolam;
                 Says A  B (Agent A)  ∈ set evs3;
                 Says B' A (Nonce NB) ∈ set evs3 |]
              ==> Says A B (Crypt (shrK A) (Nonce NB)) # evs3 ∈ woolam"

             (*Bob forwards Alice's response to the Server.  NOTE: usually
               the messages are shown in chronological order, for clarity.
               But here, exchanging the two events would cause the lemma
               WL4_analz_spies to pick up the wrong assumption!*)
       WL4:  "[| evs4 ∈ woolam;
                 Says A'  B X         ∈ set evs4;
                 Says A'' B (Agent A) ∈ set evs4 |]
              ==> Says B Server {|Agent A, Agent B, X|} # evs4 ∈ woolam"

             (*Server decrypts Alice's response for Bob.*)
       WL5:  "[| evs5 ∈ woolam;
                 Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|}
                   ∈ set evs5 |]
              ==> Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|})
                     # evs5 ∈ woolam"

    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]

    (*A "possibility property": there are traces that reach the end*)
    lemma "∃NB. ∃evs ∈ woolam.
                 Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|}) ∈ set evs"
    apply (intro exI bexI)
    apply (rule_tac [2] woolam.Nil
                        [THEN woolam.WL1, THEN woolam.WL2, THEN woolam.WL3,
                         THEN woolam.WL4, THEN woolam.WL5], possibility)
    done

    (*Could prove forwarding lemmas for WL4, but we do not need them!*)

    (**** Inductive proofs about woolam ****)

    (** Theorems of the form X ∉ parts (spies evs) imply that NOBODY
        sends messages containing X! **)

    (*Spy never sees a good agent's shared key!*)
    lemma Spy_see_shrK [simp]:
         "evs ∈ woolam ==> (Key (shrK A) ∈ parts (spies evs)) = (A ∈ bad)"
    by (erule woolam.induct, force, simp_all, blast+)

    lemma Spy_analz_shrK [simp]:
         "evs ∈ woolam ==> (Key (shrK A) ∈ analz (spies evs)) = (A ∈ bad)"
    by auto

    lemma Spy_see_shrK_D [dest!]:
         "[|Key (shrK A) ∈ parts (knows Spy evs);  evs ∈ woolam|] ==> A ∈ bad"
    by (blast dest: Spy_see_shrK)

    (**** Autheticity properties for Woo-Lam ****)

    (*** WL4 ***)

    (*If the encrypted message appears then it originated with Alice*)
    lemma NB_Crypt_imp_Alice_msg:
         "[| Crypt (shrK A) (Nonce NB) ∈ parts (spies evs);
             A ∉ bad;  evs ∈ woolam |]
          ==> ∃B. Says A B (Crypt (shrK A) (Nonce NB)) ∈ set evs"
    by (erule rev_mp, erule woolam.induct, force, simp_all, blast+)

    (*Guarantee for Server: if it gets a message containing a certificate from
      Alice, then she originated that certificate.  But we DO NOT know that B
      ever saw it: the Spy may have rerouted the message to the Server.*)
    lemma Server_trusts_WL4 [dest]:
         "[| Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|}
               ∈ set evs;
             A ∉ bad;  evs ∈ woolam |]
          ==> ∃B. Says A B (Crypt (shrK A) (Nonce NB)) ∈ set evs"
    by (blast intro!: NB_Crypt_imp_Alice_msg)

    (*** WL5 ***)

    (*Server sent WL5 only if it received the right sort of message*)
    lemma Server_sent_WL5 [dest]:
         "[| Says Server B (Crypt (shrK B) {|Agent A, NB|}) ∈ set evs;
             evs ∈ woolam |]
          ==> ∃B'. Says B' Server {|Agent A, Agent B, Crypt (shrK A) NB|}
                 ∈ set evs"
    by (erule rev_mp, erule woolam.induct, force, simp_all, blast+)

    (*If the encrypted message appears then it originated with the Server!*)
    lemma NB_Crypt_imp_Server_msg [rule_format]:
         "[| Crypt (shrK B) {|Agent A, NB|} ∈ parts (spies evs);
             B ∉ bad;  evs ∈ woolam |]
          ==> Says Server B (Crypt (shrK B) {|Agent A, NB|}) ∈ set evs"
    by (erule rev_mp, erule woolam.induct, force, simp_all, blast+)

    (*Guarantee for B.  If B gets the Server's certificate then A has encrypted
      the nonce using her key.  This event can be no older than the nonce itself.
      But A may have sent the nonce to some other agent and it could have reached
      the Server via the Spy.*)
    lemma B_trusts_WL5:
         "[| Says S B (Crypt (shrK B) {|Agent A, Nonce NB|}): set evs;
             A ∉ bad;  B ∉ bad;  evs ∈ woolam  |]
          ==> ∃B. Says A B (Crypt (shrK A) (Nonce NB)) ∈ set evs"
    by (blast dest!: NB_Crypt_imp_Server_msg)

    (*B only issues challenges in response to WL1.  Not used.*)
    lemma B_said_WL2:
         "[| Says B A (Nonce NB) ∈ set evs;  B ≠ Spy;  evs ∈ woolam |]
          ==> ∃A'. Says A' B (Agent A) ∈ set evs"
    by (erule rev_mp, erule woolam.induct, force, simp_all, blast+)

    (**CANNOT be proved because A doesn't know where challenges come from...*)
    lemma "[| A ∉ bad;  B ≠ Spy;  evs ∈ woolam |]
      ==> Crypt (shrK A) (Nonce NB) ∈ parts (spies evs) &
          Says B A (Nonce NB) ∈ set evs
          --> Says A B (Crypt (shrK A) (Nonce NB)) ∈ set evs"
    apply (erule rev_mp, erule woolam.induct, force, simp_all, blast, auto)
    oops

    end

lemma

      ∃NB. ∃evs∈woolam. Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|}) ∈ set evs

lemma Spy_see_shrK:

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

lemma Spy_analz_shrK:

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

lemma Spy_see_shrK_D:

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

lemma NB_Crypt_imp_Alice_msg:

      [| Crypt (shrK A) (Nonce NB) ∈ parts (knows Spy evs); A ∉ bad; evs ∈ woolam |]
      ==> ∃B. Says A B (Crypt (shrK A) (Nonce NB)) ∈ set evs

lemma Server_trusts_WL4:

      [| Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|} ∈ set evs;
         A ∉ bad; evs ∈ woolam |]
      ==> ∃B. Says A B (Crypt (shrK A) (Nonce NB)) ∈ set evs

lemma Server_sent_WL5:

      [| Says Server B (Crypt (shrK B) {|Agent A, NB|}) ∈ set evs; evs ∈ woolam |]
      ==> ∃B'. Says B' Server {|Agent A, Agent B, Crypt (shrK A) NB|} ∈ set evs

lemma NB_Crypt_imp_Server_msg:

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

lemma B_trusts_WL5:

      [| Says S B (Crypt (shrK B) {|Agent A, Nonce NB|}) ∈ set evs; A ∉ bad; B ∉ bad;
         evs ∈ woolam |]
      ==> ∃B. Says A B (Crypt (shrK A) (Nonce NB)) ∈ set evs

lemma B_said_WL2:

      [| Says B A (Nonce NB) ∈ set evs; B ≠ Spy; evs ∈ woolam |]
      ==> ∃A'. Says A' B (Agent A) ∈ set evs