src/HOL/Auth/Guard/Extensions.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Auth/Guard/Extensions.thy	Wed Aug 21 15:53:30 2002 +0200
@@ -0,0 +1,652 @@
+(******************************************************************************
+date: november 2001
+author: Frederic Blanqui
+email: [e-mail]
+webpage: http://www.lri.fr/~blanqui/
+
+University of Cambridge, Computer Laboratory
+William Gates Building, JJ Thomson Avenue
+Cambridge CB3 0FD, United Kingdom
+******************************************************************************)
+
+header {*Extensions to Standard Theories*}
+
+theory Extensions = Event:
+
+
+subsection{*Extensions to Theory @{text Set}*}
+
+lemma eq: "[| !!x. x:A ==> x:B; !!x. x:B ==> x:A |] ==> A=B"
+by auto
+
+lemma Un_eq: "[| A=A'; B=B' |] ==> A Un B = A' Un B'"
+by auto
+
+lemma insert_absorb_substI: "[| x:A; P (insert x A) |] ==> P A"
+by (simp add: insert_absorb)
+
+lemma insert_Diff_substD: "[| x:A; P A |] ==> P (insert x (A - {x}))"
+by (simp add: insert_Diff)
+
+lemma insert_Diff_substI: "[| x:A; P (insert x (A - {x})) |] ==> P A"
+by (simp add: insert_Diff)
+
+lemma insert_Un: "P ({x} Un A) ==> P (insert x A)"
+by simp
+
+lemma in_sub: "x:A ==> {x}<=A"
+by auto
+
+
+subsection{*Extensions to Theory @{text List}*}
+
+subsubsection{*"minus l x" erase the first element of "l" equal to "x"*}
+
+consts minus :: "'a list => 'a => 'a list"
+
+primrec
+"minus [] y = []"
+"minus (x#xs) y = (if x=y then xs else x # minus xs y)"
+
+lemma set_minus: "set (minus l x) <= set l"
+by (induct l, auto)
+
+subsection{*Extensions to Theory @{text Message}*}
+
+subsubsection{*declarations for tactics*}
+
+declare analz_subset_parts [THEN subsetD, dest]
+declare image_eq_UN [simp]
+declare parts_insert2 [simp]
+declare analz_cut [dest]
+declare split_if_asm [split]
+declare analz_insertI [intro]
+declare Un_Diff [simp]
+
+subsubsection{*extract the agent number of an Agent message*}
+
+consts agt_nb :: "msg => agent"
+
+recdef agt_nb "measure size"
+"agt_nb (Agent A) = A"
+
+subsubsection{*messages that are pairs*}
+
+constdefs is_MPair :: "msg => bool"
+"is_MPair X == EX Y Z. X = {|Y,Z|}"
+
+declare is_MPair_def [simp]
+
+lemma MPair_is_MPair [iff]: "is_MPair {|X,Y|}"
+by simp
+
+lemma Agent_isnt_MPair [iff]: "~ is_MPair (Agent A)"
+by simp
+
+lemma Number_isnt_MPair [iff]: "~ is_MPair (Number n)"
+by simp
+
+lemma Key_isnt_MPair [iff]: "~ is_MPair (Key K)"
+by simp
+
+lemma Nonce_isnt_MPair [iff]: "~ is_MPair (Nonce n)"
+by simp
+
+lemma Hash_isnt_MPair [iff]: "~ is_MPair (Hash X)"
+by simp
+
+lemma Crypt_isnt_MPair [iff]: "~ is_MPair (Crypt K X)"
+by simp
+
+syntax not_MPair :: "msg => bool"
+
+translations "not_MPair X" == "~ is_MPair X"
+
+lemma is_MPairE: "[| is_MPair X ==> P; not_MPair X ==> P |] ==> P"
+by auto
+
+declare is_MPair_def [simp del]
+
+constdefs has_no_pair :: "msg set => bool"
+"has_no_pair H == ALL X Y. {|X,Y|} ~:H"
+
+declare has_no_pair_def [simp]
+
+subsubsection{*well-foundedness of messages*}
+
+lemma wf_Crypt1 [iff]: "Crypt K X ~= X"
+by (induct X, auto)
+
+lemma wf_Crypt2 [iff]: "X ~= Crypt K X"
+by (induct X, auto)
+
+lemma parts_size: "X:parts {Y} ==> X=Y | size X < size Y"
+by (erule parts.induct, auto)
+
+lemma wf_Crypt_parts [iff]: "Crypt K X ~:parts {X}"
+by (auto dest: parts_size)
+
+subsubsection{*lemmas on keysFor*}
+
+constdefs usekeys :: "msg set => key set"
+"usekeys G == {K. EX Y. Crypt K Y:G}"
+
+lemma finite_keysFor [intro]: "finite G ==> finite (keysFor G)"
+apply (simp add: keysFor_def)
+apply (rule finite_UN_I, auto)
+apply (erule finite_induct, auto)
+apply (case_tac "EX K X. x = Crypt K X", clarsimp)
+apply (subgoal_tac "{Ka. EX Xa. (Ka=K & Xa=X) | Crypt Ka Xa:F}
+= insert K (usekeys F)", auto simp: usekeys_def)
+by (subgoal_tac "{K. EX X. Crypt K X = x | Crypt K X:F} = usekeys F",
+auto simp: usekeys_def)
+
+subsubsection{*lemmas on parts*}
+
+lemma parts_sub: "[| X:parts G; G<=H |] ==> X:parts H"
+by (auto dest: parts_mono)
+
+lemma parts_Diff [dest]: "X:parts (G - H) ==> X:parts G"
+by (erule parts_sub, auto)
+
+lemma parts_Diff_notin: "[| Y ~:H; Nonce n ~:parts (H - {Y}) |]
+==> Nonce n ~:parts H"
+by simp
+
+lemmas parts_insert_substI = parts_insert [THEN ssubst]
+lemmas parts_insert_substD = parts_insert [THEN sym, THEN ssubst]
+
+lemma finite_parts_msg [iff]: "finite (parts {X})"
+by (induct X, auto)
+
+lemma finite_parts [intro]: "finite H ==> finite (parts H)"
+apply (erule finite_induct, simp)
+by (rule parts_insert_substI, simp)
+
+lemma parts_parts: "[| X:parts {Y}; Y:parts G |] ==> X:parts G"
+by (drule_tac x=Y in in_sub, drule parts_mono, auto)
+
+lemma parts_parts_parts: "[| X:parts {Y}; Y:parts {Z}; Z:parts G |] ==> X:parts G"
+by (auto dest: parts_parts)
+
+lemma parts_parts_Crypt: "[| Crypt K X:parts G; Nonce n:parts {X} |]
+==> Nonce n:parts G"
+by (blast intro: parts.Body dest: parts_parts)
+
+subsubsection{*lemmas on synth*}
+
+lemma synth_sub: "[| X:synth G; G<=H |] ==> X:synth H"
+by (auto dest: synth_mono)
+
+lemma Crypt_synth [rule_format]: "[| X:synth G; Key K ~:G |] ==>
+Crypt K Y:parts {X} --> Crypt K Y:parts G"
+by (erule synth.induct, auto dest: parts_sub)
+
+subsubsection{*lemmas on analz*}
+
+lemma analz_UnI1 [intro]: "X:analz G ==> X:analz (G Un H)"
+by (subgoal_tac "G <= G Un H", auto dest: analz_mono)
+
+lemma analz_sub: "[| X:analz G; G <= H |] ==> X:analz H"
+by (auto dest: analz_mono)
+
+lemma analz_Diff [dest]: "X:analz (G - H) ==> X:analz G"
+by (erule analz.induct, auto)
+
+lemmas in_analz_subset_cong = analz_subset_cong [THEN subsetD]
+
+lemma analz_eq: "A=A' ==> analz A = analz A'"
+by auto
+
+lemmas insert_commute_substI = insert_commute [THEN ssubst]
+
+lemma analz_insertD: "[| Crypt K Y:H; Key (invKey K):H |]
+==> analz (insert Y H) = analz H"
+apply (rule_tac x="Crypt K Y" and P="%H. analz (insert Y H) = analz H"
+in insert_absorb_substI, simp)
+by (rule_tac insert_commute_substI, simp)
+
+lemma must_decrypt [rule_format,dest]: "[| X:analz H; has_no_pair H |] ==>
+X ~:H --> (EX K Y. Crypt K Y:H & Key (invKey K):H)"
+by (erule analz.induct, auto)
+
+lemma analz_needs_only_finite: "X:analz H ==> EX G. G <= H & finite G"
+by (erule analz.induct, auto)
+
+lemma notin_analz_insert: "X ~:analz (insert Y G) ==> X ~:analz G"
+by auto
+
+subsubsection{*lemmas on parts, synth and analz*}
+
+lemma parts_invKey [rule_format,dest]:"X:parts {Y} ==>
+X:analz (insert (Crypt K Y) H) --> X ~:analz H --> Key (invKey K):analz H"
+by (erule parts.induct, auto dest: parts.Fst parts.Snd parts.Body)
+
+lemma in_analz: "Y:analz H ==> EX X. X:H & Y:parts {X}"
+by (erule analz.induct, auto intro: parts.Fst parts.Snd parts.Body)
+
+lemmas in_analz_subset_parts = analz_subset_parts [THEN subsetD]
+
+lemma Crypt_synth_insert: "[| Crypt K X:parts (insert Y H);
+Y:synth (analz H); Key K ~:analz H |] ==> Crypt K X:parts H"
+apply (drule parts_insert_substD, clarify)
+apply (frule in_sub)
+apply (frule parts_mono)
+by auto
+
+subsubsection{*greatest nonce used in a message*}
+
+consts greatest_msg :: "msg => nat"
+
+recdef greatest_msg "measure size"
+"greatest_msg (Nonce n) = n"
+"greatest_msg {|X,Y|} = max (greatest_msg X) (greatest_msg Y)"
+"greatest_msg (Crypt K X) = greatest_msg X"
+"greatest_msg other = 0"
+
+lemma greatest_msg_is_greatest: "Nonce n:parts {X} ==> n <= greatest_msg X"
+by (induct X, auto, arith+)
+
+subsubsection{*sets of keys*}
+
+constdefs keyset :: "msg set => bool"
+"keyset G == ALL X. X:G --> (EX K. X = Key K)"
+
+lemma keyset_in [dest]: "[| keyset G; X:G |] ==> EX K. X = Key K"
+by (auto simp: keyset_def)
+
+lemma MPair_notin_keyset [simp]: "keyset G ==> {|X,Y|} ~:G"
+by auto
+
+lemma Crypt_notin_keyset [simp]: "keyset G ==> Crypt K X ~:G"
+by auto
+
+lemma Nonce_notin_keyset [simp]: "keyset G ==> Nonce n ~:G"
+by auto
+
+lemma parts_keyset [simp]: "keyset G ==> parts G = G"
+by (auto, erule parts.induct, auto)
+
+subsubsection{*keys a priori necessary for decrypting the messages of G*}
+
+constdefs keysfor :: "msg set => msg set"
+"keysfor G == Key ` keysFor (parts G)"
+
+lemma keyset_keysfor [iff]: "keyset (keysfor G)"
+by (simp add: keyset_def keysfor_def, blast)
+
+lemma keyset_Diff_keysfor [simp]: "keyset H ==> keyset (H - keysfor G)"
+by (auto simp: keyset_def)
+
+lemma keysfor_Crypt: "Crypt K X:parts G ==> Key (invKey K):keysfor G"
+by (auto simp: keysfor_def Crypt_imp_invKey_keysFor)
+
+lemma no_key_no_Crypt: "Key K ~:keysfor G ==> Crypt (invKey K) X ~:parts G"
+by (auto dest: keysfor_Crypt)
+
+lemma finite_keysfor [intro]: "finite G ==> finite (keysfor G)"
+by (auto simp: keysfor_def intro: finite_UN_I)
+
+subsubsection{*only the keys necessary for G are useful in analz*}
+
+lemma analz_keyset: "keyset H ==>
+analz (G Un H) = H - keysfor G Un (analz (G Un (H Int keysfor G)))"
+apply (rule eq)
+apply (erule analz.induct, blast)
+apply (simp, blast dest: Un_upper1)
+apply (simp, blast dest: Un_upper2)
+apply (case_tac "Key (invKey K):H - keysfor G", clarsimp)
+apply (drule_tac X=X in no_key_no_Crypt)
+by (auto intro: analz_sub)
+
+lemmas analz_keyset_substD = analz_keyset [THEN sym, THEN ssubst]
+
+
+subsection{*Extensions to Theory @{text Event}*}
+
+
+subsubsection{*general protocol properties*}
+
+constdefs is_Says :: "event => bool"
+"is_Says ev == (EX A B X. ev = Says A B X)"
+
+lemma is_Says_Says [iff]: "is_Says (Says A B X)"
+by (simp add: is_Says_def)
+
+(* one could also require that Gets occurs after Says
+but this is sufficient for our purpose *)
+constdefs Gets_correct :: "event list set => bool"
+"Gets_correct p == ALL evs B X. evs:p --> Gets B X:set evs
+--> (EX A. Says A B X:set evs)"
+
+lemma Gets_correct_Says: "[| Gets_correct p; Gets B X # evs:p |]
+==> EX A. Says A B X:set evs"
+apply (simp add: Gets_correct_def)
+by (drule_tac x="Gets B X # evs" in spec, auto)
+
+constdefs one_step :: "event list set => bool"
+"one_step p == ALL evs ev. ev#evs:p --> evs:p"
+
+lemma one_step_Cons [dest]: "[| one_step p; ev#evs:p |] ==> evs:p"
+by (unfold one_step_def, blast)
+
+lemma one_step_app: "[| evs@evs':p; one_step p; []:p |] ==> evs':p"
+by (induct evs, auto)
+
+lemma trunc: "[| evs @ evs':p; one_step p |] ==> evs':p"
+by (induct evs, auto)
+
+constdefs has_only_Says :: "event list set => bool"
+"has_only_Says p == ALL evs ev. evs:p --> ev:set evs
+--> (EX A B X. ev = Says A B X)"
+
+lemma has_only_SaysD: "[| ev:set evs; evs:p; has_only_Says p |]
+==> EX A B X. ev = Says A B X"
+by (unfold has_only_Says_def, blast)
+
+lemma in_has_only_Says [dest]: "[| has_only_Says p; evs:p; ev:set evs |]
+==> EX A B X. ev = Says A B X"
+by (auto simp: has_only_Says_def)
+
+lemma has_only_Says_imp_Gets_correct [simp]: "has_only_Says p
+==> Gets_correct p"
+by (auto simp: has_only_Says_def Gets_correct_def)
+
+subsubsection{*lemma on knows*}
+
+lemma Says_imp_spies2: "Says A B {|X,Y|}:set evs ==> Y:parts (spies evs)"
+by (drule Says_imp_spies, drule parts.Inj, drule parts.Snd, simp)
+
+lemma Says_not_parts: "[| Says A B X:set evs; Y ~:parts (spies evs) |]
+==> Y ~:parts {X}"
+by (auto dest: Says_imp_spies parts_parts)
+
+subsubsection{*knows without initState*}
+
+consts knows' :: "agent => event list => msg set"
+
+primrec
+"knows' A [] = {}"
+"knows' A (ev # evs) = (
+  if A = Spy then (
+    case ev of
+      Says A' B X => insert X (knows' A evs)
+    | Gets A' X => knows' A evs
+    | Notes A' X => if A':bad then insert X (knows' A evs) else knows' A 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
+  ))"
+
+translations "spies" == "knows Spy"
+
+syntax spies' :: "event list => msg set"
+
+translations "spies'" == "knows' Spy"
+
+subsubsection{*decomposition of knows into knows' and initState*}
+
+lemma knows_decomp: "knows A evs = knows' A evs Un (initState A)"
+by (induct evs, auto split: event.split simp: knows.simps)
+
+lemmas knows_decomp_substI = knows_decomp [THEN ssubst]
+lemmas knows_decomp_substD = knows_decomp [THEN sym, THEN ssubst]
+
+lemma knows'_sub_knows: "knows' A evs <= knows A evs"
+by (auto simp: knows_decomp)
+
+lemma knows'_Cons: "knows' A (ev#evs) = knows' A [ev] Un knows' A evs"
+by (induct ev, auto)
+
+lemmas knows'_Cons_substI = knows'_Cons [THEN ssubst]
+lemmas knows'_Cons_substD = knows'_Cons [THEN sym, THEN ssubst]
+
+lemma knows_Cons: "knows A (ev#evs) = initState A Un knows' A [ev]
+Un knows A evs"
+apply (simp only: knows_decomp)
+apply (rule_tac s="(knows' A [ev] Un knows' A evs) Un initState A" in trans)
+by (rule Un_eq, rule knows'_Cons, simp, blast)
+
+lemmas knows_Cons_substI = knows_Cons [THEN ssubst]
+lemmas knows_Cons_substD = knows_Cons [THEN sym, THEN ssubst]
+
+lemma knows'_sub_spies': "[| evs:p; has_only_Says p; one_step p |]
+==> knows' A evs <= spies' evs"
+by (induct evs, auto split: event.splits)
+
+subsubsection{*knows' is finite*}
+
+lemma finite_knows' [iff]: "finite (knows' A evs)"
+by (induct evs, auto split: event.split simp: knows.simps)
+
+subsubsection{*monotonicity of knows*}
+
+lemma knows_sub_Cons: "knows A evs <= knows A (ev#evs)"
+by (cases A, (induct evs, (induct ev, auto simp: knows.simps)+))
+
+lemma knows_ConsI: "X:knows A evs ==> X:knows A (ev#evs)"
+by (auto dest: knows_sub_Cons [THEN subsetD])
+
+lemma knows_sub_app: "knows A evs <= knows A (evs @ evs')"
+apply (induct evs, auto)
+apply (simp add: knows_decomp)
+by (case_tac a, auto simp: knows.simps)
+
+subsubsection{*maximum knowledge an agent can have
+includes messages sent to the agent*}
+
+consts knows_max' :: "agent => event list => msg set"
+
+primrec
+knows_max'_def_Nil: "knows_max' A [] = {}"
+knows_max'_def_Cons: "knows_max' A (ev # evs) = (
+  if A=Spy then (
+    case ev of
+      Says A' B X => insert X (knows_max' A evs)
+    | Gets A' X => knows_max' A evs
+    | Notes A' X =>
+      if A':bad then insert X (knows_max' A evs) else knows_max' A evs
+  ) else (
+    case ev of
+      Says A' B X =>
+      if A=A' | A=B then insert X (knows_max' A evs) else knows_max' A evs
+    | Gets A' X =>
+      if A=A' then insert X (knows_max' A evs) else knows_max' A evs
+    | Notes A' X =>
+      if A=A' then insert X (knows_max' A evs) else knows_max' A evs
+  ))"
+
+constdefs knows_max :: "agent => event list => msg set"
+"knows_max A evs == knows_max' A evs Un initState A"
+
+consts spies_max :: "event list => msg set"
+
+translations "spies_max evs" == "knows_max Spy evs"
+
+subsubsection{*basic facts about @{term knows_max}*}
+
+lemma spies_max_spies [iff]: "spies_max evs = spies evs"
+by (induct evs, auto simp: knows_max_def split: event.splits)
+
+lemma knows_max'_Cons: "knows_max' A (ev#evs)
+= knows_max' A [ev] Un knows_max' A evs"
+by (auto split: event.splits)
+
+lemmas knows_max'_Cons_substI = knows_max'_Cons [THEN ssubst]
+lemmas knows_max'_Cons_substD = knows_max'_Cons [THEN sym, THEN ssubst]
+
+lemma knows_max_Cons: "knows_max A (ev#evs)
+= knows_max' A [ev] Un knows_max A evs"
+apply (simp add: knows_max_def del: knows_max'_def_Cons)
+apply (rule_tac evs1=evs in knows_max'_Cons_substI)
+by blast
+
+lemmas knows_max_Cons_substI = knows_max_Cons [THEN ssubst]
+lemmas knows_max_Cons_substD = knows_max_Cons [THEN sym, THEN ssubst]
+
+lemma finite_knows_max' [iff]: "finite (knows_max' A evs)"
+by (induct evs, auto split: event.split)
+
+lemma knows_max'_sub_spies': "[| evs:p; has_only_Says p; one_step p |]
+==> knows_max' A evs <= spies' evs"
+by (induct evs, auto split: event.splits)
+
+lemma knows_max'_in_spies' [dest]: "[| evs:p; X:knows_max' A evs;
+has_only_Says p; one_step p |] ==> X:spies' evs"
+by (rule knows_max'_sub_spies' [THEN subsetD], auto)
+
+lemma knows_max'_app: "knows_max' A (evs @ evs')
+= knows_max' A evs Un knows_max' A evs'"
+by (induct evs, auto split: event.splits)
+
+lemma Says_to_knows_max': "Says A B X:set evs ==> X:knows_max' B evs"
+by (simp add: in_set_conv_decomp, clarify, simp add: knows_max'_app)
+
+lemma Says_from_knows_max': "Says A B X:set evs ==> X:knows_max' A evs"
+by (simp add: in_set_conv_decomp, clarify, simp add: knows_max'_app)
+
+subsubsection{*used without initState*}
+
+consts used' :: "event list => msg set"
+
+primrec
+"used' [] = {}"
+"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
+  )"
+
+constdefs init :: "msg set"
+"init == used []"
+
+lemma used_decomp: "used evs = init Un used' evs"
+by (induct evs, auto simp: init_def split: event.split)
+
+lemma used'_sub_app: "used' evs <= used' (evs@evs')"
+by (induct evs, auto split: event.split)
+
+lemma used'_parts [rule_format]: "X:used' evs ==> Y:parts {X} --> Y:used' evs"
+apply (induct evs, simp) 
+apply (case_tac a, simp_all) 
+apply (blast dest: parts_trans)+; 
+done
+
+subsubsection{*monotonicity of used*}
+
+lemma used_sub_Cons: "used evs <= used (ev#evs)"
+by (induct evs, (induct ev, auto)+)
+
+lemma used_ConsI: "X:used evs ==> X:used (ev#evs)"
+by (auto dest: used_sub_Cons [THEN subsetD])
+
+lemma notin_used_ConsD: "X ~:used (ev#evs) ==> X ~:used evs"
+by (auto dest: used_sub_Cons [THEN subsetD])
+
+lemma used_appD [dest]: "X:used (evs @ evs') ==> X:used evs | X:used evs'"
+by (induct evs, auto, case_tac a, auto)
+
+lemma used_ConsD: "X:used (ev#evs) ==> X:used [ev] | X:used evs"
+by (case_tac ev, auto)
+
+lemma used_sub_app: "used evs <= used (evs@evs')"
+by (auto simp: used_decomp dest: used'_sub_app [THEN subsetD])
+
+lemma used_appIL: "X:used evs ==> X:used (evs' @ evs)"
+by (induct evs', auto intro: used_ConsI)
+
+lemma used_appIR: "X:used evs ==> X:used (evs @ evs')"
+by (erule used_sub_app [THEN subsetD])
+
+lemma used_parts: "[| X:parts {Y}; Y:used evs |] ==> X:used evs"
+apply (auto simp: used_decomp dest: used'_parts)
+by (auto simp: init_def used_Nil dest: parts_trans)
+
+lemma parts_Says_used: "[| Says A B X:set evs; Y:parts {X} |] ==> Y:used evs"
+by (induct evs, simp_all, safe, auto intro: used_ConsI)
+
+lemma parts_used_app: "X:parts {Y} ==> X:used (evs @ Says A B Y # evs')"
+apply (drule_tac evs="[Says A B Y]" in used_parts, simp, blast)
+apply (drule_tac evs'=evs' in used_appIR)
+apply (drule_tac evs'=evs in used_appIL)
+by simp
+
+subsubsection{*lemmas on used and knows*}
+
+lemma initState_used: "X:parts (initState A) ==> X:used evs"
+by (induct evs, auto simp: used.simps split: event.split)
+
+lemma Says_imp_used: "Says A B X:set evs ==> parts {X} <= used evs"
+by (induct evs, auto intro: used_ConsI)
+
+lemma not_used_not_spied: "X ~:used evs ==> X ~:parts (spies evs)"
+by (induct evs, auto simp: used_Nil)
+
+lemma not_used_not_parts: "[| Y ~:used evs; Says A B X:set evs |]
+==> Y ~:parts {X}"
+by (induct evs, auto intro: used_ConsI)
+
+lemma not_used_parts_false: "[| X ~:used evs; Y:parts (spies evs) |]
+==> X ~:parts {Y}"
+by (auto dest: parts_parts)
+
+lemma known_used [rule_format]: "[| evs:p; Gets_correct p; one_step p |]
+==> X:parts (knows A evs) --> X:used evs"
+apply (case_tac "A=Spy", blast dest: parts_knows_Spy_subset_used)
+apply (induct evs)
+apply (simp add: used.simps, blast)
+apply (frule_tac ev=a and evs=list in one_step_Cons, simp, clarify)
+apply (drule_tac P="%G. X:parts G" in knows_Cons_substD, safe)
+apply (erule initState_used)
+apply (case_tac a, auto)
+apply (drule_tac B=A and X=msg and evs=list in Gets_correct_Says)
+by (auto dest: Says_imp_used intro: used_ConsI)
+
+lemma known_max_used [rule_format]: "[| evs:p; Gets_correct p; one_step p |]
+==> X:parts (knows_max A evs) --> X:used evs"
+apply (case_tac "A=Spy")
+apply (simp, blast dest: parts_knows_Spy_subset_used)
+apply (induct evs)
+apply (simp add: knows_max_def used.simps, blast)
+apply (frule_tac ev=a and evs=list in one_step_Cons, simp, clarify)
+apply (drule_tac P="%G. X:parts G" in knows_max_Cons_substD, safe)
+apply (case_tac a, auto)
+apply (drule_tac B=A and X=msg and evs=list in Gets_correct_Says)
+by (auto simp: knows_max'_Cons dest: Says_imp_used intro: used_ConsI)
+
+lemma not_used_not_known: "[| evs:p; X ~:used evs;
+Gets_correct p; one_step p |] ==> X ~:parts (knows A evs)"
+by (case_tac "A=Spy", auto dest: not_used_not_spied known_used)
+
+lemma not_used_not_known_max: "[| evs:p; X ~:used evs;
+Gets_correct p; one_step p |] ==> X ~:parts (knows_max A evs)"
+by (case_tac "A=Spy", auto dest: not_used_not_spied known_max_used)
+
+subsubsection{*a nonce or key in a message cannot equal a fresh nonce or key*}
+
+lemma Nonce_neq [dest]: "[| Nonce n' ~:used evs;
+Says A B X:set evs; Nonce n:parts {X} |] ==> n ~= n'"
+by (drule not_used_not_spied, auto dest: Says_imp_knows_Spy parts_sub)
+
+lemma Key_neq [dest]: "[| Key n' ~:used evs;
+Says A B X:set evs; Key n:parts {X} |] ==> n ~= n'"
+by (drule not_used_not_spied, auto dest: Says_imp_knows_Spy parts_sub)
+
+subsubsection{*message of an event*}
+
+consts msg :: "event => msg"
+
+recdef msg "measure size"
+"msg (Says A B X) = X"
+"msg (Gets A X) = X"
+"msg (Notes A X) = X"
+
+lemma used_sub_parts_used: "X:used (ev # evs) ==> X:parts {msg ev} Un used evs"
+by (induct ev, auto)
+
+
+
+end