Theory WooLam

theory WooLam
imports Public
(*  Title:      HOL/Auth/WooLam.thy
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
*}


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