diff -r c8bbf4c4bc2d -r a6816d47f41d src/HOL/Auth/WooLam.thy --- a/src/HOL/Auth/WooLam.thy Wed Apr 11 11:53:54 2001 +0200 +++ b/src/HOL/Auth/WooLam.thy Thu Apr 12 12:45:05 2001 +0200 @@ -14,52 +14,166 @@ Computer Security Foundations Workshop, 1996. *) -WooLam = Shared + +theory WooLam = Shared: -consts woolam :: event list set +consts woolam :: "event list set" inductive woolam - intrs + intros (*Initial trace is empty*) - Nil "[] \\ woolam" + 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" + 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" + 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" + 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" + 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" + 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; + WL5: "[| evs5 \ woolam; Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|} - \\ set evs5 |] + \ set evs5 |] ==> Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|}) - # evs5 \\ woolam" + # 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]) +apply 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)" +apply (erule woolam.induct, force, simp_all) +apply blast+ +done + +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" +apply (erule rev_mp, erule woolam.induct, force, simp_all) +apply blast+ +done + +(*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" +apply (erule rev_mp, erule woolam.induct, force, simp_all) +apply blast+ +done + +(*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" +apply (erule rev_mp, erule woolam.induct, force, simp_all) +apply blast+ +done + +(*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" +apply (erule rev_mp, erule woolam.induct, force, simp_all) +apply blast+ +done + + +(**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) +apply blast +apply auto +oops end