# HG changeset patch # User paulson # Date 986982834 -7200 # Node ID c8bbf4c4bc2da310927a903c284cf32ff7746d0c # Parent a0e3c67c139416d59a9a3934e16cab5e87beec70 symlinks to ../../../HOL/Auth. Fingers crossed... diff -r a0e3c67c1394 -r c8bbf4c4bc2d doc-src/TutorialI/Protocol/Event.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/TutorialI/Protocol/Event.thy Wed Apr 11 11:53:54 2001 +0200 @@ -0,0 +1,89 @@ +(* Title: HOL/Auth/Event + 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 "spies"; freshness + +"bad" agents have been broken by the Spy; their private keys and internal + stores are visible to him +*) + +theory Event = Message +files ("Event_lemmas.ML"): + +consts (*Initial states of agents -- parameter of the construction*) + initState :: "agent => msg set" + +datatype + event = Says agent agent msg + | Gets agent msg + | Notes agent msg + +consts + bad :: "agent set" (*compromised agents*) + knows :: "agent => event list => msg set" + + +(*"spies" is retained for compability's sake*) +syntax + spies :: "event list => msg set" + +translations + "spies" => "knows Spy" + + +axioms + (*Spy has access to his own key for spoof messages, but Server is secure*) + Spy_in_bad [iff] : "Spy \ bad" + Server_not_bad [iff] : "Server \ bad" + +primrec + 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) + | Gets A' X => knows Spy evs + | Notes A' X => + if A' \ bad then insert X (knows Spy evs) else knows Spy evs) + else + (case ev of + Says A' B 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 + | Notes 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: + complement of the set of fresh items*) + used :: "event list => msg set" + +primrec + used_Nil: "used [] = (UN B. parts (initState B))" + used_Cons: "used (ev # evs) = + (case ev of + Says A B X => parts {X} Un (used evs) + | Gets A X => used evs + | Notes A X => parts {X} Un (used evs))" + + +use "Event_lemmas.ML" + +method_setup analz_mono_contra = {* + Method.no_args + (Method.METHOD (fn facts => REPEAT_FIRST analz_mono_contra_tac)) *} + "for proving theorems of the form X \ analz (knows Spy evs) --> P" + +end diff -r a0e3c67c1394 -r c8bbf4c4bc2d doc-src/TutorialI/Protocol/Event_lemmas.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/TutorialI/Protocol/Event_lemmas.ML Wed Apr 11 11:53:54 2001 +0200 @@ -0,0 +1,232 @@ +(* Title: HOL/Auth/Event_lemmas + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1996 University of Cambridge +*) + + +val knows_Cons = thm "knows_Cons"; +val used_Nil = thm "used_Nil"; +val used_Cons = thm "used_Cons"; + + +(*Inserted by default but later removed. This declaration lets the file + be re-loaded.*) +Addsimps [knows_Cons, used_Nil, used_Cons]; + +(**** Function "knows" ****) + +(** Simplifying parts (insert X (knows Spy evs)) + = parts {X} Un parts (knows Spy evs) -- since general case loops*) + +bind_thm ("parts_insert_knows_Spy", + inst "H" "knows Spy evs" parts_insert); + + +val expand_event_case = thm "event.split"; + +Goal "knows Spy (Says A B X # evs) = insert X (knows Spy evs)"; +by (Simp_tac 1); +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 "knows Spy (Notes A X # evs) = \ +\ (if A:bad then insert X (knows Spy evs) else knows Spy evs)"; +by (Simp_tac 1); +qed "knows_Spy_Notes"; + +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 "knows_Spy_subset_knows_Spy_Says"; + +Goal "knows Spy evs <= knows Spy (Notes A X # evs)"; +by (Simp_tac 1); +by (Fast_tac 1); +qed "knows_Spy_subset_knows_Spy_Notes"; + +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_knows_Spy"; + +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_knows_Spy"; + + +(*Use with addSEs to derive contradictions from old Says events containing + items known to be fresh*) +bind_thms ("knows_Spy_partsEs", + map make_elim [Says_imp_knows_Spy RS parts.Inj, parts.Body]); + +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"; + +(*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 [knows_Cons]; + + +(*** Fresh nonces ***) + +Goal "parts (knows Spy evs) <= used evs"; +by (induct_tac "evs" 1); +by (ALLGOALS (asm_simp_tac + (simpset() addsimps [parts_insert_knows_Spy] + addsplits [expand_event_case]))); +by (ALLGOALS Blast_tac); +qed "parts_knows_Spy_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_knows_Spy] + addsplits [expand_event_case]))); +by (ALLGOALS Blast_tac); +bind_thm ("initState_into_used", impOfSubs (result())); + +Goal "used (Says A B X # evs) = parts{X} Un used evs"; +by (Simp_tac 1); +qed "used_Says"; +Addsimps [used_Says]; + +Goal "used (Notes A X # evs) = parts{X} Un used evs"; +by (Simp_tac 1); +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); +qed "used_nil_subset"; + +(**** NOTE REMOVAL--laws above are cleaner, as they don't involve "case" ****) +Delsimps [used_Nil, used_Cons]; + + +(*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.*) + +bind_thms ("analz_mono_contra", + [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]); + +val analz_mono_contra_tac = + let val analz_impI = inst "P" "?Y ~: analz (knows Spy ?evs)" impI + in + rtac analz_impI THEN' + REPEAT1 o + (dresolve_tac + [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*) +bind_thms ("spies_partsEs", knows_Spy_partsEs); +bind_thm ("Says_imp_spies", Says_imp_knows_Spy); +bind_thm ("parts_insert_spies", parts_insert_knows_Spy); diff -r a0e3c67c1394 -r c8bbf4c4bc2d doc-src/TutorialI/Protocol/Message.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/TutorialI/Protocol/Message.thy Wed Apr 11 11:53:54 2001 +0200 @@ -0,0 +1,147 @@ +(* Title: HOL/Auth/Message + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1996 University of Cambridge + +Datatypes of agents and messages; +Inductive relations "parts", "analz" and "synth" +*) + +theory Message = Main +files ("Message_lemmas.ML"): + +(*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*) +lemma [simp] : "A Un (B Un A) = B Un A" +by blast + +types + key = nat + +consts + invKey :: "key=>key" + +axioms + invKey [simp] : "invKey (invKey K) = K" + + (*The inverse of a symmetric key is itself; + that of a public key is the private key and vice versa*) + +constdefs + symKeys :: "key set" + "symKeys == {K. invKey K = K}" + +datatype (*We allow any number of friendly agents*) + agent = Server | Friend nat | Spy + +datatype + msg = Agent agent (*Agent names*) + | Number nat (*Ordinary integers, timestamps, ...*) + | Nonce nat (*Unguessable nonces*) + | Key key (*Crypto keys*) + | Hash msg (*Hashing*) + | MPair msg msg (*Compound messages*) + | Crypt key msg (*Encryption, public- or shared-key*) + + +(*Concrete syntax: messages appear as {|A,B,NA|}, etc...*) +syntax + "@MTuple" :: "['a, args] => 'a * 'b" ("(2{|_,/ _|})") + +syntax (xsymbols) + "@MTuple" :: "['a, args] => 'a * 'b" ("(2\_,/ _\)") + +translations + "{|x, y, z|}" == "{|x, {|y, z|}|}" + "{|x, y|}" == "MPair x y" + + +constdefs + (*Message Y, paired with a MAC computed with the help of X*) + HPair :: "[msg,msg] => msg" ("(4Hash[_] /_)" [0, 1000]) + "Hash[X] Y == {| Hash{|X,Y|}, Y|}" + + (*Keys useful to decrypt elements of a message set*) + keysFor :: "msg set => key set" + "keysFor H == invKey ` {K. \X. Crypt K X \ H}" + +(** Inductive definition of all "parts" of a message. **) + +consts parts :: "msg set => msg set" +inductive "parts H" + intros + Inj [intro]: "X \ H ==> X \ parts H" + Fst: "{|X,Y|} \ parts H ==> X \ parts H" + Snd: "{|X,Y|} \ parts H ==> Y \ parts H" + Body: "Crypt K X \ parts H ==> X \ parts H" + + +(*Monotonicity*) +lemma parts_mono: "G<=H ==> parts(G) <= parts(H)" +apply auto +apply (erule parts.induct) +apply (auto dest: Fst Snd Body) +done + + +(** Inductive definition of "analz" -- what can be broken down from a set of + messages, including keys. A form of downward closure. Pairs can + be taken apart; messages decrypted with known keys. **) + +consts analz :: "msg set => msg set" +inductive "analz H" + intros + Inj [intro,simp] : "X \ H ==> X \ analz H" + Fst: "{|X,Y|} \ analz H ==> X \ analz H" + Snd: "{|X,Y|} \ analz H ==> Y \ analz H" + Decrypt [dest]: + "[|Crypt K X \ analz H; Key(invKey K): analz H|] ==> X \ analz H" + + +(*Monotonicity; Lemma 1 of Lowe's paper*) +lemma analz_mono: "G<=H ==> analz(G) <= analz(H)" +apply auto +apply (erule analz.induct) +apply (auto dest: Fst Snd) +done + +(** Inductive definition of "synth" -- what can be built up from a set of + messages. A form of upward closure. Pairs can be built, messages + encrypted with known keys. Agent names are public domain. + Numbers can be guessed, but Nonces cannot be. **) + +consts synth :: "msg set => msg set" +inductive "synth H" + intros + Inj [intro]: "X \ H ==> X \ synth H" + Agent [intro]: "Agent agt \ synth H" + Number [intro]: "Number n \ synth H" + Hash [intro]: "X \ synth H ==> Hash X \ synth H" + MPair [intro]: "[|X \ synth H; Y \ synth H|] ==> {|X,Y|} \ synth H" + Crypt [intro]: "[|X \ synth H; Key(K) \ H|] ==> Crypt K X \ synth H" + +(*Monotonicity*) +lemma synth_mono: "G<=H ==> synth(G) <= synth(H)" +apply auto +apply (erule synth.induct) +apply (auto dest: Fst Snd Body) +done + +(*NO Agent_synth, as any Agent name can be synthesized. Ditto for Number*) +inductive_cases Nonce_synth [elim!]: "Nonce n \ synth H" +inductive_cases Key_synth [elim!]: "Key K \ synth H" +inductive_cases Hash_synth [elim!]: "Hash X \ synth H" +inductive_cases MPair_synth [elim!]: "{|X,Y|} \ synth H" +inductive_cases Crypt_synth [elim!]: "Crypt K X \ synth H" + +use "Message_lemmas.ML" + +lemma Fake_parts_insert_in_Un: + "[|Z \ parts (insert X H); X: synth (analz H)|] + ==> Z \ synth (analz H) \ parts H"; +by (blast dest: Fake_parts_insert [THEN subsetD, dest]) + +method_setup spy_analz = {* + Method.no_args (Method.METHOD (fn facts => spy_analz_tac 1)) *} + "for proving the Fake case when analz is involved" + +end diff -r a0e3c67c1394 -r c8bbf4c4bc2d doc-src/TutorialI/Protocol/Message_lemmas.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/TutorialI/Protocol/Message_lemmas.ML Wed Apr 11 11:53:54 2001 +0200 @@ -0,0 +1,899 @@ +(* Title: HOL/Auth/Message + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1996 University of Cambridge + +Datatypes of agents and messages; +Inductive relations "parts", "analz" and "synth" +*) + +(*ML bindings for definitions and axioms*) +val invKey = thm "invKey"; +val keysFor_def = thm "keysFor_def"; +val parts_mono = thm "parts_mono"; +val analz_mono = thm "analz_mono"; +val synth_mono = thm "synth_mono"; +val HPair_def = thm "HPair_def"; +val symKeys_def = thm "symKeys_def"; + +structure parts = + struct + val induct = thm "parts.induct"; + val Inj = thm "parts.Inj"; + val Fst = thm "parts.Fst"; + val Snd = thm "parts.Snd"; + val Body = thm "parts.Body"; + end; + +structure analz = + struct + val induct = thm "analz.induct"; + val Inj = thm "analz.Inj"; + val Fst = thm "analz.Fst"; + val Snd = thm "analz.Snd"; + val Decrypt = thm "analz.Decrypt"; + end; + +structure synth = + struct + val induct = thm "synth.induct"; + val Inj = thm "synth.Inj"; + val Agent = thm "synth.Agent"; + val Number = thm "synth.Number"; + val Hash = thm "synth.Hash"; + val Crypt = thm "synth.Crypt"; + end; + + +(*Equations hold because constructors are injective; cannot prove for all f*) +Goal "(Friend x \\ Friend`A) = (x:A)"; +by Auto_tac; +qed "Friend_image_eq"; + +Goal "(Key x \\ Key`A) = (x\\A)"; +by Auto_tac; +qed "Key_image_eq"; + +Goal "(Nonce x \\ Key`A)"; +by Auto_tac; +qed "Nonce_Key_image_eq"; +Addsimps [Friend_image_eq, Key_image_eq, Nonce_Key_image_eq]; + + +(** Inverse of keys **) + +Goal "(invKey K = invKey K') = (K=K')"; +by Safe_tac; +by (rtac box_equals 1); +by (REPEAT (rtac invKey 2)); +by (Asm_simp_tac 1); +qed "invKey_eq"; + +Addsimps [invKey_eq]; + + +(**** keysFor operator ****) + +Goalw [keysFor_def] "keysFor {} = {}"; +by (Blast_tac 1); +qed "keysFor_empty"; + +Goalw [keysFor_def] "keysFor (H Un H') = keysFor H Un keysFor H'"; +by (Blast_tac 1); +qed "keysFor_Un"; + +Goalw [keysFor_def] "keysFor (\\i\\A. H i) = (\\i\\A. keysFor (H i))"; +by (Blast_tac 1); +qed "keysFor_UN"; + +(*Monotonicity*) +Goalw [keysFor_def] "G\\H ==> keysFor(G) \\ keysFor(H)"; +by (Blast_tac 1); +qed "keysFor_mono"; + +Goalw [keysFor_def] "keysFor (insert (Agent A) H) = keysFor H"; +by Auto_tac; +qed "keysFor_insert_Agent"; + +Goalw [keysFor_def] "keysFor (insert (Nonce N) H) = keysFor H"; +by Auto_tac; +qed "keysFor_insert_Nonce"; + +Goalw [keysFor_def] "keysFor (insert (Number N) H) = keysFor H"; +by Auto_tac; +qed "keysFor_insert_Number"; + +Goalw [keysFor_def] "keysFor (insert (Key K) H) = keysFor H"; +by Auto_tac; +qed "keysFor_insert_Key"; + +Goalw [keysFor_def] "keysFor (insert (Hash X) H) = keysFor H"; +by Auto_tac; +qed "keysFor_insert_Hash"; + +Goalw [keysFor_def] "keysFor (insert {|X,Y|} H) = keysFor H"; +by Auto_tac; +qed "keysFor_insert_MPair"; + +Goalw [keysFor_def] + "keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)"; +by Auto_tac; +qed "keysFor_insert_Crypt"; + +Addsimps [keysFor_empty, keysFor_Un, keysFor_UN, + keysFor_insert_Agent, keysFor_insert_Nonce, + keysFor_insert_Number, keysFor_insert_Key, + keysFor_insert_Hash, keysFor_insert_MPair, keysFor_insert_Crypt]; +AddSEs [keysFor_Un RS equalityD1 RS subsetD RS UnE, + keysFor_UN RS equalityD1 RS subsetD RS UN_E]; + +Goalw [keysFor_def] "keysFor (Key`E) = {}"; +by Auto_tac; +qed "keysFor_image_Key"; +Addsimps [keysFor_image_Key]; + +Goalw [keysFor_def] "Crypt K X \\ H ==> invKey K \\ keysFor H"; +by (Blast_tac 1); +qed "Crypt_imp_invKey_keysFor"; + + +(**** Inductive relation "parts" ****) + +val major::prems = +Goal "[| {|X,Y|} \\ parts H; \ +\ [| X \\ parts H; Y \\ parts H |] ==> P \ +\ |] ==> P"; +by (cut_facts_tac [major] 1); +by (resolve_tac prems 1); +by (REPEAT (eresolve_tac [asm_rl, parts.Fst, parts.Snd] 1)); +qed "MPair_parts"; + +AddSEs [MPair_parts, make_elim parts.Body]; +(*NB These two rules are UNSAFE in the formal sense, as they discard the + compound message. They work well on THIS FILE. + MPair_parts is left as SAFE because it speeds up proofs. + The Crypt rule is normally kept UNSAFE to avoid breaking up certificates.*) + +Goal "H \\ parts(H)"; +by (Blast_tac 1); +qed "parts_increasing"; + +val parts_insertI = impOfSubs (subset_insertI RS parts_mono); + +Goal "parts{} = {}"; +by Safe_tac; +by (etac parts.induct 1); +by (ALLGOALS Blast_tac); +qed "parts_empty"; +Addsimps [parts_empty]; + +Goal "X\\ parts{} ==> P"; +by (Asm_full_simp_tac 1); +qed "parts_emptyE"; +AddSEs [parts_emptyE]; + +(*WARNING: loops if H = {Y}, therefore must not be repeated!*) +Goal "X\\ parts H ==> \\Y\\H. X\\ parts {Y}"; +by (etac parts.induct 1); +by (ALLGOALS Blast_tac); +qed "parts_singleton"; + + +(** Unions **) + +Goal "parts(G) Un parts(H) \\ parts(G Un H)"; +by (REPEAT (ares_tac [Un_least, parts_mono, Un_upper1, Un_upper2] 1)); +val parts_Un_subset1 = result(); + +Goal "parts(G Un H) \\ parts(G) Un parts(H)"; +by (rtac subsetI 1); +by (etac parts.induct 1); +by (ALLGOALS Blast_tac); +val parts_Un_subset2 = result(); + +Goal "parts(G Un H) = parts(G) Un parts(H)"; +by (REPEAT (ares_tac [equalityI, parts_Un_subset1, parts_Un_subset2] 1)); +qed "parts_Un"; + +Goal "parts (insert X H) = parts {X} Un parts H"; +by (stac (read_instantiate [("A","H")] insert_is_Un) 1); +by (simp_tac (HOL_ss addsimps [parts_Un]) 1); +qed "parts_insert"; + +(*TWO inserts to avoid looping. This rewrite is better than nothing. + Not suitable for Addsimps: its behaviour can be strange.*) +Goal "parts (insert X (insert Y H)) = parts {X} Un parts {Y} Un parts H"; +by (simp_tac (simpset() addsimps [Un_assoc]) 1); +by (simp_tac (simpset() addsimps [parts_insert RS sym]) 1); +qed "parts_insert2"; + +Goal "(\\x\\A. parts(H x)) \\ parts(\\x\\A. H x)"; +by (REPEAT (ares_tac [UN_least, parts_mono, UN_upper] 1)); +val parts_UN_subset1 = result(); + +Goal "parts(\\x\\A. H x) \\ (\\x\\A. parts(H x))"; +by (rtac subsetI 1); +by (etac parts.induct 1); +by (ALLGOALS Blast_tac); +val parts_UN_subset2 = result(); + +Goal "parts(\\x\\A. H x) = (\\x\\A. parts(H x))"; +by (REPEAT (ares_tac [equalityI, parts_UN_subset1, parts_UN_subset2] 1)); +qed "parts_UN"; + +(*Added to simplify arguments to parts, analz and synth. + NOTE: the UN versions are no longer used!*) +Addsimps [parts_Un, parts_UN]; +AddSEs [parts_Un RS equalityD1 RS subsetD RS UnE, + parts_UN RS equalityD1 RS subsetD RS UN_E]; + +Goal "insert X (parts H) \\ parts(insert X H)"; +by (blast_tac (claset() addIs [impOfSubs parts_mono]) 1); +qed "parts_insert_subset"; + +(** Idempotence and transitivity **) + +Goal "X\\ parts (parts H) ==> X\\ parts H"; +by (etac parts.induct 1); +by (ALLGOALS Blast_tac); +qed "parts_partsD"; +AddSDs [parts_partsD]; + +Goal "parts (parts H) = parts H"; +by (Blast_tac 1); +qed "parts_idem"; +Addsimps [parts_idem]; + +Goal "[| X\\ parts G; G \\ parts H |] ==> X\\ parts H"; +by (dtac parts_mono 1); +by (Blast_tac 1); +qed "parts_trans"; + +(*Cut*) +Goal "[| Y\\ parts (insert X G); X\\ parts H |] \ +\ ==> Y\\ parts (G Un H)"; +by (etac parts_trans 1); +by Auto_tac; +qed "parts_cut"; + +Goal "X\\ parts H ==> parts (insert X H) = parts H"; +by (fast_tac (claset() addSDs [parts_cut] + addIs [parts_insertI] + addss (simpset())) 1); +qed "parts_cut_eq"; + +Addsimps [parts_cut_eq]; + + +(** Rewrite rules for pulling out atomic messages **) + +fun parts_tac i = + EVERY [rtac ([subsetI, parts_insert_subset] MRS equalityI) i, + etac parts.induct i, + Auto_tac]; + +Goal "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)"; +by (parts_tac 1); +qed "parts_insert_Agent"; + +Goal "parts (insert (Nonce N) H) = insert (Nonce N) (parts H)"; +by (parts_tac 1); +qed "parts_insert_Nonce"; + +Goal "parts (insert (Number N) H) = insert (Number N) (parts H)"; +by (parts_tac 1); +qed "parts_insert_Number"; + +Goal "parts (insert (Key K) H) = insert (Key K) (parts H)"; +by (parts_tac 1); +qed "parts_insert_Key"; + +Goal "parts (insert (Hash X) H) = insert (Hash X) (parts H)"; +by (parts_tac 1); +qed "parts_insert_Hash"; + +Goal "parts (insert (Crypt K X) H) = \ +\ insert (Crypt K X) (parts (insert X H))"; +by (rtac equalityI 1); +by (rtac subsetI 1); +by (etac parts.induct 1); +by Auto_tac; +by (etac parts.induct 1); +by (ALLGOALS (blast_tac (claset() addIs [parts.Body]))); +qed "parts_insert_Crypt"; + +Goal "parts (insert {|X,Y|} H) = \ +\ insert {|X,Y|} (parts (insert X (insert Y H)))"; +by (rtac equalityI 1); +by (rtac subsetI 1); +by (etac parts.induct 1); +by Auto_tac; +by (etac parts.induct 1); +by (ALLGOALS (blast_tac (claset() addIs [parts.Fst, parts.Snd]))); +qed "parts_insert_MPair"; + +Addsimps [parts_insert_Agent, parts_insert_Nonce, + parts_insert_Number, parts_insert_Key, + parts_insert_Hash, parts_insert_Crypt, parts_insert_MPair]; + + +Goal "parts (Key`N) = Key`N"; +by Auto_tac; +by (etac parts.induct 1); +by Auto_tac; +qed "parts_image_Key"; +Addsimps [parts_image_Key]; + + +(*In any message, there is an upper bound N on its greatest nonce.*) +Goal "\\N. \\n. N\\n --> Nonce n \\ parts {msg}"; +by (induct_tac "msg" 1); +by (ALLGOALS (asm_simp_tac (simpset() addsimps [exI, parts_insert2]))); +(*MPair case: blast_tac works out the necessary sum itself!*) +by (blast_tac (claset() addSEs [add_leE]) 2); +(*Nonce case*) +by (res_inst_tac [("x","N + Suc nat")] exI 1); +by (auto_tac (claset() addSEs [add_leE], simpset())); +qed "msg_Nonce_supply"; + + +(**** Inductive relation "analz" ****) + +val major::prems = +Goal "[| {|X,Y|} \\ analz H; \ +\ [| X \\ analz H; Y \\ analz H |] ==> P \ +\ |] ==> P"; +by (cut_facts_tac [major] 1); +by (resolve_tac prems 1); +by (REPEAT (eresolve_tac [asm_rl, analz.Fst, analz.Snd] 1)); +qed "MPair_analz"; + +AddSEs [MPair_analz]; (*Making it safe speeds up proofs*) + +Goal "H \\ analz(H)"; +by (Blast_tac 1); +qed "analz_increasing"; + +Goal "analz H \\ parts H"; +by (rtac subsetI 1); +by (etac analz.induct 1); +by (ALLGOALS Blast_tac); +qed "analz_subset_parts"; + +bind_thm ("not_parts_not_analz", analz_subset_parts RS contra_subsetD); + + +Goal "parts (analz H) = parts H"; +by (rtac equalityI 1); +by (rtac (analz_subset_parts RS parts_mono RS subset_trans) 1); +by (Simp_tac 1); +by (blast_tac (claset() addIs [analz_increasing RS parts_mono RS subsetD]) 1); +qed "parts_analz"; +Addsimps [parts_analz]; + +Goal "analz (parts H) = parts H"; +by Auto_tac; +by (etac analz.induct 1); +by Auto_tac; +qed "analz_parts"; +Addsimps [analz_parts]; + +bind_thm ("analz_insertI", impOfSubs (subset_insertI RS analz_mono)); + +(** General equational properties **) + +Goal "analz{} = {}"; +by Safe_tac; +by (etac analz.induct 1); +by (ALLGOALS Blast_tac); +qed "analz_empty"; +Addsimps [analz_empty]; + +(*Converse fails: we can analz more from the union than from the + separate parts, as a key in one might decrypt a message in the other*) +Goal "analz(G) Un analz(H) \\ analz(G Un H)"; +by (REPEAT (ares_tac [Un_least, analz_mono, Un_upper1, Un_upper2] 1)); +qed "analz_Un"; + +Goal "insert X (analz H) \\ analz(insert X H)"; +by (blast_tac (claset() addIs [impOfSubs analz_mono]) 1); +qed "analz_insert"; + +(** Rewrite rules for pulling out atomic messages **) + +fun analz_tac i = + EVERY [rtac ([subsetI, analz_insert] MRS equalityI) i, + etac analz.induct i, + Auto_tac]; + +Goal "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)"; +by (analz_tac 1); +qed "analz_insert_Agent"; + +Goal "analz (insert (Nonce N) H) = insert (Nonce N) (analz H)"; +by (analz_tac 1); +qed "analz_insert_Nonce"; + +Goal "analz (insert (Number N) H) = insert (Number N) (analz H)"; +by (analz_tac 1); +qed "analz_insert_Number"; + +Goal "analz (insert (Hash X) H) = insert (Hash X) (analz H)"; +by (analz_tac 1); +qed "analz_insert_Hash"; + +(*Can only pull out Keys if they are not needed to decrypt the rest*) +Goalw [keysFor_def] + "K \\ keysFor (analz H) ==> \ +\ analz (insert (Key K) H) = insert (Key K) (analz H)"; +by (analz_tac 1); +qed "analz_insert_Key"; + +Goal "analz (insert {|X,Y|} H) = \ +\ insert {|X,Y|} (analz (insert X (insert Y H)))"; +by (rtac equalityI 1); +by (rtac subsetI 1); +by (etac analz.induct 1); +by Auto_tac; +by (etac analz.induct 1); +by (ALLGOALS (blast_tac (claset() addIs [analz.Fst, analz.Snd]))); +qed "analz_insert_MPair"; + +(*Can pull out enCrypted message if the Key is not known*) +Goal "Key (invKey K) \\ analz H ==> \ +\ analz (insert (Crypt K X) H) = \ +\ insert (Crypt K X) (analz H)"; +by (analz_tac 1); +qed "analz_insert_Crypt"; + +Goal "Key (invKey K) \\ analz H ==> \ +\ analz (insert (Crypt K X) H) \\ \ +\ insert (Crypt K X) (analz (insert X H))"; +by (rtac subsetI 1); +by (eres_inst_tac [("xa","x")] analz.induct 1); +by Auto_tac; +val lemma1 = result(); + +Goal "Key (invKey K) \\ analz H ==> \ +\ insert (Crypt K X) (analz (insert X H)) \\ \ +\ analz (insert (Crypt K X) H)"; +by Auto_tac; +by (eres_inst_tac [("xa","x")] analz.induct 1); +by Auto_tac; +by (blast_tac (claset() addIs [analz_insertI, analz.Decrypt]) 1); +val lemma2 = result(); + +Goal "Key (invKey K) \\ analz H ==> \ +\ analz (insert (Crypt K X) H) = \ +\ insert (Crypt K X) (analz (insert X H))"; +by (REPEAT (ares_tac [equalityI, lemma1, lemma2] 1)); +qed "analz_insert_Decrypt"; + +(*Case analysis: either the message is secure, or it is not! + Effective, but can cause subgoals to blow up! + Use with split_if; apparently split_tac does not cope with patterns + such as "analz (insert (Crypt K X) H)" *) +Goal "analz (insert (Crypt K X) H) = \ +\ (if (Key (invKey K) \\ analz H) \ +\ then insert (Crypt K X) (analz (insert X H)) \ +\ else insert (Crypt K X) (analz H))"; +by (case_tac "Key (invKey K) \\ analz H " 1); +by (ALLGOALS (asm_simp_tac (simpset() addsimps [analz_insert_Crypt, + analz_insert_Decrypt]))); +qed "analz_Crypt_if"; + +Addsimps [analz_insert_Agent, analz_insert_Nonce, + analz_insert_Number, analz_insert_Key, + analz_insert_Hash, analz_insert_MPair, analz_Crypt_if]; + +(*This rule supposes "for the sake of argument" that we have the key.*) +Goal "analz (insert (Crypt K X) H) \\ \ +\ insert (Crypt K X) (analz (insert X H))"; +by (rtac subsetI 1); +by (etac analz.induct 1); +by Auto_tac; +qed "analz_insert_Crypt_subset"; + + +Goal "analz (Key`N) = Key`N"; +by Auto_tac; +by (etac analz.induct 1); +by Auto_tac; +qed "analz_image_Key"; + +Addsimps [analz_image_Key]; + + +(** Idempotence and transitivity **) + +Goal "X\\ analz (analz H) ==> X\\ analz H"; +by (etac analz.induct 1); +by (ALLGOALS Blast_tac); +qed "analz_analzD"; +AddSDs [analz_analzD]; + +Goal "analz (analz H) = analz H"; +by (Blast_tac 1); +qed "analz_idem"; +Addsimps [analz_idem]; + +Goal "[| X\\ analz G; G \\ analz H |] ==> X\\ analz H"; +by (dtac analz_mono 1); +by (Blast_tac 1); +qed "analz_trans"; + +(*Cut; Lemma 2 of Lowe*) +Goal "[| Y\\ analz (insert X H); X\\ analz H |] ==> Y\\ analz H"; +by (etac analz_trans 1); +by (Blast_tac 1); +qed "analz_cut"; + +(*Cut can be proved easily by induction on + "Y: analz (insert X H) ==> X: analz H --> Y: analz H" +*) + +(*This rewrite rule helps in the simplification of messages that involve + the forwarding of unknown components (X). Without it, removing occurrences + of X can be very complicated. *) +Goal "X\\ analz H ==> analz (insert X H) = analz H"; +by (blast_tac (claset() addIs [analz_cut, analz_insertI]) 1); +qed "analz_insert_eq"; + + +(** A congruence rule for "analz" **) + +Goal "[| analz G \\ analz G'; analz H \\ analz H' \ +\ |] ==> analz (G Un H) \\ analz (G' Un H')"; +by (Clarify_tac 1); +by (etac analz.induct 1); +by (ALLGOALS (best_tac (claset() addIs [analz_mono RS subsetD]))); +qed "analz_subset_cong"; + +Goal "[| analz G = analz G'; analz H = analz H' \ +\ |] ==> analz (G Un H) = analz (G' Un H')"; +by (REPEAT_FIRST (ares_tac [equalityI, analz_subset_cong] + ORELSE' etac equalityE)); +qed "analz_cong"; + + +Goal "analz H = analz H' ==> analz(insert X H) = analz(insert X H')"; +by (asm_simp_tac (simpset() addsimps [insert_def] delsimps [singleton_conv] + setloop (rtac analz_cong)) 1); +qed "analz_insert_cong"; + +(*If there are no pairs or encryptions then analz does nothing*) +Goal "[| \\X Y. {|X,Y|} \\ H; \\X K. Crypt K X \\ H |] ==> analz H = H"; +by Safe_tac; +by (etac analz.induct 1); +by (ALLGOALS Blast_tac); +qed "analz_trivial"; + +(*These two are obsolete (with a single Spy) but cost little to prove...*) +Goal "X\\ analz (\\i\\A. analz (H i)) ==> X\\ analz (\\i\\A. H i)"; +by (etac analz.induct 1); +by (ALLGOALS (blast_tac (claset() addIs [impOfSubs analz_mono]))); +val lemma = result(); + +Goal "analz (\\i\\A. analz (H i)) = analz (\\i\\A. H i)"; +by (blast_tac (claset() addIs [lemma, impOfSubs analz_mono]) 1); +qed "analz_UN_analz"; +Addsimps [analz_UN_analz]; + + +(**** Inductive relation "synth" ****) + +Goal "H \\ synth(H)"; +by (Blast_tac 1); +qed "synth_increasing"; + +(** Unions **) + +(*Converse fails: we can synth more from the union than from the + separate parts, building a compound message using elements of each.*) +Goal "synth(G) Un synth(H) \\ synth(G Un H)"; +by (REPEAT (ares_tac [Un_least, synth_mono, Un_upper1, Un_upper2] 1)); +qed "synth_Un"; + +Goal "insert X (synth H) \\ synth(insert X H)"; +by (blast_tac (claset() addIs [impOfSubs synth_mono]) 1); +qed "synth_insert"; + +(** Idempotence and transitivity **) + +Goal "X\\ synth (synth H) ==> X\\ synth H"; +by (etac synth.induct 1); +by (ALLGOALS Blast_tac); +qed "synth_synthD"; +AddSDs [synth_synthD]; + +Goal "synth (synth H) = synth H"; +by (Blast_tac 1); +qed "synth_idem"; + +Goal "[| X\\ synth G; G \\ synth H |] ==> X\\ synth H"; +by (dtac synth_mono 1); +by (Blast_tac 1); +qed "synth_trans"; + +(*Cut; Lemma 2 of Lowe*) +Goal "[| Y\\ synth (insert X H); X\\ synth H |] ==> Y\\ synth H"; +by (etac synth_trans 1); +by (Blast_tac 1); +qed "synth_cut"; + +Goal "Agent A \\ synth H"; +by (Blast_tac 1); +qed "Agent_synth"; + +Goal "Number n \\ synth H"; +by (Blast_tac 1); +qed "Number_synth"; + +Goal "(Nonce N \\ synth H) = (Nonce N \\ H)"; +by (Blast_tac 1); +qed "Nonce_synth_eq"; + +Goal "(Key K \\ synth H) = (Key K \\ H)"; +by (Blast_tac 1); +qed "Key_synth_eq"; + +Goal "Key K \\ H ==> (Crypt K X \\ synth H) = (Crypt K X \\ H)"; +by (Blast_tac 1); +qed "Crypt_synth_eq"; + +Addsimps [Agent_synth, Number_synth, + Nonce_synth_eq, Key_synth_eq, Crypt_synth_eq]; + + +Goalw [keysFor_def] + "keysFor (synth H) = keysFor H Un invKey`{K. Key K \\ H}"; +by (Blast_tac 1); +qed "keysFor_synth"; +Addsimps [keysFor_synth]; + + +(*** Combinations of parts, analz and synth ***) + +Goal "parts (synth H) = parts H Un synth H"; +by (rtac equalityI 1); +by (rtac subsetI 1); +by (etac parts.induct 1); +by (ALLGOALS + (blast_tac (claset() addIs [synth_increasing RS parts_mono RS subsetD, + parts.Fst, parts.Snd, parts.Body]))); +qed "parts_synth"; +Addsimps [parts_synth]; + +Goal "analz (analz G Un H) = analz (G Un H)"; +by (REPEAT_FIRST (resolve_tac [equalityI, analz_subset_cong])); +by (ALLGOALS Simp_tac); +qed "analz_analz_Un"; + +Goal "analz (synth G Un H) = analz (G Un H) Un synth G"; +by (rtac equalityI 1); +by (rtac subsetI 1); +by (etac analz.induct 1); +by (blast_tac (claset() addIs [impOfSubs analz_mono]) 5); +by (ALLGOALS + (blast_tac (claset() addIs [analz.Fst, analz.Snd, analz.Decrypt]))); +qed "analz_synth_Un"; + +Goal "analz (synth H) = analz H Un synth H"; +by (cut_inst_tac [("H","{}")] analz_synth_Un 1); +by (Full_simp_tac 1); +qed "analz_synth"; +Addsimps [analz_analz_Un, analz_synth_Un, analz_synth]; + + +(** For reasoning about the Fake rule in traces **) + +Goal "X\\ G ==> parts(insert X H) \\ parts G Un parts H"; +by (rtac ([parts_mono, parts_Un_subset2] MRS subset_trans) 1); +by (Blast_tac 1); +qed "parts_insert_subset_Un"; + +(*More specifically for Fake. Very occasionally we could do with a version + of the form parts{X} \\ synth (analz H) Un parts H *) +Goal "X\\ synth (analz H) ==> \ +\ parts (insert X H) \\ synth (analz H) Un parts H"; +by (dtac parts_insert_subset_Un 1); +by (Full_simp_tac 1); +by (Blast_tac 1); +qed "Fake_parts_insert"; + +(*H is sometimes (Key ` KK Un spies evs), so can't put G=H*) +Goal "X\\ synth (analz G) ==> \ +\ analz (insert X H) \\ synth (analz G) Un analz (G Un H)"; +by (rtac subsetI 1); +by (subgoal_tac "x \\ analz (synth (analz G) Un H)" 1); +by (blast_tac (claset() addIs [impOfSubs analz_mono, + impOfSubs (analz_mono RS synth_mono)]) 2); +by (Full_simp_tac 1); +by (Blast_tac 1); +qed "Fake_analz_insert"; + +Goal "(X\\ analz H & X\\ parts H) = (X\\ analz H)"; +by (blast_tac (claset() addIs [impOfSubs analz_subset_parts]) 1); +val analz_conj_parts = result(); + +Goal "(X\\ analz H | X\\ parts H) = (X\\ parts H)"; +by (blast_tac (claset() addIs [impOfSubs analz_subset_parts]) 1); +val analz_disj_parts = result(); + +AddIffs [analz_conj_parts, analz_disj_parts]; + +(*Without this equation, other rules for synth and analz would yield + redundant cases*) +Goal "({|X,Y|} \\ synth (analz H)) = \ +\ (X \\ synth (analz H) & Y \\ synth (analz H))"; +by (Blast_tac 1); +qed "MPair_synth_analz"; + +AddIffs [MPair_synth_analz]; + +Goal "[| Key K \\ analz H; Key (invKey K) \\ analz H |] \ +\ ==> (Crypt K X \\ synth (analz H)) = (X \\ synth (analz H))"; +by (Blast_tac 1); +qed "Crypt_synth_analz"; + + +Goal "X \\ synth (analz H) \ +\ ==> (Hash{|X,Y|} \\ synth (analz H)) = (Hash{|X,Y|} \\ analz H)"; +by (Blast_tac 1); +qed "Hash_synth_analz"; +Addsimps [Hash_synth_analz]; + + +(**** HPair: a combination of Hash and MPair ****) + +(*** Freeness ***) + +Goalw [HPair_def] "Agent A ~= Hash[X] Y"; +by (Simp_tac 1); +qed "Agent_neq_HPair"; + +Goalw [HPair_def] "Nonce N ~= Hash[X] Y"; +by (Simp_tac 1); +qed "Nonce_neq_HPair"; + +Goalw [HPair_def] "Number N ~= Hash[X] Y"; +by (Simp_tac 1); +qed "Number_neq_HPair"; + +Goalw [HPair_def] "Key K ~= Hash[X] Y"; +by (Simp_tac 1); +qed "Key_neq_HPair"; + +Goalw [HPair_def] "Hash Z ~= Hash[X] Y"; +by (Simp_tac 1); +qed "Hash_neq_HPair"; + +Goalw [HPair_def] "Crypt K X' ~= Hash[X] Y"; +by (Simp_tac 1); +qed "Crypt_neq_HPair"; + +val HPair_neqs = [Agent_neq_HPair, Nonce_neq_HPair, Number_neq_HPair, + Key_neq_HPair, Hash_neq_HPair, Crypt_neq_HPair]; + +AddIffs HPair_neqs; +AddIffs (HPair_neqs RL [not_sym]); + +Goalw [HPair_def] "(Hash[X'] Y' = Hash[X] Y) = (X' = X & Y'=Y)"; +by (Simp_tac 1); +qed "HPair_eq"; + +Goalw [HPair_def] "({|X',Y'|} = Hash[X] Y) = (X' = Hash{|X,Y|} & Y'=Y)"; +by (Simp_tac 1); +qed "MPair_eq_HPair"; + +Goalw [HPair_def] "(Hash[X] Y = {|X',Y'|}) = (X' = Hash{|X,Y|} & Y'=Y)"; +by Auto_tac; +qed "HPair_eq_MPair"; + +AddIffs [HPair_eq, MPair_eq_HPair, HPair_eq_MPair]; + + +(*** Specialized laws, proved in terms of those for Hash and MPair ***) + +Goalw [HPair_def] "keysFor (insert (Hash[X] Y) H) = keysFor H"; +by (Simp_tac 1); +qed "keysFor_insert_HPair"; + +Goalw [HPair_def] + "parts (insert (Hash[X] Y) H) = \ +\ insert (Hash[X] Y) (insert (Hash{|X,Y|}) (parts (insert Y H)))"; +by (Simp_tac 1); +qed "parts_insert_HPair"; + +Goalw [HPair_def] + "analz (insert (Hash[X] Y) H) = \ +\ insert (Hash[X] Y) (insert (Hash{|X,Y|}) (analz (insert Y H)))"; +by (Simp_tac 1); +qed "analz_insert_HPair"; + +Goalw [HPair_def] "X \\ synth (analz H) \ +\ ==> (Hash[X] Y \\ synth (analz H)) = \ +\ (Hash {|X, Y|} \\ analz H & Y \\ synth (analz H))"; +by (Simp_tac 1); +by (Blast_tac 1); +qed "HPair_synth_analz"; + +Addsimps [keysFor_insert_HPair, parts_insert_HPair, analz_insert_HPair, + HPair_synth_analz, HPair_synth_analz]; + + +(*We do NOT want Crypt... messages broken up in protocols!!*) +Delrules [make_elim parts.Body]; + + +(** Rewrites to push in Key and Crypt messages, so that other messages can + be pulled out using the analz_insert rules **) + +fun insComm x y = inst "x" x (inst "y" y insert_commute); + +val pushKeys = map (insComm "Key ?K") + ["Agent ?C", "Nonce ?N", "Number ?N", + "Hash ?X", "MPair ?X ?Y", "Crypt ?X ?K'"]; + +val pushCrypts = map (insComm "Crypt ?X ?K") + ["Agent ?C", "Nonce ?N", "Number ?N", + "Hash ?X'", "MPair ?X' ?Y"]; + +(*Cannot be added with Addsimps -- we don't always want to re-order messages*) +bind_thms ("pushes", pushKeys@pushCrypts); + + +(*** Tactics useful for many protocol proofs ***) + +(*Prove base case (subgoal i) and simplify others. A typical base case + concerns Crypt K X \\ Key`shrK`bad and cannot be proved by rewriting + alone.*) +fun prove_simple_subgoals_tac i = + force_tac (claset(), simpset() addsimps [image_eq_UN]) i THEN + ALLGOALS Asm_simp_tac; + +fun Fake_parts_insert_tac i = + blast_tac (claset() addIs [parts_insertI] + addDs [impOfSubs analz_subset_parts, + impOfSubs Fake_parts_insert]) i; + +(*Apply rules to break down assumptions of the form + Y \\ parts(insert X H) and Y \\ analz(insert X H) +*) +val Fake_insert_tac = + dresolve_tac [impOfSubs Fake_analz_insert, + impOfSubs Fake_parts_insert] THEN' + eresolve_tac [asm_rl, synth.Inj]; + +fun Fake_insert_simp_tac i = + REPEAT (Fake_insert_tac i) THEN Asm_full_simp_tac i; + + +(*Analysis of Fake cases. Also works for messages that forward unknown parts, + but this application is no longer necessary if analz_insert_eq is used. + Abstraction over i is ESSENTIAL: it delays the dereferencing of claset + DEPENDS UPON "X" REFERRING TO THE FRADULENT MESSAGE *) + +val atomic_spy_analz_tac = SELECT_GOAL + (Fake_insert_simp_tac 1 + THEN + IF_UNSOLVED (Blast.depth_tac + (claset() addIs [analz_insertI, + impOfSubs analz_subset_parts]) 4 1)); + +fun spy_analz_tac i = + DETERM + (SELECT_GOAL + (EVERY + [ (*push in occurrences of X...*) + (REPEAT o CHANGED) + (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1), + (*...allowing further simplifications*) + Simp_tac 1, + REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])), + DEPTH_SOLVE (atomic_spy_analz_tac 1)]) i); + +(*By default only o_apply is built-in. But in the presence of eta-expansion + this means that some terms displayed as (f o g) will be rewritten, and others + will not!*) +Addsimps [o_def]; diff -r a0e3c67c1394 -r c8bbf4c4bc2d doc-src/TutorialI/Protocol/NS_Public.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/TutorialI/Protocol/NS_Public.thy Wed Apr 11 11:53:54 2001 +0200 @@ -0,0 +1,203 @@ +(* Title: HOL/Auth/NS_Public + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1996 University of Cambridge + +Inductive relation "ns_public" for the Needham-Schroeder Public-Key protocol. +Version incorporating Lowe's fix (inclusion of B's identity in round 2). +*) + +theory NS_Public = Public: + +consts ns_public :: "event list set" + +inductive ns_public + intros + (*Initial trace is empty*) + Nil: "[] \ ns_public" + + (*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 \ ns_public; X \ synth (analz (spies evs))\ + \ Says Spy B X # evs \ ns_public" + + (*Alice initiates a protocol run, sending a nonce to Bob*) + NS1: "\evs1 \ ns_public; Nonce NA \ used evs1\ + \ Says A B (Crypt (pubK B) \Nonce NA, Agent A\) + # evs1 \ ns_public" + + (*Bob responds to Alice's message with a further nonce*) + NS2: "\evs2 \ ns_public; Nonce NB \ used evs2; + Says A' B (Crypt (pubK B) \Nonce NA, Agent A\) \ set evs2\ + \ Says B A (Crypt (pubK A) \Nonce NA, Nonce NB, Agent B\) + # evs2 \ ns_public" + + (*Alice proves her existence by sending NB back to Bob.*) + NS3: "\evs3 \ ns_public; + Says A B (Crypt (pubK B) \Nonce NA, Agent A\) \ set evs3; + Says B' A (Crypt (pubK A) \Nonce NA, Nonce NB, Agent B\) + \ set evs3\ + \ Says A B (Crypt (pubK B) (Nonce NB)) # evs3 \ ns_public" + +declare knows_Spy_partsEs [elim] +declare analz_subset_parts [THEN subsetD, dest] +declare Fake_parts_insert [THEN subsetD, dest] +declare image_eq_UN [simp] (*accelerates proofs involving nested images*) + +(*A "possibility property": there are traces that reach the end*) +lemma "\NB. \evs \ ns_public. Says A B (Crypt (pubK B) (Nonce NB)) \ set evs" +apply (intro exI bexI) +apply (rule_tac [2] ns_public.Nil [THEN ns_public.NS1, THEN ns_public.NS2, + THEN ns_public.NS3]) +by possibility + + +(**** Inductive proofs about ns_public ****) + +(** Theorems of the form X \ parts (spies evs) imply that NOBODY + sends messages containing X! **) + +(*Spy never sees another agent's private key! (unless it's bad at start)*) +lemma Spy_see_priK [simp]: + "evs \ ns_public \ (Key (priK A) \ parts (spies evs)) = (A \ bad)" +by (erule ns_public.induct, auto) + +lemma Spy_analz_priK [simp]: + "evs \ ns_public \ (Key (priK A) \ analz (spies evs)) = (A \ bad)" +by auto + + +(*** Authenticity properties obtained from NS2 ***) + + +(*It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce + is secret. (Honest users generate fresh nonces.)*) +lemma no_nonce_NS1_NS2 [rule_format]: + "evs \ ns_public + \ Crypt (pubK C) \NA', Nonce NA, Agent D\ \ parts (spies evs) \ + Crypt (pubK B) \Nonce NA, Agent A\ \ parts (spies evs) \ + Nonce NA \ analz (spies evs)" +apply (erule ns_public.induct, simp_all) +apply (blast intro: analz_insertI)+ +done + +(*Unicity for NS1: nonce NA identifies agents A and B*) +lemma unique_NA: + "\Crypt(pubK B) \Nonce NA, Agent A \ \ parts(spies evs); + Crypt(pubK B') \Nonce NA, Agent A'\ \ parts(spies evs); + Nonce NA \ analz (spies evs); evs \ ns_public\ + \ A=A' \ B=B'" +apply (erule rev_mp, erule rev_mp, erule rev_mp) +apply (erule ns_public.induct, simp_all) +(*Fake, NS1*) +apply (blast intro: analz_insertI)+ +done + + +(*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure + The major premise "Says A B ..." makes it a dest-rule, so we use + (erule rev_mp) rather than rule_format. *) +theorem Spy_not_see_NA: + "\Says A B (Crypt(pubK B) \Nonce NA, Agent A\) \ set evs; + A \ bad; B \ bad; evs \ ns_public\ + \ Nonce NA \ analz (spies evs)" +apply (erule rev_mp) +apply (erule ns_public.induct, simp_all) +apply spy_analz +apply (blast dest: unique_NA intro: no_nonce_NS1_NS2)+ +done + + +(*Authentication for A: if she receives message 2 and has used NA + to start a run, then B has sent message 2.*) +lemma A_trusts_NS2_lemma [rule_format]: + "\A \ bad; B \ bad; evs \ ns_public\ + \ Crypt (pubK A) \Nonce NA, Nonce NB, Agent B\ \ parts (spies evs) \ + Says A B (Crypt(pubK B) \Nonce NA, Agent A\) \ set evs \ + Says B A (Crypt(pubK A) \Nonce NA, Nonce NB, Agent B\) \ set evs" +apply (erule ns_public.induct, simp_all) +(*Fake, NS1*) +apply (blast dest: Spy_not_see_NA)+ +done + +theorem A_trusts_NS2: + "\Says A B (Crypt(pubK B) \Nonce NA, Agent A\) \ set evs; + Says B' A (Crypt(pubK A) \Nonce NA, Nonce NB, Agent B\) \ set evs; + A \ bad; B \ bad; evs \ ns_public\ + \ Says B A (Crypt(pubK A) \Nonce NA, Nonce NB, Agent B\) \ set evs" +by (blast intro: A_trusts_NS2_lemma) + + +(*If the encrypted message appears then it originated with Alice in NS1*) +lemma B_trusts_NS1 [rule_format]: + "evs \ ns_public + \ Crypt (pubK B) \Nonce NA, Agent A\ \ parts (spies evs) \ + Nonce NA \ analz (spies evs) \ + Says A B (Crypt (pubK B) \Nonce NA, Agent A\) \ set evs" +apply (erule ns_public.induct, simp_all) +(*Fake*) +apply (blast intro!: analz_insertI) +done + + + +(*** Authenticity properties obtained from NS2 ***) + +(*Unicity for NS2: nonce NB identifies nonce NA and agents A, B + [unicity of B makes Lowe's fix work] + [proof closely follows that for unique_NA] *) + +lemma unique_NB [dest]: + "\Crypt(pubK A) \Nonce NA, Nonce NB, Agent B\ \ parts(spies evs); + Crypt(pubK A') \Nonce NA', Nonce NB, Agent B'\ \ parts(spies evs); + Nonce NB \ analz (spies evs); evs \ ns_public\ + \ A=A' \ NA=NA' \ B=B'" +apply (erule rev_mp, erule rev_mp, erule rev_mp) +apply (erule ns_public.induct, simp_all) +(*Fake, NS2*) +apply (blast intro: analz_insertI)+ +done + + +(*Secrecy: Spy does not see the nonce sent in msg NS2 if A and B are secure*) +theorem Spy_not_see_NB [dest]: + "\Says B A (Crypt (pubK A) \Nonce NA, Nonce NB, Agent B\) \ set evs; + A \ bad; B \ bad; evs \ ns_public\ + \ Nonce NB \ analz (spies evs)" +apply (erule rev_mp) +apply (erule ns_public.induct, simp_all) +apply spy_analz +apply (blast intro: no_nonce_NS1_NS2)+ +done + + +(*Authentication for B: if he receives message 3 and has used NB + in message 2, then A has sent message 3.*) +lemma B_trusts_NS3_lemma [rule_format]: + "\A \ bad; B \ bad; evs \ ns_public\ \ + Crypt (pubK B) (Nonce NB) \ parts (spies evs) \ + Says B A (Crypt (pubK A) \Nonce NA, Nonce NB, Agent B\) \ set evs \ + Says A B (Crypt (pubK B) (Nonce NB)) \ set evs" +by (erule ns_public.induct, auto) + +theorem B_trusts_NS3: + "\Says B A (Crypt (pubK A) \Nonce NA, Nonce NB, Agent B\) \ set evs; + Says A' B (Crypt (pubK B) (Nonce NB)) \ set evs; + A \ bad; B \ bad; evs \ ns_public\ + \ Says A B (Crypt (pubK B) (Nonce NB)) \ set evs" +by (blast intro: B_trusts_NS3_lemma) + +(*** Overall guarantee for B ***) + + +(*If NS3 has been sent and the nonce NB agrees with the nonce B joined with + NA, then A initiated the run using NA.*) +theorem B_trusts_protocol: + "\A \ bad; B \ bad; evs \ ns_public\ \ + Crypt (pubK B) (Nonce NB) \ parts (spies evs) \ + Says B A (Crypt (pubK A) \Nonce NA, Nonce NB, Agent B\) \ set evs \ + Says A B (Crypt (pubK B) \Nonce NA, Agent A\) \ set evs" +by (erule ns_public.induct, auto) + +end diff -r a0e3c67c1394 -r c8bbf4c4bc2d doc-src/TutorialI/Protocol/Public.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/TutorialI/Protocol/Public.thy Wed Apr 11 11:53:54 2001 +0200 @@ -0,0 +1,46 @@ +(* Title: HOL/Auth/Public + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1996 University of Cambridge + +Theory of Public Keys (common to all public-key protocols) + +Private and public keys; initial states of agents +*) + +theory Public = Event +files ("Public_lemmas.ML"): + +consts + pubK :: "agent => key" + +syntax + priK :: "agent => key" + +translations (*BEWARE! expressions like (inj priK) will NOT work!*) + "priK x" == "invKey(pubK x)" + +primrec + (*Agents know their private key and all public keys*) + initState_Server: "initState Server = + insert (Key (priK Server)) (Key ` range pubK)" + initState_Friend: "initState (Friend i) = + insert (Key (priK (Friend i))) (Key ` range pubK)" + initState_Spy: "initState Spy = + (Key`invKey`pubK`bad) Un (Key ` range pubK)" + + +axioms + (*Public keys are disjoint, and never clash with private keys*) + inj_pubK: "inj pubK" + priK_neq_pubK: "priK A ~= pubK B" + +use "Public_lemmas.ML" + +(*Specialized methods*) + +method_setup possibility = {* + Method.no_args (Method.METHOD (fn facts => possibility_tac)) *} + "for proving possibility theorems" + +end diff -r a0e3c67c1394 -r c8bbf4c4bc2d doc-src/TutorialI/Protocol/Public_lemmas.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/TutorialI/Protocol/Public_lemmas.ML Wed Apr 11 11:53:54 2001 +0200 @@ -0,0 +1,170 @@ +(* Title: HOL/Auth/Public_lemmas + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1996 University of Cambridge + +Theory of Public Keys (common to all symmetric-key protocols) + +Server keys; initial states of agents; new nonces and keys; function "sees" +*) + +val inj_pubK = thm "inj_pubK"; +val priK_neq_pubK = thm "priK_neq_pubK"; + +(*** Basic properties of pubK & priK ***) + +AddIffs [inj_pubK RS inj_eq]; + +Goal "(priK A = priK B) = (A=B)"; +by Safe_tac; +by (dres_inst_tac [("f","invKey")] arg_cong 1); +by (Full_simp_tac 1); +qed "priK_inj_eq"; + +AddIffs [priK_inj_eq]; +AddIffs [priK_neq_pubK, priK_neq_pubK RS not_sym]; + +Goalw [symKeys_def] "pubK A \\ symKeys"; +by (Simp_tac 1); +qed "not_symKeys_pubK"; + +Goalw [symKeys_def] "priK A \\ symKeys"; +by (Simp_tac 1); +qed "not_symKeys_priK"; + +AddIffs [not_symKeys_pubK, not_symKeys_priK]; + +Goal "(K \\ symKeys) \\ (K' \\ symKeys) ==> K \\ K'"; +by (Blast_tac 1); +qed "symKeys_neq_imp_neq"; + +Goal "[| Crypt K X \\ analz H; K \\ symKeys; Key K \\ analz H |] \ +\ ==> X \\ analz H"; +by (auto_tac(claset(), simpset() addsimps [symKeys_def])); +qed "analz_symKeys_Decrypt"; + + +(** "Image" equations that hold for injective functions **) + +Goal "(invKey x : invKey`A) = (x:A)"; +by Auto_tac; +qed "invKey_image_eq"; + +(*holds because invKey is injective*) +Goal "(pubK x : pubK`A) = (x:A)"; +by Auto_tac; +qed "pubK_image_eq"; + +Goal "(priK x ~: pubK`A)"; +by Auto_tac; +qed "priK_pubK_image_eq"; +Addsimps [invKey_image_eq, pubK_image_eq, priK_pubK_image_eq]; + + +(** Rewrites should not refer to initState(Friend i) + -- not in normal form! **) + +Goalw [keysFor_def] "keysFor (parts (initState C)) = {}"; +by (induct_tac "C" 1); +by (auto_tac (claset() addIs [range_eqI], simpset())); +qed "keysFor_parts_initState"; +Addsimps [keysFor_parts_initState]; + + +(*** Function "spies" ***) + +(*Agents see their own private keys!*) +Goal "Key (priK A) : initState A"; +by (induct_tac "A" 1); +by Auto_tac; +qed "priK_in_initState"; +AddIffs [priK_in_initState]; + +(*All public keys are visible*) +Goal "Key (pubK A) : spies evs"; +by (induct_tac "evs" 1); +by (ALLGOALS (asm_simp_tac + (simpset() addsimps [imageI, knows_Cons] + addsplits [expand_event_case]))); +qed_spec_mp "spies_pubK"; + +(*Spy sees private keys of bad agents!*) +Goal "A: bad ==> Key (priK A) : spies evs"; +by (induct_tac "evs" 1); +by (ALLGOALS (asm_simp_tac + (simpset() addsimps [imageI, knows_Cons] + addsplits [expand_event_case]))); +qed "Spy_spies_bad"; + +AddIffs [spies_pubK, spies_pubK RS analz.Inj]; +AddSIs [Spy_spies_bad]; + + +(*** Fresh nonces ***) + +Goal "Nonce N ~: parts (initState B)"; +by (induct_tac "B" 1); +by Auto_tac; +qed "Nonce_notin_initState"; +AddIffs [Nonce_notin_initState]; + +Goal "Nonce N ~: used []"; +by (simp_tac (simpset() addsimps [used_Nil]) 1); +qed "Nonce_notin_used_empty"; +Addsimps [Nonce_notin_used_empty]; + + +(*** Supply fresh nonces for possibility theorems. ***) + +(*In any trace, there is an upper bound N on the greatest nonce in use.*) +Goal "EX N. ALL n. N<=n --> Nonce n ~: used evs"; +by (induct_tac "evs" 1); +by (res_inst_tac [("x","0")] exI 1); +by (ALLGOALS (asm_simp_tac + (simpset() addsimps [used_Cons] + addsplits [expand_event_case]))); +by Safe_tac; +by (ALLGOALS (rtac (msg_Nonce_supply RS exE))); +by (ALLGOALS (blast_tac (claset() addSEs [add_leE]))); +val lemma = result(); + +Goal "EX N. Nonce N ~: used evs"; +by (rtac (lemma RS exE) 1); +by (Blast_tac 1); +qed "Nonce_supply1"; + +Goal "Nonce (@ N. Nonce N ~: used evs) ~: used evs"; +by (rtac (lemma RS exE) 1); +by (rtac someI 1); +by (Fast_tac 1); +qed "Nonce_supply"; + +(*Tactic for possibility theorems*) +fun possibility_tac st = st |> + REPEAT (*omit used_Says so that Nonces start from different traces!*) + (ALLGOALS (simp_tac (simpset() delsimps [used_Says])) + THEN + REPEAT_FIRST (eq_assume_tac ORELSE' + resolve_tac [refl, conjI, Nonce_supply])); + + +(*** Specialized rewriting for the analz_image_... theorems ***) + +Goal "insert (Key K) H = Key ` {K} Un H"; +by (Blast_tac 1); +qed "insert_Key_singleton"; + +Goal "insert (Key K) (Key`KK Un C) = Key ` (insert K KK) Un C"; +by (Blast_tac 1); +qed "insert_Key_image"; + +(*Reverse the normal simplification of "image" to build up (not break down) + the set of keys. Based on analz_image_freshK_ss, but simpler.*) +val analz_image_keys_ss = + simpset() delsimps [image_insert, image_Un] + delsimps [imp_disjL] (*reduces blow-up*) + addsimps [image_insert RS sym, image_Un RS sym, + rangeI, + insert_Key_singleton, + insert_Key_image, Un_assoc RS sym]; +