Theory WooLam

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

section‹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
›

inductive_set woolam :: "event list set"
  where
         (*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