# HG changeset patch # User paulson # Date 920973699 -3600 # Node ID 76f3865a2b1d3c674aafe22e3afb8c62ebcddc7f # Parent fdf236c98914cfbcd768f27129c676bf2d4cf702 Added Bella's "Gets" model for Otway_Rees. Also affects some other theories. Changing "spies" to "knows Spy", etc. Retaining the constant "spies" as a translation. diff -r fdf236c98914 -r 76f3865a2b1d src/HOL/Auth/Event.ML --- a/src/HOL/Auth/Event.ML Mon Mar 08 13:49:53 1999 +0100 +++ b/src/HOL/Auth/Event.ML Tue Mar 09 11:01:39 1999 +0100 @@ -2,90 +2,170 @@ ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1996 University of Cambridge - -Theory of events for security protocols - -Datatype of events; function "sees"; freshness *) AddIffs [Spy_in_bad, Server_not_bad]; -(**** Function "spies" ****) +Addsimps [knows_Cons, used_Cons]; + +(**** Function "knows" ****) -(** Simplifying parts (insert X (spies evs)) - = parts {X} Un parts (spies evs) -- since general case loops*) +(** Simplifying parts (insert X (knows Spy evs)) + = parts {X} Un parts (knows Spy evs) -- since general case loops*) -bind_thm ("parts_insert_spies", +bind_thm ("parts_insert_knows_Spy", parts_insert |> - read_instantiate_sg (sign_of thy) [("H", "spies evs")]); + read_instantiate_sg (sign_of thy) [("H", "knows Spy evs")]); -Goal "P(event_case sf nf ev) = \ +Goal "P(event_case sf nf gf ev) = \ \ ((ALL A B X. ev = Says A B X --> P(sf A B X)) & \ -\ (ALL A X. ev = Notes A X --> P(nf A X)))"; +\ (ALL A X. ev = Notes A X --> P(nf A X)) & \ +\ (ALL A X. ev = Gets A X --> P(gf A X)))"; by (induct_tac "ev" 1); by Auto_tac; qed "expand_event_case"; -Goal "spies (Says A B X # evs) = insert X (spies evs)"; +Goal "knows Spy (Says A B X # evs) = insert X (knows Spy evs)"; by (Simp_tac 1); -qed "spies_Says"; +qed "knows_Spy_Says"; (*The point of letting the Spy see "bad" agents' notes is to prevent redundant case-splits on whether A=Spy and whether A:bad*) -Goal "spies (Notes A X # evs) = \ -\ (if A:bad then insert X (spies evs) else spies evs)"; +Goal "knows Spy (Notes A X # evs) = \ +\ (if A:bad then insert X (knows Spy evs) else knows Spy evs)"; by (Simp_tac 1); -qed "spies_Notes"; +qed "knows_Spy_Notes"; -Goal "spies evs <= spies (Says A B X # evs)"; +Goal "knows Spy (Gets A X # evs) = knows Spy evs"; +by (Simp_tac 1); +qed "knows_Spy_Gets"; + +Goal "knows Spy evs <= knows Spy (Says A B X # evs)"; by (simp_tac (simpset() addsimps [subset_insertI]) 1); -qed "spies_subset_spies_Says"; +qed "knows_Spy_subset_knows_Spy_Says"; -Goal "spies evs <= spies (Notes A X # evs)"; +Goal "knows Spy evs <= knows Spy (Notes A X # evs)"; by (Simp_tac 1); by (Fast_tac 1); -qed "spies_subset_spies_Notes"; +qed "knows_Spy_subset_knows_Spy_Notes"; -(*Spy sees all traffic*) -Goal "Says A B X : set evs --> X : spies evs"; +Goal "knows Spy evs <= knows Spy (Gets A X # evs)"; +by (simp_tac (simpset() addsimps [subset_insertI]) 1); +qed "knows_Spy_subset_knows_Spy_Gets"; + +(*Spy sees what is sent on the traffic*) +Goal "Says A B X : set evs --> X : knows Spy evs"; by (induct_tac "evs" 1); by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case]))); -qed_spec_mp "Says_imp_spies"; +qed_spec_mp "Says_imp_knows_Spy"; -(*Spy sees Notes of bad agents*) -Goal "Notes A X : set evs --> A: bad --> X : spies evs"; +Goal "Notes A X : set evs --> A: bad --> X : knows Spy evs"; by (induct_tac "evs" 1); by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case]))); -qed_spec_mp "Notes_imp_spies"; +qed_spec_mp "Notes_imp_knows_Spy"; + (*Use with addSEs to derive contradictions from old Says events containing items known to be fresh*) -val spies_partsEs = make_elim (Says_imp_spies RS parts.Inj) :: partsEs; +val knows_Spy_partsEs = make_elim (Says_imp_knows_Spy RS parts.Inj) :: partsEs; + +Addsimps [knows_Spy_Says, knows_Spy_Notes, knows_Spy_Gets]; + + +(*Begin lemmas about agents' knowledge*) + +Goal "knows A (Says A B X # evs) = insert X (knows A evs)"; +by (Simp_tac 1); +qed "knows_Says"; + +Goal "knows A (Notes A X # evs) = insert X (knows A evs)"; +by (Simp_tac 1); +qed "knows_Notes"; + +Goal "A ~= Spy --> knows A (Gets A X # evs) = insert X (knows A evs)"; +by (Simp_tac 1); +qed "knows_Gets"; + + +Goal "knows A evs <= knows A (Says A B X # evs)"; +by (simp_tac (simpset() addsimps [subset_insertI]) 1); +qed "knows_subset_knows_Says"; + +Goal "knows A evs <= knows A (Notes A X # evs)"; +by (simp_tac (simpset() addsimps [subset_insertI]) 1); +qed "knows_subset_knows_Notes"; + +Goal "knows A evs <= knows A (Gets A X # evs)"; +by (simp_tac (simpset() addsimps [subset_insertI]) 1); +qed "knows_subset_knows_Gets"; -Addsimps [spies_Says, spies_Notes]; +(*Agents know what they say*) +Goal "Says A B X : set evs --> X : knows A evs"; +by (induct_tac "evs" 1); +by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case]))); +by (Blast_tac 1); +qed_spec_mp "Says_imp_knows"; + +(*Agents know what they note*) +Goal "Notes A X : set evs --> X : knows A evs"; +by (induct_tac "evs" 1); +by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case]))); +by (Blast_tac 1); +qed_spec_mp "Notes_imp_knows"; + +(*Agents know what they receive*) +Goal "A ~= Spy --> Gets A X : set evs --> X : knows A evs"; +by (induct_tac "evs" 1); +by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case]))); +qed_spec_mp "Gets_imp_knows_agents"; + + +(*What agents DIFFERENT FROM Spy know + was either said, or noted, or got, or known initially*) +Goal "[| X : knows A evs; A ~= Spy |] ==> EX B. \ +\ Says A B X : set evs | Gets A X : set evs | Notes A X : set evs | X : initState A"; +by (etac rev_mp 1); +by (induct_tac "evs" 1); +by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case]))); +by (Blast_tac 1); +qed_spec_mp "knows_imp_Says_Gets_Notes_initState"; + +(*What the Spy knows -- for the time being -- + was either said or noted, or known initially*) +Goal "[| X : knows Spy evs |] ==> EX A B. \ +\ Says A B X : set evs | Notes A X : set evs | X : initState Spy"; +by (etac rev_mp 1); +by (induct_tac "evs" 1); +by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case]))); +by (Blast_tac 1); +qed_spec_mp "knows_Spy_imp_Says_Notes_initState"; + +(*END lemmas about agents' knowledge*) + + (**** NOTE REMOVAL--laws above are cleaner, as they don't involve "case" ****) -Delsimps [spies_Cons]; +Delsimps [knows_Cons]; (*** Fresh nonces ***) -Goal "parts (spies evs) <= used evs"; +Goal "parts (knows Spy evs) <= used evs"; by (induct_tac "evs" 1); by (ALLGOALS (asm_simp_tac - (simpset() addsimps [parts_insert_spies] + (simpset() addsimps [parts_insert_knows_Spy] addsplits [expand_event_case]))); by (ALLGOALS Blast_tac); -qed "parts_spies_subset_used"; +qed "parts_knows_Spy_subset_used"; -bind_thm ("usedI", impOfSubs parts_spies_subset_used); +bind_thm ("usedI", impOfSubs parts_knows_Spy_subset_used); AddIs [usedI]; Goal "parts (initState B) <= used evs"; by (induct_tac "evs" 1); by (ALLGOALS (asm_simp_tac - (simpset() addsimps [parts_insert_spies] + (simpset() addsimps [parts_insert_knows_Spy] addsplits [expand_event_case]))); by (ALLGOALS Blast_tac); bind_thm ("initState_into_used", impOfSubs (result())); @@ -100,6 +180,11 @@ qed "used_Notes"; Addsimps [used_Notes]; +Goal "used (Gets A X # evs) = used evs"; +by (Simp_tac 1); +qed "used_Gets"; +Addsimps [used_Gets]; + Goal "used [] <= used evs"; by (Simp_tac 1); by (blast_tac (claset() addIs [initState_into_used]) 1); @@ -109,29 +194,34 @@ Delsimps [used_Nil, used_Cons]; -(*currently unused*) -Goal "used evs <= used (evs@evs')"; -by (induct_tac "evs" 1); -by (simp_tac (simpset() addsimps [used_nil_subset]) 1); -by (induct_tac "a" 1); -by (ALLGOALS Asm_simp_tac); -by (ALLGOALS Blast_tac); -qed "used_subset_append"; - - -(*For proving theorems of the form X ~: analz (spies evs) --> P +(*For proving theorems of the form X ~: analz (knows Spy evs) --> P New events added by induction to "evs" are discarded. Provided this information isn't needed, the proof will be much shorter, since it will omit complicated reasoning about analz.*) val analz_mono_contra_tac = let val analz_impI = read_instantiate_sg (sign_of thy) - [("P", "?Y ~: analz (spies ?evs)")] impI; + [("P", "?Y ~: analz (knows Spy ?evs)")] impI; in rtac analz_impI THEN' REPEAT1 o (dresolve_tac - [spies_subset_spies_Says RS analz_mono RS contra_subsetD, - spies_subset_spies_Notes RS analz_mono RS contra_subsetD]) + [knows_Spy_subset_knows_Spy_Says RS analz_mono RS contra_subsetD, + knows_Spy_subset_knows_Spy_Notes RS analz_mono RS contra_subsetD, + knows_Spy_subset_knows_Spy_Gets RS analz_mono RS contra_subsetD]) THEN' mp_tac end; + +fun Reception_tac i = + blast_tac (claset() addDs [Says_imp_knows_Spy RS parts.Inj, + impOfSubs (parts_insert RS equalityD1), + parts_trans, + Says_imp_knows_Spy RS analz.Inj, + impOfSubs analz_mono, analz_cut] + addIs [less_SucI]) i; + + +(*Compatibility for the old "spies" function*) +val spies_partsEs = knows_Spy_partsEs; +val Says_imp_spies = Says_imp_knows_Spy; +val parts_insert_spies = parts_insert_knows_Spy; diff -r fdf236c98914 -r 76f3865a2b1d src/HOL/Auth/Event.thy --- a/src/HOL/Auth/Event.thy Mon Mar 08 13:49:53 1999 +0100 +++ b/src/HOL/Auth/Event.thy Tue Mar 09 11:01:39 1999 +0100 @@ -19,24 +19,49 @@ datatype (*Messages--could add another constructor for agent knowledge*) event = Says agent agent msg | Notes agent msg + | Gets agent msg + +consts + bad :: agent set (*compromised agents*) + knows :: agent => event list => msg set -consts - bad :: agent set (*compromised agents*) + +(*"spies" is retained for compability's sake*) +syntax spies :: event list => msg set +translations + "spies" => "knows Spy" + + rules (*Spy has access to his own key for spoof messages, but Server is secure*) Spy_in_bad "Spy: bad" Server_not_bad "Server ~: bad" primrec - (*Spy reads all traffic whether addressed to him or not*) - spies_Nil "spies [] = initState Spy" - spies_Cons "spies (ev # evs) = - (case ev of - Says A B X => insert X (spies evs) - | Notes A X => - if A:bad then insert X (spies evs) else spies evs)" + knows_Nil "knows A [] = initState A" + knows_Cons "knows A (ev # evs) = + (if A = Spy then + (case ev of + Says A' B X => insert X (knows Spy evs) + | Notes A' X => + if A' : bad then insert X (knows Spy evs) else knows Spy evs + | Gets A' X => knows Spy evs) + else + (case ev of + Says A' B X => + if A'=A then insert X (knows A evs) else knows A evs + | Notes A' X => + if A'=A then insert X (knows A evs) else knows A evs + | Gets A' X => + if A'=A then insert X (knows A evs) else knows A evs))" + +(* + Case A=Spy on the Gets event + enforces the fact that if a message is received then it must have been sent, + therefore the oops case must use Notes +*) consts (*Set of items that might be visible to somebody: @@ -48,6 +73,9 @@ used_Cons "used (ev # evs) = (case ev of Says A B X => parts {X} Un (used evs) - | Notes A X => parts {X} Un (used evs))" + | Notes A X => parts {X} Un (used evs) + | Gets A X => used evs)" + + end diff -r fdf236c98914 -r 76f3865a2b1d src/HOL/Auth/OtwayRees.ML --- a/src/HOL/Auth/OtwayRees.ML Mon Mar 08 13:49:53 1999 +0100 +++ b/src/HOL/Auth/OtwayRees.ML Tue Mar 09 11:01:39 1999 +0100 @@ -12,68 +12,81 @@ Proc. Royal Soc. 426 (1989) *) -AddEs spies_partsEs; +AddEs knows_Spy_partsEs; AddDs [impOfSubs analz_subset_parts]; AddDs [impOfSubs Fake_parts_insert]; (*A "possibility property": there are traces that reach the end*) Goal "[| B ~= Server |] \ -\ ==> EX K. EX NA. EX evs: otway. \ +\ ==> EX NA K. EX evs: otway. \ \ Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \ \ : set evs"; by (REPEAT (resolve_tac [exI,bexI] 1)); -by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2); +by (rtac (otway.Nil RS + otway.OR1 RS otway.Reception RS + otway.OR2 RS otway.Reception RS + otway.OR3 RS otway.Reception RS otway.OR4) 2); by possibility_tac; result(); +Goal "[| Gets B X : set evs; evs : otway |] ==> EX A. Says A B X : set evs"; +by (etac rev_mp 1); +by (etac otway.induct 1); +by Auto_tac; +qed"Gets_imp_Says"; + +(*Must be proved separately for each protocol*) +Goal "[| Gets B X : set evs; evs : otway |] ==> X : knows Spy evs"; +by (blast_tac (claset() addSDs [Gets_imp_Says, Says_imp_knows_Spy]) 1); +qed"Gets_imp_knows_Spy"; +AddDs [Gets_imp_knows_Spy RS parts.Inj]; + (**** Inductive proofs about otway ****) (** For reasoning about the encrypted portion of messages **) -Goal "Says A' B {|N, Agent A, Agent B, X|} : set evs \ -\ ==> X : analz (spies evs)"; -by (dtac (Says_imp_spies RS analz.Inj) 1); -by (Blast_tac 1); -qed "OR2_analz_spies"; +Goal "[| Gets B {|N, Agent A, Agent B, X|} : set evs; evs : otway |] \ +\ ==> X : analz (knows Spy evs)"; +by (blast_tac (claset() addSDs [Gets_imp_knows_Spy RS analz.Inj]) 1); +qed "OR2_analz_knows_Spy"; -Goal "Says S' B {|N, X, Crypt (shrK B) X'|} : set evs \ -\ ==> X : analz (spies evs)"; -by (dtac (Says_imp_spies RS analz.Inj) 1); -by (Blast_tac 1); -qed "OR4_analz_spies"; +Goal "[| Gets B {|N, X, Crypt (shrK B) X'|} : set evs; evs : otway |] \ +\ ==> X : analz (knows Spy evs)"; +by (blast_tac (claset() addSDs [Gets_imp_knows_Spy RS analz.Inj]) 1); +qed "OR4_analz_knows_Spy"; Goal "Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \ -\ ==> K : parts (spies evs)"; +\ ==> K : parts (knows Spy evs)"; by (Blast_tac 1); -qed "Oops_parts_spies"; +qed "Oops_parts_knows_Spy"; -bind_thm ("OR2_parts_spies", - OR2_analz_spies RS (impOfSubs analz_subset_parts)); -bind_thm ("OR4_parts_spies", - OR4_analz_spies RS (impOfSubs analz_subset_parts)); +bind_thm ("OR2_parts_knows_Spy", + OR2_analz_knows_Spy RS (impOfSubs analz_subset_parts)); +bind_thm ("OR4_parts_knows_Spy", + OR4_analz_knows_Spy RS (impOfSubs analz_subset_parts)); -(*For proving the easier theorems about X ~: parts (spies evs).*) +(*For proving the easier theorems about X ~: parts (knows Spy evs).*) fun parts_induct_tac i = etac otway.induct i THEN - forward_tac [Oops_parts_spies] (i+6) THEN - forward_tac [OR4_parts_spies] (i+5) THEN - forward_tac [OR2_parts_spies] (i+3) THEN + forward_tac [Oops_parts_knows_Spy] (i+7) THEN + forward_tac [OR4_parts_knows_Spy] (i+6) THEN + forward_tac [OR2_parts_knows_Spy] (i+4) THEN prove_simple_subgoals_tac i; -(** Theorems of the form X ~: parts (spies evs) imply that NOBODY +(** Theorems of the form X ~: parts (knows Spy evs) imply that NOBODY sends messages containing X! **) (*Spy never sees a good agent's shared key!*) -Goal "evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)"; +Goal "evs : otway ==> (Key (shrK A) : parts (knows Spy evs)) = (A : bad)"; by (parts_induct_tac 1); by (ALLGOALS Blast_tac); qed "Spy_see_shrK"; Addsimps [Spy_see_shrK]; -Goal "evs : otway ==> (Key (shrK A) : analz (spies evs)) = (A : bad)"; +Goal "evs : otway ==> (Key (shrK A) : analz (knows Spy evs)) = (A : bad)"; by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset())); qed "Spy_analz_shrK"; Addsimps [Spy_analz_shrK]; @@ -83,7 +96,7 @@ (*Nobody can have used non-existent keys!*) -Goal "evs : otway ==> Key K ~: used evs --> K ~: keysFor (parts (spies evs))"; +Goal "evs : otway ==> Key K ~: used evs --> K ~: keysFor (parts (knows Spy evs))"; by (parts_induct_tac 1); (*Fake*) by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1); @@ -114,18 +127,18 @@ (*For proofs involving analz.*) -val analz_spies_tac = - dtac OR2_analz_spies 4 THEN - dtac OR4_analz_spies 6 THEN - forward_tac [Says_Server_message_form] 7 THEN assume_tac 7 THEN - REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7); +val analz_knows_Spy_tac = + dtac OR2_analz_knows_Spy 5 THEN assume_tac 5 THEN + dtac OR4_analz_knows_Spy 7 THEN assume_tac 7 THEN + forward_tac [Says_Server_message_form] 8 THEN assume_tac 8 THEN + REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 8); (**** The following is to prove theorems of the form - Key K : analz (insert (Key KAB) (spies evs)) ==> - Key K : analz (spies evs) + Key K : analz (insert (Key KAB) (knows Spy evs)) ==> + Key K : analz (knows Spy evs) A more general formula must be proved inductively. ****) @@ -135,10 +148,10 @@ (*The equality makes the induction hypothesis easier to apply*) Goal "evs : otway ==> ALL K KK. KK <= - (range shrK) --> \ -\ (Key K : analz (Key``KK Un (spies evs))) = \ -\ (K : KK | Key K : analz (spies evs))"; +\ (Key K : analz (Key``KK Un (knows Spy evs))) = \ +\ (K : KK | Key K : analz (knows Spy evs))"; by (etac otway.induct 1); -by analz_spies_tac; +by analz_knows_Spy_tac; by (REPEAT_FIRST (resolve_tac [allI, impI])); by (REPEAT_FIRST (rtac analz_image_freshK_lemma)); by (ALLGOALS (asm_simp_tac analz_image_freshK_ss)); @@ -148,8 +161,8 @@ Goal "[| evs : otway; KAB ~: range shrK |] \ -\ ==> Key K : analz (insert (Key KAB) (spies evs)) = \ -\ (K = KAB | Key K : analz (spies evs))"; +\ ==> Key K : analz (insert (Key KAB) (knows Spy evs)) = \ +\ (K = KAB | Key K : analz (knows Spy evs))"; by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1); qed "analz_insert_freshK"; @@ -169,7 +182,7 @@ by (expand_case_tac "K = ?y" 1); by (REPEAT (ares_tac [refl,exI,impI,conjI] 2)); (*...we assume X is a recent message, and handle this case by contradiction*) -by (blast_tac (claset() addSEs spies_partsEs) 1); +by (blast_tac (claset() addSEs knows_Spy_partsEs) 1); val lemma = result(); Goal "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set evs; \ @@ -179,12 +192,11 @@ qed "unique_session_keys"; - (**** Authenticity properties relating to NA ****) (*Only OR1 can have caused such a part of a message to appear.*) Goal "[| A ~: bad; evs : otway |] \ -\ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) --> \ +\ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (knows Spy evs) --> \ \ Says A B {|NA, Agent A, Agent B, \ \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \ \ : set evs"; @@ -192,12 +204,21 @@ by (Blast_tac 1); qed_spec_mp "Crypt_imp_OR1"; +Goal "[| Gets B {|NA, Agent A, Agent B, \ +\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \ +\ A ~: bad; evs : otway |] \ +\ ==> Says A B {|NA, Agent A, Agent B, \ +\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \ +\ : set evs"; +by (blast_tac (claset() addDs [Crypt_imp_OR1]) 1); +qed"Crypt_imp_OR1_Gets"; + (** The Nonce NA uniquely identifies A's message. **) Goal "[| evs : otway; A ~: bad |] \ \ ==> EX B'. ALL B. \ -\ Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) \ +\ Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (knows Spy evs) \ \ --> B = B'"; by (parts_induct_tac 1); by (Blast_tac 1); @@ -207,8 +228,8 @@ by (Blast_tac 1); val lemma = result(); -Goal "[| Crypt (shrK A) {|NA, Agent A, Agent B|}: parts (spies evs); \ -\ Crypt (shrK A) {|NA, Agent A, Agent C|}: parts (spies evs); \ +Goal "[| Crypt (shrK A) {|NA, Agent A, Agent B|}: parts (knows Spy evs); \ +\ Crypt (shrK A) {|NA, Agent A, Agent C|}: parts (knows Spy evs); \ \ evs : otway; A ~: bad |] \ \ ==> B = C"; by (prove_unique_tac lemma 1); @@ -219,19 +240,19 @@ OR2 encrypts Nonce NB. It prevents the attack that can occur in the over-simplified version of this protocol: see OtwayRees_Bad.*) Goal "[| A ~: bad; evs : otway |] \ -\ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) --> \ +\ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (knows Spy evs) --> \ \ Crypt (shrK A) {|NA', NA, Agent A', Agent A|} \ -\ ~: parts (spies evs)"; +\ ~: parts (knows Spy evs)"; by (parts_induct_tac 1); -by (ALLGOALS Blast_tac); -qed_spec_mp"no_nonce_OR1_OR2"; +by Auto_tac; +qed_spec_mp "no_nonce_OR1_OR2"; val nonce_OR1_OR2_E = no_nonce_OR1_OR2 RSN (2, rev_notE); (*Crucial property: If the encrypted message appears, and A has used NA to start a run, then it originated with the Server!*) Goal "[| A ~: bad; evs : otway |] \ -\ ==> Crypt (shrK A) {|NA, Key K|} : parts (spies evs) \ +\ ==> Crypt (shrK A) {|NA, Key K|} : parts (knows Spy evs) \ \ --> Says A B {|NA, Agent A, Agent B, \ \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \ \ : set evs --> \ @@ -253,7 +274,7 @@ (*OR3, two cases*) (** LEVEL 7 **) by (blast_tac (claset() addSEs [nonce_OR1_OR2_E] delrules [conjI] (*stop split-up into 4 subgoals*)) 2); -by (blast_tac (claset() addIs [unique_NA]) 1); +by (blast_tac (claset() addIs [unique_NA]) 1); qed_spec_mp "NA_Crypt_imp_Server_msg"; @@ -263,7 +284,7 @@ Spy_not_see_encrypted_key*) Goal "[| Says A B {|NA, Agent A, Agent B, \ \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \ -\ Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \ +\ Gets A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \ \ A ~: bad; evs : otway |] \ \ ==> EX NB. Says Server B \ \ {|NA, \ @@ -283,9 +304,9 @@ \ {|NA, Crypt (shrK A) {|NA, Key K|}, \ \ Crypt (shrK B) {|NB, Key K|}|} : set evs --> \ \ Notes Spy {|NA, NB, Key K|} ~: set evs --> \ -\ Key K ~: analz (spies evs)"; +\ Key K ~: analz (knows Spy evs)"; by (etac otway.induct 1); -by analz_spies_tac; +by analz_knows_Spy_tac; by (ALLGOALS (asm_simp_tac (simpset() addcongs [conj_cong] addsimps [analz_insert_eq, analz_insert_freshK] @@ -305,7 +326,7 @@ \ Crypt (shrK B) {|NB, Key K|}|} : set evs; \ \ Notes Spy {|NA, NB, Key K|} ~: set evs; \ \ A ~: bad; B ~: bad; evs : otway |] \ -\ ==> Key K ~: analz (spies evs)"; +\ ==> Key K ~: analz (knows Spy evs)"; by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); by (blast_tac (claset() addSEs [lemma]) 1); qed "Spy_not_see_encrypted_key"; @@ -315,10 +336,10 @@ what it is.*) Goal "[| Says A B {|NA, Agent A, Agent B, \ \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \ -\ Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \ +\ Gets A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \ \ ALL NB. Notes Spy {|NA, NB, Key K|} ~: set evs; \ \ A ~: bad; B ~: bad; evs : otway |] \ -\ ==> Key K ~: analz (spies evs)"; +\ ==> Key K ~: analz (knows Spy evs)"; by (blast_tac (claset() addSDs [A_trusts_OR4, Spy_not_see_encrypted_key]) 1); qed "A_gets_good_key"; @@ -329,7 +350,7 @@ know anything about X: it does NOT have to have the right form.*) Goal "[| B ~: bad; evs : otway |] \ \ ==> Crypt (shrK B) {|NA, NB, Agent A, Agent B|} \ -\ : parts (spies evs) --> \ +\ : parts (knows Spy evs) --> \ \ (EX X. Says B Server \ \ {|NA, Agent A, Agent B, X, \ \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|} \ @@ -343,7 +364,7 @@ Goal "[| evs : otway; B ~: bad |] \ \ ==> EX NA' A'. ALL NA A. \ -\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(spies evs) \ +\ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(knows Spy evs) \ \ --> NA = NA' & A = A'"; by (parts_induct_tac 1); by (Blast_tac 1); @@ -353,18 +374,17 @@ by (Blast_tac 1); val lemma = result(); -Goal "[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(spies evs); \ -\ Crypt (shrK B) {|NC, NB, Agent C, Agent B|} : parts(spies evs); \ +Goal "[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(knows Spy evs); \ +\ Crypt (shrK B) {|NC, NB, Agent C, Agent B|} : parts(knows Spy evs); \ \ evs : otway; B ~: bad |] \ \ ==> NC = NA & C = A"; by (prove_unique_tac lemma 1); qed "unique_NB"; - (*If the encrypted message appears, and B has used Nonce NB, then it originated with the Server!*) Goal "[| B ~: bad; evs : otway |] \ -\ ==> Crypt (shrK B) {|NB, Key K|} : parts (spies evs) \ +\ ==> Crypt (shrK B) {|NB, Key K|} : parts (knows Spy evs) \ \ --> (ALL X'. Says B Server \ \ {|NA, Agent A, Agent B, X', \ \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|} \ @@ -385,7 +405,8 @@ *) by (safe_tac (claset() delrules [disjCI, impCE])); by (Blast_tac 3); -by (blast_tac (claset() addDs [unique_NB]) 2); +by (blast_tac (claset() addSDs [unique_NB] + delrules [impCE] (*stop split-up*)) 2); by (blast_tac (claset() addSEs [nonce_OR1_OR2_E] delrules [conjI] (*stop split-up*)) 1); qed_spec_mp "NB_Crypt_imp_Server_msg"; @@ -396,7 +417,7 @@ Goal "[| Says B Server {|NA, Agent A, Agent B, X', \ \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \ \ : set evs; \ -\ Says S' B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \ +\ Gets B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \ \ B ~: bad; evs : otway |] \ \ ==> Says Server B \ \ {|NA, \ @@ -411,10 +432,10 @@ Goal "[| Says B Server {|NA, Agent A, Agent B, X', \ \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \ \ : set evs; \ -\ Says S' B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \ +\ Gets B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \ \ Notes Spy {|NA, NB, Key K|} ~: set evs; \ \ A ~: bad; B ~: bad; evs : otway |] \ -\ ==> Key K ~: analz (spies evs)"; +\ ==> Key K ~: analz (knows Spy evs)"; by (blast_tac (claset() addSDs [B_trusts_OR3, Spy_not_see_encrypted_key]) 1); qed "B_gets_good_key"; @@ -436,7 +457,7 @@ (*After getting and checking OR4, agent A can trust that B has been active. We could probably prove that X has the expected form, but that is not strictly necessary for authentication.*) -Goal "[| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \ +Goal "[| Gets A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \ \ Says A B {|NA, Agent A, Agent B, \ \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \ \ A ~: bad; B ~: bad; evs : otway |] \ diff -r fdf236c98914 -r 76f3865a2b1d src/HOL/Auth/OtwayRees.thy --- a/src/HOL/Auth/OtwayRees.thy Mon Mar 08 13:49:53 1999 +0100 +++ b/src/HOL/Auth/OtwayRees.thy Tue Mar 09 11:01:39 1999 +0100 @@ -1,19 +1,14 @@ -(* Title: HOL/Auth/OtwayRees - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1996 University of Cambridge - -Inductive relation "otway" for the Otway-Rees protocol. +(* +Inductive relation "otway" for the Otway-Rees protocol +extended by Gets primitive. Version that encrypts Nonce NB -From page 244 of - Burrows, Abadi and Needham. A Logic of Authentication. - Proc. Royal Soc. 426 (1989) *) OtwayRees = Shared + + consts otway :: event list set inductive "otway" intrs @@ -25,8 +20,13 @@ (*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: otway; X: synth (analz (spies evs)) |] - ==> Says Spy B X # evs : otway" + Fake "[| evsa: otway; X: synth (analz (knows Spy evsa)) |] + ==> Says Spy B X # evsa : otway" + + (*A message that has been sent can be received by the + intended recipient.*) + Reception "[| evsr: otway; Says A B X : set evsr |] + ==> Gets B X # evsr : otway" (*Alice initiates a protocol run*) OR1 "[| evs1: otway; Nonce NA ~: used evs1 |] @@ -38,7 +38,7 @@ the sender is, hence the A' in the sender field. Note that NB is encrypted.*) OR2 "[| evs2: otway; Nonce NB ~: used evs2; - Says A' B {|Nonce NA, Agent A, Agent B, X|} : set evs2 |] + Gets B {|Nonce NA, Agent A, Agent B, X|} : set evs2 |] ==> Says B Server {|Nonce NA, Agent A, Agent B, X, Crypt (shrK B) @@ -49,7 +49,7 @@ match. Then he sends a new session key to Bob with a packet for forwarding to Alice.*) OR3 "[| evs3: otway; Key KAB ~: used evs3; - Says B' Server + Gets Server {|Nonce NA, Agent A, Agent B, Crypt (shrK A) {|Nonce NA, Agent A, Agent B|}, Crypt (shrK B) {|Nonce NA, Nonce NB, Agent A, Agent B|}|} @@ -68,7 +68,7 @@ Crypt (shrK B) {|Nonce NA, Nonce NB, Agent A, Agent B|}|} : set evs4; - Says S' B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|} + Gets B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|} : set evs4 |] ==> Says B A {|Nonce NA, X|} # evs4 : otway" diff -r fdf236c98914 -r 76f3865a2b1d src/HOL/Auth/OtwayRees_AN.ML --- a/src/HOL/Auth/OtwayRees_AN.ML Mon Mar 08 13:49:53 1999 +0100 +++ b/src/HOL/Auth/OtwayRees_AN.ML Tue Mar 09 11:01:39 1999 +0100 @@ -12,7 +12,7 @@ IEEE Trans. SE 22 (1), 1996 *) -AddEs spies_partsEs; +AddEs knows_Spy_partsEs; AddDs [impOfSubs analz_subset_parts]; AddDs [impOfSubs Fake_parts_insert]; @@ -23,48 +23,62 @@ \ Says B A (Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}) \ \ : set evs"; by (REPEAT (resolve_tac [exI,bexI] 1)); -by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2); +by (rtac (otway.Nil RS + otway.OR1 RS otway.Reception RS + otway.OR2 RS otway.Reception RS + otway.OR3 RS otway.Reception RS otway.OR4) 2); by possibility_tac; result(); +Goal "[| Gets B X : set evs; evs : otway |] ==> EX A. Says A B X : set evs"; +by (etac rev_mp 1); +by (etac otway.induct 1); +by Auto_tac; +qed"Gets_imp_Says"; + +(*Must be proved separately for each protocol*) +Goal "[| Gets B X : set evs; evs : otway |] ==> X : knows Spy evs"; +by (blast_tac (claset() addSDs [Gets_imp_Says, Says_imp_knows_Spy]) 1); +qed"Gets_imp_knows_Spy"; +AddDs [Gets_imp_knows_Spy RS parts.Inj]; + (**** Inductive proofs about otway ****) (** For reasoning about the encrypted portion of messages **) -Goal "Says S' B {|X, Crypt(shrK B) X'|} : set evs ==> \ -\ X : analz (spies evs)"; -by (dtac (Says_imp_spies RS analz.Inj) 1); -by (Blast_tac 1); -qed "OR4_analz_spies"; +Goal "[| Gets B {|X, Crypt(shrK B) X'|} : set evs; evs : otway |] ==> \ +\ X : analz (knows Spy evs)"; +by (blast_tac (claset() addSDs [Gets_imp_knows_Spy RS analz.Inj]) 1); +qed "OR4_analz_knows_Spy"; -Goal "Says Server B {|X, Crypt K' {|NB, a, Agent B, K|}|} \ -\ : set evs ==> K : parts (spies evs)"; +Goal "Says Server B {|X, Crypt K' {|NB, a, Agent B, K|}|} : set evs \ +\ ==> K : parts (knows Spy evs)"; by (Blast_tac 1); -qed "Oops_parts_spies"; +qed "Oops_parts_knows_Spy"; -bind_thm ("OR4_parts_spies", - OR4_analz_spies RS (impOfSubs analz_subset_parts)); +bind_thm ("OR4_parts_knows_Spy", + OR4_analz_knows_Spy RS (impOfSubs analz_subset_parts)); -(*For proving the easier theorems about X ~: parts (spies evs).*) +(*For proving the easier theorems about X ~: parts (knows Spy evs).*) fun parts_induct_tac i = etac otway.induct i THEN - forward_tac [Oops_parts_spies] (i+6) THEN - forward_tac [OR4_parts_spies] (i+5) THEN + forward_tac [Oops_parts_knows_Spy] (i+7) THEN + forward_tac [OR4_parts_knows_Spy] (i+6) THEN prove_simple_subgoals_tac i; -(** Theorems of the form X ~: parts (spies evs) imply that NOBODY +(** Theorems of the form X ~: parts (knows Spy evs) imply that NOBODY sends messages containing X! **) (*Spy never sees a good agent's shared key!*) -Goal "evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)"; +Goal "evs : otway ==> (Key (shrK A) : parts (knows Spy evs)) = (A : bad)"; by (parts_induct_tac 1); by (ALLGOALS Blast_tac); qed "Spy_see_shrK"; Addsimps [Spy_see_shrK]; -Goal "evs : otway ==> (Key (shrK A) : analz (spies evs)) = (A : bad)"; +Goal "evs : otway ==> (Key (shrK A) : analz (knows Spy evs)) = (A : bad)"; by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset())); qed "Spy_analz_shrK"; Addsimps [Spy_analz_shrK]; @@ -74,7 +88,7 @@ (*Nobody can have used non-existent keys!*) -Goal "evs : otway ==> Key K ~: used evs --> K ~: keysFor (parts (spies evs))"; +Goal "evs : otway ==> Key K ~: used evs --> K ~: keysFor (parts (knows Spy evs))"; by (parts_induct_tac 1); (*Fake*) by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1); @@ -107,18 +121,17 @@ (*For proofs involving analz.*) -val analz_spies_tac = - dtac OR4_analz_spies 6 THEN - forward_tac [Says_Server_message_form] 7 THEN - assume_tac 7 THEN - REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7); +val analz_knows_Spy_tac = + dtac OR4_analz_knows_Spy 7 THEN assume_tac 7 THEN + forward_tac [Says_Server_message_form] 8 THEN assume_tac 8 THEN + REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 8); (**** The following is to prove theorems of the form - Key K : analz (insert (Key KAB) (spies evs)) ==> - Key K : analz (spies evs) + Key K : analz (insert (Key KAB) (knows Spy evs)) ==> + Key K : analz (knows Spy evs) A more general formula must be proved inductively. ****) @@ -129,10 +142,10 @@ (*The equality makes the induction hypothesis easier to apply*) Goal "evs : otway ==> \ \ ALL K KK. KK <= -(range shrK) --> \ -\ (Key K : analz (Key``KK Un (spies evs))) = \ -\ (K : KK | Key K : analz (spies evs))"; +\ (Key K : analz (Key``KK Un (knows Spy evs))) = \ +\ (K : KK | Key K : analz (knows Spy evs))"; by (etac otway.induct 1); -by analz_spies_tac; +by analz_knows_Spy_tac; by (REPEAT_FIRST (resolve_tac [allI, impI])); by (REPEAT_FIRST (rtac analz_image_freshK_lemma )); by (ALLGOALS (asm_simp_tac analz_image_freshK_ss)); @@ -142,8 +155,8 @@ Goal "[| evs : otway; KAB ~: range shrK |] ==> \ -\ Key K : analz (insert (Key KAB) (spies evs)) = \ -\ (K = KAB | Key K : analz (spies evs))"; +\ Key K : analz (insert (Key KAB) (knows Spy evs)) = \ +\ (K = KAB | Key K : analz (knows Spy evs))"; by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1); qed "analz_insert_freshK"; @@ -165,7 +178,7 @@ by (expand_case_tac "K = ?y" 1); by (REPEAT (ares_tac [refl,exI,impI,conjI] 2)); (*...we assume X is a recent message and handle this case by contradiction*) -by (blast_tac (claset() addSEs spies_partsEs) 1); +by (blast_tac (claset() addSEs knows_Spy_partsEs) 1); val lemma = result(); @@ -188,7 +201,7 @@ (*If the encrypted message appears then it originated with the Server!*) Goal "[| A ~: bad; A ~= B; evs : otway |] \ -\ ==> Crypt (shrK A) {|NA, Agent A, Agent B, Key K|} : parts (spies evs) \ +\ ==> Crypt (shrK A) {|NA, Agent A, Agent B, Key K|} : parts (knows Spy evs) \ \ --> (EX NB. Says Server B \ \ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \ \ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ @@ -203,7 +216,7 @@ (*Corollary: if A receives B's OR4 message then it originated with the Server. Freshness may be inferred from nonce NA.*) -Goal "[| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}) \ +Goal "[| Gets A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}) \ \ : set evs; \ \ A ~: bad; A ~= B; evs : otway |] \ \ ==> EX NB. Says Server B \ @@ -224,9 +237,9 @@ \ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ \ : set evs --> \ \ Notes Spy {|NA, NB, Key K|} ~: set evs --> \ -\ Key K ~: analz (spies evs)"; +\ Key K ~: analz (knows Spy evs)"; by (etac otway.induct 1); -by analz_spies_tac; +by analz_knows_Spy_tac; by (ALLGOALS (asm_simp_tac (simpset() addcongs [conj_cong, if_weak_cong] addsimps [analz_insert_eq, analz_insert_freshK] @@ -247,7 +260,7 @@ \ : set evs; \ \ Notes Spy {|NA, NB, Key K|} ~: set evs; \ \ A ~: bad; B ~: bad; evs : otway |] \ -\ ==> Key K ~: analz (spies evs)"; +\ ==> Key K ~: analz (knows Spy evs)"; by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); by (blast_tac (claset() addSEs [lemma]) 1); qed "Spy_not_see_encrypted_key"; @@ -255,11 +268,11 @@ (*A's guarantee. The Oops premise quantifies over NB because A cannot know what it is.*) -Goal "[| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}) \ +Goal "[| Gets A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}) \ \ : set evs; \ \ ALL NB. Notes Spy {|NA, NB, Key K|} ~: set evs; \ \ A ~: bad; B ~: bad; A ~= B; evs : otway |] \ -\ ==> Key K ~: analz (spies evs)"; +\ ==> Key K ~: analz (knows Spy evs)"; by (blast_tac (claset() addSDs [A_trusts_OR4, Spy_not_see_encrypted_key]) 1); qed "A_gets_good_key"; @@ -268,7 +281,7 @@ (*If the encrypted message appears then it originated with the Server!*) Goal "[| B ~: bad; A ~= B; evs : otway |] \ -\ ==> Crypt (shrK B) {|NB, Agent A, Agent B, Key K|} : parts (spies evs) \ +\ ==> Crypt (shrK B) {|NB, Agent A, Agent B, Key K|} : parts (knows Spy evs) \ \ --> (EX NA. Says Server B \ \ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \ \ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ @@ -283,7 +296,7 @@ (*Guarantee for B: if it gets a well-formed certificate then the Server has sent the correct message in round 3.*) -Goal "[| Says S' B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ +Goal "[| Gets B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ \ : set evs; \ \ B ~: bad; A ~= B; evs : otway |] \ \ ==> EX NA. Says Server B \ @@ -295,10 +308,10 @@ (*The obvious combination of B_trusts_OR3 with Spy_not_see_encrypted_key*) -Goal "[| Says S' B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ +Goal "[| Gets B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ \ : set evs; \ \ ALL NA. Notes Spy {|NA, NB, Key K|} ~: set evs; \ \ A ~: bad; B ~: bad; A ~= B; evs : otway |] \ -\ ==> Key K ~: analz (spies evs)"; +\ ==> Key K ~: analz (knows Spy evs)"; by (blast_tac (claset() addDs [B_trusts_OR3, Spy_not_see_encrypted_key]) 1); qed "B_gets_good_key"; diff -r fdf236c98914 -r 76f3865a2b1d src/HOL/Auth/OtwayRees_AN.thy --- a/src/HOL/Auth/OtwayRees_AN.thy Mon Mar 08 13:49:53 1999 +0100 +++ b/src/HOL/Auth/OtwayRees_AN.thy Tue Mar 09 11:01:39 1999 +0100 @@ -28,9 +28,14 @@ (*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: otway; X: synth (analz (spies evs)) |] + Fake "[| evs: otway; X: synth (analz (knows Spy evs)) |] ==> Says Spy B X # evs : otway" + (*A message that has been sent can be received by the + intended recipient.*) + Reception "[| evsr: otway; Says A B X : set evsr |] + ==> Gets B X # evsr : otway" + (*Alice initiates a protocol run*) OR1 "[| evs1: otway |] ==> Says A B {|Agent A, Agent B, Nonce NA|} # evs1 : otway" @@ -38,14 +43,14 @@ (*Bob's response to Alice's message. Bob doesn't know who the sender is, hence the A' in the sender field.*) OR2 "[| evs2: otway; - Says A' B {|Agent A, Agent B, Nonce NA|} : set evs2 |] + Gets B {|Agent A, Agent B, Nonce NA|} : set evs2 |] ==> Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|} # evs2 : otway" (*The Server receives Bob's message. Then he sends a new session key to Bob with a packet for forwarding to Alice.*) OR3 "[| evs3: otway; Key KAB ~: used evs3; - Says B' Server {|Agent A, Agent B, Nonce NA, Nonce NB|} + Gets Server {|Agent A, Agent B, Nonce NA, Nonce NB|} : set evs3 |] ==> Says Server B {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key KAB|}, @@ -57,7 +62,7 @@ Need B ~= Server because we allow messages to self.*) OR4 "[| evs4: otway; B ~= Server; Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|} : set evs4; - Says S' B {|X, Crypt(shrK B){|Nonce NB,Agent A,Agent B,Key K|}|} + Gets B {|X, Crypt(shrK B){|Nonce NB,Agent A,Agent B,Key K|}|} : set evs4 |] ==> Says B A X # evs4 : otway" diff -r fdf236c98914 -r 76f3865a2b1d src/HOL/Auth/OtwayRees_Bad.ML --- a/src/HOL/Auth/OtwayRees_Bad.ML Mon Mar 08 13:49:53 1999 +0100 +++ b/src/HOL/Auth/OtwayRees_Bad.ML Tue Mar 09 11:01:39 1999 +0100 @@ -15,7 +15,7 @@ indicates the possibility of this attack. *) -AddEs spies_partsEs; +AddEs knows_Spy_partsEs; AddDs [impOfSubs analz_subset_parts]; AddDs [impOfSubs Fake_parts_insert]; @@ -26,58 +26,71 @@ \ Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \ \ : set evs"; by (REPEAT (resolve_tac [exI,bexI] 1)); -by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2); +by (rtac (otway.Nil RS + otway.OR1 RS otway.Reception RS + otway.OR2 RS otway.Reception RS + otway.OR3 RS otway.Reception RS otway.OR4) 2); by possibility_tac; result(); +Goal "[| Gets B X : set evs; evs : otway |] ==> EX A. Says A B X : set evs"; +by (etac rev_mp 1); +by (etac otway.induct 1); +by Auto_tac; +qed"Gets_imp_Says"; + +(*Must be proved separately for each protocol*) +Goal "[| Gets B X : set evs; evs : otway |] ==> X : knows Spy evs"; +by (blast_tac (claset() addSDs [Gets_imp_Says, Says_imp_knows_Spy]) 1); +qed"Gets_imp_knows_Spy"; +AddDs [Gets_imp_knows_Spy RS parts.Inj]; + (**** Inductive proofs about otway ****) (** For reasoning about the encrypted portion of messages **) -Goal "Says A' B {|N, Agent A, Agent B, X|} : set evs \ -\ ==> X : analz (spies evs)"; -by (dtac (Says_imp_spies RS analz.Inj) 1); -by (Blast_tac 1); -qed "OR2_analz_spies"; +Goal "[| Gets B {|N, Agent A, Agent B, X|} : set evs; evs : otway |] \ +\ ==> X : analz (knows Spy evs)"; +by (blast_tac (claset() addSDs [Gets_imp_knows_Spy RS analz.Inj]) 1); +qed "OR2_analz_knows_Spy"; -Goal "Says S' B {|N, X, Crypt (shrK B) X'|} : set evs \ -\ ==> X : analz (spies evs)"; -by (dtac (Says_imp_spies RS analz.Inj) 1); -by (Blast_tac 1); -qed "OR4_analz_spies"; +Goal "[| Gets B {|N, X, Crypt (shrK B) X'|} : set evs; evs : otway |] \ +\ ==> X : analz (knows Spy evs)"; +by (blast_tac (claset() addSDs [Gets_imp_knows_Spy RS analz.Inj]) 1); +qed "OR4_analz_knows_Spy"; Goal "Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \ -\ ==> K : parts (spies evs)"; +\ ==> K : parts (knows Spy evs)"; by (Blast_tac 1); -qed "Oops_parts_spies"; +qed "Oops_parts_knows_Spy"; -bind_thm ("OR2_parts_spies", - OR2_analz_spies RS (impOfSubs analz_subset_parts)); -bind_thm ("OR4_parts_spies", - OR4_analz_spies RS (impOfSubs analz_subset_parts)); +bind_thm ("OR2_parts_knows_Spy", + OR2_analz_knows_Spy RS (impOfSubs analz_subset_parts)); +bind_thm ("OR4_parts_knows_Spy", + OR4_analz_knows_Spy RS (impOfSubs analz_subset_parts)); -(*For proving the easier theorems about X ~: parts (spies evs).*) +(*For proving the easier theorems about X ~: parts (knows Spy evs).*) fun parts_induct_tac i = etac otway.induct i THEN - forward_tac [Oops_parts_spies] (i+6) THEN - forward_tac [OR4_parts_spies] (i+5) THEN - forward_tac [OR2_parts_spies] (i+3) THEN + forward_tac [Oops_parts_knows_Spy] (i+7) THEN + forward_tac [OR4_parts_knows_Spy] (i+6) THEN + forward_tac [OR2_parts_knows_Spy] (i+4) THEN prove_simple_subgoals_tac i; -(** Theorems of the form X ~: parts (spies evs) imply that NOBODY +(** Theorems of the form X ~: parts (knows Spy evs) imply that NOBODY sends messages containing X! **) (*Spy never sees a good agent's shared key!*) -Goal "evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)"; +Goal "evs : otway ==> (Key (shrK A) : parts (knows Spy evs)) = (A : bad)"; by (parts_induct_tac 1); by (ALLGOALS Blast_tac); qed "Spy_see_shrK"; Addsimps [Spy_see_shrK]; -Goal "evs : otway ==> (Key (shrK A) : analz (spies evs)) = (A : bad)"; +Goal "evs : otway ==> (Key (shrK A) : analz (knows Spy evs)) = (A : bad)"; by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset())); qed "Spy_analz_shrK"; Addsimps [Spy_analz_shrK]; @@ -87,7 +100,7 @@ (*Nobody can have used non-existent keys!*) -Goal "evs : otway ==> Key K ~: used evs --> K ~: keysFor (parts (spies evs))"; +Goal "evs : otway ==> Key K ~: used evs --> K ~: keysFor (parts (knows Spy evs))"; by (parts_induct_tac 1); (*Fake*) by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1); @@ -118,18 +131,18 @@ (*For proofs involving analz.*) -val analz_spies_tac = - dtac OR2_analz_spies 4 THEN - dtac OR4_analz_spies 6 THEN - forward_tac [Says_Server_message_form] 7 THEN assume_tac 7 THEN - REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7); +val analz_knows_Spy_tac = + dtac OR2_analz_knows_Spy 5 THEN assume_tac 5 THEN + dtac OR4_analz_knows_Spy 7 THEN assume_tac 7 THEN + forward_tac [Says_Server_message_form] 8 THEN assume_tac 8 THEN + REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 8); (**** The following is to prove theorems of the form - Key K : analz (insert (Key KAB) (spies evs)) ==> - Key K : analz (spies evs) + Key K : analz (insert (Key KAB) (knows Spy evs)) ==> + Key K : analz (knows Spy evs) A more general formula must be proved inductively. ****) @@ -140,10 +153,10 @@ (*The equality makes the induction hypothesis easier to apply*) Goal "evs : otway ==> \ \ ALL K KK. KK <= - (range shrK) --> \ -\ (Key K : analz (Key``KK Un (spies evs))) = \ -\ (K : KK | Key K : analz (spies evs))"; +\ (Key K : analz (Key``KK Un (knows Spy evs))) = \ +\ (K : KK | Key K : analz (knows Spy evs))"; by (etac otway.induct 1); -by analz_spies_tac; +by analz_knows_Spy_tac; by (REPEAT_FIRST (resolve_tac [allI, impI])); by (REPEAT_FIRST (rtac analz_image_freshK_lemma )); by (ALLGOALS (asm_simp_tac analz_image_freshK_ss)); @@ -153,8 +166,8 @@ Goal "[| evs : otway; KAB ~: range shrK |] ==> \ -\ Key K : analz (insert (Key KAB) (spies evs)) = \ -\ (K = KAB | Key K : analz (spies evs))"; +\ Key K : analz (insert (Key KAB) (knows Spy evs)) = \ +\ (K = KAB | Key K : analz (knows Spy evs))"; by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1); qed "analz_insert_freshK"; @@ -174,7 +187,7 @@ by (expand_case_tac "K = ?y" 1); by (REPEAT (ares_tac [refl,exI,impI,conjI] 2)); (*...we assume X is a recent message, and handle this case by contradiction*) -by (blast_tac (claset() addSEs spies_partsEs) 1); +by (blast_tac (claset() addSEs knows_Spy_partsEs) 1); val lemma = result(); Goal "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set evs; \ @@ -193,9 +206,9 @@ \ {|NA, Crypt (shrK A) {|NA, Key K|}, \ \ Crypt (shrK B) {|NB, Key K|}|} : set evs --> \ \ Notes Spy {|NA, NB, Key K|} ~: set evs --> \ -\ Key K ~: analz (spies evs)"; +\ Key K ~: analz (knows Spy evs)"; by (etac otway.induct 1); -by analz_spies_tac; +by analz_knows_Spy_tac; by (ALLGOALS (asm_simp_tac (simpset() addcongs [conj_cong] addsimps [analz_insert_eq, analz_insert_freshK] @@ -215,7 +228,7 @@ \ Crypt (shrK B) {|NB, Key K|}|} : set evs; \ \ Notes Spy {|NA, NB, Key K|} ~: set evs; \ \ A ~: bad; B ~: bad; evs : otway |] \ -\ ==> Key K ~: analz (spies evs)"; +\ ==> Key K ~: analz (knows Spy evs)"; by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); by (blast_tac (claset() addSEs [lemma]) 1); qed "Spy_not_see_encrypted_key"; @@ -227,7 +240,7 @@ The premise A ~= B prevents OR2's similar-looking cryptogram from being picked up. Original Otway-Rees doesn't need it.*) Goal "[| A ~: bad; A ~= B; evs : otway |] \ -\ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) --> \ +\ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (knows Spy evs) --> \ \ Says A B {|NA, Agent A, Agent B, \ \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs"; by (parts_induct_tac 1); @@ -236,11 +249,12 @@ (*Crucial property: If the encrypted message appears, and A has used NA - to start a run, then it originated with the Server!*) + to start a run, then it originated with the Server! + The premise A ~= B allows use of Crypt_imp_OR1*) (*Only it is FALSE. Somebody could make a fake message to Server substituting some other nonce NA' for NB.*) -Goal "[| A ~: bad; evs : otway |] \ -\ ==> Crypt (shrK A) {|NA, Key K|} : parts (spies evs) --> \ +Goal "[| A ~: bad; A ~= B; evs : otway |] \ +\ ==> Crypt (shrK A) {|NA, Key K|} : parts (knows Spy evs) --> \ \ Says A B {|NA, Agent A, Agent B, \ \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \ \ : set evs --> \ @@ -261,7 +275,7 @@ (*OR3*) (** LEVEL 5 **) (*The hypotheses at this point suggest an attack in which nonce NB is used in two different roles: - Says B' Server + Gets Server {|Nonce NA, Agent Aa, Agent A, Crypt (shrK Aa) {|Nonce NA, Agent Aa, Agent A|}, Nonce NB, Crypt (shrK A) {|Nonce NA, Agent Aa, Agent A|}|} diff -r fdf236c98914 -r 76f3865a2b1d src/HOL/Auth/OtwayRees_Bad.thy --- a/src/HOL/Auth/OtwayRees_Bad.thy Mon Mar 08 13:49:53 1999 +0100 +++ b/src/HOL/Auth/OtwayRees_Bad.thy Tue Mar 09 11:01:39 1999 +0100 @@ -22,9 +22,14 @@ (*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: otway; X: synth (analz (spies evs)) |] + Fake "[| evs: otway; X: synth (analz (knows Spy evs)) |] ==> Says Spy B X # evs : otway" + (*A message that has been sent can be received by the + intended recipient.*) + Reception "[| evsr: otway; Says A B X : set evsr |] + ==> Gets B X # evsr : otway" + (*Alice initiates a protocol run*) OR1 "[| evs1: otway; Nonce NA ~: used evs1 |] ==> Says A B {|Nonce NA, Agent A, Agent B, @@ -35,7 +40,7 @@ the sender is, hence the A' in the sender field. We modify the published protocol by NOT encrypting NB.*) OR2 "[| evs2: otway; Nonce NB ~: used evs2; - Says A' B {|Nonce NA, Agent A, Agent B, X|} : set evs2 |] + Gets B {|Nonce NA, Agent A, Agent B, X|} : set evs2 |] ==> Says B Server {|Nonce NA, Agent A, Agent B, X, Nonce NB, Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|} @@ -45,7 +50,7 @@ match. Then he sends a new session key to Bob with a packet for forwarding to Alice.*) OR3 "[| evs3: otway; Key KAB ~: used evs3; - Says B' Server + Gets Server {|Nonce NA, Agent A, Agent B, Crypt (shrK A) {|Nonce NA, Agent A, Agent B|}, Nonce NB, @@ -60,11 +65,11 @@ (*Bob receives the Server's (?) message and compares the Nonces with those in the message he previously sent the Server. Need B ~= Server because we allow messages to self.*) - OR4 "[| evs4: otway; A ~= B; B ~= Server; + OR4 "[| evs4: otway; B ~= Server; Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB, Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|} : set evs4; - Says S' B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|} + Gets B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|} : set evs4 |] ==> Says B A {|Nonce NA, X|} # evs4 : otway" diff -r fdf236c98914 -r 76f3865a2b1d src/HOL/Auth/Public.ML --- a/src/HOL/Auth/Public.ML Mon Mar 08 13:49:53 1999 +0100 +++ b/src/HOL/Auth/Public.ML Tue Mar 09 11:01:39 1999 +0100 @@ -72,7 +72,7 @@ Goal "Key (pubK A) : spies evs"; by (induct_tac "evs" 1); by (ALLGOALS (asm_simp_tac - (simpset() addsimps [imageI, spies_Cons] + (simpset() addsimps [imageI, knows_Cons] addsplits [expand_event_case]))); qed_spec_mp "spies_pubK"; @@ -80,7 +80,7 @@ Goal "A: bad ==> Key (priK A) : spies evs"; by (induct_tac "evs" 1); by (ALLGOALS (asm_simp_tac - (simpset() addsimps [imageI, spies_Cons] + (simpset() addsimps [imageI, knows_Cons] addsplits [expand_event_case]))); qed "Spy_spies_bad"; diff -r fdf236c98914 -r 76f3865a2b1d src/HOL/Auth/Shared.ML --- a/src/HOL/Auth/Shared.ML Mon Mar 08 13:49:53 1999 +0100 +++ b/src/HOL/Auth/Shared.ML Tue Mar 09 11:01:39 1999 +0100 @@ -28,11 +28,11 @@ (*Specialized to shared-key model: no need for addss in protocol proofs*) Goal "[| K: keysFor (parts (insert X H)); X : synth (analz H) |] \ \ ==> K : keysFor (parts H) | Key K : parts H"; -by (fast_tac +by (force_tac (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono), impOfSubs (analz_subset_parts RS keysFor_mono)] - addIs [impOfSubs analz_subset_parts] - addss (simpset())) 1); + addIs [impOfSubs analz_subset_parts], + simpset()) 1); qed "keysFor_parts_insert"; Goal "Crypt K X : H ==> K : keysFor H"; @@ -41,22 +41,21 @@ qed "Crypt_imp_keysFor"; -(*** Function "spies" ***) +(*** Function "knows" ***) (*Spy sees shared keys of agents!*) -Goal "A: bad ==> Key (shrK A) : spies evs"; +Goal "A: bad ==> Key (shrK A) : knows Spy evs"; by (induct_tac "evs" 1); by (ALLGOALS (asm_simp_tac - (simpset() addsimps [imageI, spies_Cons] + (simpset() addsimps [imageI, knows_Cons] addsplits [expand_event_case]))); -qed "Spy_spies_bad"; - -AddSIs [Spy_spies_bad]; +qed "Spy_knows_Spy_bad"; +AddSIs [Spy_knows_Spy_bad]; (*For not_bad_tac*) -Goal "[| Crypt (shrK A) X : analz (spies evs); A: bad |] \ -\ ==> X : analz (spies evs)"; -by (fast_tac (claset() addSDs [analz.Decrypt] addss (simpset())) 1); +Goal "[| Crypt (shrK A) X : analz (knows Spy evs); A: bad |] \ +\ ==> X : analz (knows Spy evs)"; +by (force_tac (claset() addSDs [analz.Decrypt], simpset()) 1); qed "Crypt_Spy_analz_bad"; (*Prove that the agent is uncompromised by the confidentiality of @@ -202,7 +201,8 @@ such as Nonce ?N ~: used evs that match Nonce_supply*) fun possibility_tac st = st |> (REPEAT - (ALLGOALS (simp_tac (simpset() delsimps [used_Says] setSolver safe_solver)) + (ALLGOALS (simp_tac (simpset() delsimps [used_Says, used_Notes, used_Gets] + setSolver safe_solver)) THEN REPEAT_FIRST (eq_assume_tac ORELSE' resolve_tac [refl, conjI, Nonce_supply, Key_supply]))); diff -r fdf236c98914 -r 76f3865a2b1d src/HOL/Auth/TLS.ML --- a/src/HOL/Auth/TLS.ML Mon Mar 08 13:49:53 1999 +0100 +++ b/src/HOL/Auth/TLS.ML Tue Mar 09 11:01:39 1999 +0100 @@ -480,7 +480,7 @@ (*ClientAccepts and ServerAccepts: because PMS was already visible*) by (REPEAT (blast_tac (claset() addDs [Spy_not_see_PMS, Says_imp_spies RS analz.Inj, - Notes_imp_spies RS analz.Inj]) 6)); + Notes_imp_knows_Spy RS analz.Inj]) 6)); (*ClientHello*) by (Blast_tac 3); (*SpyKeys: by secrecy of the PMS, Spy cannot make the MS*)