(* Title: HOL/Auth/WooLam.thy Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1996 University of Cambridge
*)
section\<open>The Woo-Lam Protocol\<close>
theory WooLam imports Public begin
text\<open>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 \<close>
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))\ \<Longrightarrow> Says Spy B X # evsf \<in> 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\ \<Longrightarrow> Says B A (Nonce NB) # evs2 \<in> 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) \<in> set evs3;
Says B' A (Nonce NB) \ set evs3\ \<Longrightarrow> Says A B (Crypt (shrK A) (Nonce NB)) # evs3 \<in> 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) \<in> set evs4\<rbrakk> \<Longrightarrow> Says B Server \<lbrace>Agent A, Agent B, X\<rbrace> # evs4 \<in> woolam"
(*Server decrypts Alice's response for Bob.*)
| WL5: "\evs5 \ woolam;
Says B' Server \Agent A, Agent B, Crypt (shrK A) (Nonce NB)\ \<in> set evs5\<rbrakk> \<Longrightarrow> Says Server B (Crypt (shrK B) \<lbrace>Agent A, Nonce NB\<rbrace>)
# evs5 \<in> woolam"
(*A "possibility property": there are traces that reach the end*) lemma"\NB. \evs \ woolam.
Says Server B (Crypt (shrK B) \<lbrace>Agent A, Nonce NB\<rbrace>) \<in> 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 \<notin> 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 \<notin> bad; evs \<in> woolam\<rbrakk> \<Longrightarrow> \<exists>B. Says A B (Crypt (shrK A) (Nonce NB)) \<in> 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)\ \<in> set evs;
A \<notin> bad; evs \<in> woolam\<rbrakk> \<Longrightarrow> \<exists>B. Says A B (Crypt (shrK A) (Nonce NB)) \<in> 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 \<in> woolam\<rbrakk> \<Longrightarrow> \<exists>B'. Says B' Server \<lbrace>Agent A, Agent B, Crypt (shrK A) NB\<rbrace> \<in> 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 \<notin> bad; evs \<in> woolam\<rbrakk> \<Longrightarrow> Says Server B (Crypt (shrK B) \<lbrace>Agent A, NB\<rbrace>) \<in> 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 \<notin> bad; B \<notin> bad; evs \<in> woolam\<rbrakk> \<Longrightarrow> \<exists>B. Says A B (Crypt (shrK A) (Nonce NB)) \<in> 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\ \<Longrightarrow> \<exists>A'. Says A' B (Agent A) \<in> 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\ \<Longrightarrow> Crypt (shrK A) (Nonce NB) \<in> parts (spies evs) \<and>
Says B A (Nonce NB) \<in> set evs \<longrightarrow> Says A B (Crypt (shrK A) (Nonce NB)) \<in> set evs" apply (erule rev_mp, erule woolam.induct, force, simp_all, blast, auto) oops
end
¤ Dauer der Verarbeitung: 0.13 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
