Theory Anonymity

(*  Title:       The Relational Method with Message Anonymity for the Verification of Cryptographic Protocols
    Author:      Pasquale Noce
                 Software Engineer at HID Global, Italy
                 pasquale dot noce dot lavoro at gmail dot com
                 pasquale dot noce at hidglobal dot com
*)

section "Anonymity properties"

theory Anonymity
  imports Authentication
begin

text ‹
\label{Anonymity}
›


proposition crypts_empty [simp]:
 "crypts {} = {}"
by (rule equalityI, rule subsetI, erule crypts.induct, simp_all)

proposition crypts_mono:
 "H ⊆ H' ⟹ crypts H ⊆ crypts H'"
by (rule subsetI, erule crypts.induct, auto)

lemma crypts_union_1:
 "crypts (H ∪ H') ⊆ crypts H ∪ crypts H'"
by (rule subsetI, erule crypts.induct, auto)

lemma crypts_union_2:
 "crypts H ∪ crypts H' ⊆ crypts (H ∪ H')"
by (rule subsetI, erule UnE, erule_tac [!] crypts.induct, auto)

proposition crypts_union:
 "crypts (H ∪ H') = crypts H ∪ crypts H'"
by (rule equalityI, rule crypts_union_1, rule crypts_union_2)

proposition crypts_insert:
 "crypts (insert X H) = crypts_msg X ∪ crypts H"
by (simp only: insert_def crypts_union, subst crypts_msg_def, simp)

proposition crypts_msg_num [simp]:
 "crypts_msg (Num n) = {Num n}"
by (subst crypts_msg_def, rule equalityI, rule subsetI, erule crypts.induct, simp,
 rotate_tac [1-3], erule_tac [1-3] rev_mp, rule_tac [1-3] list.induct, simp_all,
 blast)

proposition crypts_msg_agent [simp]:
 "crypts_msg (Agent n) = {Agent n}"
by (subst crypts_msg_def, rule equalityI, rule subsetI, erule crypts.induct, simp,
 rotate_tac [1-3], erule_tac [1-3] rev_mp, rule_tac [1-3] list.induct, simp_all,
 blast)

proposition crypts_msg_pwd [simp]:
 "crypts_msg (Pwd n) = {Pwd n}"
by (subst crypts_msg_def, rule equalityI, rule subsetI, erule crypts.induct, simp,
 rotate_tac [1-3], erule_tac [1-3] rev_mp, rule_tac [1-3] list.induct, simp_all,
 blast)

proposition crypts_msg_key [simp]:
 "crypts_msg (Key K) = {Key K}"
by (subst crypts_msg_def, rule equalityI, rule subsetI, erule crypts.induct, simp,
 rotate_tac [1-3], erule_tac [1-3] rev_mp, rule_tac [1-3] list.induct, simp_all,
 blast)

proposition crypts_msg_mult [simp]:
 "crypts_msg (A ⊗ B) = {A ⊗ B}"
by (subst crypts_msg_def, rule equalityI, rule subsetI, erule crypts.induct, simp,
 rotate_tac [1-3], erule_tac [1-3] rev_mp, rule_tac [1-3] list.induct, simp_all,
 blast)

lemma crypts_hash_1:
 "crypts {Hash X} ⊆ insert (Hash X) (crypts {X})"
by (rule subsetI, erule crypts.induct, simp_all, (erule disjE, rotate_tac, erule rev_mp,
 rule list.induct, simp_all, blast, (drule crypts_hash, simp)?)+)

lemma crypts_hash_2:
 "insert (Hash X) (crypts {X}) ⊆ crypts {Hash X}"
by (rule subsetI, simp, erule disjE, blast, erule crypts.induct, simp,
 subst id_apply [symmetric], subst foldr_Nil [symmetric], rule crypts_hash, simp,
 blast+)

proposition crypts_msg_hash [simp]:
 "crypts_msg (Hash X) = insert (Hash X) (crypts_msg X)"
by (simp add: crypts_msg_def, rule equalityI, rule crypts_hash_1, rule crypts_hash_2)

proposition crypts_comp:
 "X ∈ crypts H ⟹ Crypt K X ∈ crypts (Crypt K ` H)"
by (erule crypts.induct, blast, (simp only: comp_apply
 [symmetric, where f = "Crypt K"] foldr_Cons [symmetric],
 (erule crypts_hash | erule crypts_fst | erule crypts_snd))+)

lemma crypts_crypt_1:
 "crypts {Crypt K X} ⊆ Crypt K ` crypts {X}"
by (rule subsetI, erule crypts.induct, fastforce, rotate_tac [!], erule_tac [!] rev_mp,
 rule_tac [!] list.induct, auto)

lemma crypts_crypt_2:
 "Crypt K ` crypts {X} ⊆ crypts {Crypt K X}"
by (rule subsetI, simp add: image_iff, erule bexE, drule crypts_comp, simp)

proposition crypts_msg_crypt [simp]:
 "crypts_msg (Crypt K X) = Crypt K ` crypts_msg X"
by (simp add: crypts_msg_def, rule equalityI, rule crypts_crypt_1, rule crypts_crypt_2)

lemma crypts_mpair_1:
 "crypts {⦃X, Y⦄} ⊆ insert ⦃X, Y⦄ (crypts {X} ∪ crypts {Y})"
by (rule subsetI, erule crypts.induct, simp_all, (erule disjE, rotate_tac, erule rev_mp,
 rule list.induct, (simp+, blast)+)+)

lemma crypts_mpair_2:
 "insert ⦃X, Y⦄ (crypts {X} ∪ crypts {Y}) ⊆ crypts {⦃X, Y⦄}"
by (rule subsetI, simp, erule disjE, blast, erule disjE, (erule crypts.induct, simp,
 subst id_apply [symmetric], subst foldr_Nil [symmetric], (rule crypts_fst [of _ X] |
 rule crypts_snd), rule crypts_used, simp, blast+)+)

proposition crypts_msg_mpair [simp]:
 "crypts_msg ⦃X, Y⦄ = insert ⦃X, Y⦄ (crypts_msg X ∪ crypts_msg Y)"
by (simp add: crypts_msg_def, rule equalityI, rule crypts_mpair_1, rule crypts_mpair_2)


proposition foldr_crypt_size:
 "size (foldr Crypt KS X) = size X + length KS"
by (induction KS, simp_all)

proposition key_sets_empty [simp]:
 "key_sets X {} = {}"
by (simp add: key_sets_def)

proposition key_sets_mono:
 "H ⊆ H' ⟹ key_sets X H ⊆ key_sets X H'"
by (auto simp add: key_sets_def)

proposition key_sets_union:
 "key_sets X (H ∪ H') = key_sets X H ∪ key_sets X H'"
by (auto simp add: key_sets_def)

proposition key_sets_insert:
 "key_sets X (insert Y H) = key_sets_msg X Y ∪ key_sets X H"
by (simp only: insert_def key_sets_union, subst key_sets_msg_def, simp)

proposition key_sets_msg_eq:
 "key_sets_msg X X = {{}}"
by (simp add: key_sets_msg_def key_sets_def, rule equalityI, rule subsetI, simp,
 erule exE, erule rev_mp, rule list.induct, simp, rule impI, erule conjE,
 drule arg_cong [of _ X size], simp_all add: foldr_crypt_size)

proposition key_sets_msg_num [simp]:
 "key_sets_msg X (Num n) = (if X = Num n then {{}} else {})"
by (simp add: key_sets_msg_eq, simp add: key_sets_msg_def key_sets_def, rule impI,
 rule allI, rule list.induct, simp_all)

proposition key_sets_msg_agent [simp]:
 "key_sets_msg X (Agent n) = (if X = Agent n then {{}} else {})"
by (simp add: key_sets_msg_eq, simp add: key_sets_msg_def key_sets_def, rule impI,
 rule allI, rule list.induct, simp_all)

proposition key_sets_msg_pwd [simp]:
 "key_sets_msg X (Pwd n) = (if X = Pwd n then {{}} else {})"
by (simp add: key_sets_msg_eq, simp add: key_sets_msg_def key_sets_def, rule impI,
 rule allI, rule list.induct, simp_all)

proposition key_sets_msg_key [simp]:
 "key_sets_msg X (Key K) = (if X = Key K then {{}} else {})"
by (simp add: key_sets_msg_eq, simp add: key_sets_msg_def key_sets_def, rule impI,
 rule allI, rule list.induct, simp_all)

proposition key_sets_msg_mult [simp]:
 "key_sets_msg X (A ⊗ B) = (if X = A ⊗ B then {{}} else {})"
by (simp add: key_sets_msg_eq, simp add: key_sets_msg_def key_sets_def, rule impI,
 rule allI, rule list.induct, simp_all)

proposition key_sets_msg_hash [simp]:
 "key_sets_msg X (Hash Y) = (if X = Hash Y then {{}} else {})"
by (simp add: key_sets_msg_eq, simp add: key_sets_msg_def key_sets_def, rule impI,
 rule allI, rule list.induct, simp_all)

lemma key_sets_crypt_1:
 "X ≠ Crypt K Y ⟹
    key_sets X {Crypt K Y} ⊆ insert (InvKey K) ` key_sets X {Y}"
by (rule subsetI, simp add: key_sets_def, erule exE, rotate_tac, erule rev_mp,
 rule list.induct, auto)

lemma key_sets_crypt_2:
 "insert (InvKey K) ` key_sets X {Y} ⊆ key_sets X {Crypt K Y}"
by (rule subsetI, simp add: key_sets_def image_iff, (erule exE, erule conjE)+,
 drule arg_cong [where f = "Crypt K"], simp only: comp_apply
 [symmetric, of "Crypt K"] foldr_Cons [symmetric], subst conj_commute,
 rule exI, rule conjI, assumption, simp)

proposition key_sets_msg_crypt [simp]:
 "key_sets_msg X (Crypt K Y) = (if X = Crypt K Y then {{}} else
    insert (InvKey K) ` key_sets_msg X Y)"
by (simp add: key_sets_msg_eq, simp add: key_sets_msg_def, rule impI,
 rule equalityI, erule key_sets_crypt_1 [simplified],
 rule key_sets_crypt_2 [simplified])

proposition key_sets_msg_mpair [simp]:
 "key_sets_msg X ⦃Y, Z⦄ = (if X = ⦃Y, Z⦄ then {{}} else {})"
by (simp add: key_sets_msg_eq, simp add: key_sets_msg_def key_sets_def, rule impI,
 rule allI, rule list.induct, simp_all)

proposition key_sets_range:
 "U ∈ key_sets X H ⟹ U ⊆ range Key"
by (simp add: key_sets_def, blast)

proposition key_sets_crypts_hash:
 "key_sets (Hash X) (crypts H) ⊆ key_sets X (crypts H)"
by (simp add: key_sets_def, blast)

proposition key_sets_crypts_fst:
 "key_sets ⦃X, Y⦄ (crypts H) ⊆ key_sets X (crypts H)"
by (simp add: key_sets_def, blast)

proposition key_sets_crypts_snd:
 "key_sets ⦃X, Y⦄ (crypts H) ⊆ key_sets Y (crypts H)"
by (simp add: key_sets_def, blast)


lemma log_spied_1:
 "⟦s ⊢ s';
    Log X ∈ parts (used s) ⟶ Log X ∈ spied s;
    Log X ∈ parts (used s')⟧ ⟹
  Log X ∈ spied s'"
by (simp add: rel_def, ((erule disjE)?, ((erule exE)+)?, simp add: parts_insert,
 ((subst (asm) disj_assoc [symmetric])?, erule disjE, (drule parts_dec |
 drule parts_enc | drule parts_sep | drule parts_con), simp+)?)+)

proposition log_spied [rule_format]:
 "s⇩0 ⊨ s ⟹
    Log X ∈ parts (used s) ⟶
  Log X ∈ spied s"
by (erule rtrancl_induct, subst parts_init, simp add: Range_iff image_def, rule impI,
 rule log_spied_1)


proposition log_dec:
 "⟦s⇩0 ⊨ s; s' = insert (Spy, X) s ∧ (Spy, Crypt K X) ∈ s ∧
    (Spy, Key (InvK K)) ∈ s⟧ ⟹
  key_sets Y (crypts {Y. Log Y = X}) ⊆ key_sets Y (crypts (Log -` spied s))"
by (rule key_sets_mono, rule crypts_mono, rule subsetI, simp, drule parts_dec
 [where Y = X], drule_tac [!] sym, simp_all, rule log_spied [simplified])

proposition log_sep:
 "⟦s⇩0 ⊨ s; s' = insert (Spy, X) (insert (Spy, Y) s) ∧ (Spy, ⦃X, Y⦄) ∈ s⟧ ⟹
    key_sets Z (crypts {Z. Log Z = X}) ⊆ key_sets Z (crypts (Log -` spied s)) ∧
    key_sets Z (crypts {Z. Log Z = Y}) ⊆ key_sets Z (crypts (Log -` spied s))"
by (rule conjI, (rule key_sets_mono, rule crypts_mono, rule subsetI, simp,
 frule parts_sep [where Z = X], drule_tac [2] parts_sep [where Z = Y],
 simp_all add: parts_msg_def, blast+, drule sym, simp,
 rule log_spied [simplified], assumption+)+)


lemma idinfo_spied_1:
 "⟦s ⊢ s';
    ⟨n, X⟩ ∈ parts (used s) ⟶ ⟨n, X⟩ ∈ spied s;
    ⟨n, X⟩ ∈ parts (used s')⟧ ⟹
  ⟨n, X⟩ ∈ spied s'"
by (simp add: rel_def, (erule disjE, (erule exE)+, simp add: parts_insert,
 ((subst (asm) disj_assoc [symmetric])?, erule disjE, (drule parts_dec |
 drule parts_enc | drule parts_sep | drule parts_con), simp+)?)+,
 auto simp add: parts_insert)

proposition idinfo_spied [rule_format]:
 "s⇩0 ⊨ s ⟹
    ⟨n, X⟩ ∈ parts (used s) ⟶
  ⟨n, X⟩ ∈ spied s"
by (erule rtrancl_induct, subst parts_init, simp add: Range_iff image_def, rule impI,
 rule idinfo_spied_1)


proposition idinfo_dec:
 "⟦s⇩0 ⊨ s; s' = insert (Spy, X) s ∧ (Spy, Crypt K X) ∈ s ∧
    (Spy, Key (InvK K)) ∈ s; ⟨n, Y⟩ = X⟧ ⟹
  ⟨n, Y⟩ ∈ spied s"
by (drule parts_dec [where Y = "⟨n, Y⟩"], drule sym, simp, rule idinfo_spied)

proposition idinfo_sep:
 "⟦s⇩0 ⊨ s; s' = insert (Spy, X) (insert (Spy, Y) s) ∧ (Spy, ⦃X, Y⦄) ∈ s;
    ⟨n, Z⟩ = X ∨ ⟨n, Z⟩ = Y⟧ ⟹
  ⟨n, Z⟩ ∈ spied s"
by (drule parts_sep [where Z = "⟨n, Z⟩"], erule disjE, (drule sym, simp)+,
 rule idinfo_spied)


lemma idinfo_msg_1:
  assumes A: "s⇩0 ⊨ s"
  shows "⟦s ⊢ s'; ⟨n, X⟩ ∈ spied s ⟶ X ∈ spied s; ⟨n, X⟩ ∈ spied s'⟧ ⟹
    X ∈ spied s'"
by (simp add: rel_def, (erule disjE, (erule exE)+, simp, ((subst (asm) disj_assoc
 [symmetric])?, erule disjE, (drule idinfo_dec [OF A] | drule idinfo_sep [OF A]),
 simp+ | erule disjE, (simp add: image_iff)+, blast?)?)+)

proposition idinfo_msg [rule_format]:
 "s⇩0 ⊨ s ⟹
    ⟨n, X⟩ ∈ spied s ⟶
  X ∈ spied s"
by (erule rtrancl_induct, simp, blast, rule impI, rule idinfo_msg_1)


proposition parts_agent_start:
 "⟦s ⊢ s'; Agent n ∈ parts (used s'); Agent n ∉ parts (used s)⟧ ⟹ False"
by (simp add: rel_def, (((erule disjE)?, ((erule exE)+)?, simp add: parts_insert
 image_iff)+, ((drule parts_dec | drule parts_enc | drule parts_sep | drule parts_con),
 simp+)?)+)

proposition parts_agent [rotated]:
  assumes A: "n ∉ bad_agent"
  shows "s⇩0 ⊨ s ⟹ Agent n ∉ parts (used s)"
by (rule notI, drule rtrancl_start, assumption, subst parts_init, simp add:
 Range_iff image_def A, (erule exE)+, (erule conjE)+, drule parts_agent_start)


lemma idinfo_init_1 [rule_format]:
  assumes A: "s⇩0 ⊨ s"
  shows "⟦s ⊢ s'; n ∉ bad_id_password ∪ bad_id_pubkey ∪ bad_id_shakey;
    ∀X. ⟨n, X⟩ ∉ spied s⟧ ⟹
  ⟨n, X⟩ ∉ spied s'"
by (rule notI, simp add: rel_def, ((erule disjE)?, (erule exE)+, (blast | simp,
 ((drule idinfo_dec [OF A] | drule idinfo_sep [OF A]), simp, blast |
 (erule conjE)+, drule parts_agent [OF A], blast))?)+)

proposition idinfo_init:
 "⟦s⇩0 ⊨ s; n ∉ bad_id_password ∪ bad_id_pubkey ∪ bad_id_shakey⟧ ⟹
  ⟨n, X⟩ ∉ spied s"
by (induction arbitrary: X rule: rtrancl_induct, simp add: image_def, blast,
 rule idinfo_init_1)


lemma idinfo_mpair_1 [rule_format]:
 "⟦(s, s') ∈ rel_id_hash ∪ rel_id_crypt ∪ rel_id_sep ∪ rel_id_con;
    ∀X Y. ⟨n, ⦃X, Y⦄⟩ ∈ spied s ⟶
      key_sets ⦃X, Y⦄ (crypts (Log -` spied s)) ≠ {};
    ⟨n, ⦃X, Y⦄⟩ ∈ spied s'⟧ ⟹
  key_sets ⦃X, Y⦄ (crypts (Log -` spied s')) ≠ {}"
by ((erule disjE)?, clarify?, simp add: image_iff Image_def, (drule subsetD
 [OF key_sets_crypts_hash] | drule key_sets_range, blast | (drule spec)+,
 drule mp, simp, simp add: ex_in_conv [symmetric], erule exE, frule subsetD
 [OF key_sets_crypts_fst], drule subsetD [OF key_sets_crypts_snd])?)+

lemma idinfo_mpair_2 [rule_format]:
  assumes A: "s⇩0 ⊨ s"
  shows "⟦s ⊢ s'; (s, s') ∉ rel_id_hash ∪ rel_id_crypt ∪ rel_id_sep ∪ rel_id_con;
    ∀X Y. ⟨n, ⦃X, Y⦄⟩ ∈ spied s ⟶
      key_sets ⦃X, Y⦄ (crypts (Log -` spied s)) ≠ {};
    ⟨n, ⦃X, Y⦄⟩ ∈ spied s'⟧ ⟹
  key_sets ⦃X, Y⦄ (crypts (Log -` spied s')) ≠ {}"
by (simp only: rel_def Un_iff de_Morgan_disj, simp, ((erule disjE)?, (erule exE)+,
 simp add: Image_def, (simp only: Collect_disj_eq crypts_union key_sets_union, simp)?,
 ((subst (asm) disj_assoc [symmetric])?, erule disjE, (drule idinfo_dec [OF A] |
 drule idinfo_sep [OF A]), simp+)?)+)

proposition idinfo_mpair [rule_format]:
 "s⇩0 ⊨ s ⟹
    ⟨n, ⦃X, Y⦄⟩ ∈ spied s ⟶
  key_sets ⦃X, Y⦄ (crypts (Log -` spied s)) ≠ {}"
proof (induction arbitrary: X Y rule: rtrancl_induct, simp add: image_def,
 rule impI)
  fix s s' X Y
  assume
   "s⇩0 ⊨ s" and
   "s ⊢ s'" and
   "⋀X Y. ⟨n, ⦃X, Y⦄⟩ ∈ spied s ⟶
      key_sets ⦃X, Y⦄ (crypts (Log -` spied s)) ≠ {}" and
   "⟨n, ⦃X, Y⦄⟩ ∈ spied s'"
  thus "key_sets ⦃X, Y⦄ (crypts (Log -` spied s')) ≠ {}"
    by (cases "(s, s') ∈ rel_id_hash ∪ rel_id_crypt ∪ rel_id_sep ∪ rel_id_con",
     erule_tac [2] idinfo_mpair_2, erule_tac idinfo_mpair_1, simp_all)
qed


proposition key_sets_pwd_empty:
 "s⇩0 ⊨ s ⟹
    key_sets (Hash (Pwd n)) (crypts (Log -` spied s)) = {} ∧
    key_sets ⦃Pwd n, X⦄ (crypts (Log -` spied s)) = {} ∧
    key_sets ⦃X, Pwd n⦄ (crypts (Log -` spied s)) = {}"
  (is "_ ⟹ key_sets ?X (?H s) = _ ∧ key_sets ?Y _ = _ ∧ key_sets ?Z _ = _")
proof (erule rtrancl_induct, simp add: image_iff Image_def)
  fix s s'
  assume
    A: "s⇩0 ⊨ s" and
    B: "s ⊢ s'" and
    C: "key_sets (Hash (Pwd n)) (?H s) = {} ∧
      key_sets ⦃Pwd n, X⦄ (?H s) = {} ∧
      key_sets ⦃X, Pwd n⦄ (?H s) = {}"
  show "key_sets (Hash (Pwd n)) (?H s') = {} ∧
    key_sets ⦃Pwd n, X⦄ (?H s') = {} ∧
    key_sets ⦃X, Pwd n⦄ (?H s') = {}"
    by (insert B C, simp add: rel_def, ((erule disjE)?, ((erule exE)+)?, simp add:
     image_iff Image_def, (simp only: Collect_disj_eq crypts_union
     key_sets_union, simp add: crypts_insert key_sets_insert)?,
     (frule log_dec [OF A, where Y = "?X"],
     frule log_dec [OF A, where Y = "?Y"], drule log_dec [OF A, where Y = "?Z"] |
     frule log_sep [OF A, where Z = "?X"], frule log_sep [OF A, where Z = "?Y"],
     drule log_sep [OF A, where Z = "?Z"])?)+)
qed

proposition key_sets_pwd_seskey [rule_format]:
 "s⇩0 ⊨ s ⟹
    U ∈ key_sets (Pwd n) (crypts (Log -` spied s)) ⟶
  (∃SK. U = {SesKey SK} ∧
    ((Owner n, Crypt (SesK SK) (Pwd n)) ∈ s ∨
     (Asset n, Crypt (SesK SK) (Num 0)) ∈ s))"
  (is "_ ⟹ _ ⟶ ?P s")
proof (erule rtrancl_induct, simp add: image_iff Image_def, rule impI)
  fix s s'
  assume
    A: "s⇩0 ⊨ s" and
    B: "s ⊢ s'" and
    C: "U ∈ key_sets (Pwd n) (crypts (Log -` spied s)) ⟶ ?P s" and
    D: "U ∈ key_sets (Pwd n) (crypts (Log -` spied s'))"
  show "?P s'"
    by (insert B C D, simp add: rel_def, ((erule disjE)?, ((erule exE)+)?, simp
     add: image_iff Image_def, (simp only: Collect_disj_eq crypts_union
     key_sets_union, simp add: crypts_insert key_sets_insert split: if_split_asm,
     blast?)?, (erule disjE, (drule log_dec [OF A] | drule log_sep [OF A]),
     (erule conjE)?, drule subsetD, simp)?)+)
qed


lemma pwd_anonymous_1 [rule_format]:
 "⟦s⇩0 ⊨ s; n ∉ bad_id_password⟧ ⟹
    ⟨n, Pwd n⟩ ∈ spied s ⟶
  (∃SK. SesKey SK ∈ spied s ∧
    ((Owner n, Crypt (SesK SK) (Pwd n)) ∈ s ∨
     (Asset n, Crypt (SesK SK) (Num 0)) ∈ s))"
  (is "⟦_; _⟧ ⟹ _ ⟶ ?P s")
proof (erule rtrancl_induct, simp add: image_def, rule impI)
  fix s s'
  assume
    A: "s⇩0 ⊨ s" and
    B: "s ⊢ s'" and
    C: "⟨n, Pwd n⟩ ∈ spied s ⟶ ?P s" and
    D: "⟨n, Pwd n⟩ ∈ spied s'"
  show "?P s'"
    by (insert B C D, simp add: rel_def, ((erule disjE)?, (erule exE)+, simp add:
     image_iff, blast?, ((subst (asm) disj_assoc [symmetric])?, erule disjE,
     (drule idinfo_dec [OF A] | drule idinfo_sep [OF A]), simp, blast+ |
     insert key_sets_pwd_empty [OF A], clarsimp)?, (((erule disjE)?, erule
     conjE, drule sym, simp, (drule key_sets_pwd_seskey [OF A] | drule
     idinfo_mpair [OF A, simplified]), simp)+ | drule key_sets_range, blast)?)+)
qed

theorem pwd_anonymous:
  assumes
    A: "s⇩0 ⊨ s" and
    B: "n ∉ bad_id_password" and
    C: "n ∉ bad_shakey ∩ (bad_pwd ∪ bad_prikey) ∩ (bad_id_pubkey ∪ bad_id_shak)"
  shows "⟨n, Pwd n⟩ ∉ spied s"
proof
  assume D: "⟨n, Pwd n⟩ ∈ spied s"
  hence "n ∈ bad_id_password ∪ bad_id_pubkey ∪ bad_id_shakey"
    by (rule contrapos_pp, rule_tac idinfo_init [OF A])
  moreover have "∃SK. SesKey SK ∈ spied s ∧
    ((Owner n, Crypt (SesK SK) (Pwd n)) ∈ s ∨
     (Asset n, Crypt (SesK SK) (Num 0)) ∈ s)"
    (is "∃SK. ?P SK ∧ (?Q SK ∨ ?R SK)")
    by (rule pwd_anonymous_1 [OF A B D])
  then obtain SK where "?P SK" and "?Q SK ∨ ?R SK" by blast
  moreover {
    assume "?Q SK"
    hence "n ∈ bad_shakey ∩ bad_prikey"
      by (rule_tac contrapos_pp [OF ‹?P SK›], rule_tac owner_seskey_secret [OF A])
  }
  moreover {
    assume "?R SK"
    hence "n ∈ bad_shakey ∩ (bad_pwd ∪ bad_prikey)"
      by (rule_tac contrapos_pp [OF ‹?P SK›], rule_tac asset_seskey_secret [OF A])
  }
  ultimately show False
    using B and C by blast
qed


proposition idinfo_pwd_start:
  assumes
    A: "s⇩0 ⊨ s" and
    B: "n ∉ bad_agent"
  shows "⟦s ⊢ s'; ∃X. ⟨n, X⟩ ∈ spied s' ∧ X ≠ Pwd n;
    ¬ (∃X. ⟨n, X⟩ ∈ spied s ∧ X ≠ Pwd n)⟧ ⟹
      ∃SK. SesKey SK ∈ spied s ∧
        ((Owner n, Crypt (SesK SK) (Pwd n)) ∈ s ∨
         (Asset n, Crypt (SesK SK) (Num 0)) ∈ s)"
proof (simp add: rel_def, insert parts_agent [OF A B], insert key_sets_pwd_empty
 [OF A], (erule disjE, (erule exE)+, simp, erule conjE, (subst (asm) disj_assoc
 [symmetric])?, (erule disjE)?, (drule idinfo_dec [OF A] | drule idinfo_sep
 [OF A] | drule spec, drule mp), simp+)+, auto, rule FalseE, rule_tac [3] FalseE)
  fix X U K
  assume "∀X. (Spy, ⟨n, X⟩) ∈ s ⟶ X = Pwd n" and "(Spy, ⟨n, K⟩) ∈ s"
  hence "K = Pwd n" by simp
  moreover assume "U ∈ key_sets X (crypts (Log -` spied s))"
  hence "U ⊆ range Key"
    by (rule key_sets_range)
  moreover assume "K ∈ U"
  ultimately show False by blast
next
  fix X U
  assume "∀X. (Spy, ⟨n, X⟩) ∈ s ⟶ X = Pwd n" and "(Spy, ⟨n, X⟩) ∈ s"
  hence C: "X = Pwd n" by simp
  moreover assume "U ∈ key_sets X (crypts (Log -` spied s))"
  ultimately have "U ∈ key_sets (Pwd n) (crypts (Log -` spied s))" by simp
  hence "∃SK. U = {SesKey SK} ∧
    ((Owner n, Crypt (SesK SK) (Pwd n)) ∈ s ∨
     (Asset n, Crypt (SesK SK) (Num 0)) ∈ s)"
    by (rule key_sets_pwd_seskey [OF A])
  moreover assume "U ⊆ spied s"
  ultimately show "∃x U V. (Spy, Key (SesK (x, U, V))) ∈ s ∧
    ((Owner n, Crypt (SesK (x, U, V)) X) ∈ s ∨
     (Asset n, Crypt (SesK (x, U, V)) (Num 0)) ∈ s)"
    using C by auto
next
  fix X U K
  assume "∀X. (Spy, ⟨n, X⟩) ∈ s ⟶ X = Pwd n" and "(Spy, ⟨n, K⟩) ∈ s"
  hence "K = Pwd n" by simp
  moreover assume "U ∈ key_sets X (crypts (Log -` spied s))"
  hence "U ⊆ range Key"
    by (rule key_sets_range)
  moreover assume "K ∈ U"
  ultimately show False by blast
qed

proposition idinfo_pwd:
 "⟦s⇩0 ⊨ s; ∃X. ⟨n, X⟩ ∈ spied s ∧ X ≠ Pwd n;
    n ∉ bad_id_pubkey ∪ bad_id_shakey⟧ ⟹
  ∃SK. SesKey SK ∈ spied s ∧
    ((Owner n, Crypt (SesK SK) (Pwd n)) ∈ s ∨
     (Asset n, Crypt (SesK SK) (Num 0)) ∈ s)"
by (drule rtrancl_start, assumption, simp, blast, (erule exE)+, (erule conjE)+,
 frule idinfo_pwd_start [of _ n], simp+, drule r_into_rtrancl, drule rtrancl_trans,
 assumption, (drule state_subset)+, blast)


theorem auth_prikey_anonymous:
  assumes
    A: "s⇩0 ⊨ s" and
    B: "n ∉ bad_id_prikey" and
    C: "n ∉ bad_shakey ∩ bad_prikey ∩ (bad_id_password ∪ bad_id_shak)"
  shows "⟨n, Auth_PriKey n⟩ ∉ spied s"
proof
  assume D: "⟨n, Auth_PriKey n⟩ ∈ spied s"
  hence "n ∈ bad_id_password ∪ bad_id_pubkey ∪ bad_id_shakey"
    by (rule contrapos_pp, rule_tac idinfo_init [OF A])
  moreover have "Auth_PriKey n ∈ spied s"
    by (rule idinfo_msg [OF A D])
  hence "n ∈ bad_prikey"
    by (rule contrapos_pp, rule_tac auth_prikey_secret [OF A])
  moreover from this have E: "n ∉ bad_id_pubkey"
    using B by simp
  moreover have "n ∈ bad_shakey"
  proof (cases "n ∈ bad_id_shakey", simp)
    case False
    with D and E have "∃SK. SesKey SK ∈ spied s ∧
      ((Owner n, Crypt (SesK SK) (Pwd n)) ∈ s ∨
       (Asset n, Crypt (SesK SK) (Num 0)) ∈ s)"
      (is "∃SK. ?P SK ∧ (?Q SK ∨ ?R SK)")
      by (rule_tac idinfo_pwd [OF A], rule_tac exI [of _ "Auth_PriKey n"], simp_all)
    then obtain SK where "?P SK" and "?Q SK ∨ ?R SK" by blast
    moreover {
      assume "?Q SK"
      hence "n ∈ bad_shakey ∩ bad_prikey"
        by (rule_tac contrapos_pp [OF ‹?P SK›], rule_tac owner_seskey_secret
         [OF A])
    }
    moreover {
      assume "?R SK"
      hence "n ∈ bad_shakey ∩ (bad_pwd ∪ bad_prikey)"
        by (rule_tac contrapos_pp [OF ‹?P SK›], rule_tac asset_seskey_secret
         [OF A])
    }
    ultimately show ?thesis by blast
  qed
  ultimately show False
    using C by blast
qed


theorem auth_shakey_anonymous:
  assumes
    A: "s⇩0 ⊨ s" and
    B: "n ∉ bad_id_shakey" and
    C: "n ∉ bad_shakey ∩ (bad_id_password ∪ bad_id_pubkey)"
  shows "⟨n, Key (Auth_ShaKey n)⟩ ∉ spied s"
proof
  assume D: "⟨n, Key (Auth_ShaKey n)⟩ ∈ spied s"
  hence "n ∈ bad_id_password ∪ bad_id_pubkey ∪ bad_id_shakey"
    by (rule contrapos_pp, rule_tac idinfo_init [OF A])
  moreover have "Key (Auth_ShaKey n) ∈ spied s"
    by (rule idinfo_msg [OF A D])
  hence "n ∈ bad_shakey"
    by (rule contrapos_pp, rule_tac auth_shakey_secret [OF A])
  ultimately show False
    using B and C by blast
qed

end