# HG changeset patch # User paulson # Date 849192964 -3600 # Node ID 1b1b46adc9b34a0808f058d2c92ecad9133d26a6 # Parent d1bcc10be8d7773b7dc2223841cf67da40d3418b Addition of Woo-Lam protocol diff -r d1bcc10be8d7 -r 1b1b46adc9b3 src/HOL/Auth/ROOT.ML --- a/src/HOL/Auth/ROOT.ML Thu Nov 28 12:47:48 1996 +0100 +++ b/src/HOL/Auth/ROOT.ML Thu Nov 28 15:56:04 1996 +0100 @@ -17,6 +17,7 @@ use_thy "OtwayRees"; use_thy "OtwayRees_AN"; use_thy "OtwayRees_Bad"; +use_thy "WooLam"; use_thy "Yahalom"; use_thy "Yahalom2"; diff -r d1bcc10be8d7 -r 1b1b46adc9b3 src/HOL/Auth/WooLam.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Auth/WooLam.ML Thu Nov 28 15:56:04 1996 +0100 @@ -0,0 +1,209 @@ +(* Title: HOL/Auth/WooLam + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1996 University of Cambridge + +Inductive relation "woolam" for the Woo-Lam protocol. + +Simplified version from page 11 of + Abadi and Needham. Prudent Engineering Practice for Cryptographic Protocols. + IEEE Trans. S.E. 22(1), 1996, pages 6-15. +*) + +open WooLam; + +proof_timing:=true; +HOL_quantifiers := false; +Pretty.setdepth 20; + + +(*Weak liveness: there are traces that reach the end*) +goal thy + "!!A B. [| A ~= B; A ~= Server; B ~= Server |] \ +\ ==> EX NB. EX evs: woolam lost. \ +\ Says Server B (Crypt {|Agent A, Nonce NB|} (shrK B)) \ +\ : set_of_list evs"; +by (REPEAT (resolve_tac [exI,bexI] 1)); +by (rtac (woolam.Nil RS woolam.WL1 RS woolam.WL2 RS woolam.WL3 RS + woolam.WL4 RS woolam.WL5) 2); +by (ALLGOALS (simp_tac (!simpset setsolver safe_solver))); +by (REPEAT_FIRST (resolve_tac [refl, conjI])); +by (REPEAT_FIRST (fast_tac (!claset addss (!simpset setsolver safe_solver)))); +result(); + + +(**** Inductive proofs about woolam ****) + +(*Nobody sends themselves messages*) +goal thy "!!evs. evs : woolam lost ==> ALL A X. Says A A X ~: set_of_list evs"; +by (etac woolam.induct 1); +by (Auto_tac()); +qed_spec_mp "not_Says_to_self"; +Addsimps [not_Says_to_self]; +AddSEs [not_Says_to_self RSN (2, rev_notE)]; + + +(** For reasoning about the encrypted portion of messages **) + +goal thy "!!evs. Says A' B X : set_of_list evs \ +\ ==> X : analz (sees lost Spy evs)"; +by (etac (Says_imp_sees_Spy RS analz.Inj) 1); +qed "WL4_analz_sees_Spy"; + +bind_thm ("WL4_parts_sees_Spy", + WL4_analz_sees_Spy RS (impOfSubs analz_subset_parts)); + +(*We instantiate the variable to "lost". Leaving it as a Var makes proofs + harder to complete, since simplification does less for us.*) +val parts_Fake_tac = forw_inst_tac [("lost","lost")] WL4_parts_sees_Spy 6; + +(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *) +fun parts_induct_tac i = SELECT_GOAL + (DETERM (etac woolam.induct 1 THEN parts_Fake_tac THEN + (*Fake message*) + TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts, + impOfSubs Fake_parts_insert] + addss (!simpset)) 2)) THEN + (*Base case*) + fast_tac (!claset addss (!simpset)) 1 THEN + ALLGOALS Asm_simp_tac) i; + +(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY + sends messages containing X! **) + +(*Spy never sees another agent's shared key! (unless it's lost at start)*) +goal thy + "!!evs. evs : woolam lost \ +\ ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)"; +by (parts_induct_tac 1); +by (Auto_tac()); +qed "Spy_see_shrK"; +Addsimps [Spy_see_shrK]; + +goal thy + "!!evs. evs : woolam lost \ +\ ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)"; +by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset)); +qed "Spy_analz_shrK"; +Addsimps [Spy_analz_shrK]; + +goal thy "!!A. [| Key (shrK A) : parts (sees lost Spy evs); \ +\ evs : woolam lost |] ==> A:lost"; +by (fast_tac (!claset addDs [Spy_see_shrK]) 1); +qed "Spy_see_shrK_D"; + +bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D); +AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D]; + + +(*** Future nonces can't be seen or used! ***) + +goal thy "!!evs. evs : woolam lost ==> \ +\ length evs <= length evt --> \ +\ Nonce (newN evt) ~: parts (sees lost Spy evs)"; +by (parts_induct_tac 1); +by (REPEAT_FIRST (fast_tac (!claset + addSEs partsEs + addSDs [Says_imp_sees_Spy RS parts.Inj] + addEs [leD RS notE] + addDs [impOfSubs analz_subset_parts, + impOfSubs parts_insert_subset_Un, + Suc_leD] + addss (!simpset)))); +qed_spec_mp "new_nonces_not_seen"; +Addsimps [new_nonces_not_seen]; + + +(**** Autheticity properties for Woo-Lam ****) + + +(*** WL4 ***) + +(*If the encrypted message appears then it originated with Alice*) +goal thy + "!!evs. [| A ~: lost; evs : woolam lost |] \ +\ ==> Crypt (Nonce NB) (shrK A) : parts (sees lost Spy evs) \ +\ --> (EX B. Says A B (Crypt (Nonce NB) (shrK A)) : set_of_list evs)"; +by (parts_induct_tac 1); +by (Fast_tac 1); +qed_spec_mp "NB_Crypt_imp_Alice_msg"; + +(*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.*) +goal thy + "!!evs. [| A ~: lost; evs : woolam lost; \ +\ Says B' Server {|Agent A, Agent B, Crypt (Nonce NB) (shrK A)|} \ +\ : set_of_list evs |] \ +\ ==> EX B. Says A B (Crypt (Nonce NB) (shrK A)) : set_of_list evs"; +by (fast_tac (!claset addSIs [NB_Crypt_imp_Alice_msg] + addSEs [MPair_parts] + addDs [Says_imp_sees_Spy RS parts.Inj]) 1); +qed "Server_trust_WL4"; + + +(*** WL5 ***) + +(*Server sent WL5 only if it received the right sort of message*) +goal thy + "!!evs. evs : woolam lost ==> \ +\ Says Server B (Crypt {|Agent A, NB|} (shrK B)) : set_of_list evs \ +\ --> (EX B'. Says B' Server {|Agent A, Agent B, Crypt NB (shrK A)|} \ +\ : set_of_list evs)"; +by (parts_induct_tac 1); +by (ALLGOALS Fast_tac); +bind_thm ("Server_sent_WL5", result() RSN (2, rev_mp)); + + +(*If the encrypted message appears then it originated with the Server!*) +goal thy + "!!evs. [| B ~: lost; evs : woolam lost |] \ +\ ==> Crypt {|Agent A, NB|} (shrK B) : parts (sees lost Spy evs) \ +\ --> Says Server B (Crypt {|Agent A, NB|} (shrK B)) : set_of_list evs"; +by (parts_induct_tac 1); +qed_spec_mp "NB_Crypt_imp_Server_msg"; + +(*Partial guarantee for B: if it gets a message of correct form then the Server + sent the same message.*) +goal thy + "!!evs. [| Says S B (Crypt {|Agent A, NB|} (shrK B)) : set_of_list evs; \ +\ B ~: lost; evs : woolam lost |] \ +\ ==> Says Server B (Crypt {|Agent A, NB|} (shrK B)) : set_of_list evs"; +by (fast_tac (!claset addSIs [NB_Crypt_imp_Server_msg] + addDs [Says_imp_sees_Spy RS parts.Inj]) 1); +qed "B_got_WL5"; + +(*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.*) +goal thy + "!!evs. [| Says S B (Crypt {|Agent A, Nonce NB|} (shrK B)): set_of_list evs; \ +\ A ~: lost; B ~: lost; evs : woolam lost |] \ +\ ==> EX B. Says A B (Crypt (Nonce NB) (shrK A)) : set_of_list evs"; +by (fast_tac (!claset addIs [Server_trust_WL4] + addSDs [B_got_WL5 RS Server_sent_WL5]) 1); +qed "B_trust_WL5"; + + +(*B only issues challenges in response to WL1. Useful??*) +goal thy + "!!evs. [| B ~= Spy; evs : woolam lost |] \ +\ ==> Says B A (Nonce NB) : set_of_list evs \ +\ --> (EX A'. Says A' B (Agent A) : set_of_list evs)"; +by (parts_induct_tac 1); +by (ALLGOALS Fast_tac); +bind_thm ("B_said_WL2", result() RSN (2, rev_mp)); + + +(**CANNOT be proved because A doesn't know where challenges come from... +goal thy + "!!evs. [| A ~: lost; B ~= Spy; evs : woolam lost |] \ +\ ==> Crypt (Nonce NB) (shrK A) : parts (sees lost Spy evs) & \ +\ Says B A (Nonce NB) : set_of_list evs \ +\ --> Says A B (Crypt (Nonce NB) (shrK A)) : set_of_list evs"; +by (parts_induct_tac 1); +by (Step_tac 1); +by (best_tac (!claset addSEs partsEs + addEs [new_nonces_not_seen RSN(2,rev_notE)]) 1); +**) diff -r d1bcc10be8d7 -r 1b1b46adc9b3 src/HOL/Auth/WooLam.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Auth/WooLam.thy Thu Nov 28 15:56:04 1996 +0100 @@ -0,0 +1,62 @@ +(* Title: HOL/Auth/WooLam + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1996 University of Cambridge + +Inductive relation "woolam" for the Woo-Lam protocol. + +Simplified version from page 11 of + Abadi and Needham. Prudent Engineering Practice for Cryptographic Protocols. + IEEE Trans. S.E. 22(1), 1996, pages 6-15. + +Note: this differs from the Woo-Lam protocol discussed by Lowe in his paper + Some New Attacks upon Security Protocols. + Computer Security Foundations Workshop, 1996. +*) + +WooLam = Shared + + +consts woolam :: "agent set => event list set" +inductive "woolam lost" + intrs + (*Initial trace is empty*) + Nil "[]: woolam lost" + + (*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 "[| evs: woolam lost; B ~= Spy; + X: synth (analz (sees lost Spy evs)) |] + ==> Says Spy B X # evs : woolam lost" + + (*Alice initiates a protocol run*) + WL1 "[| evs: woolam lost; A ~= B |] + ==> Says A B (Agent A) # evs : woolam lost" + + (*Bob responds to Alice's message with a challenge.*) + WL2 "[| evs: woolam lost; A ~= B; + Says A' B (Agent A) : set_of_list evs |] + ==> Says B A (Nonce (newN evs)) # evs : woolam lost" + + (*Alice responds to Bob's challenge by encrypting NB with her key. + B is *not* properly determined -- Alice essentially broadcasts + her reply.*) + WL3 "[| evs: woolam lost; A ~= B; + Says B' A (Nonce NB) : set_of_list evs; + Says A B (Agent A) : set_of_list evs |] + ==> Says A B (Crypt (Nonce NB) (shrK A)) # evs : woolam lost" + + (*Bob forwards Alice's response to the Server.*) + WL4 "[| evs: woolam lost; B ~= Server; + Says A' B X : set_of_list evs; + Says A'' B (Agent A) : set_of_list evs |] + ==> Says B Server {|Agent A, Agent B, X|} # evs : woolam lost" + + (*Server decrypts Alice's response for Bob.*) + WL5 "[| evs: woolam lost; B ~= Server; + Says B' Server {|Agent A, Agent B, Crypt (Nonce NB) (shrK A)|} + : set_of_list evs |] + ==> Says Server B (Crypt {|Agent A, Nonce NB|} (shrK B)) + # evs : woolam lost" + +end diff -r d1bcc10be8d7 -r 1b1b46adc9b3 src/HOL/Makefile --- a/src/HOL/Makefile Thu Nov 28 12:47:48 1996 +0100 +++ b/src/HOL/Makefile Thu Nov 28 15:56:04 1996 +0100 @@ -136,7 +136,7 @@ ##Authentication & Security Protocols Auth_NAMES = Message Shared NS_Shared OtwayRees OtwayRees_AN OtwayRees_Bad \ - Yahalom Yahalom2 + WooLam Yahalom Yahalom2 AUTH_FILES = Auth/ROOT.ML $(AUTH_NAMES:%=Auth/%.thy) $(AUTH_NAMES:%=Auth/%.ML)