Quelle Extensions.thy Sprache: Isabelle

(*  Title:      HOL/Auth/Guard/Extensions.thy
    Author:     Frederic Blanqui, University of Cambridge Computer Laboratory
    Copyright   2001  University of Cambridge
*)

section \<open>Extensions to Standard Theories\<close>

theory Extensions
imports "../Event"
begin

subsection\<open>Extensions to Theory \<open>Set\<close>\<close>

lemma eq: "\\x. x\A \ x\B; \x. x\B \ x\A\ \ A=B"
by auto

lemma insert_Un: "P ({x} \ A) \ P (insert x A)"
by simp

lemma in_sub: "x\A \ {x}\A"
by auto

subsection\<open>Extensions to Theory \<open>List\<close>\<close>

subsubsection\<open>"remove l x" erase the first element of "l" equal to "x"\<close>

primrec remove :: "'a list => 'a => 'a list" where
"remove [] y = []" |
"remove (x#xs) y = (if x=y then xs else x # remove xs y)"

lemma set_remove: "set (remove l x) <= set l"
by (induct l, auto)

subsection\<open>Extensions to Theory \<open>Message\<close>\<close>

subsubsection\<open>declarations for tactics\<close>

declare analz_subset_parts [THEN subsetD, dest]
declare parts_insert2 [simp]
declare analz_cut [dest]
declare if_split_asm [split]
declare analz_insertI [intro]
declare Un_Diff [simp]

subsubsection\<open>extract the agent number of an Agent message\<close>

primrec agt_nb :: "msg => agent" where
"agt_nb (Agent A) = A"

subsubsection\<open>messages that are pairs\<close>

definition is_MPair :: "msg => bool" where
"is_MPair X == \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

abbreviation
  not_MPair :: "msg => bool" where
  "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]

definition has_no_pair :: "msg set => bool" where
"has_no_pair H == \X Y. \X,Y\ \ H"

declare has_no_pair_def [simp]

subsubsection\<open>well-foundedness of messages\<close>

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\<open>lemmas on keysFor\<close>

definition usekeys :: "msg set => key set" where
"usekeys G \ {K. \Y. Crypt K Y \ G}"

lemma finite_keysFor [intro]: "finite G \ finite (keysFor G)"
apply (simp add: keysFor_def)
apply (rule finite_imageI)
apply (induct G rule: finite_induct)
apply auto
apply (case_tac "\K X. x = Crypt K X", clarsimp)
apply (subgoal_tac "{Ka. \Xa. (Ka=K \ Xa=X) \ Crypt Ka Xa \ F}
= insert K (usekeys F)", auto simp: usekeys_def)
by (subgoal_tac "{K. \X. Crypt K X = x \ Crypt K X \ F} = usekeys F",
auto simp: usekeys_def)

subsubsection\<open>lemmas on parts\<close>

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})\
\<Longrightarrow> Nonce n \<notin> 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 (frule parts_cut, 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}\
\<Longrightarrow> Nonce n \<in> parts G"
by (blast intro: parts.Body dest: parts_parts)

subsubsection\<open>lemmas on synth\<close>

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 \<in> parts {X} \<longrightarrow> Crypt K Y \<in> parts G"
by (erule synth.induct, auto dest: parts_sub)

subsubsection\<open>lemmas on analz\<close>

lemma analz_UnI1 [intro]: "X \ analz G \ X \ analz (G \ H)"
  by (subgoal_tac "G <= G Un H") (blast 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"
by (blast intro: analz.Decrypt analz_insert_eq)

lemma must_decrypt [rule_format,dest]: "\X \ analz H; has_no_pair H\ \
X \<notin> H \<longrightarrow> (\<exists>K Y. Crypt K Y \<in> H \<and> Key (invKey K) \<in> H)"
by (erule analz.induct, auto)

lemma analz_needs_only_finite: "X \ analz H \ \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\<open>lemmas on parts, synth and analz\<close>

lemma parts_invKey [rule_format,dest]:"X \ parts {Y} \
X \<in> analz (insert (Crypt K Y) H) \<longrightarrow> X \<notin> analz H \<longrightarrow> Key (invKey K) \<in> analz H"
by (erule parts.induct, auto dest: parts.Fst parts.Snd parts.Body)

lemma in_analz: "Y \ analz H \ \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 \<in> synth (analz H); Key K \<notin> analz H\<rbrakk> \<Longrightarrow> Crypt K X \<in> parts H"
apply (drule parts_insert_substD, clarify)
apply (frule in_sub)
apply (frule parts_mono)
apply auto
done

subsubsection\<open>greatest nonce used in a message\<close>

fun greatest_msg :: "msg => nat"
where
  "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)

subsubsection\<open>sets of keys\<close>

definition keyset :: "msg set => bool" where
"keyset G \ \X. X \ G \ (\K. X = Key K)"

lemma keyset_in [dest]: "\keyset G; X \ G\ \ \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\<open>keys a priori necessary for decrypting the messages of G\<close>

definition keysfor :: "msg set => msg set" where
"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\<open>only the keys necessary for G are useful in analz\<close>

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)
apply (simp, blast)
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\<open>Extensions to Theory \<open>Event\<close>\<close>

subsubsection\<open>general protocol properties\<close>

definition is_Says :: "event => bool" where
"is_Says ev == (\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 *)
definition Gets_correct :: "event list set => bool" where
"Gets_correct p == \evs B X. evs \ p \ Gets B X \ set evs
\<longrightarrow> (\<exists>A. Says A B X \<in> set evs)"

lemma Gets_correct_Says: "\Gets_correct p; Gets B X # evs \ p\
\<Longrightarrow> \<exists>A. Says A B X \<in> set evs"
apply (simp add: Gets_correct_def)
by (drule_tac x="Gets B X # evs" in spec, auto)

definition one_step :: "event list set => bool" where
"one_step p == \evs ev. ev#evs \ p \ evs \ p"

lemma one_step_Cons [dest]: "\one_step p; ev#evs \ p\ \ evs \ p"
  unfolding one_step_def by 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)

definition has_only_Says :: "event list set => bool" where
"has_only_Says p \ \evs ev. evs \ p \ ev \ set evs
\<longrightarrow> (\<exists>A B X. ev = Says A B X)"

lemma has_only_SaysD: "\ev \ set evs; evs \ p; has_only_Says p\
\<Longrightarrow> \<exists>A B X. ev = Says A B X"
  unfolding has_only_Says_def by blast

lemma in_has_only_Says [dest]: "\has_only_Says p; evs \ p; ev \ set evs\
\<Longrightarrow> \<exists>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
\<Longrightarrow> Gets_correct p"
by (auto simp: has_only_Says_def Gets_correct_def)

subsubsection\<open>lemma on knows\<close>

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)\
\<Longrightarrow> Y \<notin> parts {X}"
by (auto dest: Says_imp_spies parts_parts)

subsubsection\<open>knows without initState\<close>

primrec knows' :: "agent => event list => msg set" where
  knows'_Nil: "knows' A [] = {}" |
  knows'_Cons0:
"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' \<in> 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
   ))"

abbreviation
  spies' :: "event list => msg set" where
  "spies' == knows' Spy"

subsubsection\<open>decomposition of knows into knows' and initState\<close>

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)
apply (simp only: knows'_Cons [of A ev evs] Un_ac)
apply blast
done

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\
\<Longrightarrow> knows' A evs \<subseteq> spies' evs"
by (induct evs, auto split: event.splits)

subsubsection\<open>knows' is finite\<close>

lemma finite_knows' [iff]: "finite (knows' A evs)"
by (induct evs, auto split: event.split simp: knows.simps)

subsubsection\<open>monotonicity of knows\<close>

lemma knows_sub_Cons: "knows A evs <= knows A (ev#evs)"
by(cases A, induct evs, auto simp: knows.simps split:event.split)

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)
apply (rename_tac a b c)
by (case_tac a, auto simp: knows.simps)

subsubsection\<open>maximum knowledge an agent can have
includes messages sent to the agent\<close>

primrec knows_max' :: "agent => event list => msg set" where
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
  ))"

definition knows_max :: "agent => event list => msg set" where
"knows_max A evs == knows_max' A evs Un initState A"

abbreviation
  spies_max :: "event list => msg set" where
  "spies_max evs == knows_max Spy evs"

subsubsection\<open>basic facts about \<^term>\<open>knows_max\<close>\<close>

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 evs=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\
\<Longrightarrow> knows_max' A evs \<subseteq> 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\<rbrakk> \<Longrightarrow> X \<in> 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\<open>used without initState\<close>

primrec used' :: "event list => msg set" where
"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
  )"

definition init :: "msg set" where
"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 \<subseteq> 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 (rename_tac a b)
apply (case_tac a, simp_all)
apply (blast dest: parts_trans)+
done

subsubsection\<open>monotonicity of used\<close>

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, rename_tac a b, 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\<open>lemmas on used and knows\<close>

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\
\<Longrightarrow> Y \<notin> parts {X}"
by (induct evs, auto intro: used_ConsI)

lemma not_used_parts_false: "\X \ used evs; Y \ parts (spies evs)\
\<Longrightarrow> X \<notin> parts {Y}"
by (auto dest: parts_parts)

lemma known_used [rule_format]: "\evs \ p; Gets_correct p; one_step p\
\<Longrightarrow> X \<in> parts (knows A evs) \<longrightarrow> X \<in> used evs"
apply (case_tac "A=Spy", blast)
apply (induct evs)
apply (simp add: used.simps, blast)
apply (rename_tac a evs)
apply (frule_tac ev=a and evs=evs 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 (rename_tac msg)
apply (drule_tac B=A and X=msg and evs=evs 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\
\<Longrightarrow> X \<in> parts (knows_max A evs) \<longrightarrow> X \<in> used evs"
apply (case_tac "A=Spy")
apply force
apply (induct evs)
apply (simp add: knows_max_def used.simps, blast)
apply (rename_tac a evs)
apply (frule_tac ev=a and evs=evs 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 (rename_tac msg)
apply (drule_tac B=A and X=msg and evs=evs 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\<rbrakk> \<Longrightarrow> X \<notin> 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\<rbrakk> \<Longrightarrow> X \<notin> parts (knows_max A evs)"
by (case_tac "A=Spy", auto dest: not_used_not_spied known_max_used)

subsubsection\<open>a nonce or key in a message cannot equal a fresh nonce or key\<close>

lemma Nonce_neq [dest]: "\Nonce n' \ used evs;
Says A B X \<in> set evs; Nonce n \<in> parts {X}\<rbrakk> \<Longrightarrow> n \<noteq> 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 \<in> set evs; Key n \<in> parts {X}\<rbrakk> \<Longrightarrow> n ~= n'"
by (drule not_used_not_spied, auto dest: Says_imp_knows_Spy parts_sub)

subsubsection\<open>message of an event\<close>

primrec msg :: "event => msg"
where
  "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} \ used evs"
by (induct ev, auto)

end

quality100%

¤ Dauer der Verarbeitung: 0.11 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.