diff --git a/thys/Relational_Method/Anonymity.thy b/thys/Relational_Method/Anonymity.thy
--- a/thys/Relational_Method/Anonymity.thy
+++ b/thys/Relational_Method/Anonymity.thy
@@ -1,591 +1,599 @@
 (*  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 \<open>
 \label{Anonymity}
 \<close>
 
 
 proposition crypts_empty [simp]:
  "crypts {} = {}"
 by (rule equalityI, rule subsetI, erule crypts.induct, simp_all)
 
 proposition crypts_mono:
  "H \<subseteq> H' \<Longrightarrow> crypts H \<subseteq> crypts H'"
 by (rule subsetI, erule crypts.induct, auto)
 
 lemma crypts_union_1:
  "crypts (H \<union> H') \<subseteq> crypts H \<union> crypts H'"
 by (rule subsetI, erule crypts.induct, auto)
 
 lemma crypts_union_2:
  "crypts H \<union> crypts H' \<subseteq> crypts (H \<union> H')"
 by (rule subsetI, erule UnE, erule_tac [!] crypts.induct, auto)
 
 proposition crypts_union:
  "crypts (H \<union> H') = crypts H \<union> crypts H'"
 by (rule equalityI, rule crypts_union_1, rule crypts_union_2)
 
 proposition crypts_insert:
  "crypts (insert X H) = crypts_msg X \<union> 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 \<otimes> B) = {A \<otimes> 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} \<subseteq> 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}) \<subseteq> 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 \<in> crypts H \<Longrightarrow> Crypt K X \<in> 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} \<subseteq> 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} \<subseteq> 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 {\<lbrace>X, Y\<rbrace>} \<subseteq> insert \<lbrace>X, Y\<rbrace> (crypts {X} \<union> 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 \<lbrace>X, Y\<rbrace> (crypts {X} \<union> crypts {Y}) \<subseteq> crypts {\<lbrace>X, Y\<rbrace>}"
 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 \<lbrace>X, Y\<rbrace> = insert \<lbrace>X, Y\<rbrace> (crypts_msg X \<union> 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 \<subseteq> H' \<Longrightarrow> key_sets X H \<subseteq> key_sets X H'"
 by (auto simp add: key_sets_def)
 
 proposition key_sets_union:
  "key_sets X (H \<union> H') = key_sets X H \<union> 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 \<union> 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 \<otimes> B) = (if X = A \<otimes> 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 \<noteq> Crypt K Y \<Longrightarrow>
     key_sets X {Crypt K Y} \<subseteq> 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} \<subseteq> 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 \<lbrace>Y, Z\<rbrace> = (if X = \<lbrace>Y, Z\<rbrace> 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 \<in> key_sets X H \<Longrightarrow> U \<subseteq> range Key"
 by (simp add: key_sets_def, blast)
 
 proposition key_sets_crypts_hash:
  "key_sets (Hash X) (crypts H) \<subseteq> key_sets X (crypts H)"
 by (simp add: key_sets_def, blast)
 
 proposition key_sets_crypts_fst:
  "key_sets \<lbrace>X, Y\<rbrace> (crypts H) \<subseteq> key_sets X (crypts H)"
 by (simp add: key_sets_def, blast)
 
 proposition key_sets_crypts_snd:
  "key_sets \<lbrace>X, Y\<rbrace> (crypts H) \<subseteq> key_sets Y (crypts H)"
 by (simp add: key_sets_def, blast)
 
 
 lemma log_spied_1:
  "\<lbrakk>s \<turnstile> s';
     Log X \<in> parts (used s) \<longrightarrow> Log X \<in> spied s;
     Log X \<in> parts (used s')\<rbrakk> \<Longrightarrow>
   Log X \<in> 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\<^sub>0 \<Turnstile> s \<Longrightarrow>
     Log X \<in> parts (used s) \<longrightarrow>
   Log X \<in> spied s"
 by (erule rtrancl_induct, subst parts_init, simp add: Range_iff image_def, rule impI,
  rule log_spied_1)
 
 
 proposition log_dec:
  "\<lbrakk>s\<^sub>0 \<Turnstile> s; s' = insert (Spy, X) s \<and> (Spy, Crypt K X) \<in> s \<and>
     (Spy, Key (InvK K)) \<in> s\<rbrakk> \<Longrightarrow>
   key_sets Y (crypts {Y. Log Y = X}) \<subseteq> 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:
  "\<lbrakk>s\<^sub>0 \<Turnstile> s; s' = insert (Spy, X) (insert (Spy, Y) s) \<and> (Spy, \<lbrace>X, Y\<rbrace>) \<in> s\<rbrakk> \<Longrightarrow>
     key_sets Z (crypts {Z. Log Z = X}) \<subseteq> key_sets Z (crypts (Log -` spied s)) \<and>
     key_sets Z (crypts {Z. Log Z = Y}) \<subseteq> 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:
  "\<lbrakk>s \<turnstile> s';
     \<langle>n, X\<rangle> \<in> parts (used s) \<longrightarrow> \<langle>n, X\<rangle> \<in> spied s;
     \<langle>n, X\<rangle> \<in> parts (used s')\<rbrakk> \<Longrightarrow>
   \<langle>n, X\<rangle> \<in> 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\<^sub>0 \<Turnstile> s \<Longrightarrow>
     \<langle>n, X\<rangle> \<in> parts (used s) \<longrightarrow>
   \<langle>n, X\<rangle> \<in> spied s"
 by (erule rtrancl_induct, subst parts_init, simp add: Range_iff image_def, rule impI,
  rule idinfo_spied_1)
 
 
 proposition idinfo_dec:
  "\<lbrakk>s\<^sub>0 \<Turnstile> s; s' = insert (Spy, X) s \<and> (Spy, Crypt K X) \<in> s \<and>
     (Spy, Key (InvK K)) \<in> s; \<langle>n, Y\<rangle> = X\<rbrakk> \<Longrightarrow>
   \<langle>n, Y\<rangle> \<in> spied s"
 by (drule parts_dec [where Y = "\<langle>n, Y\<rangle>"], drule sym, simp, rule idinfo_spied)
 
 proposition idinfo_sep:
  "\<lbrakk>s\<^sub>0 \<Turnstile> s; s' = insert (Spy, X) (insert (Spy, Y) s) \<and> (Spy, \<lbrace>X, Y\<rbrace>) \<in> s;
     \<langle>n, Z\<rangle> = X \<or> \<langle>n, Z\<rangle> = Y\<rbrakk> \<Longrightarrow>
   \<langle>n, Z\<rangle> \<in> spied s"
 by (drule parts_sep [where Z = "\<langle>n, Z\<rangle>"], erule disjE, (drule sym, simp)+,
  rule idinfo_spied)
 
 
 lemma idinfo_msg_1:
   assumes A: "s\<^sub>0 \<Turnstile> s"
   shows "\<lbrakk>s \<turnstile> s'; \<langle>n, X\<rangle> \<in> spied s \<longrightarrow> X \<in> spied s; \<langle>n, X\<rangle> \<in> spied s'\<rbrakk> \<Longrightarrow>
     X \<in> 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\<^sub>0 \<Turnstile> s \<Longrightarrow>
     \<langle>n, X\<rangle> \<in> spied s \<longrightarrow>
   X \<in> spied s"
 by (erule rtrancl_induct, simp, blast, rule impI, rule idinfo_msg_1)
 
 
 proposition parts_agent:
  "\<lbrakk>s\<^sub>0 \<Turnstile> s; n \<notin> bad_agent\<rbrakk> \<Longrightarrow> Agent n \<notin> parts (used s)"
-by (erule rtrancl_induct, subst parts_init, simp add: Range_iff image_def, simp
- add: rel_def, ((erule disjE)?, (erule exE)+, simp add: parts_insert image_iff,
+  apply (erule rtrancl_induct)
+  subgoal
+    apply (subst parts_init)
+    apply (simp add: Range_iff image_def)
+    done
+  subgoal
+    apply (simp add: rel_def)
+    apply ((erule disjE)?, (erule exE)+, simp add: parts_insert image_iff,
  (rule ccontr, (drule parts_dec | drule parts_enc | drule parts_sep |
- drule parts_con), simp+)?)+)
+ drule parts_con), simp+)?)+
+    done
+  done
 
 lemma idinfo_init_1 [rule_format]:
   assumes A: "s\<^sub>0 \<Turnstile> s"
   shows "\<lbrakk>s \<turnstile> s'; n \<notin> bad_id_password \<union> bad_id_pubkey \<union> bad_id_shakey;
     \<forall>X. \<langle>n, X\<rangle> \<notin> spied s\<rbrakk> \<Longrightarrow>
   \<langle>n, X\<rangle> \<notin> 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:
  "\<lbrakk>s\<^sub>0 \<Turnstile> s; n \<notin> bad_id_password \<union> bad_id_pubkey \<union> bad_id_shakey\<rbrakk> \<Longrightarrow>
   \<langle>n, X\<rangle> \<notin> spied s"
 by (induction arbitrary: X rule: rtrancl_induct, simp add: image_def, blast,
  rule idinfo_init_1)
 
 
 lemma idinfo_mpair_1 [rule_format]:
  "\<lbrakk>(s, s') \<in> rel_id_hash \<union> rel_id_crypt \<union> rel_id_sep \<union> rel_id_con;
     \<forall>X Y. \<langle>n, \<lbrace>X, Y\<rbrace>\<rangle> \<in> spied s \<longrightarrow>
       key_sets \<lbrace>X, Y\<rbrace> (crypts (Log -` spied s)) \<noteq> {};
     \<langle>n, \<lbrace>X, Y\<rbrace>\<rangle> \<in> spied s'\<rbrakk> \<Longrightarrow>
   key_sets \<lbrace>X, Y\<rbrace> (crypts (Log -` spied s')) \<noteq> {}"
 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\<^sub>0 \<Turnstile> s"
   shows "\<lbrakk>s \<turnstile> s'; (s, s') \<notin> rel_id_hash \<union> rel_id_crypt \<union> rel_id_sep \<union> rel_id_con;
     \<forall>X Y. \<langle>n, \<lbrace>X, Y\<rbrace>\<rangle> \<in> spied s \<longrightarrow>
       key_sets \<lbrace>X, Y\<rbrace> (crypts (Log -` spied s)) \<noteq> {};
     \<langle>n, \<lbrace>X, Y\<rbrace>\<rangle> \<in> spied s'\<rbrakk> \<Longrightarrow>
   key_sets \<lbrace>X, Y\<rbrace> (crypts (Log -` spied s')) \<noteq> {}"
 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\<^sub>0 \<Turnstile> s \<Longrightarrow>
     \<langle>n, \<lbrace>X, Y\<rbrace>\<rangle> \<in> spied s \<longrightarrow>
   key_sets \<lbrace>X, Y\<rbrace> (crypts (Log -` spied s)) \<noteq> {}"
 proof (induction arbitrary: X Y rule: rtrancl_induct, simp add: image_def,
  rule impI)
   fix s s' X Y
   assume
    "s\<^sub>0 \<Turnstile> s" and
    "s \<turnstile> s'" and
    "\<And>X Y. \<langle>n, \<lbrace>X, Y\<rbrace>\<rangle> \<in> spied s \<longrightarrow>
       key_sets \<lbrace>X, Y\<rbrace> (crypts (Log -` spied s)) \<noteq> {}" and
    "\<langle>n, \<lbrace>X, Y\<rbrace>\<rangle> \<in> spied s'"
   thus "key_sets \<lbrace>X, Y\<rbrace> (crypts (Log -` spied s')) \<noteq> {}"
     by (cases "(s, s') \<in> rel_id_hash \<union> rel_id_crypt \<union> rel_id_sep \<union> rel_id_con",
      erule_tac [2] idinfo_mpair_2, erule_tac idinfo_mpair_1, simp_all)
 qed
 
 
 proposition key_sets_pwd_empty:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow>
     key_sets (Hash (Pwd n)) (crypts (Log -` spied s)) = {} \<and>
     key_sets \<lbrace>Pwd n, X\<rbrace> (crypts (Log -` spied s)) = {} \<and>
     key_sets \<lbrace>X, Pwd n\<rbrace> (crypts (Log -` spied s)) = {}"
   (is "_ \<Longrightarrow> key_sets ?X (?H s) = _ \<and> key_sets ?Y _ = _ \<and> key_sets ?Z _ = _")
 proof (erule rtrancl_induct, simp add: image_iff Image_def)
   fix s s'
   assume
     A: "s\<^sub>0 \<Turnstile> s" and
     B: "s \<turnstile> s'" and
     C: "key_sets (Hash (Pwd n)) (?H s) = {} \<and>
       key_sets \<lbrace>Pwd n, X\<rbrace> (?H s) = {} \<and>
       key_sets \<lbrace>X, Pwd n\<rbrace> (?H s) = {}"
   show "key_sets (Hash (Pwd n)) (?H s') = {} \<and>
     key_sets \<lbrace>Pwd n, X\<rbrace> (?H s') = {} \<and>
     key_sets \<lbrace>X, Pwd n\<rbrace> (?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\<^sub>0 \<Turnstile> s \<Longrightarrow>
     U \<in> key_sets (Pwd n) (crypts (Log -` spied s)) \<longrightarrow>
   (\<exists>SK. U = {SesKey SK} \<and>
     ((Owner n, Crypt (SesK SK) (Pwd n)) \<in> s \<or>
      (Asset n, Crypt (SesK SK) (Num 0)) \<in> s))"
   (is "_ \<Longrightarrow> _ \<longrightarrow> ?P s")
 proof (erule rtrancl_induct, simp add: image_iff Image_def, rule impI)
   fix s s'
   assume
     A: "s\<^sub>0 \<Turnstile> s" and
     B: "s \<turnstile> s'" and
     C: "U \<in> key_sets (Pwd n) (crypts (Log -` spied s)) \<longrightarrow> ?P s" and
     D: "U \<in> 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]:
  "\<lbrakk>s\<^sub>0 \<Turnstile> s; n \<notin> bad_id_password\<rbrakk> \<Longrightarrow>
     \<langle>n, Pwd n\<rangle> \<in> spied s \<longrightarrow>
   (\<exists>SK. SesKey SK \<in> spied s \<and>
     ((Owner n, Crypt (SesK SK) (Pwd n)) \<in> s \<or>
      (Asset n, Crypt (SesK SK) (Num 0)) \<in> s))"
   (is "\<lbrakk>_; _\<rbrakk> \<Longrightarrow> _ \<longrightarrow> ?P s")
 proof (erule rtrancl_induct, simp add: image_def, rule impI)
   fix s s'
   assume
     A: "s\<^sub>0 \<Turnstile> s" and
     B: "s \<turnstile> s'" and
     C: "\<langle>n, Pwd n\<rangle> \<in> spied s \<longrightarrow> ?P s" and
     D: "\<langle>n, Pwd n\<rangle> \<in> 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\<^sub>0 \<Turnstile> s" and
     B: "n \<notin> bad_id_password" and
     C: "n \<notin> bad_shakey \<inter> (bad_pwd \<union> bad_prikey) \<inter> (bad_id_pubkey \<union> bad_id_shak)"
   shows "\<langle>n, Pwd n\<rangle> \<notin> spied s"
 proof
   assume D: "\<langle>n, Pwd n\<rangle> \<in> spied s"
   hence "n \<in> bad_id_password \<union> bad_id_pubkey \<union> bad_id_shakey"
     by (rule contrapos_pp, rule_tac idinfo_init [OF A])
   moreover have "\<exists>SK. SesKey SK \<in> spied s \<and>
     ((Owner n, Crypt (SesK SK) (Pwd n)) \<in> s \<or>
      (Asset n, Crypt (SesK SK) (Num 0)) \<in> s)"
     (is "\<exists>SK. ?P SK \<and> (?Q SK \<or> ?R SK)")
     by (rule pwd_anonymous_1 [OF A B D])
   then obtain SK where "?P SK" and "?Q SK \<or> ?R SK" by blast
   moreover {
     assume "?Q SK"
     hence "n \<in> bad_shakey \<inter> bad_prikey"
       by (rule_tac contrapos_pp [OF `?P SK`], rule_tac owner_seskey_secret [OF A])
   }
   moreover {
     assume "?R SK"
     hence "n \<in> bad_shakey \<inter> (bad_pwd \<union> 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\<^sub>0 \<Turnstile> s" and
     B: "n \<notin> bad_agent"
   shows "\<lbrakk>s \<turnstile> s'; \<exists>X. \<langle>n, X\<rangle> \<in> spied s' \<and> X \<noteq> Pwd n;
     \<not> (\<exists>X. \<langle>n, X\<rangle> \<in> spied s \<and> X \<noteq> Pwd n)\<rbrakk> \<Longrightarrow>
       \<exists>SK. SesKey SK \<in> spied s \<and>
         ((Owner n, Crypt (SesK SK) (Pwd n)) \<in> s \<or>
          (Asset n, Crypt (SesK SK) (Num 0)) \<in> 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 "\<forall>X. (Spy, \<langle>n, X\<rangle>) \<in> s \<longrightarrow> X = Pwd n" and "(Spy, \<langle>n, K\<rangle>) \<in> s"
   hence "K = Pwd n" by simp
   moreover assume "U \<in> key_sets X (crypts (Log -` spied s))"
   hence "U \<subseteq> range Key"
     by (rule key_sets_range)
   moreover assume "K \<in> U"
   ultimately show False by blast
 next
   fix X U
   assume "\<forall>X. (Spy, \<langle>n, X\<rangle>) \<in> s \<longrightarrow> X = Pwd n" and "(Spy, \<langle>n, X\<rangle>) \<in> s"
   hence C: "X = Pwd n" by simp
   moreover assume "U \<in> key_sets X (crypts (Log -` spied s))"
   ultimately have "U \<in> key_sets (Pwd n) (crypts (Log -` spied s))" by simp
   hence "\<exists>SK. U = {SesKey SK} \<and>
     ((Owner n, Crypt (SesK SK) (Pwd n)) \<in> s \<or>
      (Asset n, Crypt (SesK SK) (Num 0)) \<in> s)"
     by (rule key_sets_pwd_seskey [OF A])
   moreover assume "U \<subseteq> spied s"
   ultimately show "\<exists>x U V. (Spy, Key (SesK (x, U, V))) \<in> s \<and>
     ((Owner n, Crypt (SesK (x, U, V)) X) \<in> s \<or>
      (Asset n, Crypt (SesK (x, U, V)) (Num 0)) \<in> s)"
     using C by auto
 next
   fix X U K
   assume "\<forall>X. (Spy, \<langle>n, X\<rangle>) \<in> s \<longrightarrow> X = Pwd n" and "(Spy, \<langle>n, K\<rangle>) \<in> s"
   hence "K = Pwd n" by simp
   moreover assume "U \<in> key_sets X (crypts (Log -` spied s))"
   hence "U \<subseteq> range Key"
     by (rule key_sets_range)
   moreover assume "K \<in> U"
   ultimately show False by blast
 qed
 
 proposition idinfo_pwd:
  "\<lbrakk>s\<^sub>0 \<Turnstile> s; \<exists>X. \<langle>n, X\<rangle> \<in> spied s \<and> X \<noteq> Pwd n;
     n \<notin> bad_id_pubkey \<union> bad_id_shakey\<rbrakk> \<Longrightarrow>
   \<exists>SK. SesKey SK \<in> spied s \<and>
     ((Owner n, Crypt (SesK SK) (Pwd n)) \<in> s \<or>
      (Asset n, Crypt (SesK SK) (Num 0)) \<in> 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\<^sub>0 \<Turnstile> s" and
     B: "n \<notin> bad_id_prikey" and
     C: "n \<notin> bad_shakey \<inter> bad_prikey \<inter> (bad_id_password \<union> bad_id_shak)"
   shows "\<langle>n, Auth_PriKey n\<rangle> \<notin> spied s"
 proof
   assume D: "\<langle>n, Auth_PriKey n\<rangle> \<in> spied s"
   hence "n \<in> bad_id_password \<union> bad_id_pubkey \<union> bad_id_shakey"
     by (rule contrapos_pp, rule_tac idinfo_init [OF A])
   moreover have "Auth_PriKey n \<in> spied s"
     by (rule idinfo_msg [OF A D])
   hence "n \<in> bad_prikey"
     by (rule contrapos_pp, rule_tac auth_prikey_secret [OF A])
   moreover from this have E: "n \<notin> bad_id_pubkey"
     using B by simp
   moreover have "n \<in> bad_shakey"
   proof (cases "n \<in> bad_id_shakey", simp)
     case False
     with D and E have "\<exists>SK. SesKey SK \<in> spied s \<and>
       ((Owner n, Crypt (SesK SK) (Pwd n)) \<in> s \<or>
        (Asset n, Crypt (SesK SK) (Num 0)) \<in> s)"
       (is "\<exists>SK. ?P SK \<and> (?Q SK \<or> ?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 \<or> ?R SK" by blast
     moreover {
       assume "?Q SK"
       hence "n \<in> bad_shakey \<inter> bad_prikey"
         by (rule_tac contrapos_pp [OF `?P SK`], rule_tac owner_seskey_secret
          [OF A])
     }
     moreover {
       assume "?R SK"
       hence "n \<in> bad_shakey \<inter> (bad_pwd \<union> 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\<^sub>0 \<Turnstile> s" and
     B: "n \<notin> bad_id_shakey" and
     C: "n \<notin> bad_shakey \<inter> (bad_id_password \<union> bad_id_pubkey)"
   shows "\<langle>n, Key (Auth_ShaKey n)\<rangle> \<notin> spied s"
 proof
   assume D: "\<langle>n, Key (Auth_ShaKey n)\<rangle> \<in> spied s"
   hence "n \<in> bad_id_password \<union> bad_id_pubkey \<union> bad_id_shakey"
     by (rule contrapos_pp, rule_tac idinfo_init [OF A])
   moreover have "Key (Auth_ShaKey n) \<in> spied s"
     by (rule idinfo_msg [OF A D])
   hence "n \<in> bad_shakey"
     by (rule contrapos_pp, rule_tac auth_shakey_secret [OF A])
   ultimately show False
     using B and C by blast
 qed
 
 
-end
+end
\ No newline at end of file
diff --git a/thys/Relational_Method/Authentication.thy b/thys/Relational_Method/Authentication.thy
--- a/thys/Relational_Method/Authentication.thy
+++ b/thys/Relational_Method/Authentication.thy
@@ -1,1903 +1,1903 @@
 (*  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 "Confidentiality and authenticity properties"
 
 theory Authentication
   imports Definitions
 begin
 
 text \<open>
 \label{Authentication}
 \<close>
 
 
 proposition rtrancl_start [rule_format]:
  "(x, y) \<in> r\<^sup>* \<Longrightarrow> P y \<longrightarrow> \<not> P x \<longrightarrow>
     (\<exists>u v. (x, u) \<in> r\<^sup>* \<and> (u, v) \<in> r \<and> (v, y) \<in> r\<^sup>* \<and> \<not> P u \<and> P v)"
   (is "_ \<Longrightarrow> _ \<longrightarrow> _ \<longrightarrow> (\<exists>u v. ?Q x y u v)")
 proof (erule rtrancl_induct, simp, (rule impI)+)
   fix y z
   assume
     A: "(x, y) \<in> r\<^sup>*" and
     B: "(y, z) \<in> r" and
     C: "P z"
   assume "P y \<longrightarrow> \<not> P x \<longrightarrow>(\<exists>u v. ?Q x y u v)" and "\<not> P x"
   hence D: "P y \<longrightarrow> (\<exists>u v. ?Q x y u v)" by simp
   show "\<exists>u v. ?Q x z u v"
   proof (cases "P y")
     case True
     with D obtain u v where "?Q x y u v" by blast
     moreover from this and B have "(v, z) \<in> r\<^sup>*" by auto
     ultimately show ?thesis by blast
   next
     case False
     with A and B and C have "?Q x z y z" by simp
     thus ?thesis by blast
   qed
 qed
 
 
 proposition state_subset:
  "s \<Turnstile> s' \<Longrightarrow> s \<subseteq> s'"
 by (erule rtrancl_induct, auto simp add: rel_def image_def)
 
 proposition spied_subset:
  "s \<Turnstile> s' \<Longrightarrow> spied s \<subseteq> spied s'"
 by (rule Image_mono, erule state_subset, simp)
 
 proposition used_subset:
  "s \<Turnstile> s' \<Longrightarrow> used s \<subseteq> used s'"
 by (rule Range_mono, rule state_subset)
 
 proposition asset_ii_init:
  "\<lbrakk>s\<^sub>0 \<Turnstile> s; (Asset n, \<lbrace>Num 2, PubKey A\<rbrace>) \<in> s\<rbrakk> \<Longrightarrow>
     PriKey A \<notin> spied s\<^sub>0"
 by (drule rtrancl_start, assumption, simp add: image_def, (erule exE)+,
  erule conjE, rule notI, drule spied_subset, drule subsetD, assumption,
  auto simp add: rel_def)
 
 proposition auth_prikey_used:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow> Auth_PriKey n \<in> used s"
 by (drule used_subset, erule subsetD, simp add: Range_iff image_def, blast)
 
 proposition asset_i_used:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow>
     (Asset n, Crypt (Auth_ShaKey n) (PriKey A)) \<in> s \<longrightarrow>
   PriKey A \<in> used s"
 by (erule rtrancl_induct, auto simp add: rel_def image_def)
 
 proposition owner_ii_used:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow>
     (Owner n, \<lbrace>Num 1, PubKey A\<rbrace>) \<in> s \<longrightarrow>
   PriKey A \<in> used s"
 by (erule rtrancl_induct, auto simp add: rel_def image_def)
 
 proposition asset_ii_used:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow>
     (Asset n, \<lbrace>Num 2, PubKey A\<rbrace>) \<in> s \<longrightarrow>
   PriKey A \<in> used s"
 by (erule rtrancl_induct, auto simp add: rel_def image_def)
 
 proposition owner_iii_used:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow>
     (Owner n, \<lbrace>Num 3, PubKey A\<rbrace>) \<in> s \<longrightarrow>
   PriKey A \<in> used s"
 by (erule rtrancl_induct, auto simp add: rel_def image_def)
 
 proposition asset_iii_used:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow>
     (Asset n, \<lbrace>Num 4, PubKey A\<rbrace>) \<in> s \<longrightarrow>
   PriKey A \<in> used s"
 by (erule rtrancl_induct, auto simp add: rel_def image_def)
 
 proposition asset_i_unique [rule_format]:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow>
     (Asset m, Crypt (Auth_ShaKey m) (PriKey A)) \<in> s \<longrightarrow>
     (Asset n, Crypt (Auth_ShaKey n) (PriKey A)) \<in> s \<longrightarrow>
   m = n"
 by (erule rtrancl_induct, simp add: image_def, frule asset_i_used [of _ m A],
  drule asset_i_used [of _ n A], auto simp add: rel_def)
 
 proposition owner_ii_unique [rule_format]:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow>
     (Owner m, \<lbrace>Num 1, PubKey A\<rbrace>) \<in> s \<longrightarrow>
     (Owner n, \<lbrace>Num 1, PubKey A\<rbrace>) \<in> s \<longrightarrow>
   m = n"
 by (erule rtrancl_induct, simp add: image_def, frule owner_ii_used [of _ m A],
  drule owner_ii_used [of _ n A], auto simp add: rel_def)
 
 proposition asset_ii_unique [rule_format]:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow>
     (Asset m, \<lbrace>Num 2, PubKey A\<rbrace>) \<in> s \<longrightarrow>
     (Asset n, \<lbrace>Num 2, PubKey A\<rbrace>) \<in> s \<longrightarrow>
   m = n"
 by (erule rtrancl_induct, simp add: image_def, frule asset_ii_used [of _ m A],
  drule asset_ii_used [of _ n A], auto simp add: rel_def)
 
 proposition auth_prikey_asset_i [rule_format]:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow>
     (Asset m, Crypt (Auth_ShaKey m) (Auth_PriKey n)) \<in> s \<longrightarrow>
   False"
 by (erule rtrancl_induct, simp add: image_def, drule auth_prikey_used [of _ n],
  auto simp add: rel_def)
 
 proposition auth_pubkey_owner_ii [rule_format]:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow>
     (Owner m, \<lbrace>Num 1, Auth_PubKey n\<rbrace>) \<in> s \<longrightarrow>
   False"
 by (erule rtrancl_induct, simp add: image_def, drule auth_prikey_used [of _ n],
  auto simp add: rel_def)
 
 proposition auth_pubkey_asset_ii [rule_format]:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow>
     (Asset m, \<lbrace>Num 2, Auth_PubKey n\<rbrace>) \<in> s \<longrightarrow>
   False"
 by (erule rtrancl_induct, simp add: image_def, drule auth_prikey_used [of _ n],
  auto simp add: rel_def)
 
 proposition asset_i_owner_ii [rule_format]:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow>
     (Asset m, Crypt (Auth_ShaKey m) (PriKey A)) \<in> s \<longrightarrow>
     (Owner n, \<lbrace>Num 1, PubKey A\<rbrace>) \<in> s \<longrightarrow>
   False"
 by (erule rtrancl_induct, simp add: image_def, frule asset_i_used [of _ m A],
  drule owner_ii_used [of _ n A], auto simp add: rel_def)
 
 proposition asset_i_asset_ii [rule_format]:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow>
     (Asset m, Crypt (Auth_ShaKey m) (PriKey A)) \<in> s \<longrightarrow>
     (Asset n, \<lbrace>Num 2, PubKey A\<rbrace>) \<in> s \<longrightarrow>
   False"
 by (erule rtrancl_induct, simp add: image_def, frule asset_i_used [of _ m A],
  drule asset_ii_used [of _ n A], auto simp add: rel_def)
 
 proposition asset_ii_owner_ii [rule_format]:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow>
     (Asset m, \<lbrace>Num 2, PubKey A\<rbrace>) \<in> s \<longrightarrow>
     (Owner n, \<lbrace>Num 1, PubKey A\<rbrace>) \<in> s \<longrightarrow>
   False"
 by (erule rtrancl_induct, simp add: image_def, frule asset_ii_used [of _ m A],
  drule owner_ii_used [of _ n A], auto simp add: rel_def)
 
 proposition asset_iii_owner_iii [rule_format]:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow>
     (Asset m, \<lbrace>Num 4, PubKey A\<rbrace>) \<in> s \<longrightarrow>
     (Owner n, \<lbrace>Num 3, PubKey A\<rbrace>) \<in> s \<longrightarrow>
   False"
 by (erule rtrancl_induct, simp add: image_def, frule asset_iii_used [of _ m A],
  drule owner_iii_used [of _ n A], auto simp add: rel_def)
 
 proposition asset_iv_state [rule_format]:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow>
     (Asset n, Token n (Auth_PriK n) B C SK) \<in> s \<longrightarrow>
   (\<exists>A D. fst (snd SK) = {A, B} \<and> snd (snd SK) = {C, D} \<and>
     (Asset n, \<lbrace>Num 2, PubKey B\<rbrace>) \<in> s \<and> (Asset n, \<lbrace>Num 4, PubKey D\<rbrace>) \<in> s \<and>
     Crypt (SesK SK) (PubKey D) \<in> used s \<and> (Asset n, PubKey B) \<in> s)"
 by (erule rtrancl_induct, auto simp add: rel_def)
 
 proposition owner_v_state [rule_format]:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow>
     (Owner n, Crypt (SesK SK) (Pwd n)) \<in> s \<longrightarrow>
   (Owner n, SesKey SK) \<in> s \<and>
   (\<exists>A B C. Token n A B C SK \<in> used s \<and> B \<in> fst (snd SK))"
 by (erule rtrancl_induct, auto simp add: rel_def, blast)
 
 proposition asset_v_state [rule_format]:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow>
     (Asset n, Crypt (SesK SK) (Num 0)) \<in> s \<longrightarrow>
   (Asset n, SesKey SK) \<in> s \<and> Crypt (SesK SK) (Pwd n) \<in> used s"
 by (erule rtrancl_induct, simp_all add: rel_def image_def,
  ((erule disjE)?, (erule exE)+, simp add: Range_Un_eq)+)
 
 lemma owner_seskey_nonce_1:
  "\<lbrakk>s \<turnstile> s';
     (Owner n, SesKey SK) \<in> s \<longrightarrow>
       (\<exists>S. fst SK = Some S \<and> Crypt (Auth_ShaKey n) (PriKey S) \<in> used s) \<or>
       fst SK = None;
     (Owner n, SesKey SK) \<in> s'\<rbrakk> \<Longrightarrow>
   (\<exists>S. fst SK = Some S \<and> Crypt (Auth_ShaKey n) (PriKey S) \<in> used s') \<or>
   fst SK = None"
 by (simp add: rel_def, (erule disjE, (erule exE)+, simp+)+,
  split if_split_asm, auto)
 
 proposition owner_seskey_nonce [rule_format]:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow>
     (Owner n, SesKey SK) \<in> s \<longrightarrow>
   (\<exists>S. fst SK = Some S \<and> Crypt (Auth_ShaKey n) (PriKey S) \<in> used s) \<or>
   fst SK = None"
 by (erule rtrancl_induct, simp add: image_def, rule impI, rule owner_seskey_nonce_1)
 
 proposition owner_seskey_other [rule_format]:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow>
     (Owner n, SesKey SK) \<in> s \<longrightarrow>
   (\<exists>A B C D. fst (snd SK) = {A, B} \<and> snd (snd SK) = {C, D} \<and>
     (Owner n, \<lbrace>Num 1, PubKey A\<rbrace>) \<in> s \<and>
     (Owner n, \<lbrace>Num 3, PubKey C\<rbrace>) \<in> s \<and>
     (Owner n, Crypt (SesK SK) (PubKey D)) \<in> s)"
 by (erule rtrancl_induct, auto simp add: rel_def, blast+)
 
 proposition asset_seskey_nonce [rule_format]:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow>
     (Asset n, SesKey SK) \<in> s \<longrightarrow>
   (\<exists>S. fst SK = Some S \<and> (Asset n, Crypt (Auth_ShaKey n) (PriKey S)) \<in> s)"
 by (erule rtrancl_induct, auto simp add: rel_def)
 
 proposition asset_seskey_other [rule_format]:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow>
     (Asset n, SesKey SK) \<in> s \<longrightarrow>
   (\<exists>A B C D. fst (snd SK) = {A, B} \<and> snd (snd SK) = {C, D} \<and>
     (Asset n, \<lbrace>Num 2, PubKey B\<rbrace>) \<in> s \<and> (Asset n, \<lbrace>Num 4, PubKey D\<rbrace>) \<in> s \<and>
     (Asset n, Token n (Auth_PriK n) B C SK) \<in> s)"
 by (erule rtrancl_induct, auto simp add: rel_def, blast)
 
 
 declare Range_Un_eq [simp]
 
 proposition used_prod [simp]:
  "A \<noteq> {} \<Longrightarrow> used (A \<times> H) = H"
 by (simp add: Range_snd)
 
 proposition parts_idem [simp]:
  "parts (parts H) = parts H"
 by (rule equalityI, rule subsetI, erule parts.induct, auto)
 
 proposition parts_mono:
  "H \<subseteq> H' \<Longrightarrow> parts H \<subseteq> parts H'"
 by (rule subsetI, erule parts.induct, auto)
 
 proposition parts_msg_mono:
  "X \<in> H \<Longrightarrow> parts_msg X \<subseteq> parts H"
 by (subgoal_tac "{X} \<subseteq> H", subst parts_msg_def, erule parts_mono, simp)
 
 lemma parts_union_1:
  "parts (H \<union> H') \<subseteq> parts H \<union> parts H'"
 by (rule subsetI, erule parts.induct, auto)
 
 lemma parts_union_2:
  "parts H \<union> parts H' \<subseteq> parts (H \<union> H')"
 by (rule subsetI, erule UnE, erule_tac [!] parts.induct, auto)
 
 proposition parts_union [simp]:
  "parts (H \<union> H') = parts H \<union> parts H'"
 by (rule equalityI, rule parts_union_1, rule parts_union_2)
 
 proposition parts_insert:
  "parts (insert X H) = parts_msg X \<union> parts H"
 by (simp only: insert_def parts_union, subst parts_msg_def, simp)
 
 proposition parts_msg_num [simp]:
  "parts_msg (Num n) = {Num n}"
 by (subst parts_msg_def, rule equalityI, rule subsetI, erule parts.induct, auto)
 
 proposition parts_msg_pwd [simp]:
  "parts_msg (Pwd n) = {Pwd n}"
 by (subst parts_msg_def, rule equalityI, rule subsetI, erule parts.induct, auto)
 
 proposition parts_msg_key [simp]:
  "parts_msg (Key K) = {Key K}"
 by (subst parts_msg_def, rule equalityI, rule subsetI, erule parts.induct, auto)
 
 proposition parts_msg_mult [simp]:
  "parts_msg (A \<otimes> B) = {A \<otimes> B}"
 by (subst parts_msg_def, rule equalityI, rule subsetI, erule parts.induct, auto)
 
 proposition parts_msg_hash [simp]:
  "parts_msg (Hash X) = {Hash X}"
 by (subst parts_msg_def, rule equalityI, rule subsetI, erule parts.induct, auto)
 
 lemma parts_crypt_1:
  "parts {Crypt K X} \<subseteq> insert (Crypt K X) (parts {X})"
 by (rule subsetI, erule parts.induct, auto)
 
 lemma parts_crypt_2:
  "insert (Crypt K X) (parts {X}) \<subseteq> parts {Crypt K X}"
 by (rule subsetI, simp, erule disjE, blast, erule parts.induct, auto)
 
 proposition parts_msg_crypt [simp]:
  "parts_msg (Crypt K X) = insert (Crypt K X) (parts_msg X)"
 by (simp add: parts_msg_def, rule equalityI, rule parts_crypt_1, rule parts_crypt_2)
 
 lemma parts_mpair_1:
  "parts {\<lbrace>X, Y\<rbrace>} \<subseteq> insert \<lbrace>X, Y\<rbrace> (parts {X} \<union> parts {Y})"
 by (rule subsetI, erule parts.induct, auto)
 
 lemma parts_mpair_2:
  "insert \<lbrace>X, Y\<rbrace> (parts {X} \<union> parts {Y}) \<subseteq> parts {\<lbrace>X, Y\<rbrace>}"
 by (rule subsetI, simp, erule disjE, blast, erule disjE, erule_tac [!] parts.induct,
  auto)
 
 proposition parts_msg_mpair [simp]:
  "parts_msg \<lbrace>X, Y\<rbrace> = insert \<lbrace>X, Y\<rbrace> (parts_msg X \<union> parts_msg Y)"
 by (simp add: parts_msg_def, rule equalityI, rule parts_mpair_1, rule parts_mpair_2)
 
 proposition parts_msg_idinfo [simp]:
  "parts_msg \<langle>n, X\<rangle> = {\<langle>n, X\<rangle>}"
 by (subst parts_msg_def, rule equalityI, rule subsetI, erule parts.induct, auto)
 
 proposition parts_msg_trace [simp]:
  "parts_msg (Log X) = {Log X}"
 by (subst parts_msg_def, rule equalityI, rule subsetI, erule parts.induct, auto)
 
 proposition parts_idinfo [simp]:
  "parts (IDInfo n ` H) = IDInfo n ` H"
 by (rule equalityI, rule subsetI, erule parts.induct, auto)
 
 proposition parts_trace [simp]:
  "parts (Log ` H) = Log ` H"
 by (rule equalityI, rule subsetI, erule parts.induct, auto)
 
 proposition parts_dec:
  "\<lbrakk>s' = insert (Spy, X) s \<and> (Spy, Crypt K X) \<in> s \<and> (Spy, Key (InvK K)) \<in> s;
     Y \<in> parts_msg X\<rbrakk> \<Longrightarrow>
   Y \<in> parts (used s)"
 by (subgoal_tac "X \<in> parts (used s)", drule parts_msg_mono [of X], auto)
 
 proposition parts_enc:
  "\<lbrakk>s' = insert (Spy, Crypt K X) s \<and> (Spy, X) \<in> s \<and> (Spy, Key K) \<in> s;
     Y \<in> parts_msg X\<rbrakk> \<Longrightarrow>
   Y \<in> parts (used s)"
 by (subgoal_tac "X \<in> parts (used s)", drule parts_msg_mono [of X], auto)
 
 proposition parts_sep:
  "\<lbrakk>s' = insert (Spy, X) (insert (Spy, Y) s) \<and> (Spy, \<lbrace>X, Y\<rbrace>) \<in> s;
     Z \<in> parts_msg X \<or> Z \<in> parts_msg Y\<rbrakk> \<Longrightarrow>
   Z \<in> parts (used s)"
 by (erule disjE, subgoal_tac "X \<in> parts (used s)", drule parts_msg_mono [of X],
  subgoal_tac [3] "Y \<in> parts (used s)", drule_tac [3] parts_msg_mono [of Y], auto)
 
 proposition parts_con:
  "\<lbrakk>s' = insert (Spy, \<lbrace>X, Y\<rbrace>) s \<and> (Spy, X) \<in> s \<and> (Spy, Y) \<in> s;
     Z \<in> parts_msg X \<or> Z \<in> parts_msg Y\<rbrakk> \<Longrightarrow>
   Z \<in> parts (used s)"
 by (erule disjE, subgoal_tac "X \<in> parts (used s)", drule parts_msg_mono [of X],
  subgoal_tac [3] "Y \<in> parts (used s)", drule_tac [3] parts_msg_mono [of Y], auto)
 
 lemma parts_init_1:
  "parts (used s\<^sub>0) \<subseteq> used s\<^sub>0 \<union> range (Hash \<circ> Agent) \<union>
     range (Hash \<circ> Auth_PubKey) \<union>
     range (\<lambda>n. \<lbrace>Hash (Agent n), Hash (Auth_PubKey n)\<rbrace>)"
 by (rule subsetI, erule parts.induct, (clarify | simp add: Range_iff image_def)+)
 
 lemma parts_init_2:
  "used s\<^sub>0 \<union> range (Hash \<circ> Agent) \<union> range (Hash \<circ> Auth_PubKey) \<union>
     range (\<lambda>n. \<lbrace>Hash (Agent n), Hash (Auth_PubKey n)\<rbrace>) \<subseteq> parts (used s\<^sub>0)"
 by (rule subsetI, auto simp add: parts_insert)
 
 proposition parts_init:
  "parts (used s\<^sub>0) = used s\<^sub>0 \<union> range (Hash \<circ> Agent) \<union>
     range (Hash \<circ> Auth_PubKey) \<union>
     range (\<lambda>n. \<lbrace>Hash (Agent n), Hash (Auth_PubKey n)\<rbrace>)"
 by (rule equalityI, rule parts_init_1, rule parts_init_2)
 
 
 proposition parts_crypt_prikey_start:
  "\<lbrakk>s \<turnstile> s'; Crypt K (PriKey A) \<in> parts (used s');
     Crypt K (PriKey A) \<notin> parts (used s)\<rbrakk> \<Longrightarrow>
   (\<exists>n. K = Auth_ShaKey n \<and>
     (Asset n, Crypt (Auth_ShaKey n) (PriKey A)) \<in> s') \<or>
   {PriKey A, Key K} \<subseteq> spied s'"
 by (simp add: rel_def, erule disjE, (erule exE)+, simp add: parts_insert, blast,
  (((erule disjE)?, (erule exE)+, simp add: parts_insert image_iff)+,
  ((drule parts_dec | erule disjE, simp, drule parts_enc |
  drule parts_sep | drule parts_con), simp+)?)+)
 
 proposition parts_crypt_prikey:
  "\<lbrakk>s\<^sub>0 \<Turnstile> s; Crypt K (PriKey A) \<in> parts (used s)\<rbrakk> \<Longrightarrow>
     (\<exists>n. K = Auth_ShaKey n \<and>
       (Asset n, Crypt (Auth_ShaKey n) (PriKey A)) \<in> s) \<or>
     {PriKey A, Key K} \<subseteq> spied s"
 by (drule rtrancl_start, assumption, subst parts_init, simp add: Range_iff image_def,
  (erule exE)+, (erule conjE)+, frule parts_crypt_prikey_start, assumption+,
  (drule state_subset)+, blast)
 
 
 proposition parts_crypt_pubkey_start:
  "\<lbrakk>s \<turnstile> s'; Crypt (SesK SK) (PubKey C) \<in> parts (used s');
     Crypt (SesK SK) (PubKey C) \<notin> parts (used s)\<rbrakk> \<Longrightarrow>
   C \<in> snd (snd SK) \<and> ((\<exists>n. (Owner n, SesKey SK) \<in> s') \<or>
     (\<exists>n B. (Asset n, Token n (Auth_PriK n) B C SK) \<in> s')) \<or>
   SesKey SK \<in> spied s'"
 by (simp add: rel_def, (erule disjE, (erule exE)+, simp add: parts_insert image_iff)+,
  blast, erule disjE, (erule exE)+, simp add: parts_insert image_iff, blast,
  (((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_crypt_pubkey:
  "\<lbrakk>s\<^sub>0 \<Turnstile> s; Crypt (SesK SK) (PubKey C) \<in> parts (used s)\<rbrakk> \<Longrightarrow>
     C \<in> snd (snd SK) \<and> ((\<exists>n. (Owner n, SesKey SK) \<in> s) \<or>
       (\<exists>n B. (Asset n, Token n (Auth_PriK n) B C SK) \<in> s)) \<or>
     SesKey SK \<in> spied s"
 by (drule rtrancl_start, assumption, subst parts_init, simp add: Range_iff image_def,
  (erule exE)+, (erule conjE)+, frule parts_crypt_pubkey_start, assumption+,
  (drule state_subset)+, blast)
 
 
 proposition parts_crypt_key_start:
  "\<lbrakk>s \<turnstile> s'; Crypt K (Key K') \<in> parts (used s');
     Crypt K (Key K') \<notin> parts (used s); K' \<notin> range PriK \<union> range PubK\<rbrakk> \<Longrightarrow>
   {Key K', Key K} \<subseteq> spied s'"
 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_crypt_key:
  "\<lbrakk>s\<^sub>0 \<Turnstile> s; Crypt K (Key K') \<in> parts (used s);
     K' \<notin> range PriK \<union> range PubK\<rbrakk> \<Longrightarrow>
   {Key K', Key K} \<subseteq> spied s"
 by (drule rtrancl_start, assumption, subst parts_init, simp add: Range_iff image_def,
  (erule exE)+, (erule conjE)+, frule parts_crypt_key_start, assumption+,
  (drule state_subset)+, blast)
 
 
 proposition parts_crypt_sign_start:
  "\<lbrakk>s \<turnstile> s'; Crypt (SesK SK) (Sign n A) \<in> parts (used s');
     Crypt (SesK SK) (Sign n A) \<notin> parts (used s)\<rbrakk> \<Longrightarrow>
   (Asset n, SesKey SK) \<in> s' \<or> SesKey SK \<in> spied s'"
 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_crypt_sign:
  "\<lbrakk>s\<^sub>0 \<Turnstile> s; Crypt (SesK SK) (Sign n A) \<in> parts (used s)\<rbrakk> \<Longrightarrow>
     (Asset n, SesKey SK) \<in> s \<or> SesKey SK \<in> spied s"
 by (drule rtrancl_start, assumption, subst parts_init, simp add: Range_iff image_def,
  (erule exE)+, (erule conjE)+, frule parts_crypt_sign_start, assumption+,
  (drule state_subset)+, blast)
 
 
 proposition parts_crypt_pwd_start:
  "\<lbrakk>s \<turnstile> s'; Crypt K (Pwd n) \<in> parts (used s');
     Crypt K (Pwd n) \<notin> parts (used s)\<rbrakk> \<Longrightarrow>
   (\<exists>SK. K = SesK SK \<and> (Owner n, Crypt (SesK SK) (Pwd n)) \<in> s') \<or>
   {Pwd n, Key K} \<subseteq> spied s'"
 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_crypt_pwd:
  "\<lbrakk>s\<^sub>0 \<Turnstile> s; Crypt K (Pwd n) \<in> parts (used s)\<rbrakk> \<Longrightarrow>
     (\<exists>SK. K = SesK SK \<and> (Owner n, Crypt (SesK SK) (Pwd n)) \<in> s) \<or>
     {Pwd n, Key K} \<subseteq> spied s"
 by (drule rtrancl_start, assumption, subst parts_init, simp add: Range_iff image_def,
  (erule exE)+, (erule conjE)+, frule parts_crypt_pwd_start, assumption+,
  (drule state_subset)+, blast)
 
 
 proposition parts_crypt_num_start:
  "\<lbrakk>s \<turnstile> s'; Crypt (SesK SK) (Num 0) \<in> parts (used s');
     Crypt (SesK SK) (Num 0) \<notin> parts (used s)\<rbrakk> \<Longrightarrow>
   (\<exists>n. (Asset n, Crypt (SesK SK) (Num 0)) \<in> s') \<or> SesKey SK \<in> spied s'"
 by (simp add: rel_def, (erule disjE, (erule exE)+, simp add: parts_insert image_iff)+,
  blast, (((erule disjE)?, (erule exE)+, simp add: parts_insert image_iff)+,
  ((drule parts_dec | erule disjE, simp, drule parts_enc |
  drule parts_sep | drule parts_con), simp+)?)+)
 
 proposition parts_crypt_num:
  "\<lbrakk>s\<^sub>0 \<Turnstile> s; Crypt (SesK SK) (Num 0) \<in> parts (used s)\<rbrakk> \<Longrightarrow>
     (\<exists>n. (Asset n, Crypt (SesK SK) (Num 0)) \<in> s) \<or> SesKey SK \<in> spied s"
 by (drule rtrancl_start, assumption, subst parts_init, simp add: Range_iff image_def,
  (erule exE)+, (erule conjE)+, frule parts_crypt_num_start, assumption+,
  (drule state_subset)+, blast)
 
 
 proposition parts_crypt_mult_start:
  "\<lbrakk>s \<turnstile> s'; Crypt (SesK SK) (A \<otimes> B) \<in> parts (used s');
     Crypt (SesK SK) (A \<otimes> B) \<notin> parts (used s)\<rbrakk> \<Longrightarrow>
   B \<in> fst (snd SK) \<and> (\<exists>n C. (Asset n, Token n (Auth_PriK n) B C SK) \<in> s') \<or>
   {A \<otimes> B, SesKey SK} \<subseteq> spied s"
 by (simp add: rel_def, (erule disjE, (erule exE)+, simp add: parts_insert image_iff)+,
  blast, (((erule disjE)?, (erule exE)+, simp add: parts_insert image_iff)+,
  ((drule parts_dec | erule disjE, simp, drule parts_enc |
  drule parts_sep | drule parts_con), simp+)?)+)
 
 proposition parts_crypt_mult:
  "\<lbrakk>s\<^sub>0 \<Turnstile> s; Crypt (SesK SK) (A \<otimes> B) \<in> parts (used s)\<rbrakk> \<Longrightarrow>
     B \<in> fst (snd SK) \<and> (\<exists>n C. (Asset n, Token n (Auth_PriK n) B C SK) \<in> s) \<or>
     {A \<otimes> B, SesKey SK} \<subseteq> spied s"
 by (drule rtrancl_start, assumption, subst parts_init, simp add: Range_iff image_def,
  (erule exE)+, (erule conjE)+, frule parts_crypt_mult_start, assumption+,
  drule converse_rtrancl_into_rtrancl, assumption, drule state_subset [of _ s],
  drule spied_subset [of _ s], blast)
 
 
 proposition parts_mult_start:
  "\<lbrakk>s \<turnstile> s'; A \<otimes> B \<in> parts (used s'); A \<otimes> B \<notin> parts (used s)\<rbrakk> \<Longrightarrow>
     (\<exists>n SK. A = Auth_PriK n \<and> (Asset n, \<lbrace>Num 2, PubKey B\<rbrace>) \<in> s' \<and>
       Crypt (SesK SK) (A \<otimes> B) \<in> parts (used s')) \<or>
     {PriKey A, PriKey B} \<subseteq> spied s'"
 by (simp add: rel_def, (erule disjE, (erule exE)+, simp add: parts_insert image_iff)+,
  blast, (((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_mult:
  "\<lbrakk>s\<^sub>0 \<Turnstile> s; A \<otimes> B \<in> parts (used s)\<rbrakk> \<Longrightarrow>
     (\<exists>n. A = Auth_PriK n \<and> (Asset n, \<lbrace>Num 2, PubKey B\<rbrace>) \<in> s) \<or>
     {PriKey A, PriKey B} \<subseteq> spied s"
 by (drule rtrancl_start, assumption, subst parts_init, simp add: Range_iff image_def,
  (erule exE)+, (erule conjE)+, frule parts_mult_start, assumption+,
  (drule state_subset)+, blast)
 
 
 proposition parts_mpair_key_start:
  "\<lbrakk>s \<turnstile> s'; \<lbrace>X, Y\<rbrace> \<in> parts (used s'); \<lbrace>X, Y\<rbrace> \<notin> parts (used s);
     X = Key K \<or> Y = Key K \<and> K \<notin> range PubK\<rbrakk> \<Longrightarrow>
   {X, Y} \<subseteq> spied s'"
 by (erule disjE, simp_all add: rel_def,
  (((erule disjE)?, (erule exE)+, simp add: parts_insert image_iff)+,
  ((drule parts_dec | drule parts_enc |
  drule parts_sep | erule disjE, simp, drule parts_con), simp+)?)+)
 
 proposition parts_mpair_key:
  "\<lbrakk>s\<^sub>0 \<Turnstile> s; \<lbrace>X, Y\<rbrace> \<in> parts (used s);
     X = Key K \<or> Y = Key K \<and> K \<notin> range PubK\<rbrakk> \<Longrightarrow>
   {X, Y} \<subseteq> spied s"
 by (drule rtrancl_start, assumption, subst parts_init, simp add: Range_iff image_def,
  blast, (erule exE)+, (erule conjE)+, frule parts_mpair_key_start, assumption+,
  (drule state_subset)+, blast)
 
 
 proposition parts_mpair_pwd_start:
  "\<lbrakk>s \<turnstile> s'; \<lbrace>X, Y\<rbrace> \<in> parts (used s'); \<lbrace>X, Y\<rbrace> \<notin> parts (used s);
     X = Pwd n \<or> Y = Pwd n\<rbrakk> \<Longrightarrow>
   {X, Y} \<subseteq> spied s'"
 by (erule disjE, simp_all add: rel_def,
  (((erule disjE)?, (erule exE)+, simp add: parts_insert image_iff)+,
  ((drule parts_dec | drule parts_enc |
  drule parts_sep | erule disjE, simp, drule parts_con), simp+)?)+)
 
 proposition parts_mpair_pwd:
  "\<lbrakk>s\<^sub>0 \<Turnstile> s; \<lbrace>X, Y\<rbrace> \<in> parts (used s); X = Pwd n \<or> Y = Pwd n\<rbrakk> \<Longrightarrow>
     {X, Y} \<subseteq> spied s"
 by (drule rtrancl_start, assumption, subst parts_init, simp add: Range_iff image_def,
  blast, (erule exE)+, (erule conjE)+, frule parts_mpair_pwd_start, assumption+,
  (drule state_subset)+, blast)
 
 
 proposition parts_pubkey_false_start:
   assumes
     A: "s\<^sub>0 \<Turnstile> s" and
     B: "s \<turnstile> s'" and
     C: "Crypt (SesK SK) (PubKey C) \<in> parts (used s')" and
     D: "Crypt (SesK SK) (PubKey C) \<notin> parts (used s)" and
     E: "\<forall>n. (Owner n, SesKey SK) \<notin> s'" and
     F: "SesKey SK \<notin> spied s'"
   shows False
 proof -
   have "C \<in> snd (snd SK) \<and> ((\<exists>n. (Owner n, SesKey SK) \<in> s') \<or>
     (\<exists>n B. (Asset n, Token n (Auth_PriK n) B C SK) \<in> s')) \<or>
     SesKey SK \<in> spied s'"
     (is "?P C \<and> ((\<exists>n. ?Q n s') \<or> (\<exists>n B. ?R n B C s')) \<or> ?S s'")
     by (rule parts_crypt_pubkey_start [OF B C D])
   then obtain n B where "?P C" and "?R n B C s'"
     using E and F by blast
   moreover have "\<not> ?R n B C s"
     using D by blast
   ultimately have "\<exists>D. Crypt (SesK SK) (PubKey D) \<in> used s"
     (is "\<exists>D. ?U D")
     using B by (auto simp add: rel_def)
   then obtain D where "?U D" ..
   hence "?P D \<and> ((\<exists>n. ?Q n s) \<or> (\<exists>n B. ?R n B D s)) \<or> ?S s"
     by (rule_tac parts_crypt_pubkey [OF A], blast)
   moreover have G: "s \<subseteq> s'"
     by (rule state_subset, insert B, simp)
   have "\<forall>n. (Owner n, SesKey SK) \<notin> s"
     by (rule allI, rule notI, drule subsetD [OF G], insert E, simp)
   moreover have H: "spied s \<subseteq> spied s'"
     by (rule Image_mono [OF G], simp)
   have "SesKey SK \<notin> spied s"
     by (rule notI, drule subsetD [OF H], insert F, contradiction)
   ultimately obtain n' B' where "?R n' B' D s" by blast
   have "\<exists>A' D'. fst (snd SK) = {A', B'} \<and> snd (snd SK) = {D, D'} \<and>
     (Asset n', \<lbrace>Num 2, PubKey B'\<rbrace>) \<in> s \<and>
     (Asset n', \<lbrace>Num 4, PubKey D'\<rbrace>) \<in> s \<and>
     ?U D' \<and> (Asset n', PubKey B') \<in> s"
     by (rule asset_iv_state [OF A `?R n' B' D s`])
   then obtain D' where "snd (snd SK) = {D, D'}" and "?U D'" by blast
   hence "Crypt (SesK SK) (PubKey C) \<in> parts (used s)"
     using `?P C` and `?U D` by auto
   thus False
     using D by contradiction
 qed
 
 proposition parts_pubkey_false:
  "\<lbrakk>s\<^sub>0 \<Turnstile> s; Crypt (SesK SK) (PubKey C) \<in> parts (used s);
     \<forall>n. (Owner n, SesKey SK) \<notin> s; SesKey SK \<notin> spied s\<rbrakk> \<Longrightarrow>
   False"
 proof (drule rtrancl_start, assumption, subst parts_init, simp add: Range_iff image_def,
  (erule exE)+, (erule conjE)+, erule parts_pubkey_false_start, assumption+,
  rule allI, rule_tac [!] notI)
   fix v n
   assume "(Owner n, SesKey SK) \<in> v" and "v \<Turnstile> s"
   hence "(Owner n, SesKey SK) \<in> s"
     by (erule_tac rev_subsetD, rule_tac state_subset)
   moreover assume "\<forall>n. (Owner n, SesKey SK) \<notin> s"
   ultimately show False by simp
 next
   fix v
   assume "SesKey SK \<in> spied v" and "v \<Turnstile> s"
   hence "SesKey SK \<in> spied s"
     by (erule_tac rev_subsetD, rule_tac spied_subset)
   moreover assume "SesKey SK \<notin> spied s"
   ultimately show False by contradiction
 qed
 
 
 proposition asset_ii_spied_start:
   assumes
     A: "s\<^sub>0 \<Turnstile> s" and
     B: "s \<turnstile> s'" and
     C: "PriKey B \<in> spied s'" and
     D: "PriKey B \<notin> spied s" and
     E: "(Asset n, \<lbrace>Num 2, PubKey B\<rbrace>) \<in> s"
   shows "Auth_PriKey n \<in> spied s \<and>
     (\<exists>C SK. (Asset n, Token n (Auth_PriK n) B C SK) \<in> s)"
     (is "_ \<and> (\<exists>C SK. ?P n C SK s)")
 proof -
   have "\<exists>A. (A \<otimes> B \<in> spied s \<or> B \<otimes> A \<in> spied s) \<and> PriKey A \<in> spied s"
   proof (insert B C D, auto simp add: rel_def, rule_tac [!] FalseE)
     assume "Key (PriK B) \<notin> used s"
     moreover have "PriKey B \<in> used s"
       by (rule asset_ii_used [OF A, THEN mp, OF E])
     ultimately show False by simp
   next
     fix K
     assume "(Spy, Crypt K (Key (PriK B))) \<in> s"
     hence "Crypt K (PriKey B) \<in> parts (used s)" by auto
     hence "(\<exists>m. K = Auth_ShaKey m \<and>
       (Asset m, Crypt (Auth_ShaKey m) (PriKey B)) \<in> s) \<or>
       {PriKey B, Key K} \<subseteq> spied s"
       (is "(\<exists>m. _ \<and> ?P m) \<or> _")
       by (rule parts_crypt_prikey [OF A])
     then obtain m where "?P m"
       using D by blast
     thus False
       by (rule asset_i_asset_ii [OF A _ E])
   next
     fix Y
     assume "(Spy, \<lbrace>Key (PriK B), Y\<rbrace>) \<in> s"
     hence "\<lbrace>PriKey B, Y\<rbrace> \<in> parts (used s)" by auto
     hence "{PriKey B, Y} \<subseteq> spied s"
       by (rule parts_mpair_key [OF A, where K = "PriK B"], simp)
     thus False
       using D by simp
   next
     fix X
     assume "(Spy, \<lbrace>X, Key (PriK B)\<rbrace>) \<in> s"
     hence "\<lbrace>X, PriKey B\<rbrace> \<in> parts (used s)" by auto
     hence "{X, PriKey B} \<subseteq> spied s"
       by (rule parts_mpair_key [OF A, where K = "PriK B"], simp add: image_def)
     thus False
       using D by simp
   qed
   then obtain A where F: "PriKey A \<in> spied s" and
     "A \<otimes> B \<in> spied s \<or> B \<otimes> A \<in> spied s"
     by blast
   hence "A \<otimes> B \<in> parts (used s) \<or> B \<otimes> A \<in> parts (used s)" by blast
   moreover have "B \<otimes> A \<notin> parts (used s)"
   proof
     assume "B \<otimes> A \<in> parts (used s)"
     hence "(\<exists>m. B = Auth_PriK m \<and> (Asset m, \<lbrace>Num 2, PubKey A\<rbrace>) \<in> s) \<or>
       {PriKey B, PriKey A} \<subseteq> spied s"
       by (rule parts_mult [OF A])
     then obtain m where "B = Auth_PriK m"
       using D by blast
     hence "(Asset n, \<lbrace>Num 2, Auth_PubKey m\<rbrace>) \<in> s"
       using E by simp
     thus False
       by (rule auth_pubkey_asset_ii [OF A])
   qed
   ultimately have "A \<otimes> B \<in> parts (used s)" by simp
   with A have "\<exists>u v. s\<^sub>0 \<Turnstile> u \<and> u \<turnstile> v \<and> v \<Turnstile> s \<and>
     A \<otimes> B \<notin> parts (used u) \<and> A \<otimes> B \<in> parts (used v)"
     by (rule rtrancl_start, subst parts_init, simp add: Range_iff image_def)
   then obtain u v where G: "u \<turnstile> v" and H: "v \<Turnstile> s" and
     I: "A \<otimes> B \<notin> parts (used u)" and "A \<otimes> B \<in> parts (used v)"
     by blast
   hence "(\<exists>m SK. A = Auth_PriK m \<and> (Asset m, \<lbrace>Num 2, PubKey B\<rbrace>) \<in> v \<and>
     Crypt (SesK SK) (A \<otimes> B) \<in> parts (used v)) \<or>
     {PriKey A, PriKey B} \<subseteq> spied v"
     by (rule_tac parts_mult_start, simp_all)
   moreover have "PriKey B \<notin> spied v"
   proof
     assume "PriKey B \<in> spied v"
     hence "PriKey B \<in> spied s"
       by (rule rev_subsetD, rule_tac spied_subset [OF H])
     thus False
       using D by contradiction
   qed
   ultimately obtain m SK where
     J: "Crypt (SesK SK) (A \<otimes> B) \<in> parts (used v)" and
     "A = Auth_PriK m" and "(Asset m, \<lbrace>Num 2, PubKey B\<rbrace>) \<in> v"
     by blast
   moreover from this have "(Asset m, \<lbrace>Num 2, PubKey B\<rbrace>) \<in> s"
     by (erule_tac rev_subsetD, rule_tac state_subset [OF H])
   hence "m = n"
     by (rule asset_ii_unique [OF A _ E])
   ultimately have K: "Auth_PriKey n \<in> spied s"
     using F by simp
   have "Crypt (SesK SK) (A \<otimes> B) \<notin> parts (used u)"
     using I by blast
   hence "B \<in> fst (snd SK) \<and> (\<exists>m C. ?P m C SK v) \<or>
     {A \<otimes> B, SesKey SK} \<subseteq> spied u"
     by (rule parts_crypt_mult_start [OF G J])
   moreover have "A \<otimes> B \<notin> spied u"
     using I by blast
   ultimately obtain m' C where "?P m' C SK v" by blast
   hence "?P m' C SK s"
     by (rule rev_subsetD, rule_tac state_subset [OF H])
   moreover from this have "\<exists>A' D. fst (snd SK) = {A', B} \<and>
     snd (snd SK) = {C, D} \<and> (Asset m', \<lbrace>Num 2, PubKey B\<rbrace>) \<in> s \<and>
     (Asset m', \<lbrace>Num 4, PubKey D\<rbrace>) \<in> s \<and>
     Crypt (SesK SK) (PubKey D) \<in> used s \<and> (Asset m', PubKey B) \<in> s"
     by (rule asset_iv_state [OF A])
   hence "(Asset m', \<lbrace>Num 2, PubKey B\<rbrace>) \<in> s" by blast
   hence "m' = n"
     by (rule asset_ii_unique [OF A _ E])
   ultimately show ?thesis
     using K by blast
 qed
 
 proposition asset_ii_spied:
   assumes
     A: "s\<^sub>0 \<Turnstile> s" and
     B: "PriKey B \<in> spied s" and
     C: "(Asset n, \<lbrace>Num 2, PubKey B\<rbrace>) \<in> s"
   shows "Auth_PriKey n \<in> spied s \<and>
     (\<exists>C SK. (Asset n, Token n (Auth_PriK n) B C SK) \<in> s)"
     (is "?P s")
 proof -
   have "\<exists>u v. s\<^sub>0 \<Turnstile> u \<and> u \<turnstile> v \<and> v \<Turnstile> s \<and>
     (Asset n, \<lbrace>Num 2, PubKey B\<rbrace>) \<notin> u \<and> (Asset n, \<lbrace>Num 2, PubKey B\<rbrace>) \<in> v"
     using A and C by (rule rtrancl_start, auto)
   then obtain u v where "v \<Turnstile> s" and "(Asset n, \<lbrace>Num 2, PubKey B\<rbrace>) \<notin> u" and
     D: "s\<^sub>0 \<Turnstile> u" and E: "u \<turnstile> v" and F: "(Asset n, \<lbrace>Num 2, PubKey B\<rbrace>) \<in> v"
     by blast
   moreover from this have "PriKey B \<notin> spied v"
     by (auto simp add: rel_def)
   ultimately have "\<exists>w x. v \<Turnstile> w \<and> w \<turnstile> x \<and> x \<Turnstile> s \<and>
     PriKey B \<notin> spied w \<and> PriKey B \<in> spied x"
     using B by (rule_tac rtrancl_start, simp_all)
   then obtain w x where "PriKey B \<notin> spied w" and "PriKey B \<in> spied x" and
     G: "v \<Turnstile> w" and H: "w \<turnstile> x" and I: "x \<Turnstile> s"
     by blast
   moreover from this have "s\<^sub>0 \<Turnstile> w"
     using D and E by simp
   moreover have "(Asset n, \<lbrace>Num 2, PubKey B\<rbrace>) \<in> w"
     by (rule rev_subsetD [OF F], rule state_subset [OF G])
   ultimately have "?P w"
     by (rule_tac asset_ii_spied_start, simp_all)
   moreover have "w \<subseteq> s"
     using H and I by (rule_tac state_subset, simp)
   ultimately show ?thesis by blast
 qed
 
 
 proposition asset_iv_unique:
   assumes
     A: "s\<^sub>0 \<Turnstile> s" and
     B: "(Asset m, Token m (Auth_PriK m) B C' SK') \<in> s" and
     C: "(Asset n, Token n (Auth_PriK n) B C SK) \<in> s"
       (is "?P n C SK s")
   shows "m = n \<and> C' = C \<and> SK' = SK"
 proof (subst (2) cases_simp [of "m = n", symmetric], simp, rule conjI, rule impI,
  rule ccontr)
   assume D: "\<not> (C' = C \<and> SK' = SK)" and "m = n"
   moreover have "\<exists>u v. s\<^sub>0 \<Turnstile> u \<and> u \<turnstile> v \<and> v \<Turnstile> s \<and>
     \<not> (?P m C' SK' u \<and> ?P n C SK u) \<and> ?P m C' SK' v \<and> ?P n C SK v"
     using B and C by (rule_tac rtrancl_start [OF A], auto)
   ultimately obtain u v where E: "s\<^sub>0 \<Turnstile> u" and F: "u \<turnstile> v" and
     G: "?P n C' SK' v" and H: "?P n C SK v" and
     "\<not> ?P n C' SK' u \<or> \<not> ?P n C SK u"
     by blast
   moreover {
     assume I: "\<not> ?P n C' SK' u"
     hence "?P n C SK u"
       by (insert D F G H, auto simp add: rel_def)
     hence "\<exists>A D. fst (snd SK) = {A, B} \<and> snd (snd SK) = {C, D} \<and>
       (Asset n, \<lbrace>Num 2, PubKey B\<rbrace>) \<in> u \<and> (Asset n, \<lbrace>Num 4, PubKey D\<rbrace>) \<in> u \<and>
       Crypt (SesK SK) (PubKey D) \<in> used u \<and> (Asset n, PubKey B) \<in> u"
       by (rule asset_iv_state [OF E])
     moreover have "(Asset n, PubKey B) \<notin> u"
       by (insert F G I, auto simp add: rel_def)
     ultimately have False by simp
   }
   moreover {
     assume I: "\<not> ?P n C SK u"
     hence "?P n C' SK' u"
       by (insert D F G H, auto simp add: rel_def)
     hence "\<exists>A D. fst (snd SK') = {A, B} \<and> snd (snd SK') = {C', D} \<and>
       (Asset n, \<lbrace>Num 2, PubKey B\<rbrace>) \<in> u \<and> (Asset n, \<lbrace>Num 4, PubKey D\<rbrace>) \<in> u \<and>
       Crypt (SesK SK') (PubKey D) \<in> used u \<and> (Asset n, PubKey B) \<in> u"
       by (rule asset_iv_state [OF E])
     moreover have "(Asset n, PubKey B) \<notin> u"
       by (insert F H I, auto simp add: rel_def)
     ultimately have False by simp
   }
   ultimately show False by blast
 next
   have "\<exists>A D. fst (snd SK') = {A, B} \<and> snd (snd SK') = {C', D} \<and>
     (Asset m, \<lbrace>Num 2, PubKey B\<rbrace>) \<in> s \<and> (Asset m, \<lbrace>Num 4, PubKey D\<rbrace>) \<in> s \<and>
     Crypt (SesK SK') (PubKey D) \<in> used s \<and> (Asset m, PubKey B) \<in> s"
     (is "?Q m C' SK'")
     by (rule asset_iv_state [OF A B])
   hence "(Asset m, \<lbrace>Num 2, PubKey B\<rbrace>) \<in> s" by blast
   moreover have "?Q n C SK"
     by (rule asset_iv_state [OF A C])
   hence "(Asset n, \<lbrace>Num 2, PubKey B\<rbrace>) \<in> s" by blast
   ultimately show "m = n"
     by (rule asset_ii_unique [OF A])
 qed
 
 
 theorem sigkey_secret:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow> SigKey \<notin> spied s"
 proof (erule rtrancl_induct, simp add: image_def)
   fix s s'
   assume
     A: "s\<^sub>0 \<Turnstile> s" and
     B: "s \<turnstile> s'" and
     C: "SigKey \<notin> spied s"
   show "SigKey \<notin> spied s'"
   proof (insert B C, auto simp add: rel_def)
     fix K
     assume "(Spy, Crypt K SigKey) \<in> s"
     hence "Crypt K SigKey \<in> parts (used s)" by blast
     hence "{SigKey, Key K} \<subseteq> spied s"
       by (rule parts_crypt_key [OF A], simp add: image_def)
     with C show False by simp
   next
     fix Y
     assume "(Spy, \<lbrace>SigKey, Y\<rbrace>) \<in> s"
     hence "\<lbrace>SigKey, Y\<rbrace> \<in> parts (used s)" by blast
     hence "{SigKey, Y} \<subseteq> spied s"
       by (rule parts_mpair_key [OF A, where K = "SigK"], simp)
     with C show False by simp
   next
     fix X
     assume "(Spy, \<lbrace>X, SigKey\<rbrace>) \<in> s"
     hence "\<lbrace>X, SigKey\<rbrace> \<in> parts (used s)" by blast
     hence "{X, SigKey} \<subseteq> spied s"
       by (rule parts_mpair_key [OF A, where K = "SigK"], simp add: image_def)
     with C show False by simp
   qed
 qed
 
 proposition parts_sign_start:
   assumes A: "s\<^sub>0 \<Turnstile> s"
   shows "\<lbrakk>s \<turnstile> s'; Sign n A \<in> parts (used s'); Sign n A \<notin> parts (used s)\<rbrakk> \<Longrightarrow>
     A = Auth_PriK n"
 by (simp add: rel_def, (((erule disjE)?, (erule exE)+, simp add: parts_insert image_iff)+,
  ((drule parts_dec | erule disjE, insert sigkey_secret [OF A], simp, drule parts_enc |
  drule parts_sep | drule parts_con), simp+)?)+)
 
 proposition parts_sign:
  "\<lbrakk>s\<^sub>0 \<Turnstile> s; Sign n A \<in> parts (used s)\<rbrakk> \<Longrightarrow>
     A = Auth_PriK n"
 by (rule classical, drule rtrancl_start, assumption, subst parts_init, simp add:
  Range_iff image_def, (erule exE)+, (erule conjE)+, drule parts_sign_start)
 
 
 theorem auth_shakey_secret:
  "\<lbrakk>s\<^sub>0 \<Turnstile> s; n \<notin> bad_shakey\<rbrakk> \<Longrightarrow>
     Key (Auth_ShaKey n) \<notin> spied s"
 proof (erule rtrancl_induct, simp add: image_def)
   fix s s'
   assume
     A: "s\<^sub>0 \<Turnstile> s" and
     B: "s \<turnstile> s'" and
     C: "Key (Auth_ShaKey n) \<notin> spied s"
   show "Key (Auth_ShaKey n) \<notin> spied s'"
   proof (insert B C, auto simp add: rel_def)
     fix K
     assume "(Spy, Crypt K (Key (ShaK (Auth_ShaK n)))) \<in> s"
     hence "Crypt K (Key (Auth_ShaKey n)) \<in> parts (used s)" by auto
     hence "{Key (Auth_ShaKey n), Key K} \<subseteq> spied s"
       by (rule parts_crypt_key [OF A], simp add: image_def)
     with C show False by simp
   next
     fix Y
     assume "(Spy, \<lbrace>Key (ShaK (Auth_ShaK n)), Y\<rbrace>) \<in> s"
     hence "\<lbrace>Key (Auth_ShaKey n), Y\<rbrace> \<in> parts (used s)" by auto
     hence "{Key (Auth_ShaKey n), Y} \<subseteq> spied s"
       by (rule parts_mpair_key [OF A, where K = "Auth_ShaKey n"], simp)
     with C show False by simp
   next
     fix X
     assume "(Spy, \<lbrace>X, Key (ShaK (Auth_ShaK n))\<rbrace>) \<in> s"
     hence "\<lbrace>X, Key (Auth_ShaKey n)\<rbrace> \<in> parts (used s)" by auto
     hence "{X, Key (Auth_ShaKey n)} \<subseteq> spied s"
       by (rule parts_mpair_key [OF A, where K = "Auth_ShaKey n"],
        simp add: image_def)
     with C show False by simp
   qed
 qed
 
 
 theorem auth_prikey_secret:
   assumes
     A: "s\<^sub>0 \<Turnstile> s" and
     B: "n \<notin> bad_prikey"
   shows "Auth_PriKey n \<notin> spied s"
 proof
   assume "Auth_PriKey n \<in> spied s"
   moreover have "Auth_PriKey n \<notin> spied s\<^sub>0"
     using B by auto
   ultimately have "\<exists>u v. s\<^sub>0 \<Turnstile> u \<and> u \<turnstile> v \<and> v \<Turnstile> s \<and>
     Auth_PriKey n \<notin> spied u \<and> Auth_PriKey n \<in> spied v"
     by (rule rtrancl_start [OF A])
   then obtain u v where C: "s\<^sub>0 \<Turnstile> u" and D: "u \<turnstile> v" and
     E: "Auth_PriKey n \<notin> spied u" and F: "Auth_PriKey n \<in> spied v"
     by blast
   have "\<exists>B. (Auth_PriK n \<otimes> B \<in> spied u \<or> B \<otimes> Auth_PriK n \<in> spied u) \<and>
     PriKey B \<in> spied u"
   proof (insert D E F, auto simp add: rel_def, rule_tac [!] FalseE)
     assume "Key (PriK (Auth_PriK n)) \<notin> used u"
     moreover have "Auth_PriKey n \<in> used u"
       by (rule auth_prikey_used [OF C])
     ultimately show False by simp
   next
     fix K
     assume "(Spy, Crypt K (Key (PriK (Auth_PriK n)))) \<in> u"
     hence "Crypt K (PriKey (Auth_PriK n)) \<in> parts (used u)" by auto
     hence "(\<exists>m. K = Auth_ShaKey m \<and>
       (Asset m, Crypt (Auth_ShaKey m) (PriKey (Auth_PriK n))) \<in> u) \<or>
       {PriKey (Auth_PriK n), Key K} \<subseteq> spied u"
       by (rule parts_crypt_prikey [OF C])
     then obtain m where
       "(Asset m, Crypt (Auth_ShaKey m) (Auth_PriKey n)) \<in> u"
       using E by auto
     thus False
       by (rule auth_prikey_asset_i [OF C])
   next
     fix Y
     assume "(Spy, \<lbrace>Key (PriK (Auth_PriK n)), Y\<rbrace>) \<in> u"
     hence "\<lbrace>Auth_PriKey n, Y\<rbrace> \<in> parts (used u)" by auto
     hence "{Auth_PriKey n, Y} \<subseteq> spied u"
       by (rule parts_mpair_key [OF C, where K = "PriK (Auth_PriK n)"], simp)
     thus False
       using E by simp
   next
     fix X
     assume "(Spy, \<lbrace>X, Key (PriK (Auth_PriK n))\<rbrace>) \<in> u"
     hence "\<lbrace>X, Auth_PriKey n\<rbrace> \<in> parts (used u)" by auto
     hence "{X, Auth_PriKey n} \<subseteq> spied u"
       by (rule parts_mpair_key [OF C, where K = "PriK (Auth_PriK n)"], simp
        add: image_def)
     thus False
       using E by simp
   qed
   then obtain B where G: "PriKey B \<in> spied u" and
     "Auth_PriK n \<otimes> B \<in> spied u \<or> B \<otimes> Auth_PriK n \<in> spied u"
     by blast
   hence "Auth_PriK n \<otimes> B \<in> parts (used u) \<or> B \<otimes> Auth_PriK n \<in> parts (used u)"
     by blast
   moreover have "B \<otimes> Auth_PriK n \<notin> parts (used u)"
   proof
     assume "B \<otimes> Auth_PriK n \<in> parts (used u)"
     hence "(\<exists>m. B = Auth_PriK m \<and>
       (Asset m, \<lbrace>Num 2, PubKey (Auth_PriK n)\<rbrace>) \<in> u) \<or>
       {PriKey B, PriKey (Auth_PriK n)} \<subseteq> spied u"
       by (rule parts_mult [OF C])
     then obtain m where "(Asset m, \<lbrace>Num 2, Auth_PubKey n\<rbrace>) \<in> u"
       using E by auto
     thus False
       by (rule auth_pubkey_asset_ii [OF C])
   qed
   ultimately have "Auth_PriK n \<otimes> B \<in> parts (used u)" by simp
   hence "(\<exists>m. Auth_PriK n = Auth_PriK m \<and>
     (Asset m, \<lbrace>Num 2, PubKey B\<rbrace>) \<in> u) \<or>
     {PriKey (Auth_PriK n), PriKey B} \<subseteq> spied u"
     by (rule parts_mult [OF C])
   then obtain m where "Auth_PriK n = Auth_PriK m" and
     "(Asset m, \<lbrace>Num 2, PubKey B\<rbrace>) \<in> u"
     using E by auto
   moreover from this have "Auth_PriKey m \<in> spied u \<and>
     (\<exists>C SK. (Asset m, Token m (Auth_PriK m) B C SK) \<in> u)"
     by (rule_tac asset_ii_spied [OF C G])
   ultimately show False
     using E by simp
 qed
 
 proposition asset_ii_secret:
  "\<lbrakk>s\<^sub>0 \<Turnstile> s; n \<notin> bad_prikey; (Asset n, \<lbrace>Num 2, PubKey B\<rbrace>) \<in> s\<rbrakk> \<Longrightarrow>
     PriKey B \<notin> spied s"
 by (rule notI, frule asset_ii_spied, assumption+, drule auth_prikey_secret, simp+)
 
 
 proposition asset_i_secret [rule_format]:
   assumes
     A: "s\<^sub>0 \<Turnstile> s" and
     B: "n \<notin> bad_shakey"
   shows "(Asset n, Crypt (Auth_ShaKey n) (PriKey S)) \<in> s \<longrightarrow>
     PriKey S \<notin> spied s"
 proof (rule rtrancl_induct [OF A], simp add: image_def, rule impI)
   fix s s'
   assume
     C: "s\<^sub>0 \<Turnstile> s" and
     D: "s \<turnstile> s'" and
     E: "(Asset n, Crypt (Auth_ShaKey n) (PriKey S)) \<in> s \<longrightarrow>
       PriKey S \<notin> spied s" and
     F: "(Asset n, Crypt (Auth_ShaKey n) (PriKey S)) \<in> s'"
   show "PriKey S \<notin> spied s'"
   proof (insert D E F, auto simp add: rel_def)
     assume "(Asset n, Crypt (ShaK (Auth_ShaK n)) (Key (PriK S))) \<in> s"
     hence "(Asset n, Crypt (Auth_ShaKey n) (PriKey S)) \<in> s" by simp
     hence "PriKey S \<in> used s"
       by (rule asset_i_used [OF C, THEN mp])
     moreover assume "Key (PriK S) \<notin> used s"
     ultimately show False by simp
   next
     fix K
     assume "(Spy, Crypt K (Key (PriK S))) \<in> s"
     hence "Crypt K (PriKey S) \<in> parts (used s)" by auto
     hence "(\<exists>m. K = Auth_ShaKey m \<and>
       (Asset m, Crypt (Auth_ShaKey m) (PriKey S)) \<in> s) \<or>
       {PriKey S, Key K} \<subseteq> spied s"
       (is "(\<exists>m. ?P m \<and> ?Q m) \<or> _")
       by (rule parts_crypt_prikey [OF C])
     moreover assume "(Spy, Key (PriK S)) \<notin> s"
     ultimately obtain m where G: "?P m \<and> ?Q m" by auto
     hence "?Q m" ..
     moreover assume
       "(Asset n, Crypt (ShaK (Auth_ShaK n)) (Key (PriK S))) \<in> s"
     hence "(Asset n, Crypt (Auth_ShaKey n) (PriKey S)) \<in> s" by simp
     ultimately have "m = n"
       by (rule asset_i_unique [OF C])
     moreover assume "(Spy, Key (InvK K)) \<in> s"
     ultimately have "Key (Auth_ShaKey n) \<in> spied s"
       using G by simp
     moreover have "Key (Auth_ShaKey n) \<notin> spied s"
       by (rule auth_shakey_secret [OF C B])
     ultimately show False by contradiction
   next
     fix B
     assume "(Spy, S \<otimes> B) \<in> s"
     hence "S \<otimes> B \<in> parts (used s)" by blast
     hence "(\<exists>m. S = Auth_PriK m \<and> (Asset m, \<lbrace>Num 2, PubKey B\<rbrace>) \<in> s) \<or>
       {PriKey S, PriKey B} \<subseteq> spied s"
       (is "(\<exists>m. ?P m \<and> _) \<or> _")
       by (rule parts_mult [OF C])
     moreover assume "(Spy, Key (PriK S)) \<notin> s"
     ultimately obtain m where "?P m" by auto
     moreover assume
       "(Asset n, Crypt (ShaK (Auth_ShaK n)) (Key (PriK S))) \<in> s"
     ultimately have "(Asset n, Crypt (Auth_ShaKey n) (Auth_PriKey m)) \<in> s"
       by simp
     thus False
       by (rule auth_prikey_asset_i [OF C])
   next
     fix A
     assume "(Spy, A \<otimes> S) \<in> s"
     hence "A \<otimes> S \<in> parts (used s)" by blast
     hence "(\<exists>m. A = Auth_PriK m \<and> (Asset m, \<lbrace>Num 2, PubKey S\<rbrace>) \<in> s) \<or>
       {PriKey A, PriKey S} \<subseteq> spied s"
       (is "(\<exists>m. _ \<and> ?P m) \<or> _")
       by (rule parts_mult [OF C])
     moreover assume "(Spy, Key (PriK S)) \<notin> s"
     ultimately obtain m where "?P m" by auto
     assume "(Asset n, Crypt (ShaK (Auth_ShaK n)) (Key (PriK S))) \<in> s"
     hence "(Asset n, Crypt (Auth_ShaKey n) (PriKey S)) \<in> s" by simp
     thus False
       by (rule asset_i_asset_ii [OF C _ `?P m`])
   next
     fix Y
     assume "(Spy, \<lbrace>Key (PriK S), Y\<rbrace>) \<in> s"
     hence "\<lbrace>PriKey S, Y\<rbrace> \<in> parts (used s)" by auto
     hence "{PriKey S, Y} \<subseteq> spied s"
       by (rule parts_mpair_key [OF C, where K = "PriK S"], simp)
     moreover assume "(Spy, Key (PriK S)) \<notin> s"
     ultimately show False by simp
   next
     fix X
     assume "(Spy, \<lbrace>X, Key (PriK S)\<rbrace>) \<in> s"
     hence "\<lbrace>X, PriKey S\<rbrace> \<in> parts (used s)" by auto
     hence "{X, PriKey S} \<subseteq> spied s"
       by (rule parts_mpair_key [OF C, where K = "PriK S"], simp add: image_def)
     moreover assume "(Spy, Key (PriK S)) \<notin> s"
     ultimately show False by simp
   qed
 qed
 
 proposition owner_ii_secret [rule_format]:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow>
     (Owner n, \<lbrace>Num 1, PubKey A\<rbrace>) \<in> s \<longrightarrow>
   PriKey A \<notin> spied s"
 proof (erule rtrancl_induct, simp add: image_def, rule impI)
   fix s s'
   assume
     A: "s\<^sub>0 \<Turnstile> s" and
     B: "s \<turnstile> s'" and
     C: "(Owner n, \<lbrace>Num 1, PubKey A\<rbrace>) \<in> s \<longrightarrow> PriKey A \<notin> spied s" and
     D: "(Owner n, \<lbrace>Num 1, PubKey A\<rbrace>) \<in> s'"
   show "PriKey A \<notin> spied s'"
   proof (insert B C D, auto simp add: rel_def)
     assume "(Owner n, \<lbrace>Num (Suc 0), Key (PubK A)\<rbrace>) \<in> s"
     hence "(Owner n, \<lbrace>Num 1, PubKey A\<rbrace>) \<in> s" by simp
     hence "PriKey A \<in> used s"
       by (rule owner_ii_used [OF A, THEN mp])
     moreover assume "Key (PriK A) \<notin> used s"
     ultimately show False by simp
   next
     fix K
     assume "(Spy, Crypt K (Key (PriK A))) \<in> s"
     hence "Crypt K (PriKey A) \<in> parts (used s)" by auto
     hence "(\<exists>m. K = Auth_ShaKey m \<and>
       (Asset m, Crypt (Auth_ShaKey m) (PriKey A)) \<in> s) \<or>
       {PriKey A, Key K} \<subseteq> spied s"
       (is "(\<exists>m. _ \<and> ?P m) \<or> _")
       by (rule parts_crypt_prikey [OF A])
     moreover assume "(Spy, Key (PriK A)) \<notin> s"
     ultimately obtain m where "?P m" by auto
     moreover assume "(Owner n, \<lbrace>Num (Suc 0), Key (PubK A)\<rbrace>) \<in> s"
     hence "(Owner n, \<lbrace>Num 1, PubKey A\<rbrace>) \<in> s" by simp
     ultimately show False
       by (rule asset_i_owner_ii [OF A])
   next
     fix B
     assume "(Spy, A \<otimes> B) \<in> s"
     hence "A \<otimes> B \<in> parts (used s)" by blast
     hence "(\<exists>m. A = Auth_PriK m \<and> (Asset m, \<lbrace>Num 2, PubKey B\<rbrace>) \<in> s) \<or>
       {PriKey A, PriKey B} \<subseteq> spied s"
       (is "(\<exists>m. ?P m \<and> _) \<or> _")
       by (rule parts_mult [OF A])
     moreover assume "(Spy, Key (PriK A)) \<notin> s"
     ultimately obtain m where "?P m" by auto
     moreover assume "(Owner n, \<lbrace>Num (Suc 0), Key (PubK A)\<rbrace>) \<in> s"
     ultimately have "(Owner n, \<lbrace>Num 1, Auth_PubKey m\<rbrace>) \<in> s" by simp
     thus False
       by (rule auth_pubkey_owner_ii [OF A])
   next
     fix B
     assume "(Spy, B \<otimes> A) \<in> s"
     hence "B \<otimes> A \<in> parts (used s)" by blast
     hence "(\<exists>m. B = Auth_PriK m \<and> (Asset m, \<lbrace>Num 2, PubKey A\<rbrace>) \<in> s) \<or>
       {PriKey B, PriKey A} \<subseteq> spied s"
       (is "(\<exists>m. _ \<and> ?P m) \<or> _")
       by (rule parts_mult [OF A])
     moreover assume "(Spy, Key (PriK A)) \<notin> s"
     ultimately obtain m where "?P m" by auto
     moreover assume "(Owner n, \<lbrace>Num (Suc 0), Key (PubK A)\<rbrace>) \<in> s"
     hence "(Owner n, \<lbrace>Num 1, PubKey A\<rbrace>) \<in> s" by simp
     ultimately show False
       by (rule asset_ii_owner_ii [OF A])
   next
     fix Y
     assume "(Spy, \<lbrace>Key (PriK A), Y\<rbrace>) \<in> s"
     hence "\<lbrace>PriKey A, Y\<rbrace> \<in> parts (used s)" by auto
     hence "{PriKey A, Y} \<subseteq> spied s"
       by (rule parts_mpair_key [OF A, where K = "PriK A"], simp)
     moreover assume "(Spy, Key (PriK A)) \<notin> s"
     ultimately show False by simp
   next
     fix X
     assume "(Spy, \<lbrace>X, Key (PriK A)\<rbrace>) \<in> s"
     hence "\<lbrace>X, PriKey A\<rbrace> \<in> parts (used s)" by auto
     hence "{X, PriKey A} \<subseteq> spied s"
       by (rule parts_mpair_key [OF A, where K = "PriK A"], simp add: image_def)
     moreover assume "(Spy, Key (PriK A)) \<notin> s"
     ultimately show False by simp
   qed
 qed
 
 proposition seskey_spied [rule_format]:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow>
     SesKey SK \<in> spied s \<longrightarrow>
   (\<exists>S A C. fst SK = Some S \<and> A \<in> fst (snd SK) \<and> C \<in> snd (snd SK) \<and>
     {PriKey S, PriKey A, PriKey C} \<subseteq> spied s)"
   (is "_ \<Longrightarrow> _ \<longrightarrow> (\<exists>S A C. ?P S A C s)")
 proof (erule rtrancl_induct, simp add: image_def, rule impI)
   fix s s'
   assume
     A: "s\<^sub>0 \<Turnstile> s" and
     B: "s \<turnstile> s'" and
     C: "SesKey SK \<in> spied s \<longrightarrow> (\<exists>S A C. ?P S A C s)" and
     D: "SesKey SK \<in> spied s'"
   show "\<exists>S A C. ?P S A C s'"
   proof (insert B C D, auto simp add: rel_def, blast, rule_tac [!] FalseE)
     fix K
     assume "(Spy, Crypt K (Key (SesK SK))) \<in> s"
     hence "Crypt K (Key (SesK SK)) \<in> parts (used s)" by blast
     hence "{Key (SesK SK), Key K} \<subseteq> spied s"
       by (rule parts_crypt_key [OF A], simp add: image_def)
     moreover assume "(Spy, Key (SesK SK)) \<notin> s"
     ultimately show False by simp
   next
     fix Y
     assume "(Spy, \<lbrace>Key (SesK SK), Y\<rbrace>) \<in> s"
     hence "\<lbrace>SesKey SK, Y\<rbrace> \<in> parts (used s)" by auto
     hence "{SesKey SK, Y} \<subseteq> spied s"
       by (rule parts_mpair_key [OF A, where K = "SesK SK"], simp)
     moreover assume "(Spy, Key (SesK SK)) \<notin> s"
     ultimately show False by simp
   next
     fix X
     assume "(Spy, \<lbrace>X, Key (SesK SK)\<rbrace>) \<in> s"
     hence "\<lbrace>X, SesKey SK\<rbrace> \<in> parts (used s)" by auto
     hence "{X, SesKey SK} \<subseteq> spied s"
       by (rule parts_mpair_key [OF A, where K = "SesK SK"], simp add: image_def)
     moreover assume "(Spy, Key (SesK SK)) \<notin> s"
     ultimately show False by simp
   qed
 qed
 
 proposition owner_seskey_shakey:
   assumes
     A: "s\<^sub>0 \<Turnstile> s" and
     B: "n \<notin> bad_shakey" and
     C: "(Owner n, SesKey SK) \<in> s"
   shows "SesKey SK \<notin> spied s"
 proof
   have "(\<exists>S. fst SK = Some S \<and> Crypt (Auth_ShaKey n) (PriKey S) \<in> used s) \<or>
     fst SK = None"
     (is "(\<exists>S. ?P S) \<or> _")
     by (rule owner_seskey_nonce [OF A C])
   moreover assume "SesKey SK \<in> spied s"
   hence D: "\<exists>S A C. fst SK = Some S \<and> A \<in> fst (snd SK) \<and>
     C \<in> snd (snd SK) \<and> {PriKey S, PriKey A, PriKey C} \<subseteq> spied s"
     by (rule seskey_spied [OF A])
   ultimately obtain S where "?P S" by auto
   hence "Crypt (Auth_ShaKey n) (PriKey S) \<in> parts (used s)" by blast
   hence "(\<exists>m. Auth_ShaKey n = Auth_ShaKey m \<and>
     (Asset m, Crypt (Auth_ShaKey m) (PriKey S)) \<in> s) \<or>
     {PriKey S, Key (Auth_ShaKey n)} \<subseteq> spied s"
     (is "(\<exists>m. ?Q m \<and> ?R m) \<or> _")
     by (rule parts_crypt_prikey [OF A])
   moreover have "Key (Auth_ShaKey n) \<notin> spied s"
     by (rule auth_shakey_secret [OF A B])
   ultimately obtain m where "?Q m" and "?R m" by blast
   hence "m \<notin> bad_shakey"
     using B by simp
   hence "PriKey S \<notin> spied s"
     by (rule asset_i_secret [OF A _ `?R m`])
   moreover have "PriKey S \<in> spied s"
     using D and `?P S` by auto
   ultimately show False by contradiction
 qed
 
 proposition owner_seskey_prikey:
   assumes
     A: "s\<^sub>0 \<Turnstile> s" and
     B: "n \<notin> bad_prikey" and
     C: "(Owner m, SesKey SK) \<in> s" and
     D: "(Asset n, \<lbrace>Num 2, PubKey B\<rbrace>) \<in> s" and
     E: "B \<in> fst (snd SK)"
   shows "SesKey SK \<notin> spied s"
 proof
   have "\<exists>A B C D. fst (snd SK) = {A, B} \<and> snd (snd SK) = {C, D} \<and>
     (Owner m, \<lbrace>Num 1, PubKey A\<rbrace>) \<in> s \<and>
     (Owner m, \<lbrace>Num 3, PubKey C\<rbrace>) \<in> s \<and>
     (Owner m, Crypt (SesK SK) (PubKey D)) \<in> s"
     (is "\<exists>A B C D. ?P A B \<and> _ \<and> ?Q A \<and> _")
     by (rule owner_seskey_other [OF A C])
   then obtain A B' where "?P A B'" and "?Q A" by blast
   assume "SesKey SK \<in> spied s"
   hence "\<exists>S A' C. fst SK = Some S \<and> A' \<in> fst (snd SK) \<and> C \<in> snd (snd SK) \<and>
     {PriKey S, PriKey A', PriKey C} \<subseteq> spied s"
     (is "\<exists>S A' C. _ \<and> ?R A' \<and> _")
     by (rule seskey_spied [OF A])
   then obtain A' where "A' \<in> fst (snd SK)" and "PriKey A' \<in> spied s" (is "?R A'")
     by blast
   hence "{A', A, B} \<subseteq> {A, B'}"
     using E and `?P A B'` by simp
   hence "card {A', A, B} \<le> card {A, B'}"
     by (rule_tac card_mono, simp)
   also have "\<dots> \<le> Suc (Suc 0)"
     by (rule card_insert_le_m1, simp_all)
   finally have "card {A', A, B} \<le> Suc (Suc 0)" .
   moreover have "card {A', A, B} = Suc (card {A, B})"
   proof (rule card_insert_disjoint, simp_all, rule conjI, rule_tac [!] notI)
     assume "A' = A"
     hence "?R A"
       using `?R A'` by simp
     moreover have "\<not> ?R A"
       by (rule owner_ii_secret [OF A `?Q A`])
     ultimately show False by contradiction
   next
     assume "A' = B"
     hence "?R B"
       using `?R A'` by simp
     moreover have "\<not> ?R B"
       by (rule asset_ii_secret [OF A B D])
     ultimately show False by contradiction
   qed
   moreover have "card {A, B} = Suc (card {B})"
   proof (rule card_insert_disjoint, simp_all, rule notI)
     assume "A = B"
     hence "(Asset n, \<lbrace>Num 2, PubKey A\<rbrace>) \<in> s"
       using D by simp
     thus False
       by (rule asset_ii_owner_ii [OF A _ `?Q A`])
   qed
   ultimately show False by simp
 qed
 
 proposition asset_seskey_shakey:
   assumes
     A: "s\<^sub>0 \<Turnstile> s" and
     B: "n \<notin> bad_shakey" and
     C: "(Asset n, SesKey SK) \<in> s"
   shows "SesKey SK \<notin> spied s"
 proof
   have "\<exists>S. fst SK = Some S \<and>
     (Asset n, Crypt (Auth_ShaKey n) (PriKey S)) \<in> s"
     (is "\<exists>S. ?P S \<and> ?Q S")
     by (rule asset_seskey_nonce [OF A C])
   then obtain S where "?P S" and "?Q S" by blast
   have "PriKey S \<notin> spied s"
     by (rule asset_i_secret [OF A B `?Q S`])
   moreover assume "SesKey SK \<in> spied s"
   hence "\<exists>S A C. fst SK = Some S \<and> A \<in> fst (snd SK) \<and> C \<in> snd (snd SK) \<and>
     {PriKey S, PriKey A, PriKey C} \<subseteq> spied s"
     by (rule seskey_spied [OF A])
   hence "PriKey S \<in> spied s"
     using `?P S` by auto
   ultimately show False by contradiction
 qed
 
 
 theorem owner_seskey_unique:
   assumes
     A: "s\<^sub>0 \<Turnstile> s" and
     B: "(Owner m, Crypt (SesK SK) (Pwd m)) \<in> s" and
     C: "(Owner n, Crypt (SesK SK) (Pwd n)) \<in> s"
   shows "m = n"
 proof (rule ccontr)
   have D: "(Owner m, SesKey SK) \<in> s \<and>
     (\<exists>A B C. Token m A B C SK \<in> used s \<and> B \<in> fst (snd SK))"
     (is "?P m \<and> (\<exists>A B C. ?Q m A B C)")
     by (rule owner_v_state [OF A B])
   hence "?P m" by blast
   hence "\<exists>A B C D. fst (snd SK) = {A, B} \<and> snd (snd SK) = {C, D} \<and>
     (Owner m, \<lbrace>Num 1, PubKey A\<rbrace>) \<in> s \<and>
     (Owner m, \<lbrace>Num 3, PubKey C\<rbrace>) \<in> s \<and>
     (Owner m, Crypt (SesK SK) (PubKey D)) \<in> s"
     (is "\<exists>A B C D. ?R A B \<and> ?S C D \<and> ?T m A \<and> ?U m C D")
     by (rule owner_seskey_other [OF A])
   then obtain A B where "?R A B" and "?T m A" by blast
   have "?P n \<and> (\<exists>A B C. ?Q n A B C)"
     by (rule owner_v_state [OF A C])
   hence "?P n" by blast
   hence "\<exists>A B C D. ?R A B \<and> ?S C D \<and> ?T n A \<and> ?U n C D"
     by (rule owner_seskey_other [OF A])
   then obtain A' B' where "?R A' B'" and "?T n A'" by blast
   from D obtain A'' B'' C where "?Q m A'' B'' C" by blast
   hence "Token m A'' B'' C SK \<in> parts (used s)" by blast
   hence "Crypt (SesK SK) (A'' \<otimes> B'') \<in> parts (used s)" by blast
   hence "B'' \<in> fst (snd SK) \<and>
     (\<exists>i C'. (Asset i, Token i (Auth_PriK i) B'' C' SK) \<in> s) \<or>
     {A'' \<otimes> B'', SesKey SK} \<subseteq> spied s"
     (is "?V B'' \<and> (\<exists>i C'. ?W i B'' C') \<or> _")
     by (rule parts_crypt_mult [OF A])
   hence "\<exists>D. ?V D \<and> D \<notin> {A, A'}"
   proof (rule disjE, (erule_tac conjE, ((erule_tac exE)+)?)+)
     fix i C'
     assume "?V B''" and "?W i B'' C'"
     have "\<exists>A D. ?R A B'' \<and> ?S C' D \<and>
       (Asset i, \<lbrace>Num 2, PubKey B''\<rbrace>) \<in> s \<and> (Asset i, \<lbrace>Num 4, PubKey D\<rbrace>) \<in> s \<and>
       Crypt (SesK SK) (PubKey D) \<in> used s \<and> (Asset i, PubKey B'') \<in> s"
       (is "\<exists>A D. _ \<and> _ \<and> ?X i B'' \<and> _")
       by (rule asset_iv_state [OF A `?W i B'' C'`])
     hence "?X i B''" by blast
     have "B'' \<noteq> A"
     proof
       assume "B'' = A"
       hence "?X i A"
         using `?X i B''` by simp
       thus False
         by (rule asset_ii_owner_ii [OF A _ `?T m A`])
     qed
     moreover have "B'' \<noteq> A'"
     proof
       assume "B'' = A'"
       hence "?X i A'"
         using `?X i B''` by simp
       thus False
         by (rule asset_ii_owner_ii [OF A _ `?T n A'`])
     qed
     ultimately show ?thesis
       using `?V B''` by blast
   next
     assume "{A'' \<otimes> B'', SesKey SK} \<subseteq> spied s"
     hence "SesKey SK \<in> spied s" by simp
     hence "\<exists>S D E. fst SK = Some S \<and> ?V D \<and> E \<in> snd (snd SK) \<and>
       {PriKey S, PriKey D, PriKey E} \<subseteq> spied s"
       by (rule seskey_spied [OF A])
     then obtain D where "?V D" and "PriKey D \<in> spied s" (is "?X D")
       by blast
     moreover have "D \<noteq> A"
     proof
       assume "D = A"
       hence "?X A"
         using `?X D` by simp
       moreover have "\<not> ?X A"
         by (rule owner_ii_secret [OF A `?T m A`])
       ultimately show False by contradiction
     qed
     moreover have "D \<noteq> A'"
     proof
       assume "D = A'"
       hence "?X A'"
         using `?X D` by simp
       moreover have "\<not> ?X A'"
         by (rule owner_ii_secret [OF A `?T n A'`])
       ultimately show False by contradiction
     qed
     ultimately show ?thesis by blast
   qed
   then obtain D where "?V D" and E: "D \<notin> {A, A'}" by blast
   hence "{D, A, A'} \<subseteq> {A, B}"
     using `?R A B` and `?R A' B'` by blast
   hence "card {D, A, A'} \<le> card {A, B}"
     by (rule_tac card_mono, simp)
   also have "\<dots> \<le> Suc (Suc 0)"
     by (rule card_insert_le_m1, simp_all)
   finally have "card {D, A, A'} \<le> Suc (Suc 0)" .
   moreover have "card {D, A, A'} = Suc (card {A, A'})"
     by (rule card_insert_disjoint [OF _ E], simp)
   moreover assume "m \<noteq> n"
   hence "card {A, A'} = Suc (card {A'})"
   proof (rule_tac card_insert_disjoint, simp_all, erule_tac contrapos_nn)
     assume "A = A'"
     hence "?T n A"
       using `?T n A'` by simp
     thus "m = n"
       by (rule owner_ii_unique [OF A `?T m A`])
   qed
   ultimately show False by simp
 qed
 
 
 theorem owner_seskey_secret:
   assumes
     A: "s\<^sub>0 \<Turnstile> s" and
     B: "n \<notin> bad_shakey \<inter> bad_prikey" and
     C: "(Owner n, Crypt (SesK SK) (Pwd n)) \<in> s"
   shows "SesKey SK \<notin> spied s"
 proof -
   have "(Owner n, SesKey SK) \<in> s \<and>
     (\<exists>A B C. Token n A B C SK \<in> used s \<and> B \<in> fst (snd SK))"
     (is "?P \<and> (\<exists>A B C. ?Q A B C \<and> ?R B)")
     by (rule owner_v_state [OF A C])
   then obtain A B C where "?P" and "?Q A B C" and "?R B" by blast
   have "n \<in> bad_shakey \<or> n \<notin> bad_shakey" by simp
   moreover {
     assume "n \<in> bad_shakey"
     hence D: "n \<notin> bad_prikey"
       using B by simp
     hence "Auth_PriKey n \<notin> spied s"
       by (rule auth_prikey_secret [OF A])
     moreover have "Sign n A \<in> parts (used s)"
       using `?Q A B C` by blast
     hence "A = Auth_PriK n"
       by (rule parts_sign [OF A])
     hence "?Q (Auth_PriK n) B C"
       using `?Q A B C` by simp
     hence "Auth_PriK n \<otimes> B \<in> parts (used s)" by blast
     hence "(\<exists>m. Auth_PriK n = Auth_PriK m \<and>
       (Asset m, \<lbrace>Num 2, PubKey B\<rbrace>) \<in> s) \<or>
       {PriKey (Auth_PriK n), PriKey B} \<subseteq> spied s"
       (is "(\<exists>m. ?S m \<and> ?T m) \<or> _")
       by (rule parts_mult [OF A])
     ultimately obtain m where "?S m" and "?T m" by auto
     hence "m \<notin> bad_prikey"
       using D by simp
     hence ?thesis
       by (rule owner_seskey_prikey [OF A _ `?P` `?T m` `?R B`])
   }
   moreover {
     assume "n \<notin> bad_shakey"
     hence ?thesis
       by (rule owner_seskey_shakey [OF A _ `?P`])
   }
   ultimately show ?thesis ..
 qed
 
 
 theorem owner_num_genuine:
   assumes
     A: "s\<^sub>0 \<Turnstile> s" and
     B: "n \<notin> bad_shakey \<inter> bad_prikey" and
     C: "(Owner n, Crypt (SesK SK) (Pwd n)) \<in> s" and
     D: "Crypt (SesK SK) (Num 0) \<in> used s"
   shows "(Asset n, Crypt (SesK SK) (Num 0)) \<in> s"
 proof -
   have "Crypt (SesK SK) (Num 0) \<in> parts (used s)"
     using D ..
   hence "(\<exists>m. (Asset m, Crypt (SesK SK) (Num 0)) \<in> s) \<or>
     SesKey SK \<in> spied s"
     by (rule parts_crypt_num [OF A])
   moreover have E: "SesKey SK \<notin> spied s"
     by (rule owner_seskey_secret [OF A B C])
   ultimately obtain m where "(Asset m, Crypt (SesK SK) (Num 0)) \<in> s"
     by blast
   moreover from this have "(Asset m, SesKey SK) \<in> s \<and>
     Crypt (SesK SK) (Pwd m) \<in> used s"
     by (rule asset_v_state [OF A])
   hence "Crypt (SesK SK) (Pwd m) \<in> parts (used s)" by blast
   hence "(\<exists>SK'. SesK SK = SesK SK' \<and>
     (Owner m, Crypt (SesK SK') (Pwd m)) \<in> s) \<or>
     {Pwd m, Key (SesK SK)} \<subseteq> spied s"
     by (rule parts_crypt_pwd [OF A])
   hence "(Owner m, Crypt (SesK SK) (Pwd m)) \<in> s"
     using E by simp
   hence "m = n"
     by (rule owner_seskey_unique [OF A _ C])
   ultimately show ?thesis by simp
 qed
 
 
 theorem owner_token_genuine:
   assumes
     A: "s\<^sub>0 \<Turnstile> s" and
     B: "n \<notin> bad_shakey \<inter> bad_prikey" and
     C: "(Owner n, \<lbrace>Num 3, PubKey C\<rbrace>) \<in> s" and
     D: "(Owner n, Crypt (SesK SK) (Pwd n)) \<in> s" and
     E: "Token n A B C SK \<in> used s"
   shows "A = Auth_PriK n \<and> B \<in> fst (snd SK) \<and> C \<in> snd (snd SK) \<and>
     (Asset n, \<lbrace>Num 2, PubKey B\<rbrace>) \<in> s \<and> (Asset n, Token n A B C SK) \<in> s"
     (is "?P n A \<and> ?Q B \<and> ?R C \<and> ?S n B \<and> _")
 proof -
   have "Crypt (SesK SK) (Sign n A) \<in> parts (used s)"
     using E by blast
   hence "(Asset n, SesKey SK) \<in> s \<or> SesKey SK \<in> spied s"
     by (rule parts_crypt_sign [OF A])
   moreover have "SesKey SK \<notin> spied s"
     by (rule owner_seskey_secret [OF A B D])
   ultimately have "(Asset n, SesKey SK) \<in> s" by simp
   hence "\<exists>A B C D. fst (snd SK) = {A, B} \<and> snd (snd SK) = {C, D} \<and>
     ?S n B \<and> (Asset n, \<lbrace>Num 4, PubKey D\<rbrace>) \<in> s \<and>
     (Asset n, Token n (Auth_PriK n) B C SK) \<in> s"
     (is "\<exists>A B C D. ?T A B \<and> ?U C D \<and> _ \<and> ?V n D \<and> ?W n B C")
     by (rule asset_seskey_other [OF A])
   then obtain A' B' C' D where
    "?T A' B'" and "?U C' D" and "?S n B'" and "?V n D" and "?W n B' C'"
     by blast
   have "Sign n A \<in> parts (used s)"
     using E by blast
   hence "?P n A"
     by (rule parts_sign [OF A])
   have "Crypt (SesK SK) (A \<otimes> B) \<in> parts (used s)"
     using E by blast
   hence "?Q B \<and> (\<exists>m C''. ?W m B C'') \<or> {A \<otimes> B, SesKey SK} \<subseteq> spied s"
     by (rule parts_crypt_mult [OF A])
   moreover have F: "SesKey SK \<notin> spied s"
     by (rule owner_seskey_secret [OF A B D])
   ultimately obtain m C'' where "?Q B" and "?W m B C''" by blast
   have "\<exists>A D. ?T A B \<and> ?U C'' D \<and> ?S m B \<and> ?V m D \<and>
     Crypt (SesK SK) (PubKey D) \<in> used s \<and> (Asset m, PubKey B) \<in> s"
     by (rule asset_iv_state [OF A `?W m B C''`])
   hence "?S m B" by blast
   have "(Owner n, SesKey SK) \<in> s \<and>
     (\<exists>A B C. Token n A B C SK \<in> used s \<and> B \<in> fst (snd SK))"
     by (rule owner_v_state [OF A D])
   hence "(Owner n, SesKey SK) \<in> s" by blast
   hence "\<exists>A B C D. ?T A B \<and> ?U C D \<and>
     (Owner n, \<lbrace>Num 1, PubKey A\<rbrace>) \<in> s \<and>
     (Owner n, \<lbrace>Num 3, PubKey C\<rbrace>) \<in> s \<and>
     (Owner n, Crypt (SesK SK) (PubKey D)) \<in> s"
     (is "\<exists>A B C D. _ \<and> _ \<and> ?X A \<and> _")
     by (rule owner_seskey_other [OF A])
   then obtain A'' where "?Q A''" and "?X A''" by blast
   have G: "B' = B"
   proof (rule ccontr)
     have "{A'', B', B} \<subseteq> {A', B'}"
       using `?T A' B'` and `?Q B` and `?Q A''` by simp
     hence "card {A'', B', B} \<le> card {A', B'}"
       by (rule_tac card_mono, simp)
     also have "\<dots> \<le> Suc (Suc 0)"
       by (rule card_insert_le_m1, simp_all)
     finally have "card {A'', B', B} \<le> Suc (Suc 0)" .
     moreover have "A'' \<notin> {B', B}"
     proof (simp, rule conjI, rule_tac [!] notI)
       assume "A'' = B'"
       hence "?S n A''"
         using `?S n B'` by simp
       thus False
         by (rule asset_ii_owner_ii [OF A _ `?X A''`])
     next
       assume "A'' = B"
       hence "?S m A''"
         using `?S m B` by simp
       thus False
         by (rule asset_ii_owner_ii [OF A _ `?X A''`])
     qed
     hence "card {A'', B', B} = Suc (card {B', B})"
       by (rule_tac card_insert_disjoint, simp)
     moreover assume "B' \<noteq> B"
     hence "card {B', B} = Suc (card {B})"
       by (rule_tac card_insert_disjoint, simp_all)
     ultimately show False by simp
   qed
   hence "?S n B"
     using `?S n B'` by simp
   have "Crypt (SesK SK) (PubKey C) \<in> parts (used s)"
     using E by blast
   hence "?R C \<and> ((\<exists>n. (Owner n, SesKey SK) \<in> s) \<or> (\<exists>n B. ?W n B C)) \<or>
     SesKey SK \<in> spied s"
     by (rule parts_crypt_pubkey [OF A])
   hence "?R C"
     using F by simp
   hence "C \<in> {C', D}"
     using `?U C' D` by simp
   moreover have "C \<noteq> D"
   proof
     assume "C = D"
     hence "?V n C"
       using `?V n D` by simp
     thus False
       by (rule asset_iii_owner_iii [OF A _ C])
   qed
   ultimately have "C = C'" by simp
   hence "(Asset n, Token n A B C SK) \<in> s"
     using G and `?P n A` and `?W n B' C'` by simp
   thus ?thesis
     using `?P n A` and `?Q B` and `?R C` and `?S n B` by simp
 qed
 
 
 theorem pwd_secret:
   assumes
     A: "s\<^sub>0 \<Turnstile> s" and
     B: "n \<notin> bad_pwd \<union> bad_shakey \<inter> bad_prikey"
   shows "Pwd n \<notin> spied s"
 proof (rule rtrancl_induct [OF A], insert B, simp add: image_def)
   fix s s'
   assume
     C: "s\<^sub>0 \<Turnstile> s" and
     D: "s \<turnstile> s'" and
     E: "Pwd n \<notin> spied s"
   show "Pwd n \<notin> spied s'"
   proof (insert D E, auto simp add: rel_def)
     fix K
     assume "(Spy, Crypt K (Pwd n)) \<in> s"
     hence "Crypt K (Pwd n) \<in> parts (used s)" by blast
     hence "(\<exists>SK. K = SesK SK \<and> (Owner n, Crypt (SesK SK) (Pwd n)) \<in> s) \<or>
       {Pwd n, Key K} \<subseteq> spied s"
       (is "(\<exists>SK. ?P SK \<and> ?Q SK) \<or> _")
       by (rule parts_crypt_pwd [OF C])
     then obtain SK where "?P SK" and "?Q SK"
       using E by blast
     have "n \<notin> bad_shakey \<inter> bad_prikey"
       using B by simp
     hence "SesKey SK \<notin> spied s"
       by (rule owner_seskey_secret [OF C _ `?Q SK`])
     moreover assume "(Spy, Key (InvK K)) \<in> s"
     ultimately show False
       using `?P SK` by simp
   next
     fix Y
     assume "(Spy, \<lbrace>Pwd n, Y\<rbrace>) \<in> s"
     hence "\<lbrace>Pwd n, Y\<rbrace> \<in> parts (used s)" by blast
     hence "{Pwd n, Y} \<subseteq> spied s"
       by (rule parts_mpair_pwd [OF C, where n = n], simp)
     with E show False by simp
   next
     fix X
     assume "(Spy, \<lbrace>X, Pwd n\<rbrace>) \<in> s"
     hence "\<lbrace>X, Pwd n\<rbrace> \<in> parts (used s)" by blast
     hence "{X, Pwd n} \<subseteq> spied s"
       by (rule parts_mpair_pwd [OF C, where n = n], simp)
     with E show False by simp
   qed
 qed
 
 
 theorem asset_seskey_unique:
   assumes
     A: "s\<^sub>0 \<Turnstile> s" and
     B: "(Asset m, Token m (Auth_PriK m) B' C' SK) \<in> s" and
     C: "(Asset n, Token n (Auth_PriK n) B C SK) \<in> s"
       (is "?P n B C SK s")
   shows "m = n \<and> B' = B \<and> C' = C"
 proof (subst (2) cases_simp [of "B' = B", symmetric], simp, rule conjI, rule impI,
  insert B C, simp only:, drule asset_iv_unique [OF A], simp, simp, rule ccontr)
   assume "B' \<noteq> B"
   moreover have "\<exists>A D. fst (snd SK) = {A, B'} \<and> snd (snd SK) = {C', D} \<and>
     (Asset m, \<lbrace>Num 2, PubKey B'\<rbrace>) \<in> s \<and> (Asset m, \<lbrace>Num 4, PubKey D\<rbrace>) \<in> s \<and>
     Crypt (SesK SK) (PubKey D) \<in> used s \<and> (Asset m, PubKey B') \<in> s"
     (is "?Q m B' C'")
     by (rule asset_iv_state [OF A B])
   then obtain A where "fst (snd SK) = {A, B'}" and
     "(Asset m, \<lbrace>Num 2, PubKey B'\<rbrace>) \<in> s"
     by blast
   moreover have "?Q n B C"
     by (rule asset_iv_state [OF A C])
   hence "B \<in> fst (snd SK)" and "(Asset n, \<lbrace>Num 2, PubKey B\<rbrace>) \<in> s"
     by auto
   ultimately have D: "\<forall>A \<in> fst (snd SK).
     \<exists>i C. (Asset i, \<lbrace>Num 2, PubKey A\<rbrace>) \<in> s \<and> ?P i A C SK s"
     using B and C by auto
   have "Crypt (SesK SK) (PubKey C) \<in> parts (used s)"
     using C by blast
   thus False
   proof (rule parts_pubkey_false [OF A], rule_tac allI, rule_tac [!] notI)
     fix i
     assume "(Owner i, SesKey SK) \<in> s"
     hence "\<exists>A B C D. fst (snd SK) = {A, B} \<and> snd (snd SK) = {C, D} \<and>
       (Owner i, \<lbrace>Num 1, PubKey A\<rbrace>) \<in> s \<and>
       (Owner i, \<lbrace>Num 3, PubKey C\<rbrace>) \<in> s \<and>
       (Owner i, Crypt (SesK SK) (PubKey D)) \<in> s"
       by (rule owner_seskey_other [OF A])
     then obtain A where "A \<in> fst (snd SK)" and
       E: "(Owner i, \<lbrace>Num 1, PubKey A\<rbrace>) \<in> s"
       by blast
     then obtain j where "(Asset j, \<lbrace>Num 2, PubKey A\<rbrace>) \<in> s"
       using D by blast
     thus False
       by (rule asset_ii_owner_ii [OF A _ E])
   next
     assume "SesKey SK \<in> spied s"
     hence "\<exists>S A C. fst SK = Some S \<and> A \<in> fst (snd SK) \<and> C \<in> snd (snd SK) \<and>
       {PriKey S, PriKey A, PriKey C} \<subseteq> spied s"
       (is "?R s")
       by (rule seskey_spied [OF A])
     moreover have "\<not> (\<exists>A \<in> fst (snd SK). PriKey A \<in> spied s)"
       (is "\<not> ?S s")
     proof
       assume "?S s"
       moreover have "\<not> ?S s\<^sub>0"
         by (subst bex_simps, rule ballI, drule bspec [OF D], (erule exE)+,
          erule conjE, rule asset_ii_init [OF A])
       ultimately have "\<exists>u v. s\<^sub>0 \<Turnstile> u \<and> u \<turnstile> v \<and> v \<Turnstile> s \<and> \<not> ?S u \<and> ?S v"
         by (rule rtrancl_start [OF A])
       then obtain u v A where E: "s\<^sub>0 \<Turnstile> u" and F: "u \<turnstile> v" and G: "v \<Turnstile> s" and
         H: "\<not> ?S u" and I: "A \<in> fst (snd SK)" and J: "PriKey A \<notin> spied u" and
         K: "PriKey A \<in> spied v"
         by blast
       then obtain i where "(Asset i, \<lbrace>Num 2, PubKey A\<rbrace>) \<in> s"
         using D by blast
       hence "(Asset i, \<lbrace>Num 2, PubKey A\<rbrace>) \<in> v"
       proof (rule_tac ccontr, drule_tac rtrancl_start [OF G], simp,
        (erule_tac exE)+, (erule_tac conjE)+)
         fix w x
         assume "w \<turnstile> x" and "(Asset i, \<lbrace>Num 2, PubKey A\<rbrace>) \<notin> w" and
           "(Asset i, \<lbrace>Num 2, PubKey A\<rbrace>) \<in> x"
         hence "PriKey A \<notin> spied w"
           by (auto simp add: rel_def)
         moreover assume "v \<Turnstile> w"
         hence "PriKey A \<in> spied w"
           by (rule_tac rev_subsetD [OF K], rule spied_subset)
         ultimately show False by contradiction
       qed
       hence "(Asset i, \<lbrace>Num 2, PubKey A\<rbrace>) \<in> u"
         using F and K by (auto simp add: rel_def)
       hence "Auth_PriKey i \<in> spied u \<and> (\<exists>C SK. ?P i A C SK u)"
         by (rule asset_ii_spied_start [OF E F K J])
       then obtain C' SK' where L: "?P i A C' SK' u" by blast
       moreover have M: "u \<Turnstile> s"
         using F and G by simp
       ultimately have "?P i A C' SK' s"
         by (erule_tac rev_subsetD, rule_tac state_subset)
       moreover obtain j C where "?P j A C SK s"
         using D and I by blast
       ultimately have "i = j \<and> C' = C \<and> SK' = SK"
         by (rule asset_iv_unique [OF A])
       hence "Crypt (SesK SK) (PubKey C) \<in> parts (used u)"
         using L by blast
       thus False
       proof (rule parts_pubkey_false [OF E], rule_tac allI, rule_tac [!] notI)
         fix i
         assume "(Owner i, SesKey SK) \<in> u"
         hence "\<exists>A B C D. fst (snd SK) = {A, B} \<and> snd (snd SK) = {C, D} \<and>
           (Owner i, \<lbrace>Num 1, PubKey A\<rbrace>) \<in> u \<and>
           (Owner i, \<lbrace>Num 3, PubKey C\<rbrace>) \<in> u \<and>
           (Owner i, Crypt (SesK SK) (PubKey D)) \<in> u"
           by (rule owner_seskey_other [OF E])
         then obtain A where "A \<in> fst (snd SK)" and
           N: "(Owner i, \<lbrace>Num 1, PubKey A\<rbrace>) \<in> u"
           by blast
         then obtain j where "(Asset j, \<lbrace>Num 2, PubKey A\<rbrace>) \<in> s"
           using D by blast
         moreover have "(Owner i, \<lbrace>Num 1, PubKey A\<rbrace>) \<in> s"
           by (rule rev_subsetD [OF N], rule state_subset [OF M])
         ultimately show False
           by (rule asset_ii_owner_ii [OF A])
       next
         assume "SesKey SK \<in> spied u"
         hence "?R u"
           by (rule seskey_spied [OF E])
         thus False
           using H by blast
       qed
     qed
     ultimately show False by blast
   qed
 qed
 
 
 theorem asset_seskey_secret:
   assumes
     A: "s\<^sub>0 \<Turnstile> s" and
     B: "n \<notin> bad_shakey \<inter> (bad_pwd \<union> bad_prikey)" and
     C: "(Asset n, Crypt (SesK SK) (Num 0)) \<in> s"
   shows "SesKey SK \<notin> spied s"
 proof -
   have D: "(Asset n, SesKey SK) \<in> s \<and> Crypt (SesK SK) (Pwd n) \<in> used s"
     by (rule asset_v_state [OF A C])
   have "n \<in> bad_shakey \<or> n \<notin> bad_shakey" by simp
   moreover {
     assume "n \<in> bad_shakey"
     hence "Pwd n \<notin> spied s"
       using B by (rule_tac pwd_secret [OF A], simp)
     moreover have "Crypt (SesK SK) (Pwd n) \<in> parts (used s)"
       using D by blast
     hence "(\<exists>SK'. SesK SK = SesK SK' \<and>
       (Owner n, Crypt (SesK SK') (Pwd n)) \<in> s) \<or>
       {Pwd n, Key (SesK SK)} \<subseteq> spied s"
       by (rule parts_crypt_pwd [OF A])
     ultimately have "(Owner n, Crypt (SesK SK) (Pwd n)) \<in> s" by simp
     hence ?thesis
       using B by (rule_tac owner_seskey_secret [OF A], simp_all)
   }
   moreover {
     assume "n \<notin> bad_shakey"
     hence ?thesis
       using D by (rule_tac asset_seskey_shakey [OF A], simp_all)
   }
   ultimately show ?thesis ..
 qed
 
 
 theorem asset_pwd_genuine:
   assumes
     A: "s\<^sub>0 \<Turnstile> s" and
     B: "n \<notin> bad_shakey \<inter> (bad_pwd \<union> bad_prikey)" and
     C: "(Asset n, Crypt (SesK SK) (Num 0)) \<in> s"
   shows "(Owner n, Crypt (SesK SK) (Pwd n)) \<in> s"
 proof -
   have "(Asset n, SesKey SK) \<in> s \<and> Crypt (SesK SK) (Pwd n) \<in> used s"
     by (rule asset_v_state [OF A C])
   hence "Crypt (SesK SK) (Pwd n) \<in> parts (used s)" by blast
   hence "(\<exists>SK'. SesK SK = SesK SK' \<and>
     (Owner n, Crypt (SesK SK') (Pwd n)) \<in> s) \<or>
     {Pwd n, Key (SesK SK)} \<subseteq> spied s"
     by (rule parts_crypt_pwd [OF A])
   moreover have "SesKey SK \<notin> spied s"
     by (rule asset_seskey_secret [OF A B C])
   ultimately show ?thesis by simp
 qed
 
 
 theorem asset_token_genuine:
   assumes
     A: "s\<^sub>0 \<Turnstile> s" and
     B: "n \<notin> bad_shakey \<inter> (bad_pwd \<union> bad_prikey)" and
     C: "(Asset n, \<lbrace>Num 4, PubKey D\<rbrace>) \<in> s" and
     D: "(Asset n, Crypt (SesK SK) (Num 0)) \<in> s" and
     E: "D \<in> snd (snd SK)"
   shows "(Owner n, Crypt (SesK SK) (PubKey D)) \<in> s"
 proof -
   have "(Owner n, Crypt (SesK SK) (Pwd n)) \<in> s"
     by (rule asset_pwd_genuine [OF A B D])
   hence "(Owner n, SesKey SK) \<in> s \<and>
     (\<exists>A B C. Token n A B C SK \<in> used s \<and> B \<in> fst (snd SK))"
     by (rule owner_v_state [OF A])
   hence "(Owner n, SesKey SK) \<in> s" ..
   hence "\<exists>A B C D. fst (snd SK) = {A, B} \<and> snd (snd SK) = {C, D} \<and>
     (Owner n, \<lbrace>Num 1, PubKey A\<rbrace>) \<in> s \<and>
     (Owner n, \<lbrace>Num 3, PubKey C\<rbrace>) \<in> s \<and>
     (Owner n, Crypt (SesK SK) (PubKey D)) \<in> s"
     (is "\<exists>A B C D. _ \<and> ?P C D \<and> _ \<and> ?Q C \<and> ?R D")
     by (rule owner_seskey_other [OF A])
   then obtain C D' where "?P C D'" and "?Q C" and "?R D'" by blast
   have "D \<noteq> C"
   proof
     assume "D = C"
     hence "?Q D"
       using `?Q C` by simp
     thus False
       by (rule asset_iii_owner_iii [OF A C])
   qed
   hence "D = D'"
     using E and `?P C D'` by simp
   thus ?thesis
     using `?R D'` by simp
 qed
 
 
-end
+end
\ No newline at end of file
diff --git a/thys/Relational_Method/Definitions.thy b/thys/Relational_Method/Definitions.thy
--- a/thys/Relational_Method/Definitions.thy
+++ b/thys/Relational_Method/Definitions.thy
@@ -1,869 +1,869 @@
 (*  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 "The relational method and message anonymity"
 
 theory Definitions
   imports Main
 begin
 
 text \<open>
 \null
 
 \emph{This paper is dedicated to my mother, my favourite chess opponent -- in addition to being many
 other wonderful things!}
 \<close>
 
 
 subsection "Introduction"
 
 text \<open>
 As Bertrand Russell says in the last pages of \emph{A History of Western Philosophy}, a distinctive
 feature of science is that "we can make successive approximations to the truth, in which each new
 stage results from an improvement, not a rejection, of what has gone before". When dealing with a
 formal verification method for information processing systems, such as Paulson's inductive method
 for the verification of cryptographic protocols (cf. @{cite "Paulson98"}, @{cite "Paulson20"}), a
 more modest goal for this iterative improvement process, yet of significant practical importance, is
 to streamline the definitions and proofs needed to model such a system and verify its properties.
 
 With this aim, specially when it comes to verifying protocols using public key cryptography, this
 paper proposes an enhancement of the inductive method, named \emph{relational method} for reasons
 clarified in what follows, and puts it into practice by verifying a sample protocol. This new method
 is the result of some changes to the way how events, states, spy's capabilities, and the protocol
 itself are formalized in the inductive method. Here below is a description of these changes, along
 with a rationale for them.
 
   \<^descr>[Events.] In the inductive method, the fundamental building blocks of cryptographic protocols are
 events of the form @{text "Says A B X"}, where @{text X} is a message being exchanged, @{text A} is
 the agent that sends it, and @{text B} is the agent to which it is addressed.
 \\However, any exchanged message can be intercepted by the spy and forwarded to any other agent, so
 its intended recipient is not relevant for the protocol \emph{security} correctness -- though of
 course being relevant for the protocol \emph{functional} correctness. Moreover, a legitimate agent
 may also generate messages, e.g. ephemeral private keys, that she will never exchange with any other
 agent. To model such an event, a datatype constructor other than @{text Says} should be used. How to
 make things simpler?
 \\The solution adopted in the relational method is to model events just as ordered pairs of the form
 @{text "(A, X)"}, where @{text A} is an agent and @{text X} is a message. If event @{text "(A, X)"}
 stands for @{text A}'s sending of @{text X} to another agent, where @{text A} is a legitimate agent,
 then this event will be accompanied by event @{text "(Spy, X)"}, representing the spy's interception
 of @{text X}. If event @{text "(A, X)"} rather stands for @{text A}'s generation of private message
 @{text X}, e.g. an ephemeral private key, for her own exclusive use -- and if the spy has not hacked
 @{text A} so as to steal her private messages as well --, then no companion event @{text "(Spy, X)"}
 will occur instead.
 
   \<^descr>[States.] In the inductive method, the possible states of a cryptographic protocol are modeled as
 event \emph{traces}, i.e. lists, and the protocol itself is formalized as a set of such traces.
 Consequently, the protocol rules and security properties are expressed as formulae satisfied by any
 event trace @{text evs} belonging to this set.
 \\However, these formulae are such that their truth values depend only on the events contained in
 @{text evs}, rather than on the actual order in which they occur -- in fact, robust protocol rules
 and security properties cannot depend on the exact sequence of message exchanges in a scenario where
 the spy can freely intercept and forward messages, or even generate and send her own ones. Thus, one
 library function, @{const set}, and two custom recursive functions, @{text used} and @{text knows},
 are needed to convert event traces into event sets and message sets, respectively.
 \\In the relational method, protocol states are simply modeled as event sets, so that the occurrence
 of event @{text "(A, X)"} in state @{text s} can be expressed as the transition to the augmented
 state @{term "insert (A, X) s"}. Hence, states consist of relations between agents and messages. As
 a result, function @{const set} need not be used any longer, whereas functions @{text used} and
 @{text spied} -- the latter one being a replacement for @{text "knows Spy"} --, which take a state
 @{text s} as input, are mere abbreviations for @{term "Range s"} and @{term "s `` {Spy}"}.
 
   \<^descr>[Spy's capabilities.] In the inductive method, the spy's attack capabilities are formalized via
 two inductively defined functions, @{text analz} and @{text synth}, used to construct the sets of
 all the messages that the spy can learn -- @{text "analz (knows Spy evs)"} -- and send to legitimate
 agents -- @{text "synth (analz (knows Spy evs))"} -- downstream of event trace @{text evs}.
 \\Indeed, the introduction of these functions goes in the direction of decoupling the formalization
 of the spy's capabilities from that of the protocol itself, consistently with the fact that what the
 spy can do is independent of how the protocol works -- which only matters when it comes to verifying
 protocol security.
 \\In principle, this promises to provide a relevant benefit: these functions need to be defined, and
 their properties to be proven, just once, whereupon such definitions and properties can be reused in
 the formalization and verification of whatever protocol.
 \\In practice, since both functions are of type @{text "msg set \<Rightarrow> msg set"}, where @{text msg} is
 the datatype defining all possible message formats, this benefit only applies as long as message
 formats remain unchanged. However, when it comes to verifying a protocol making use of public key
 cryptography, some new message format, and consequently some new related spy's capability as well,
 are likely to be required. An example of this will be provided right away by the protocol considered
 in this paper.
 \\In the relational method, the representation of events as agent-message pairs offers a simpler way
 to model the spy's capabilities, namely as supplementary protocol rules, analogous to the inductive
 method's @{text Fake} rule, augmenting a state by one or more events of the form @{text "(Spy, X)"}.
 In addition to eliminating the need for functions @{text analz} and @{text synth} -- which, in light
 of the above considerations, does not significantly harm reusability --, this choice also abolishes
 any distinction between what the spy can learn and what she can send. In fact, a state containing
 event @{text "(Spy, X)"} is interpreted as one where the spy both knows message @{text X} and may
 have sent it to whatever legitimate agent. Actually, this formalizes the facts that a real-world
 attacker is free to send any message she has learned to any other party, and conversely to use any
 message she has generated to further augment her knowledge.
 \\In the inductive method, the former fact is modeled by property @{term "H \<subseteq> synth H"} of function
 @{text synth}, but the latter one has no formal counterpart, as in general @{term "H \<subset> synth H"}.
 This limitation on the spy's capabilities is not significant as long as the protocol makes use of
 static keys only, but it is if session keys or ephemeral key pairs are generated -- as happens in
 key establishment protocols, even in those using symmetric cryptography alone. In any such case, a
 realistic spy must also be able to learn from anything she herself has generated, such as a nonce or
 an ephemeral private key -- a result achieved without effort in the relational method.
 \\An additional, nontrivial problem for the inductive method is that many protocols, including key
 establishment ones, require the spy to be able to generate \emph{fresh} ephemeral messages only, as
 otherwise the spy could succeed in breaking the protocol by just guessing the ephemeral messages
 already generated at random by some legitimate agent -- a quite unrealistic attack pattern, provided
 that such messages vary in a sufficiently wide range. At first glance, this need could be addressed
 by extending the inductive definition of function @{text synth} with introduction rules of the form
 @{term "Nonce n \<notin> H \<Longrightarrow> Nonce n \<in> synth H"} or @{term "PriKey A \<notin> H \<Longrightarrow> PriKey A \<in> synth H"}.
 However, private ephemeral messages are not in general included in @{text "analz (knows Spy evs)"},
 since nonces may be encrypted with uncompromised keys when exchanged and private keys are usually
 not exchanged at all, so this approach would not work. The only satisfactory alternative would be to
 change the signature of function @{text synth}, e.g. by adding a second input message set @{text H'}
 standing for @{text "used evs"}, or else by replacing @{text H} with event trace @{text evs} itself,
 but this would render the function definition much more convoluted -- a problem easily bypassed in
 the relational method.
 
   \<^descr>[Protocol.] In the inductive method, a cryptographic protocol consists of an inductively defined
 set of event traces. This enables to prove the protocol security properties by induction using the
 induction rule automatically generated as a result of such an inductive definition, i.e. by means of
 \emph{rule induction}. Actually, this feature is exactly what gives the method its very name. Hence,
 a consistent way to name a protocol verification method using some other form of induction would be
 to replace adjective "inductive" with another one referring to that form of induction.
 \\The relational method owes its name to this consideration. In this method, the introduction rules
 defining \emph{protocol rules}, i.e. the possible transitions between protocol states, are replaced
 with \emph{relations} between states, henceforth named \emph{protocol relations}. That is, for any
 two states @{text s} and @{text s'}, there exists a transition leading from @{text s} to @{text s'}
 just in case the ordered pair @{term "(s, s')"} is contained in at least one protocol relation --
 a state of affairs denoted using infix notation @{text "s \<turnstile> s'"}. Then, the inductively defined set
 itself is replaced with the \emph{reflexive transitive closure} of the union of protocol relations.
 Namely, any state @{text s} may be reached from \emph{initial state} @{text s\<^sub>0}, viz. is a possible
 protocol state, just in case pair @{term "(s\<^sub>0, s)"} lies within this reflexive transitive closure --
 a state of affairs denoted using infix notation @{text "s\<^sub>0 \<Turnstile> s"}. As a result, rule induction is
 replaced with induction over reflexive transitive closures via rule @{thm [source] rtrancl_induct},
 which is the circumstance that originates the method name.
 \\These changes provide the following important benefits.
 
     \<^item> Inserting and modifying the formal definition of a protocol is much more comfortable. In fact,
 any change even to a single introduction rule within a monolithic inductive set definition entails a
 re-evaluation of the whole definition, whereas each protocol relation will have its own stand-alone
 definition, which also makes it easier to find errors. This advantage may go almost unnoticed for a
 very simple protocol providing for just a few protocol rules, but gets evident in case of a complex
 protocol. An example of this will be provided by the protocol considered in this paper: when looking
 at the self-contained abbreviations used to define protocol relations, the reader will easily grasp
 how much more convoluted an equivalent inductive set definition would have been.
 
     \<^item> In addition to induction via rule @{thm [source] rtrancl_induct}, a further powerful reasoning
 pattern turns out to be available. It is based on the following general rule applying to reflexive
 transitive closures (indeed, a rule so general and useful that it could rightfully become part of
 the standard library), later on proven and assigned the name @{text rtrancl_start}:
 @{prop [display] "\<lbrakk>(x, y) \<in> r\<^sup>*; P y; \<not> P x\<rbrakk> \<Longrightarrow>
 \<exists>u v. (x, u) \<in> r\<^sup>* \<and> (u, v) \<in> r \<and> (v, y) \<in> r\<^sup>* \<and> \<not> P u \<and> P v"}
 In natural language, this rule states that for any chain of elements linked by a relation, if some
 predicate is false for the first element of the chain and true for the last one, there must exist a
 link in the chain where the predicate becomes true.
 \\This rule can be used to prove propositions of the form @{text "\<lbrakk>s \<Turnstile> s'; P s'[; Q]\<rbrakk> \<Longrightarrow> R s'"} for
 any state @{text s} and predicate @{text P} such that @{term "\<not> P s"}, with an optional additional
 assumption @{text Q}, without resorting to induction. Notably, \emph{regularity lemmas} have exactly
 this form, where @{term "s = s\<^sub>0"}, @{term "P = (\<lambda>s. X \<in> parts (used s))"} for some term @{text X} of
 type @{text msg}, and @{text Q}, if present, puts some constraint on @{text X} or its components.
 \\Such a proof consists of two steps. First, lemma @{text "\<lbrakk>s \<turnstile> s'; P s'; \<not> P s[; Q]\<rbrakk> \<Longrightarrow> R s'"} is
 proven by simplification, using the definitions of protocol relations. Then, the target proposition
 is proven by applying rule @{text rtrancl_start} as a destruction rule (cf. @{cite "Paulson20"}) and
 proving @{term "P s'"} by assumption, @{term "\<not> P s"} by simplification, and the residual subgoal
 by means of the previous lemma.
 
 In addition to the relational method, this paper is aimed at introducing still another enhancement:
 besides message confidentiality and authenticity, it takes into consideration a further important
 security property, \emph{message anonymity}. Being legitimate agents identified via natural numbers,
 the fact that in state @{text s} the spy ignores that message @{text X\<^sub>n} is associated with agent
 @{text n}, viz. @{text X\<^sub>n}'s property of being \emph{anonymous} in state @{text s}, can be expressed
 as @{text "\<langle>n, X\<^sub>n\<rangle> \<notin> spied s"}, where notation @{text "\<langle>n, X\<^sub>n\<rangle>"} refers to a new constructor added to
 datatype @{text msg} precisely for this purpose.
 
 A basic constraint upon any protocol relation augmenting the spy's knowledge with @{text "\<langle>n, X\<rangle>"}
 is that the spy must know message @{text X} in the current state, as it is impossible to identify
 the agent associated with an unknown message. There is also an additional, more subtle constraint.
 Any such protocol relation either augments a state in which the spy knows @{text "\<langle>n, C X\<^sub>1 \<dots> X\<^sub>m\<rangle>"},
 i.e. containing event @{text "(Spy, \<langle>n, C X\<^sub>1 \<dots> X\<^sub>m\<rangle>)"}, with event @{text "(Spy, \<langle>n, X\<^sub>i\<rangle>)"}, where
 $1 \leq i \leq m$ and @{text C} is some constructor of datatype @{text msg}, or conversely augments
 a state containing event @{text "(Spy, \<langle>n, X\<^sub>i\<rangle>)"} with @{text "(Spy, \<langle>n, C X\<^sub>1 \<dots> X\<^sub>m\<rangle>)"}. However, the
 latter spy's inference is justified only if the compound message @{text "C X\<^sub>1 \<dots> X\<^sub>m"} is part of a
 message generated or accepted by some legitimate agent according to the protocol rules. Otherwise,
 that is, if @{text "C X\<^sub>1 \<dots> X\<^sub>m"} were just a message generated at random by the spy, her inference
 would be as sound as those of most politicians and all advertisements: even if the conclusion were
 true, it would be so by pure chance.
 
 This problem can be solved as follows.
 
   \<^item> A further constructor @{text Log}, taking a message as input, is added to datatype @{text msg},
 and every protocol relation modeling the generation or acceptance of a message @{text X} by some
 legitimate agent must augment the current state with event @{term "(Spy, Log X)"}.
 \\In this way, the set of all the messages that have been generated or accepted by some legitimate
 agent in state @{text s} matches @{term "Log -` spied s"}.
 
   \<^item> A function @{text crypts} is defined inductively. It takes a message set @{text H} as input, and
 returns the least message set @{text H'} such that @{term "H \<subseteq> H'"} and for any (even empty) list
 of keys @{text KS}, if the encryption of @{text "\<lbrace>X, Y\<rbrace>"}, @{text "\<lbrace>Y, X\<rbrace>"}, or @{text "Hash X"}
 with @{text KS} is contained in @{text H'}, then the encryption of @{text X} with @{text KS} is
 contained in @{text H'} as well. 
 \\In this way, the set of all the messages that are part of messages exchanged by legitimate agents,
 viz. that may be mapped to agents, in state @{text s} matches @{term "crypts (Log -` spied s)"}.
 
   \<^item> Another function @{text key_sets} is defined, too. It takes two inputs, a message @{text X} and
 a message set @{text H}, and returns the set of the sets of @{text KS}' inverse keys for any list of
 keys @{text KS} such that the encryption of @{text X} with @{text KS} is included in @{text H}.
 \\In this way, the fact that in state @{text s} the spy can map a compound message @{text X} to some
 agent, provided that she knows all the keys in set @{text U}, can be expressed through conditions
 @{term "U \<in> key_sets X (crypts (Log -` spied s))"} and @{term "U \<subseteq> spied s"}.
 \\The choice to define @{text key_sets} so as to collect the inverse keys of encryption keys, viz.
 decryption ones, depends on the fact that the sample protocol verified in this paper uses symmetric
 keys alone -- which match their own inverse keys -- for encryption, whereas asymmetric key pairs are
 used in cryptograms only for signature generation -- so that the inverse keys are public ones. In
 case of a protocol (also) using public keys for encryption, encryption keys themselves should (also)
 be collected, since the corresponding decryption keys, i.e. private keys, would be unknown to the
 spy by default. This would formalize the fact that encrypted messages can be mapped to agents not
 only by decrypting them, but also by recomputing the cryptograms (provided that the plaintexts are
 known) and checking whether they match the exchanged ones.
 \<close>
 
 
 subsection "A sample protocol"
 
 text \<open>
 As previously mentioned, this paper tries the relational method, including message anonymity, by
 applying it to the verification of a sample authentication protocol in which Password Authenticated
 Connection Establishment (PACE) with Chip Authentication Mapping (cf. @{cite "ICAO15"}) is first
 used by an \emph{owner} to establish a secure channel with her own \emph{asset} and authenticate it,
 and then the owner sends a password (other than the PACE one) to the asset over that channel so as
 to authenticate herself. This enables to achieve a reliable mutual authentication even if the PACE
 key is shared by multiple owners or is weak, as happens in electronic passports. Although the PACE
 mechanism is specified for use in electronic documents, nothing prevents it in principle from being
 used in other kinds of smart cards or even outside of the smart card world, which is the reason why
 this paper uses the generic names \emph{asset} and \emph{owner} for the card and the cardholder,
 respectively.
 
 In more detail, this protocol provides for the following steps. In this list, messages are specified
 using the same syntax that will be adopted in the formal text (for further information about PACE
 with Chip Authentication Mapping, cf. @{cite "ICAO15"}).
 
   \<^enum> \emph{Asset n} $\rightarrow$ \emph{Owner n}:
 \\\hspace*{1em}@{text "Crypt (Auth_ShaKey n) (PriKey S)"}
 
   \<^enum> \emph{Owner n} $\rightarrow$ \emph{Asset n}:
 \\\hspace*{1em}@{text "\<lbrace>Num 1, PubKey A\<rbrace>"}
 
   \<^enum> \emph{Asset n} $\rightarrow$ \emph{Owner n}:
 \\\hspace*{1em}@{text "\<lbrace>Num 2, PubKey B\<rbrace>"}
 
   \<^enum> \emph{Owner n} $\rightarrow$ \emph{Asset n}:
 \\\hspace*{1em}@{text "\<lbrace>Num 3, PubKey C\<rbrace>"}
 
   \<^enum> \emph{Asset n} $\rightarrow$ \emph{Owner n}:
 \\\hspace*{1em}@{text "\<lbrace>Num 4, PubKey D\<rbrace>"}
 
   \<^enum> \emph{Owner n} $\rightarrow$ \emph{Asset n}:
 \\\hspace*{1em}@{text "Crypt (SesK SK) (PubKey D)"}
 
   \<^enum> \emph{Asset n} $\rightarrow$ \emph{Owner n}:
 \\\hspace*{1em}@{text "\<lbrace>Crypt (SesK SK) (PubKey C),"}
 \\\hspace*{1.5em}@{text "Crypt (SesK SK) (Auth_PriK n \<otimes> B),"}
 \\\hspace*{1.5em}@{text "Crypt (SesK SK) (Crypt SigK"}
 \\\hspace*{2em}@{text "\<lbrace>Hash (Agent n), Hash (Auth_PubKey n)\<rbrace>)\<rbrace>"}
 
   \<^enum> \emph{Owner n} $\rightarrow$ \emph{Asset n}:
 \\\hspace*{1em}@{text "Crypt (SesK SK) (Pwd n)"}
 
   \<^enum> \emph{Asset n} $\rightarrow$ \emph{Owner n}:
 \\\hspace*{1em}@{text "Crypt (SesK SK) (Num 0)"}
 
 Legitimate agents consist of an infinite population of assets and owners. For each natural number
 @{text n}, @{text "Owner n"} is an owner and @{text "Asset n"} is her own asset, and these agents
 are assigned the following authentication data.
 
   \<^item> @{text "Key (Auth_ShaKey n)"}: static symmetric PACE key shared by both agents.
 
   \<^item> @{text "Auth_PriKey n"}, @{text "Auth_PubKey n"}: static private and public keys stored on
 @{text "Asset n"} and used for @{text "Asset n"}'s authentication via Chip Authentication Mapping.
 
   \<^item> @{text "Pwd n"}: unique password (other than the PACE one) shared by both agents and used for
 @{text "Owner n"}'s authentication.
 
 Function @{text Pwd} is defined as a constructor of datatype @{text msg} and then is injective,
 which formalizes the assumption that each asset-owner pair has a distinct password, whereas no such
 constraint is put on functions @{text Auth_ShaKey}, @{text Auth_PriKey}, and @{text Auth_PubKey},
 which allows multiple asset-owner pairs to be assigned the same keys. On the other hand, function
 @{text Auth_PriKey} is constrained to be such that the complement of its range is infinite. As each
 protocol run requires the generation of fresh ephemeral private keys, this constraint ensures that
 an unbounded number of protocol runs can be carried out. All assumptions are formalized by applying
 the definitional approach, viz. without introducing any axiom, and so is this constraint, expressed
 by defining function @{text Auth_PriKey} using the indefinite description operator @{text SOME}.
 
 The protocol starts with @{text "Asset n"} sending an ephemeral private key encrypted with the PACE
 key to @{text "Owner n"}. Actually, if @{text "Asset n"} is a smart card, the protocol should rather
 start with @{text "Owner n"} sending a plain request for such encrypted nonce, but this preliminary
 step is omitted here as it is irrelevant for protocol security. After that, @{text "Owner n"} and
 @{text "Asset n"} generate two ephemeral key pairs each and send the respective public keys to the
 other party.
 
 Then, both parties agree on the same session key by deriving it from the ephemeral keys generated
 previously (actually, two distinct session keys would be derived, one for encryption and the other
 one for MAC computation, but such a level of detail is unnecessary for protocol verification). The
 session key is modeled as @{text "Key (SesK SK)"}, where @{text SesK} is an apposite constructor
 added to datatype @{text key} and @{term "SK = (Some S, {A, B}, {C, D})"}. The adoption of type
 @{typ "nat option"} for the first component enables to represent as @{term "(None, {A, B}, {C, D})"}
 the wrong session key derived from @{text "Owner n"} if @{text "PriKey S"} was encrypted using a key
 other than @{text "Key (Auth_ShaKey n)"} -- which reflects the fact that the protocol goes on even
 without the two parties sharing the same session key. The use of type @{typ "nat set"} for the other
 two components enables the spy to compute @{text "Key (SesK SK)"} if she knows \emph{either} private
 key and the other public key referenced by each set, as long as she also knows @{text "PriKey S"} --
 which reflects the fact that given two key pairs, Diffie-Hellman key agreement generates the same
 shared secret independently of which of the respective private keys is used for computation.
 
 This session key is used by both parties to compute their authentication tokens. Both encrypt the
 other party's second ephemeral public key, but @{text "Asset n"} appends two further fields: the
 Encrypted Chip Authentication Data, as provided for by Chip Authentication Mapping, and an encrypted
 signature of the hash values of @{text "Agent n"} and @{text "Auth_PubKey n"}. Infix notation
 @{text "Auth_PriK n \<otimes> B"} refers to a constructor of datatype @{text msg} standing for plain Chip
 Authentication Data, and @{text Agent} is another such constructor standing for agent identification
 data. @{text "Owner n"} is expected to validate this signature by also checking @{text "Agent n"}'s
 hash value against reference identification data known by other means -- otherwise, the spy would
 not be forced to know @{text "Auth_PriKey n"} to masquerade as @{text "Asset n"}, since she could do
 that by just knowing @{text "Auth_PriKey m"} for some other @{text m}, even if @{term "Auth_PriKey m
 \<noteq> Auth_PriKey n"}. If @{text "Asset n"} is an electronic passport, the owner, i.e. the inspection
 system, could get cardholder's identification data by reading her personal data on the booklet, and
 such a signature could be retrieved from the chip (actually through a distinct message, but this is
 irrelevant for protocol security as long as the password is sent after the signature's validation)
 by reading the Document Security Object -- provided that @{text "Auth_PubKey n"} is included within
 Data Group 14.
 
 The protocol ends with @{text "Owner n"} sending her password, encrypted with the session key, to
 @{text "Asset n"}, who validates it and replies with an encrypted acknowledgment.
 
 Here below are some concluding remarks about the way how this sample protocol is formalized.
 
   \<^item> A single signature private key, unknown to the spy, is assumed to be used for all legitimate
 agents. Similarly, the spy might have hacked some legitimate agent so as to steal her ephemeral
 private keys as soon as they are generated, but here all legitimate agents are assumed to be out of
 the spy's reach in this respect. Of course, this is just the choice of one of multiple possible
 scenarios, and nothing prevents these assumptions from being dropped.
 
   \<^item> In the real world, a legitimate agent would use any one of her ephemeral private keys just once,
 after which the key would be destroyed. On the contrary, no such constraint is enforced here, since
 it turns out to be unnecessary for protocol verification. There is a single exception, required for
 the proof of a unicity lemma: after @{text "Asset n"} has used @{text "PriKey B"} to compute her
 authentication token, she must discard @{text "PriKey B"} so as not to use this key any longer. The
 way how this requirement is expressed emphasizes once more the flexibility of the modeling of events
 in the relational method: @{text "Asset n"} may use @{text "PriKey B"} in this computation only if
 event @{text "(Asset n, PubKey B)"} is not yet contained in the current state @{text s}, and then
 @{text s} is augmented with that event. Namely, events can also be used to model garbage collection!
 
   \<^item> The sets of the legitimate agents whose authentication data have been identified in advance (or
 equivalently, by means other than attacking the protocol, e.g. by social engineering) by the spy are
 defined consistently with the constraint that known data alone can be mapped to agents, as well as
 with the definition of initial state @{text s\<^sub>0}. For instance, the set @{text bad_id_prikey} of the
 agents whose Chip Authentication private keys have been identified is defined as a subset of the set
 @{text bad_prikey} of the agents whose Chip Authentication private keys have been stolen. Moreover,
 all the signatures included in assets' authentication tokens are assumed to be already known to the
 spy in state @{text s\<^sub>0}, so that @{text bad_id_prikey} includes also any agent whose identification
 data or Chip Authentication public key have been identified in advance.
 
   \<^item> The protocol rules augmenting the spy's knowledge with some message of the form @{text "\<langle>n, X\<rangle>"}
 generally require the spy to already know some other message of the same form. There is just one
 exception: the spy can infer @{text "\<langle>n, Agent n\<rangle>"} from @{text "Agent n"}. This expresses the fact
 that the detection of identification data within a message generated or accepted by some legitimate
 agent is in itself sufficient to map any known component of that message to the identified agent,
 regardless of whether any data were already mapped to that agent in advance.
 
   \<^item> As opposed to what happens for constructors @{text "(\<otimes>)"} and @{text "MPair"}, there do not
 exist two protocol rules enabling the spy to infer @{text "\<langle>n, Crypt K X\<rangle>"} from @{text "\<langle>n, X\<rangle>"} or
 @{text "\<langle>n, Key K\<rangle>"} and vice versa. A single protocol rule is rather defined, which enables the spy
 to infer @{text "\<langle>n, X\<rangle>"} from @{text "\<langle>n, Key K\<rangle>"} or vice versa, provided that @{text "Crypt K X"}
 has been exchanged by some legitimate agent. In fact, the protocol provides for just one compound
 message made up of cryptograms, i.e. the asset's authentication token, and all these cryptograms are
 generated using the same encryption key @{text "Key (SesK SK)"}. Thus, if two such cryptograms have
 plaintexts @{text X\<^sub>1}, @{text X\<^sub>2} and the spy knows @{text "\<langle>n, X\<^sub>1\<rangle>"}, she can infer @{text "\<langle>n, X\<^sub>2\<rangle>"}
 by inferring @{text "\<langle>n, Key (SesK SK)\<rangle>"}, viz. she need not know @{text "\<langle>n, Crypt (SesK SK) X\<^sub>1\<rangle>"}
 to do that.
 
 The formal content is split into the following sections.
 
   \<^item> Section \ref{Definitions}, \emph{Definitions}, contains all the definitions needed to formalize
 the sample protocol by means of the relational method, including message anonymity.
 
   \<^item> Section \ref{Authentication}, \emph{Confidentiality and authenticity properties}, proves that
 the following theorems hold under appropriate assumptions.
 
     \<^enum> Theorem @{text sigkey_secret}: the signature private key is secret.
 
     \<^enum> Theorem @{text auth_shakey_secret}: an asset-owner pair's PACE key is secret.
 
     \<^enum> Theorem @{text auth_prikey_secret}: an asset's Chip Authentication private key is secret.
 
     \<^enum> Theorem @{text owner_seskey_unique}: an owner's session key is unknown to other owners.
 
     \<^enum> Theorem @{text owner_seskey_secret}: an owner's session key is secret.
 
     \<^enum> Theorem @{text owner_num_genuine}: the encrypted acknowledgment received by an owner has been
 sent by the respective asset.
 
     \<^enum> Theorem @{text owner_token_genuine}: the PACE authentication token received by an owner has
 been generated by the respective asset, using her Chip Authentication private key and the same
 ephemeral keys used to derive the session key.
 
     \<^enum> Theorem @{text pwd_secret}: an asset-owner pair's password is secret.
 
     \<^enum> Theorem @{text asset_seskey_unique}: an asset's session key is unknown to other assets, and
 may be used by that asset to compute just one PACE authentication token.
 
     \<^enum> Theorem @{text asset_seskey_secret}: an asset's session key is secret.
 
     \<^enum> Theorem @{text asset_pwd_genuine}: the encrypted password received by an asset has been sent
 by the respective owner.
 
     \<^enum> Theorem @{text asset_token_genuine}: the PACE authentication token received by an asset has
 been generated by the respective owner, using the same ephemeral key used to derive the session key.
 
   Particularly, these proofs confirm that the mutual authentication between an owner and her asset
 is reliable even if their PACE key is compromised, unless either their Chip Authentication private
 key or their password also is -- namely, the protocol succeeds in implementing a two-factor mutual
 authentication.
 
   \<^item> Section \ref{Anonymity}, \emph{Anonymity properties}, proves that the following theorems hold
 under appropriate assumptions.
 
     \<^enum> Theorem @{text pwd_anonymous}: an asset-owner pair's password is anonymous.
 
     \<^enum> Theorem @{text auth_prikey_anonymous}: an asset's Chip Authentication private key is
 anonymous.
 
     \<^enum> Theorem @{text auth_shakey_anonymous}: an asset-owner pair's PACE key is anonymous.
 
   \<^item> Section \ref{Possibility}, \emph{Possibility properties}, shows how possibility properties (cf.
 @{cite "Paulson98"}) can be proven by constructing sample protocol runs, either ordinary or attack
 ones. Two such properties are proven:
 
     \<^enum> Theorem @{text runs_unbounded}: for any possible protocol state @{text s} and any asset-owner
 pair, there exists a state @{text s'} reachable from @{text s} in which a protocol run has been
 completed by those agents using an ephemeral private key @{text "PriKey S"} not yet exchanged in
 @{text s} -- namely, an unbounded number of protocol runs can be carried out by legitimate agents.
 
     \<^enum> Theorem @{text pwd_compromised}: in a scenario not satisfying the assumptions of theorem
 @{text pwd_anonymous}, the spy can steal an asset-owner pair's password and even identify those
 agents.
 
   The latter is an example of a possibility property aimed at confirming that the assumptions of a
 given confidentiality, authenticity, or anonymity property are necessary for it to hold.
 
 For further information about the formal definitions and proofs contained in these sections, see
 Isabelle documentation, particularly @{cite "Paulson20"}, @{cite "Nipkow20"}, @{cite "Krauss20"},
 and @{cite "Nipkow11"}.
 
 \textbf{Important note.} This sample protocol was already considered in a former paper of mine (cf.
 @{cite "Noce17"}). For any purpose, that paper should be regarded as being obsolete and superseded
 by the present paper.
 \<close>
 
 
 subsection "Definitions"
 
 text \<open>
 \label{Definitions}
 \<close>
 
 type_synonym agent_id = nat
 
 type_synonym key_id = nat
 
 type_synonym seskey_in = "key_id option \<times> key_id set \<times> key_id set"
 
 datatype agent =
   Asset agent_id |
   Owner agent_id |
   Spy
 
 datatype key =
   SigK |
   VerK |
   PriK key_id |
   PubK key_id |
   ShaK key_id |
   SesK seskey_in
 
 datatype msg =
   Num nat |
   Agent agent_id |
   Pwd agent_id |
   Key key |
   Mult key_id key_id (infixl "\<otimes>" 70) |
   Hash msg |
   Crypt key msg |
   MPair msg msg |
   IDInfo agent_id msg |
   Log msg
 
 syntax
   "_MPair"  :: "['a, args] \<Rightarrow> 'a * 'b"  ("(2\<lbrace>_,/ _\<rbrace>)")
   "_IDInfo" :: "[agent_id, msg] \<Rightarrow> msg"      ("(2\<langle>_,/ _\<rangle>)")
 translations
   "\<lbrace>X, Y, Z\<rbrace>" \<rightleftharpoons> "\<lbrace>X, \<lbrace>Y, Z\<rbrace>\<rbrace>"
   "\<lbrace>X, Y\<rbrace>" \<rightleftharpoons> "CONST MPair X Y"
   "\<langle>n, X\<rangle>" \<rightleftharpoons> "CONST IDInfo n X"
 
 
 abbreviation SigKey :: "msg" where
 "SigKey \<equiv> Key SigK"
 
 abbreviation VerKey :: "msg" where
 "VerKey \<equiv> Key VerK"
 
 abbreviation PriKey :: "key_id \<Rightarrow> msg" where
 "PriKey \<equiv> Key \<circ> PriK"
 
 abbreviation PubKey :: "key_id \<Rightarrow> msg" where
 "PubKey \<equiv> Key \<circ> PubK"
 
 abbreviation ShaKey :: "key_id \<Rightarrow> msg" where
 "ShaKey \<equiv> Key \<circ> ShaK"
 
 abbreviation SesKey :: "seskey_in \<Rightarrow> msg" where
 "SesKey \<equiv> Key \<circ> SesK"
 
 primrec InvK :: "key \<Rightarrow> key" where
 "InvK SigK = VerK" |
 "InvK VerK = SigK" |
 "InvK (PriK A) = PubK A" |
 "InvK (PubK A) = PriK A" |
 "InvK (ShaK SK) = ShaK SK" |
 "InvK (SesK SK) = SesK SK"
 
 abbreviation InvKey :: "key \<Rightarrow> msg" where
 "InvKey \<equiv> Key \<circ> InvK"
 
 
 inductive_set parts :: "msg set \<Rightarrow> msg set"
   for H :: "msg set" where
 
 parts_used [intro]:
   "X \<in> H \<Longrightarrow> X \<in> parts H" |
 
 parts_crypt [intro]:
   "Crypt K X \<in> parts H \<Longrightarrow> X \<in> parts H" |
 
 parts_fst [intro]:
   "\<lbrace>X, Y\<rbrace> \<in> parts H \<Longrightarrow> X \<in> parts H" |
 
 parts_snd [intro]:
   "\<lbrace>X, Y\<rbrace> \<in> parts H \<Longrightarrow> Y \<in> parts H"
 
 
 inductive_set crypts :: "msg set \<Rightarrow> msg set"
   for H :: "msg set" where
 
 crypts_used [intro]:
   "X \<in> H \<Longrightarrow> X \<in> crypts H" |
 
 crypts_hash [intro]:
   "foldr Crypt KS (Hash X) \<in> crypts H \<Longrightarrow> foldr Crypt KS X \<in> crypts H" |
 
 crypts_fst [intro]:
   "foldr Crypt KS \<lbrace>X, Y\<rbrace> \<in> crypts H \<Longrightarrow> foldr Crypt KS X \<in> crypts H" |
 
 crypts_snd [intro]:
   "foldr Crypt KS \<lbrace>X, Y\<rbrace> \<in> crypts H \<Longrightarrow> foldr Crypt KS Y \<in> crypts H"
 
 
 definition key_sets :: "msg \<Rightarrow> msg set \<Rightarrow> msg set set" where
 "key_sets X H \<equiv> {InvKey ` set KS | KS. foldr Crypt KS X \<in> H}"
 
 definition parts_msg :: "msg \<Rightarrow> msg set" where
 "parts_msg X \<equiv> parts {X}"
 
 definition crypts_msg :: "msg \<Rightarrow> msg set" where
 "crypts_msg X \<equiv> crypts {X}"
 
 definition key_sets_msg :: "msg \<Rightarrow> msg \<Rightarrow> msg set set" where
 "key_sets_msg X Y \<equiv> key_sets X {Y}"
 
 fun seskey_set :: "seskey_in \<Rightarrow> key_id set" where
 "seskey_set (Some S, U, V) = insert S (U \<union> V)" |
 "seskey_set (None, U, V) = U \<union> V"
 
 
 definition Auth_PriK :: "agent_id \<Rightarrow> key_id" where
 "Auth_PriK \<equiv> SOME f. infinite (- range f)"
 
 abbreviation Auth_PriKey :: "agent_id \<Rightarrow> msg" where
 "Auth_PriKey \<equiv> PriKey \<circ> Auth_PriK"
 
 abbreviation Auth_PubKey :: "agent_id \<Rightarrow> msg" where
 "Auth_PubKey \<equiv> PubKey \<circ> Auth_PriK"
 
 consts Auth_ShaK :: "agent_id \<Rightarrow> key_id"
 
 abbreviation Auth_ShaKey :: "agent_id \<Rightarrow> key" where
 "Auth_ShaKey \<equiv> ShaK \<circ> Auth_ShaK"
 
 abbreviation Sign :: "agent_id \<Rightarrow> key_id \<Rightarrow> msg" where
 "Sign n A \<equiv> Crypt SigK \<lbrace>Hash (Agent n), Hash (PubKey A)\<rbrace>"
 
 abbreviation Token :: "agent_id \<Rightarrow> key_id \<Rightarrow> key_id \<Rightarrow> key_id \<Rightarrow> seskey_in \<Rightarrow> msg"
 where "Token n A B C SK \<equiv> \<lbrace>Crypt (SesK SK) (PubKey C),
   Crypt (SesK SK) (A \<otimes> B), Crypt (SesK SK) (Sign n A)\<rbrace>"
 
 
 consts bad_agent :: "agent_id set"
 
 consts bad_pwd :: "agent_id set"
 
 consts bad_shak :: "key_id set"
 
 consts bad_id_pwd :: "agent_id set"
 
 consts bad_id_prik :: "agent_id set"
 
 consts bad_id_pubk :: "agent_id set"
 
 consts bad_id_shak :: "agent_id set"
 
 definition bad_prik :: "key_id set" where
 "bad_prik \<equiv> SOME U. U \<subseteq> range Auth_PriK"
 
 abbreviation bad_prikey :: "agent_id set" where
 "bad_prikey \<equiv> Auth_PriK -` bad_prik"
 
 abbreviation bad_shakey :: "agent_id set" where
 "bad_shakey \<equiv> Auth_ShaK -` bad_shak"
 
 abbreviation bad_id_password :: "agent_id set" where
 "bad_id_password \<equiv> bad_id_pwd \<inter> bad_pwd"
 
 abbreviation bad_id_prikey :: "agent_id set" where
 "bad_id_prikey \<equiv> (bad_agent \<union> bad_id_pubk \<union> bad_id_prik) \<inter> bad_prikey"
 
 abbreviation bad_id_pubkey :: "agent_id set" where
 "bad_id_pubkey \<equiv> bad_agent \<union> bad_id_pubk \<union> bad_id_prik \<inter> bad_prikey"
 
 abbreviation bad_id_shakey :: "agent_id set" where
 "bad_id_shakey \<equiv> bad_id_shak \<inter> bad_shakey"
 
 
 type_synonym event = "agent \<times> msg"
 
 type_synonym state = "event set"
 
 abbreviation used :: "state \<Rightarrow> msg set" where
 "used s \<equiv> Range s"
 
 abbreviation spied :: "state \<Rightarrow> msg set" where
 "spied s \<equiv> s `` {Spy}"
 
 abbreviation s\<^sub>0 :: state where
 "s\<^sub>0 \<equiv> range (\<lambda>n. (Asset n, Auth_PriKey n)) \<union> {Spy} \<times> insert VerKey
   (range Num \<union> range Auth_PubKey \<union> range (\<lambda>n. Sign n (Auth_PriK n)) \<union>
    Agent ` bad_agent \<union> Pwd ` bad_pwd \<union> PriKey ` bad_prik \<union> ShaKey ` bad_shak \<union>
    (\<lambda>n. \<langle>n, Pwd n\<rangle>) ` bad_id_password \<union>
    (\<lambda>n. \<langle>n, Auth_PriKey n\<rangle>) ` bad_id_prikey \<union>
    (\<lambda>n. \<langle>n, Auth_PubKey n\<rangle>) ` bad_id_pubkey \<union>
    (\<lambda>n. \<langle>n, Key (Auth_ShaKey n)\<rangle>) ` bad_id_shakey)"
 
 
 abbreviation rel_asset_i :: "(state \<times> state) set" where
 "rel_asset_i \<equiv> {(s, s') | s s' n S.
   s' = insert (Asset n, PriKey S) s \<union>
     {Asset n, Spy} \<times> {Crypt (Auth_ShaKey n) (PriKey S)} \<union>
     {(Spy, Log (Crypt (Auth_ShaKey n) (PriKey S)))} \<and>
   PriKey S \<notin> used s}"
 
 abbreviation rel_owner_ii :: "(state \<times> state) set" where
 "rel_owner_ii \<equiv> {(s, s') | s s' n S A K.
   s' = insert (Owner n, PriKey A) s \<union>
     {Owner n, Spy} \<times> {\<lbrace>Num 1, PubKey A\<rbrace>} \<union>
     {Spy} \<times> Log ` {Crypt K (PriKey S), \<lbrace>Num 1, PubKey A\<rbrace>} \<and>
   Crypt K (PriKey S) \<in> used s \<and>
   PriKey A \<notin> used s}"
 
 abbreviation rel_asset_ii :: "(state \<times> state) set" where
 "rel_asset_ii \<equiv> {(s, s') | s s' n A B.
   s' = insert (Asset n, PriKey B) s \<union>
     {Asset n, Spy} \<times> {\<lbrace>Num 2, PubKey B\<rbrace>} \<union>
     {Spy} \<times> Log ` {\<lbrace>Num 1, PubKey A\<rbrace>, \<lbrace>Num 2, PubKey B\<rbrace>} \<and>
   \<lbrace>Num 1, PubKey A\<rbrace> \<in> used s \<and>
   PriKey B \<notin> used s}"
 
 abbreviation rel_owner_iii :: "(state \<times> state) set" where
 "rel_owner_iii \<equiv> {(s, s') | s s' n B C.
   s' = insert (Owner n, PriKey C) s \<union>
     {Owner n, Spy} \<times> {\<lbrace>Num 3, PubKey C\<rbrace>} \<union>
     {Spy} \<times> Log ` {\<lbrace>Num 2, PubKey B\<rbrace>, \<lbrace>Num 3, PubKey C\<rbrace>} \<and>
   \<lbrace>Num 2, PubKey B\<rbrace> \<in> used s \<and>
   PriKey C \<notin> used s}"
 
 abbreviation rel_asset_iii :: "(state \<times> state) set" where
 "rel_asset_iii \<equiv> {(s, s') | s s' n C D.
   s' = insert (Asset n, PriKey D) s \<union>
     {Asset n, Spy} \<times> {\<lbrace>Num 4, PubKey D\<rbrace>} \<union>
     {Spy} \<times> Log ` {\<lbrace>Num 3, PubKey C\<rbrace>, \<lbrace>Num 4, PubKey D\<rbrace>} \<and>
   \<lbrace>Num 3, PubKey C\<rbrace> \<in> used s \<and>
   PriKey D \<notin> used s}"
 
 abbreviation rel_owner_iv :: "(state \<times> state) set" where
 "rel_owner_iv \<equiv> {(s, s') | s s' n S A B C D K SK.
   s' = insert (Owner n, SesKey SK) s \<union>
     {Owner n, Spy} \<times> {Crypt (SesK SK) (PubKey D)} \<union>
     {Spy} \<times> Log ` {\<lbrace>Num 4, PubKey D\<rbrace>, Crypt (SesK SK) (PubKey D)} \<and>
   {Crypt K (PriKey S), \<lbrace>Num 2, PubKey B\<rbrace>, \<lbrace>Num 4, PubKey D\<rbrace>} \<subseteq> used s \<and>
   {Owner n} \<times> {\<lbrace>Num 1, PubKey A\<rbrace>, \<lbrace>Num 3, PubKey C\<rbrace>} \<subseteq> s \<and>
   SK = (if K = Auth_ShaKey n then Some S else None, {A, B}, {C, D})}"
 
 abbreviation rel_asset_iv :: "(state \<times> state) set" where
 "rel_asset_iv \<equiv> {(s, s') | s s' n S A B C D SK.
   s' = s \<union> {Asset n} \<times> {SesKey SK, PubKey B} \<union>
     {Asset n, Spy} \<times> {Token n (Auth_PriK n) B C SK} \<union>
     {Spy} \<times> Log ` {Crypt (SesK SK) (PubKey D),
       Token n (Auth_PriK n) B C SK} \<and>
   {Asset n} \<times> {Crypt (Auth_ShaKey n) (PriKey S),
     \<lbrace>Num 2, PubKey B\<rbrace>, \<lbrace>Num 4, PubKey D\<rbrace>} \<subseteq> s \<and>
   {\<lbrace>Num 1, PubKey A\<rbrace>, \<lbrace>Num 3, PubKey C\<rbrace>,
     Crypt (SesK SK) (PubKey D)} \<subseteq> used s \<and>
   (Asset n, PubKey B) \<notin> s \<and>
   SK = (Some S, {A, B}, {C, D})}"
 
 abbreviation rel_owner_v :: "(state \<times> state) set" where
 "rel_owner_v \<equiv> {(s, s') | s s' n A B C SK.
   s' = s \<union> {Owner n, Spy} \<times> {Crypt (SesK SK) (Pwd n)} \<union>
     {Spy} \<times> Log ` {Token n A B C SK, Crypt (SesK SK) (Pwd n)} \<and>
   Token n A B C SK \<in> used s \<and>
   (Owner n, SesKey SK) \<in> s \<and>
   B \<in> fst (snd SK)}"
 
 abbreviation rel_asset_v :: "(state \<times> state) set" where
 "rel_asset_v \<equiv> {(s, s') | s s' n SK.
   s' = s \<union> {Asset n, Spy} \<times> {Crypt (SesK SK) (Num 0)} \<union>
     {Spy} \<times> Log ` {Crypt (SesK SK) (Pwd n), Crypt (SesK SK) (Num 0)} \<and>
   (Asset n, SesKey SK) \<in> s \<and>
   Crypt (SesK SK) (Pwd n) \<in> used s}"
 
 
 abbreviation rel_prik :: "(state \<times> state) set" where
 "rel_prik \<equiv> {(s, s') | s s' A.
   s' = insert (Spy, PriKey A) s \<and>
   PriKey A \<notin> used s}"
 
 abbreviation rel_pubk :: "(state \<times> state) set" where
 "rel_pubk \<equiv> {(s, s') | s s' A.
   s' = insert (Spy, PubKey A) s \<and>
   PriKey A \<in> spied s}"
 
 abbreviation rel_sesk :: "(state \<times> state) set" where
 "rel_sesk \<equiv> {(s, s') | s s' A B C D S.
   s' = insert (Spy, SesKey (Some S, {A, B}, {C, D})) s \<and>
   {PriKey S, PriKey A, PubKey B, PriKey C, PubKey D} \<subseteq> spied s}"
 
 abbreviation rel_fact :: "(state \<times> state) set" where
 "rel_fact \<equiv> {(s, s') | s s' A B.
   s' = s \<union> {Spy} \<times> {PriKey A, PriKey B} \<and>
   A \<otimes> B \<in> spied s \<and>
   (PriKey A \<in> spied s \<or> PriKey B \<in> spied s)}"
 
 abbreviation rel_mult :: "(state \<times> state) set" where
 "rel_mult \<equiv> {(s, s') | s s' A B.
   s' = insert (Spy, A \<otimes> B) s \<and>
   {PriKey A, PriKey B} \<subseteq> spied s}"
 
 abbreviation rel_hash :: "(state \<times> state) set" where
 "rel_hash \<equiv> {(s, s') | s s' X.
   s' = insert (Spy, Hash X) s \<and>
   X \<in> spied s}"
 
 abbreviation rel_dec :: "(state \<times> state) set" where
 "rel_dec \<equiv> {(s, s') | s s' K X.
   s' = insert (Spy, X) s \<and>
   {Crypt K X, InvKey K} \<subseteq> spied s}"
 
 abbreviation rel_enc :: "(state \<times> state) set" where
 "rel_enc \<equiv> {(s, s') | s s' K X.
   s' = insert (Spy, Crypt K X) s \<and>
   {X, Key K} \<subseteq> spied s}"
 
 abbreviation rel_sep :: "(state \<times> state) set" where
 "rel_sep \<equiv> {(s, s') | s s' X Y.
   s' = s \<union> {Spy} \<times> {X, Y} \<and>
   \<lbrace>X, Y\<rbrace> \<in> spied s}"
 
 abbreviation rel_con :: "(state \<times> state) set" where
 "rel_con \<equiv> {(s, s') | s s' X Y.
   s' = insert (Spy, \<lbrace>X, Y\<rbrace>) s \<and>
   {X, Y} \<subseteq> spied s}"
 
 
 abbreviation rel_id_agent :: "(state \<times> state) set" where
 "rel_id_agent \<equiv> {(s, s') | s s' n.
   s' = insert (Spy, \<langle>n, Agent n\<rangle>) s \<and>
   Agent n \<in> spied s}"
 
 abbreviation rel_id_invk :: "(state \<times> state) set" where
 "rel_id_invk \<equiv> {(s, s') | s s' n K.
   s' = insert (Spy, \<langle>n, InvKey K\<rangle>) s \<and>
   {InvKey K, \<langle>n, Key K\<rangle>} \<subseteq> spied s}"
 
 abbreviation rel_id_sesk :: "(state \<times> state) set" where
 "rel_id_sesk \<equiv> {(s, s') | s s' n A SK X U.
   s' = s \<union> {Spy} \<times> {\<langle>n, PubKey A\<rangle>, \<langle>n, SesKey SK\<rangle>} \<and>
   {PubKey A, SesKey SK} \<subseteq> spied s \<and>
   (\<langle>n, PubKey A\<rangle> \<in> spied s \<or> \<langle>n, SesKey SK\<rangle> \<in> spied s) \<and>
   A \<in> seskey_set SK \<and>
   SesKey SK \<in> U \<and>
   U \<in> key_sets X (crypts (Log -` spied s))}"
 
 abbreviation rel_id_fact :: "(state \<times> state) set" where
 "rel_id_fact \<equiv> {(s, s') | s s' n A B.
   s' = s \<union> {Spy} \<times> {\<langle>n, PriKey A\<rangle>, \<langle>n, PriKey B\<rangle>} \<and>
   {PriKey A, PriKey B, \<langle>n, A \<otimes> B\<rangle>} \<subseteq> spied s}"
 
 abbreviation rel_id_mult :: "(state \<times> state) set" where
 "rel_id_mult \<equiv> {(s, s') | s s' n A B U.
   s' = insert (Spy, \<langle>n, A \<otimes> B\<rangle>) s \<and>
   U \<union> {PriKey A, PriKey B, A \<otimes> B} \<subseteq> spied s \<and>
   (\<langle>n, PriKey A\<rangle> \<in> spied s \<or> \<langle>n, PriKey B\<rangle> \<in> spied s) \<and>
   U \<in> key_sets (A \<otimes> B) (crypts (Log -` spied s))}"
 
 abbreviation rel_id_hash :: "(state \<times> state) set" where
 "rel_id_hash \<equiv> {(s, s') | s s' n X U.
   s' = s \<union> {Spy} \<times> {\<langle>n, X\<rangle>, \<langle>n, Hash X\<rangle>} \<and>
   U \<union> {X, Hash X} \<subseteq> spied s \<and>
   (\<langle>n, X\<rangle> \<in> spied s \<or> \<langle>n, Hash X\<rangle> \<in> spied s) \<and>
   U \<in> key_sets (Hash X) (crypts (Log -` spied s))}"
 
 abbreviation rel_id_crypt :: "(state \<times> state) set" where
 "rel_id_crypt \<equiv> {(s, s') | s s' n X U.
   s' = s \<union> {Spy} \<times> IDInfo n ` insert X U \<and>
   insert X U \<subseteq> spied s \<and>
   (\<langle>n, X\<rangle> \<in> spied s \<or> (\<exists>K \<in> U. \<langle>n, K\<rangle> \<in> spied s)) \<and>
   U \<in> key_sets X (crypts (Log -` spied s))}"
 
 abbreviation rel_id_sep :: "(state \<times> state) set" where
 "rel_id_sep \<equiv> {(s, s') | s s' n X Y.
   s' = s \<union> {Spy} \<times> {\<langle>n, X\<rangle>, \<langle>n, Y\<rangle>} \<and>
   {X, Y, \<langle>n, \<lbrace>X, Y\<rbrace>\<rangle>} \<subseteq> spied s}"
 
 abbreviation rel_id_con :: "(state \<times> state) set" where
 "rel_id_con \<equiv> {(s, s') | s s' n X Y U.
   s' = insert (Spy, \<langle>n, \<lbrace>X, Y\<rbrace>\<rangle>) s \<and>
   U \<union> {X, Y, \<lbrace>X, Y\<rbrace>} \<subseteq> spied s \<and>
   (\<langle>n, X\<rangle> \<in> spied s \<or> \<langle>n, Y\<rangle> \<in> spied s) \<and>
   U \<in> key_sets \<lbrace>X, Y\<rbrace> (crypts (Log -` spied s))}"
 
 
 definition rel :: "(state \<times> state) set" where
 "rel \<equiv> rel_asset_i \<union> rel_owner_ii \<union> rel_asset_ii \<union> rel_owner_iii \<union>
   rel_asset_iii \<union> rel_owner_iv \<union> rel_asset_iv \<union> rel_owner_v \<union> rel_asset_v \<union>
   rel_prik \<union> rel_pubk \<union> rel_sesk \<union> rel_fact \<union> rel_mult \<union> rel_hash \<union> rel_dec \<union>
   rel_enc \<union> rel_sep \<union> rel_con \<union> rel_id_agent \<union> rel_id_invk \<union> rel_id_sesk \<union>
   rel_id_fact \<union> rel_id_mult \<union> rel_id_hash \<union> rel_id_crypt \<union> rel_id_sep \<union> rel_id_con"
 
 abbreviation in_rel :: "state \<Rightarrow> state \<Rightarrow> bool" (infix "\<turnstile>" 60) where
 "s \<turnstile> s' \<equiv> (s, s') \<in> rel"
 
 abbreviation in_rel_rtrancl :: "state \<Rightarrow> state \<Rightarrow> bool" (infix "\<Turnstile>" 60) where
 "s \<Turnstile> s' \<equiv> (s, s') \<in> rel\<^sup>*"
 
 
-end
+end
\ No newline at end of file
diff --git a/thys/Relational_Method/Possibility.thy b/thys/Relational_Method/Possibility.thy
--- a/thys/Relational_Method/Possibility.thy
+++ b/thys/Relational_Method/Possibility.thy
@@ -1,990 +1,990 @@
 (*  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 "Possibility properties"
 
 theory Possibility
   imports Anonymity
 begin
 
 text \<open>
 \label{Possibility}
 \<close>
 
 
 type_synonym seskey_tuple = "key_id \<times> key_id \<times> key_id \<times> key_id \<times> key_id"
 
 type_synonym stage = "state \<times> seskey_tuple"
 
 
 abbreviation pred_asset_i :: "agent_id \<Rightarrow> state \<Rightarrow> stage \<Rightarrow> bool" where
 "pred_asset_i n s x \<equiv>
   \<exists>S. PriKey S \<notin> used s \<and> x = (insert (Asset n, PriKey S) s \<union>
     {Asset n, Spy} \<times> {Crypt (Auth_ShaKey n) (PriKey S)} \<union>
     {(Spy, Log (Crypt (Auth_ShaKey n) (PriKey S)))},
     S, 0, 0, 0, 0)"
 
 definition run_asset_i :: "agent_id \<Rightarrow> state \<Rightarrow> stage" where
 "run_asset_i n s \<equiv> SOME x. pred_asset_i n s x"
 
 
 abbreviation pred_owner_ii :: "agent_id \<Rightarrow> stage \<Rightarrow> stage \<Rightarrow> bool" where
 "pred_owner_ii n x y \<equiv> case x of (s, S, _) \<Rightarrow>
   \<exists>A. PriKey A \<notin> used s \<and> y = (insert (Owner n, PriKey A) s \<union>
     {Owner n, Spy} \<times> {\<lbrace>Num 1, PubKey A\<rbrace>} \<union>
     {Spy} \<times> Log ` {Crypt (Auth_ShaKey n) (PriKey S), \<lbrace>Num 1, PubKey A\<rbrace>},
     S, A, 0, 0, 0)"
 
 definition run_owner_ii :: "agent_id \<Rightarrow> state \<Rightarrow> stage" where
 "run_owner_ii n s \<equiv> SOME x. pred_owner_ii n (run_asset_i n s) x"
 
 
 abbreviation pred_asset_ii :: "agent_id \<Rightarrow> stage \<Rightarrow> stage \<Rightarrow> bool" where
 "pred_asset_ii n x y \<equiv> case x of (s, S, A, _) \<Rightarrow>
   \<exists>B. PriKey B \<notin> used s \<and> y = (insert (Asset n, PriKey B) s \<union>
     {Asset n, Spy} \<times> {\<lbrace>Num 2, PubKey B\<rbrace>} \<union>
     {Spy} \<times> Log ` {\<lbrace>Num 1, PubKey A\<rbrace>, \<lbrace>Num 2, PubKey B\<rbrace>},
     S, A, B, 0, 0)"
 
 definition run_asset_ii :: "agent_id \<Rightarrow> state \<Rightarrow> stage" where
 "run_asset_ii n s \<equiv> SOME x. pred_asset_ii n (run_owner_ii n s) x"
 
 
 abbreviation pred_owner_iii :: "agent_id \<Rightarrow> stage \<Rightarrow> stage \<Rightarrow> bool" where
 "pred_owner_iii n x y \<equiv> case x of (s, S, A, B, _) \<Rightarrow>
   \<exists>C. PriKey C \<notin> used s \<and> y = (insert (Owner n, PriKey C) s \<union>
     {Owner n, Spy} \<times> {\<lbrace>Num 3, PubKey C\<rbrace>} \<union>
     {Spy} \<times> Log ` {\<lbrace>Num 2, PubKey B\<rbrace>, \<lbrace>Num 3, PubKey C\<rbrace>},
     S, A, B, C, 0)"
 
 definition run_owner_iii :: "agent_id \<Rightarrow> state \<Rightarrow> stage" where
 "run_owner_iii n s \<equiv> SOME x. pred_owner_iii n (run_asset_ii n s) x"
 
 
 abbreviation pred_asset_iii :: "agent_id \<Rightarrow> stage \<Rightarrow> stage \<Rightarrow> bool" where
 "pred_asset_iii n x y \<equiv> case x of (s, S, A, B, C, _) \<Rightarrow>
   \<exists>D. PriKey D \<notin> used s \<and> y = (insert (Asset n, PriKey D) s \<union>
     {Asset n, Spy} \<times> {\<lbrace>Num 4, PubKey D\<rbrace>} \<union>
     {Spy} \<times> Log ` {\<lbrace>Num 3, PubKey C\<rbrace>, \<lbrace>Num 4, PubKey D\<rbrace>},
     S, A, B, C, D)"
 
 definition run_asset_iii :: "agent_id \<Rightarrow> state \<Rightarrow> stage" where
 "run_asset_iii n s \<equiv> SOME x. pred_asset_iii n (run_owner_iii n s) x"
 
 
 abbreviation stage_owner_iv :: "agent_id \<Rightarrow> stage \<Rightarrow> stage" where
 "stage_owner_iv n x \<equiv> let (s, S, A, B, C, D) = x;
   SK = (Some S, {A, B}, {C, D}) in
   (insert (Owner n, SesKey SK) s \<union>
     {Owner n, Spy} \<times> {Crypt (SesK SK) (PubKey D)} \<union>
     {Spy} \<times> Log ` {\<lbrace>Num 4, PubKey D\<rbrace>, Crypt (SesK SK) (PubKey D)},
     S, A, B, C, D)"
 
 definition run_owner_iv :: "agent_id \<Rightarrow> state \<Rightarrow> stage" where
 "run_owner_iv n s \<equiv> stage_owner_iv n (run_asset_iii n s)"
 
 
 abbreviation stage_asset_iv :: "agent_id \<Rightarrow> stage \<Rightarrow> stage" where
 "stage_asset_iv n x \<equiv> let (s, S, A, B, C, D) = x;
   SK = (Some S, {A, B}, {C, D}) in
   (s \<union> {Asset n} \<times> {SesKey SK, PubKey B} \<union>
     {Asset n, Spy} \<times> {Token n (Auth_PriK n) B C SK} \<union>
     {Spy} \<times> Log ` {Crypt (SesK SK) (PubKey D),
       Token n (Auth_PriK n) B C SK},
     S, A, B, C, D)"
 
 definition run_asset_iv :: "agent_id \<Rightarrow> state \<Rightarrow> stage" where
 "run_asset_iv n s \<equiv> stage_asset_iv n (run_owner_iv n s)"
 
 
 abbreviation stage_owner_v :: "agent_id \<Rightarrow> stage \<Rightarrow> stage" where
 "stage_owner_v n x \<equiv> let (s, S, A, B, C, D) = x;
   SK = (Some S, {A, B}, {C, D}) in
   (s \<union> {Owner n, Spy} \<times> {Crypt (SesK SK) (Pwd n)} \<union>
     {Spy} \<times> Log ` {Token n (Auth_PriK n) B C SK, Crypt (SesK SK) (Pwd n)},
     S, A, B, C, D)"
 
 definition run_owner_v :: "agent_id \<Rightarrow> state \<Rightarrow> stage" where
 "run_owner_v n s \<equiv> stage_owner_v n (run_asset_iv n s)"
 
 
 abbreviation stage_asset_v :: "agent_id \<Rightarrow> stage \<Rightarrow> stage" where
 "stage_asset_v n x \<equiv> let (s, S, A, B, C, D) = x;
   SK = (Some S, {A, B}, {C, D}) in
   (s \<union> {Asset n, Spy} \<times> {Crypt (SesK SK) (Num 0)} \<union>
     {Spy} \<times> Log ` {Crypt (SesK SK) (Pwd n), Crypt (SesK SK) (Num 0)},
     S, A, B, C, D)"
 
 definition run_asset_v :: "agent_id \<Rightarrow> state \<Rightarrow> stage" where
 "run_asset_v n s \<equiv> stage_asset_v n (run_owner_v n s)"
 
 
 lemma prikey_unused_1:
  "infinite {A. PriKey A \<notin> used s\<^sub>0}"
 by (rule infinite_super [of "- range Auth_PriK"], rule subsetI, simp add:
  image_def bad_prik_def, rule someI2 [of _ "{}"], simp, blast, subst Auth_PriK_def,
  rule someI [of _ "\<lambda>n. 0"], simp)
 
 lemma prikey_unused_2:
  "\<lbrakk>s \<turnstile> s'; infinite {A. PriKey A \<notin> used s}\<rbrakk> \<Longrightarrow>
     infinite {A. PriKey A \<notin> used s'}"
 by (simp add: rel_def, ((erule disjE)?, (erule exE)+, simp add: image_iff,
  (((subst conj_commute | subst Int_commute), simp add: Collect_conj_eq Collect_neg_eq
  Diff_eq [symmetric])+)?, ((rule Diff_infinite_finite, rule msg.induct, simp_all,
  rule key.induct, simp_all)+)?)+)
 
 proposition prikey_unused:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow> \<exists>A. PriKey A \<notin> used s"
 by (subgoal_tac "infinite {A. PriKey A \<notin> used s}", drule infinite_imp_nonempty,
  simp, erule rtrancl_induct, rule prikey_unused_1, rule prikey_unused_2)
 
 
 lemma pubkey_unused_1:
  "\<lbrakk>s \<turnstile> s'; PubKey A \<in> parts (used s) \<longrightarrow> PriKey A \<in> used s;
     PubKey A \<in> parts (used s')\<rbrakk> \<Longrightarrow>
   PriKey A \<in> used s'"
 by (simp add: rel_def, ((erule disjE)?, ((erule exE)+)?, simp add: parts_insert
  image_iff split: if_split_asm, ((erule conjE)+, drule RangeI, (drule parts_used,
  drule parts_snd)?, simp | (subst (asm) disj_assoc [symmetric])?, erule disjE,
  (drule parts_dec | drule parts_enc | drule parts_sep | drule parts_con), simp)?)+)
 
 proposition pubkey_unused [rule_format]:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow>
     PriKey A \<notin> used s \<longrightarrow>
   PubKey A \<notin> parts (used s)"
 by (erule rtrancl_induct, subst parts_init, simp add: Range_iff image_def, rule impI,
  erule contrapos_nn [OF _ pubkey_unused_1], blast+)
 
 
 proposition run_asset_i_ex:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow> pred_asset_i n s (run_asset_i n s)"
 by (drule prikey_unused, erule exE, subst run_asset_i_def, rule someI_ex, blast)
 
 proposition run_asset_i_rel:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow> s \<Turnstile> fst (run_asset_i n s)"
     (is "_ \<Longrightarrow> _ \<Turnstile> ?t")
 by (drule run_asset_i_ex [of _ n], rule r_into_rtrancl,
  subgoal_tac "(s, ?t) \<in> rel_asset_i", simp_all add: rel_def, erule exE, auto)
 
 proposition run_asset_i_msg:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow>
     case run_asset_i n s of (s', S, _) \<Rightarrow>
       (Asset n, Crypt (Auth_ShaKey n) (PriKey S)) \<in> s'"
 by (drule run_asset_i_ex [of _ n], auto)
 
 proposition run_asset_i_nonce:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow> PriKey (fst (snd (run_asset_i n s))) \<notin> used s"
 by (drule run_asset_i_ex [of _ n], auto)
 
 proposition run_asset_i_unused:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow> \<exists>A. PriKey A \<notin> used (fst (run_asset_i n s))"
 by (rule prikey_unused, rule rtrancl_trans, simp, rule run_asset_i_rel)
 
 
 proposition run_owner_ii_ex:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow> pred_owner_ii n (run_asset_i n s) (run_owner_ii n s)"
 by (drule run_asset_i_unused, erule exE, subst run_owner_ii_def, rule someI_ex,
  auto simp add: split_def)
 
 proposition run_owner_ii_rel:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow> s \<Turnstile> fst (run_owner_ii n s)"
     (is "_ \<Longrightarrow> _ \<Turnstile> ?t")
 by (rule rtrancl_into_rtrancl, erule run_asset_i_rel [of _ n], frule run_asset_i_msg,
  drule run_owner_ii_ex, subgoal_tac "(fst (run_asset_i n s), ?t) \<in> rel_owner_ii",
  simp_all add: rel_def split_def, erule exE, (rule exI)+, auto)
 
 proposition run_owner_ii_msg:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow>
     case run_owner_ii n s of (s', S, A, _) \<Rightarrow>
       {(Asset n, Crypt (Auth_ShaKey n) (PriKey S)),
         (Owner n, \<lbrace>Num 1, PubKey A\<rbrace>)} \<subseteq> s'"
 by (frule run_asset_i_msg [of _ n], drule run_owner_ii_ex [of _ n], auto)
 
 proposition run_owner_ii_nonce:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow> PriKey (fst (snd (run_owner_ii n s))) \<notin> used s"
 by (frule run_asset_i_nonce [of _ n], drule run_owner_ii_ex [of _ n], auto)
 
 proposition run_owner_ii_unused:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow> \<exists>B. PriKey B \<notin> used (fst (run_owner_ii n s))"
 by (rule prikey_unused, rule rtrancl_trans, simp, rule run_owner_ii_rel)
 
 
 proposition run_asset_ii_ex:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow> pred_asset_ii n (run_owner_ii n s) (run_asset_ii n s)"
 by (drule run_owner_ii_unused, erule exE, subst run_asset_ii_def, rule someI_ex,
  auto simp add: split_def)
 
 proposition run_asset_ii_rel:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow> s \<Turnstile> fst (run_asset_ii n s)"
     (is "_ \<Longrightarrow> _ \<Turnstile> ?t")
 by (rule rtrancl_into_rtrancl, erule run_owner_ii_rel [of _ n], frule run_owner_ii_msg,
  drule run_asset_ii_ex, subgoal_tac "(fst (run_owner_ii n s), ?t) \<in> rel_asset_ii",
  simp_all add: rel_def split_def, erule exE, (rule exI)+, auto)
 
 proposition run_asset_ii_msg:
   assumes A: "s\<^sub>0 \<Turnstile> s"
   shows "case run_asset_ii n s of (s', S, A, B, _) \<Rightarrow>
     insert (Owner n, \<lbrace>Num 1, PubKey A\<rbrace>)
       ({Asset n} \<times> {Crypt (Auth_ShaKey n) (PriKey S),
        \<lbrace>Num 2, PubKey B\<rbrace>}) \<subseteq> s' \<and>
     (Asset n, PubKey B) \<notin> s'"
 by (insert run_owner_ii_msg [OF A, of n], insert run_asset_ii_ex [OF A, of n],
  simp add: split_def, erule exE, simp, insert run_owner_ii_rel [OF A, of n],
  drule rtrancl_trans [OF A], drule pubkey_unused, auto)
 
 proposition run_asset_ii_nonce:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow> PriKey (fst (snd (run_asset_ii n s))) \<notin> used s"
 by (frule run_owner_ii_nonce [of _ n], drule run_asset_ii_ex [of _ n], auto)
 
 proposition run_asset_ii_unused:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow> \<exists>C. PriKey C \<notin> used (fst (run_asset_ii n s))"
 by (rule prikey_unused, rule rtrancl_trans, simp, rule run_asset_ii_rel)
 
 
 proposition run_owner_iii_ex:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow> pred_owner_iii n (run_asset_ii n s) (run_owner_iii n s)"
 by (drule run_asset_ii_unused, erule exE, subst run_owner_iii_def, rule someI_ex,
  auto simp add: split_def)
 
 proposition run_owner_iii_rel:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow> s \<Turnstile> fst (run_owner_iii n s)"
     (is "_ \<Longrightarrow> _ \<Turnstile> ?t")
 by (rule rtrancl_into_rtrancl, erule run_asset_ii_rel [of _ n], frule run_asset_ii_msg,
  drule run_owner_iii_ex, subgoal_tac "(fst (run_asset_ii n s), ?t) \<in> rel_owner_iii",
  simp_all add: rel_def split_def, erule exE, (rule exI)+, auto)
 
 proposition run_owner_iii_msg:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow>
     case run_owner_iii n s of (s', S, A, B, C, _) \<Rightarrow>
       {Asset n} \<times> {Crypt (Auth_ShaKey n) (PriKey S), \<lbrace>Num 2, PubKey B\<rbrace>} \<union>
       {Owner n} \<times> {\<lbrace>Num 1, PubKey A\<rbrace>, \<lbrace>Num 3, PubKey C\<rbrace>} \<subseteq> s' \<and>
       (Asset n, PubKey B) \<notin> s'"
 by (frule run_asset_ii_msg [of _ n], drule run_owner_iii_ex [of _ n], auto)
 
 proposition run_owner_iii_nonce:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow> PriKey (fst (snd (run_owner_iii n s))) \<notin> used s"
 by (frule run_asset_ii_nonce [of _ n], drule run_owner_iii_ex [of _ n], auto)
 
 proposition run_owner_iii_unused:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow> \<exists>D. PriKey D \<notin> used (fst (run_owner_iii n s))"
 by (rule prikey_unused, rule rtrancl_trans, simp, rule run_owner_iii_rel)
 
 
 proposition run_asset_iii_ex:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow> pred_asset_iii n (run_owner_iii n s) (run_asset_iii n s)"
 by (drule run_owner_iii_unused, erule exE, subst run_asset_iii_def, rule someI_ex,
  auto simp add: split_def)
 
 proposition run_asset_iii_rel:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow> s \<Turnstile> fst (run_asset_iii n s)"
     (is "_ \<Longrightarrow> _ \<Turnstile> ?t")
 by (rule rtrancl_into_rtrancl, erule run_owner_iii_rel [of _ n], frule run_owner_iii_msg,
  drule run_asset_iii_ex, subgoal_tac "(fst (run_owner_iii n s), ?t) \<in> rel_asset_iii",
  simp_all add: rel_def split_def, erule exE, (rule exI)+, auto)
 
 proposition run_asset_iii_msg:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow>
     case run_asset_iii n s of (s', S, A, B, C, D) \<Rightarrow>
       {Asset n} \<times> {Crypt (Auth_ShaKey n) (PriKey S), \<lbrace>Num 2, PubKey B\<rbrace>,
         \<lbrace>Num 4, PubKey D\<rbrace>} \<union>
       {Owner n} \<times> {\<lbrace>Num 1, PubKey A\<rbrace>, \<lbrace>Num 3, PubKey C\<rbrace>} \<subseteq> s' \<and>
       (Asset n, PubKey B) \<notin> s'"
 by (frule run_owner_iii_msg [of _ n], drule run_asset_iii_ex [of _ n], auto)
 
 proposition run_asset_iii_nonce:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow> PriKey (fst (snd (run_asset_iii n s))) \<notin> used s"
 by (frule run_owner_iii_nonce [of _ n], drule run_asset_iii_ex [of _ n], auto)
 
 
 lemma run_owner_iv_rel_1:
  "\<lbrakk>s\<^sub>0 \<Turnstile> s; run_asset_iii n s = (s', S, A, B, C, D)\<rbrakk> \<Longrightarrow>
     s \<Turnstile> fst (run_owner_iv n s)"
       (is "\<lbrakk>_; _\<rbrakk> \<Longrightarrow> _ \<Turnstile> ?t")
 by (rule rtrancl_into_rtrancl, erule run_asset_iii_rel [of _ n], drule run_asset_iii_msg
  [of _ n], subgoal_tac "(s', ?t) \<in> rel_owner_iv", simp_all add: rel_def run_owner_iv_def
  Let_def, rule exI [of _ n], rule exI [of _ S], rule exI [of _ A], rule exI [of _ B],
  rule exI [of _ C], rule exI [of _ D], rule exI [of _ "Auth_ShaKey n"], auto)
 
 proposition run_owner_iv_rel:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow> s \<Turnstile> fst (run_owner_iv n s)"
 by (insert run_owner_iv_rel_1, cases "run_asset_iii n s", simp)
 
 proposition run_owner_iv_msg:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow>
     let (s', S, A, B, C, D) = run_owner_iv n s;
       SK = (Some S, {A, B}, {C, D}) in
       {Asset n} \<times> {Crypt (Auth_ShaKey n) (PriKey S), \<lbrace>Num 2, PubKey B\<rbrace>,
         \<lbrace>Num 4, PubKey D\<rbrace>} \<union>
       {Owner n} \<times> {\<lbrace>Num 1, PubKey A\<rbrace>, \<lbrace>Num 3, PubKey C\<rbrace>, SesKey SK,
         Crypt (SesK SK) (PubKey D)} \<subseteq> s' \<and>
       (Asset n, PubKey B) \<notin> s'"
 by (drule run_asset_iii_msg [of _ n], simp add: run_owner_iv_def split_def Let_def)
 
 proposition run_owner_iv_nonce:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow> PriKey (fst (snd (run_owner_iv n s))) \<notin> used s"
 by (drule run_asset_iii_nonce [of _ n], simp add: run_owner_iv_def split_def Let_def)
 
 
 proposition run_asset_iv_rel:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow> s \<Turnstile> fst (run_asset_iv n s)"
     (is "_ \<Longrightarrow> _ \<Turnstile> ?t")
 by (rule rtrancl_into_rtrancl, erule run_owner_iv_rel [of _ n], drule run_owner_iv_msg
  [of _ n], subgoal_tac "(fst (run_owner_iv n s), ?t) \<in> rel_asset_iv", simp_all add:
  rel_def run_asset_iv_def split_def Let_def, blast)
 
 proposition run_asset_iv_msg:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow>
     let (s', S, A, B, C, D) = run_asset_iv n s; SK = (Some S, {A, B}, {C, D}) in
       insert (Owner n, SesKey SK)
         ({Asset n} \<times> {SesKey SK, Token n (Auth_PriK n) B C SK}) \<subseteq> s'"
 by (drule run_owner_iv_msg [of _ n], simp add: run_asset_iv_def split_def Let_def)
 
 proposition run_asset_iv_nonce:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow> PriKey (fst (snd (run_asset_iv n s))) \<notin> used s"
 by (drule run_owner_iv_nonce [of _ n], simp add: run_asset_iv_def split_def Let_def)
 
 
 proposition run_owner_v_rel:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow> s \<Turnstile> fst (run_owner_v n s)"
     (is "_ \<Longrightarrow> _ \<Turnstile> ?t")
 by (rule rtrancl_into_rtrancl, erule run_asset_iv_rel [of _ n], drule run_asset_iv_msg
  [of _ n], subgoal_tac "(fst (run_asset_iv n s), ?t) \<in> rel_owner_v", simp_all add:
  rel_def run_owner_v_def split_def Let_def, blast)
 
 proposition run_owner_v_msg:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow>
     let (s', S, A, B, C, D) = run_owner_v n s;
       SK = (Some S, {A, B}, {C, D}) in
       {(Asset n, SesKey SK),
         (Owner n, Crypt (SesK SK) (Pwd n))} \<subseteq> s'"
 by (drule run_asset_iv_msg [of _ n], simp add: run_owner_v_def split_def Let_def)
 
 proposition run_owner_v_nonce:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow> PriKey (fst (snd (run_owner_v n s))) \<notin> used s"
 by (drule run_asset_iv_nonce [of _ n], simp add: run_owner_v_def split_def Let_def)
 
 
 proposition run_asset_v_rel:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow> s \<Turnstile> fst (run_asset_v n s)"
     (is "_ \<Longrightarrow> _ \<Turnstile> ?t")
 by (rule rtrancl_into_rtrancl, erule run_owner_v_rel [of _ n], drule run_owner_v_msg
  [of _ n], subgoal_tac "(fst (run_owner_v n s), ?t) \<in> rel_asset_v", simp_all add:
  rel_def run_asset_v_def split_def Let_def, blast)
 
 proposition run_asset_v_msg:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow>
     let (s', S, A, B, C, D) = run_asset_v n s; SK = (Some S, {A, B}, {C, D}) in
       {(Owner n, Crypt (SesK SK) (Pwd n)),
         (Asset n, Crypt (SesK SK) (Num 0))} \<subseteq> s'"
 by (drule run_owner_v_msg [of _ n], simp add: run_asset_v_def split_def Let_def)
 
 proposition run_asset_v_nonce:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow> PriKey (fst (snd (run_asset_v n s))) \<notin> used s"
 by (drule run_owner_v_nonce [of _ n], simp add: run_asset_v_def split_def Let_def)
 
 
 lemma runs_unbounded_1:
  "\<lbrakk>s\<^sub>0 \<Turnstile> s; run_asset_v n s = (s', S, A, B, C, D)\<rbrakk> \<Longrightarrow>
     \<exists>s' S SK. (Asset n, Crypt (Auth_ShaKey n) (PriKey S)) \<notin> s \<and>
       {(Owner n, Crypt (SesK SK) (Pwd n)),
        (Asset n, Crypt (SesK SK) (Num 0))} \<subseteq> s' \<and>
       s \<Turnstile> s' \<and> fst SK = Some S"
 by (rule exI [of _ s'], rule exI [of _ S], rule exI [of _ "(Some S, {A, B}, {C, D})"],
  rule conjI, rule notI, frule run_asset_v_nonce [of _ n], frule asset_i_used [of _ n S],
  simp, frule run_asset_v_rel [of _ n], drule run_asset_v_msg [of _ n],
  simp add: Let_def)
 
 theorem runs_unbounded:
  "s\<^sub>0 \<Turnstile> s \<Longrightarrow> \<exists>s' S SK. s \<Turnstile> s' \<and> fst SK = Some S \<and>
     (Asset n, Crypt (Auth_ShaKey n) (PriKey S)) \<notin> s \<and>
     {(Owner n, Crypt (SesK SK) (Pwd n)),
      (Asset n, Crypt (SesK SK) (Num 0))} \<subseteq> s'"
 by (insert runs_unbounded_1, cases "run_asset_v n s", blast)
 
 
 definition pwd_spy_i :: "agent_id \<Rightarrow> stage" where
 "pwd_spy_i n \<equiv>
   (insert (Spy, Crypt (Auth_ShaKey n) (Auth_PriKey n)) s\<^sub>0,
     Auth_PriK n, 0, 0, 0, 0)"
 
 definition pwd_owner_ii :: "agent_id \<Rightarrow> stage" where
 "pwd_owner_ii n \<equiv> SOME x. pred_owner_ii n (pwd_spy_i n) x"
 
 definition pwd_spy_ii :: "agent_id \<Rightarrow> stage" where
 "pwd_spy_ii n \<equiv>
   case pwd_owner_ii n of (s, S, A, _) \<Rightarrow>
     (insert (Spy, \<lbrace>Num 2, PubKey S\<rbrace>) s, S, A, S, 0, 0)"
 
 definition pwd_owner_iii :: "agent_id \<Rightarrow> stage" where
 "pwd_owner_iii n \<equiv> SOME x. pred_owner_iii n (pwd_spy_ii n) x"
 
 definition pwd_spy_iii :: "agent_id \<Rightarrow> stage" where
 "pwd_spy_iii n \<equiv>
   case pwd_owner_iii n of (s, S, A, B, C, _) \<Rightarrow>
     (insert (Spy, \<lbrace>Num 4, PubKey S\<rbrace>) s, S, A, B, C, S)"
 
 definition pwd_owner_iv :: "agent_id \<Rightarrow> stage" where
 "pwd_owner_iv n \<equiv> stage_owner_iv n (pwd_spy_iii n)"
 
 
 definition pwd_spy_sep_map :: "agent_id \<Rightarrow> stage" where
 "pwd_spy_sep_map n \<equiv>
   case pwd_owner_iv n of (s, S, A, B, C, D) \<Rightarrow>
     (insert (Spy, PubKey A) s, S, A, B, C, D)"
 
 definition pwd_spy_sep_agr :: "agent_id \<Rightarrow> stage" where
 "pwd_spy_sep_agr n \<equiv>
   case pwd_spy_sep_map n of (s, S, A, B, C, D) \<Rightarrow>
     (insert (Spy, PubKey C) s, S, A, B, C, D)"
 
 definition pwd_spy_sesk :: "agent_id \<Rightarrow> stage" where
 "pwd_spy_sesk n \<equiv>
   let (s, S, A, B, C, D) = pwd_spy_sep_agr n;
     SK = (Some S, {A, B}, {C, D}) in
     (insert (Spy, SesKey SK) s, S, A, B, C, D)"
 
 definition pwd_spy_mult :: "agent_id \<Rightarrow> stage" where
 "pwd_spy_mult n \<equiv>
   case pwd_spy_sesk n of (s, S, A, B, C, D) \<Rightarrow>
     (insert (Spy, Auth_PriK n \<otimes> B) s, S, A, B, C, D)"
 
 definition pwd_spy_enc_pubk :: "agent_id \<Rightarrow> stage" where
 "pwd_spy_enc_pubk n \<equiv>
   let (s, S, A, B, C, D) = pwd_spy_mult n; SK = (Some S, {A, B}, {C, D}) in
     (insert (Spy, Crypt (SesK SK) (PubKey C)) s, S, A, B, C, D)"
 
 definition pwd_spy_enc_mult :: "agent_id \<Rightarrow> stage" where
 "pwd_spy_enc_mult n \<equiv>
   let (s, S, A, B, C, D) = pwd_spy_enc_pubk n;
     SK = (Some S, {A, B}, {C, D}) in
     (insert (Spy, Crypt (SesK SK) (Auth_PriK n \<otimes> B)) s, S, A, B, C, D)"
 
 definition pwd_spy_enc_sign :: "agent_id \<Rightarrow> stage" where
 "pwd_spy_enc_sign n \<equiv>
   let (s, S, A, B, C, D) = pwd_spy_enc_mult n;
     SK = (Some S, {A, B}, {C, D}) in
     (insert (Spy, Crypt (SesK SK) (Sign n (Auth_PriK n))) s, S, A, B, C, D)"
 
 definition pwd_spy_con :: "agent_id \<Rightarrow> stage" where
 "pwd_spy_con n \<equiv>
   let (s, S, A, B, C, D) = pwd_spy_enc_sign n;
     SK = (Some S, {A, B}, {C, D}) in
     (insert (Spy, \<lbrace>Crypt (SesK SK) (Auth_PriK n \<otimes> B),
       Crypt (SesK SK) (Sign n (Auth_PriK n))\<rbrace>) s, S, A, B, C, D)"
 
 definition pwd_spy_iv :: "agent_id \<Rightarrow> stage" where
 "pwd_spy_iv n \<equiv>
   let (s, S, A, B, C, D) = pwd_spy_con n; SK = (Some S, {A, B}, {C, D}) in
     (insert (Spy, Token n (Auth_PriK n) B C SK) s, S, A, B, C, D)"
 
 
 definition pwd_owner_v :: "agent_id \<Rightarrow> stage" where
 "pwd_owner_v n \<equiv> stage_owner_v n (pwd_spy_iv n)"
 
 definition pwd_spy_dec :: "agent_id \<Rightarrow> stage" where
 "pwd_spy_dec n \<equiv>
   case pwd_owner_v n of (s, S, A, B, C, D) \<Rightarrow>
     (insert (Spy, Pwd n) s, S, A, B, C, D)"
 
 definition pwd_spy_id_prik :: "agent_id \<Rightarrow> stage" where
 "pwd_spy_id_prik n \<equiv>
   case pwd_spy_dec n of (s, S, A, B, C, D) \<Rightarrow>
     (insert (Spy, \<langle>n, PriKey S\<rangle>) s, S, A, B, C, D)"
 
 definition pwd_spy_id_pubk :: "agent_id \<Rightarrow> stage" where
 "pwd_spy_id_pubk n \<equiv>
   case pwd_spy_id_prik n of (s, S, A, B, C, D) \<Rightarrow>
     (insert (Spy, \<langle>n, PubKey S\<rangle>) s, S, A, B, C, D)"
 
 definition pwd_spy_id_sesk :: "agent_id \<Rightarrow> stage" where
 "pwd_spy_id_sesk n \<equiv>
   let (s, S, A, B, C, D) = pwd_spy_id_pubk n;
     SK = (Some S, {A, B}, {C, D}) in
     (insert (Spy, \<langle>n, SesKey SK\<rangle>) s, S, A, B, C, D)"
 
 definition pwd_spy_id_pwd :: "agent_id \<Rightarrow> stage" where
 "pwd_spy_id_pwd n \<equiv>
   case pwd_spy_id_sesk n of (s, S, A, B, C, D) \<Rightarrow>
     (insert (Spy, \<langle>n, Pwd n\<rangle>) s, S, A, B, C, D)"
 
 
 proposition key_sets_crypts_subset:
  "\<lbrakk>U \<in> key_sets X (crypts (Log -` spied H)); H \<subseteq> H'\<rbrakk> \<Longrightarrow>
     U \<in> key_sets X (crypts (Log -` spied H'))"
       (is "\<lbrakk>_ \<in> ?A; _\<rbrakk> \<Longrightarrow> _")
 by (rule subsetD [of ?A], rule key_sets_mono, rule crypts_mono, blast)
 
 
 fun pwd_spy_i_state :: "agent_id \<Rightarrow> seskey_tuple \<Rightarrow> state" where
 "pwd_spy_i_state n (S, _) = {Spy} \<times> ({PriKey S, PubKey S, Key (Auth_ShaKey n),
   Auth_PriKey n, Sign n (Auth_PriK n), Crypt (Auth_ShaKey n) (PriKey S),
   \<langle>n, Key (Auth_ShaKey n)\<rangle>} \<union> range Num)"
 
 proposition pwd_spy_i_rel:
  "n \<in> bad_prikey \<inter> bad_id_shakey \<Longrightarrow> s\<^sub>0 \<Turnstile> fst (pwd_spy_i n)"
     (is "_ \<Longrightarrow> _ \<Turnstile> ?t")
 by (rule r_into_rtrancl, subgoal_tac "(s\<^sub>0, ?t) \<in> rel_enc", simp_all add: rel_def
  pwd_spy_i_def, blast)
 
 proposition pwd_spy_i_msg:
  "n \<in> bad_prikey \<inter> bad_id_shakey \<Longrightarrow>
     case pwd_spy_i n of (s, S, A, B, C, D) \<Rightarrow>
       pwd_spy_i_state n (S, A, B, C, D) \<subseteq> s"
 by (simp add: pwd_spy_i_def, blast)
 
 proposition pwd_spy_i_unused:
  "n \<in> bad_prikey \<inter> bad_id_shakey \<Longrightarrow> \<exists>A. PriKey A \<notin> used (fst (pwd_spy_i n))"
 by (drule pwd_spy_i_rel, rule prikey_unused)
 
 
 fun pwd_owner_ii_state :: "agent_id \<Rightarrow> seskey_tuple \<Rightarrow> state" where
 "pwd_owner_ii_state n (S, A, B, C, D) =
   pwd_spy_i_state n (S, A, B, C, D) \<union> {Owner n, Spy} \<times> {\<lbrace>Num 1, PubKey A\<rbrace>}"
 
 proposition pwd_owner_ii_ex:
  "n \<in> bad_prikey \<inter> bad_id_shakey \<Longrightarrow>
     pred_owner_ii n (pwd_spy_i n) (pwd_owner_ii n)"
 by (drule pwd_spy_i_unused, erule exE, subst pwd_owner_ii_def, rule someI_ex,
  auto simp add: split_def)
 
 proposition pwd_owner_ii_rel:
  "n \<in> bad_prikey \<inter> bad_id_shakey \<Longrightarrow> s\<^sub>0 \<Turnstile> fst (pwd_owner_ii n)"
     (is "_ \<Longrightarrow> _ \<Turnstile> ?t")
 by (rule rtrancl_into_rtrancl, erule pwd_spy_i_rel, frule pwd_spy_i_msg,
  drule pwd_owner_ii_ex, subgoal_tac "(fst (pwd_spy_i n), ?t) \<in> rel_owner_ii",
  simp_all add: rel_def split_def, erule exE, rule exI, auto)
 
 proposition pwd_owner_ii_msg:
  "n \<in> bad_prikey \<inter> bad_id_shakey \<Longrightarrow>
     case pwd_owner_ii n of (s, S, A, B, C, D) \<Rightarrow>
       pwd_owner_ii_state n (S, A, B, C, D) \<subseteq> s \<and>
       {Key (Auth_ShaKey n)} \<in> key_sets (PriKey S) (crypts (Log -` spied s))"
 by (frule pwd_spy_i_msg, drule pwd_owner_ii_ex, simp add: split_def, erule exE,
  simp add: Image_def, simp only: Collect_disj_eq crypts_union key_sets_union,
  simp add: crypts_insert key_sets_insert, blast)
 
 
 fun pwd_spy_ii_state :: "agent_id \<Rightarrow> seskey_tuple \<Rightarrow> state" where
 "pwd_spy_ii_state n (S, A, B, C, D) =
   pwd_owner_ii_state n (S, A, B, C, D) \<union> {Spy} \<times> {PriKey B,
     \<lbrace>Num 2, PubKey B\<rbrace>}"
 
 proposition pwd_spy_ii_rel:
  "n \<in> bad_prikey \<inter> bad_id_shakey \<Longrightarrow> s\<^sub>0 \<Turnstile> fst (pwd_spy_ii n)"
     (is "_ \<Longrightarrow> _ \<Turnstile> ?t")
 by (rule rtrancl_into_rtrancl, erule pwd_owner_ii_rel, drule pwd_owner_ii_msg,
  subgoal_tac "(fst (pwd_owner_ii n), ?t) \<in> rel_con", simp_all add: rel_def
  pwd_spy_ii_def split_def, blast)
 
 proposition pwd_spy_ii_msg:
  "n \<in> bad_prikey \<inter> bad_id_shakey \<Longrightarrow>
     case pwd_spy_ii n of (s, S, A, B, C, D) \<Rightarrow>
       pwd_spy_ii_state n (S, A, B, C, D) \<subseteq> s \<and>
       {Key (Auth_ShaKey n)} \<in> key_sets (PriKey S) (crypts (Log -` spied s))"
 by (drule pwd_owner_ii_msg, simp add: pwd_spy_ii_def split_def,
  (erule conjE)+, ((rule conjI | erule key_sets_crypts_subset), blast)+)
 
 proposition pwd_spy_ii_unused:
  "n \<in> bad_prikey \<inter> bad_id_shakey \<Longrightarrow> \<exists>C. PriKey C \<notin> used (fst (pwd_spy_ii n))"
 by (drule pwd_spy_ii_rel, rule prikey_unused)
 
 
 fun pwd_owner_iii_state :: "agent_id \<Rightarrow> seskey_tuple \<Rightarrow> state" where
 "pwd_owner_iii_state n (S, A, B, C, D) =
   pwd_spy_ii_state n (S, A, B, C, D) \<union> {Owner n, Spy} \<times> {\<lbrace>Num 3, PubKey C\<rbrace>}"
 
 proposition pwd_owner_iii_ex:
  "n \<in> bad_prikey \<inter> bad_id_shakey \<Longrightarrow>
     pred_owner_iii n (pwd_spy_ii n) (pwd_owner_iii n)"
 by (drule pwd_spy_ii_unused, erule exE, subst pwd_owner_iii_def, rule someI_ex,
  auto simp add: split_def)
 
 proposition pwd_owner_iii_rel:
  "n \<in> bad_prikey \<inter> bad_id_shakey \<Longrightarrow> s\<^sub>0 \<Turnstile> fst (pwd_owner_iii n)"
     (is "_ \<Longrightarrow> _ \<Turnstile> ?t")
 by (rule rtrancl_into_rtrancl, erule pwd_spy_ii_rel, frule pwd_spy_ii_msg,
  drule pwd_owner_iii_ex, subgoal_tac "(fst (pwd_spy_ii n), ?t) \<in> rel_owner_iii",
  simp_all add: rel_def split_def, rule exI, rule exI, auto)
 
 proposition pwd_owner_iii_msg:
  "n \<in> bad_prikey \<inter> bad_id_shakey \<Longrightarrow>
     case pwd_owner_iii n of (s, S, A, B, C, D) \<Rightarrow>
       pwd_owner_iii_state n (S, A, B, C, D) \<subseteq> s \<and>
       {Key (Auth_ShaKey n)} \<in> key_sets (PriKey S) (crypts (Log -` spied s))"
 by (frule pwd_spy_ii_msg, drule pwd_owner_iii_ex, simp add: split_def, erule exE,
  simp, (erule conjE)+, ((rule conjI | erule key_sets_crypts_subset), blast)+)
 
 
 fun pwd_spy_iii_state :: "agent_id \<Rightarrow> seskey_tuple \<Rightarrow> state" where
 "pwd_spy_iii_state n (S, A, B, C, D) =
   pwd_owner_iii_state n (S, A, B, C, D) \<union> {Spy} \<times> {PriKey D,
     \<lbrace>Num 4, PubKey D\<rbrace>}"
 
 proposition pwd_spy_iii_rel:
  "n \<in> bad_prikey \<inter> bad_id_shakey \<Longrightarrow> s\<^sub>0 \<Turnstile> fst (pwd_spy_iii n)"
     (is "_ \<Longrightarrow> _ \<Turnstile> ?t")
 by (rule rtrancl_into_rtrancl, erule pwd_owner_iii_rel, drule pwd_owner_iii_msg,
  subgoal_tac "(fst (pwd_owner_iii n), ?t) \<in> rel_con", simp_all add: rel_def
  pwd_spy_iii_def split_def, blast)
 
 proposition pwd_spy_iii_msg:
  "n \<in> bad_prikey \<inter> bad_id_shakey \<Longrightarrow>
     case pwd_spy_iii n of (s, S, A, B, C, D) \<Rightarrow>
       pwd_spy_iii_state n (S, A, B, C, D) \<subseteq> s \<and>
       {Key (Auth_ShaKey n)} \<in> key_sets (PriKey S) (crypts (Log -` spied s))"
 by (drule pwd_owner_iii_msg, simp add: pwd_spy_iii_def split_def,
  (erule conjE)+, ((rule conjI | erule key_sets_crypts_subset), blast)+)
 
 
 fun pwd_owner_iv_state :: "agent_id \<Rightarrow> seskey_tuple \<Rightarrow> state" where
 "pwd_owner_iv_state n (S, A, B, C, D) = (let SK = (Some S, {A, B}, {C, D}) in
   insert (Owner n, SesKey SK) (pwd_spy_iii_state n (S, A, B, C, D)))"
 
 lemma pwd_owner_iv_rel_1:
  "\<lbrakk>n \<in> bad_prikey \<inter> bad_id_shakey; pwd_spy_iii n = (s, S, A, B, C, D)\<rbrakk> \<Longrightarrow>
     s\<^sub>0 \<Turnstile> fst (pwd_owner_iv n)"
       (is "\<lbrakk>_; _\<rbrakk> \<Longrightarrow> _ \<Turnstile> ?t")
 by (rule rtrancl_into_rtrancl, erule pwd_spy_iii_rel, drule pwd_spy_iii_msg,
  subgoal_tac "(s, ?t) \<in> rel_owner_iv", simp_all add: rel_def pwd_owner_iv_def
  Let_def, rule exI [of _ n], rule exI [of _ S], rule exI [of _ A], rule exI [of _ B],
  rule exI [of _ C], rule exI [of _ D], rule exI [of _ "Auth_ShaKey n"], auto)
 
 proposition pwd_owner_iv_rel:
  "n \<in> bad_prikey \<inter> bad_id_shakey \<Longrightarrow> s\<^sub>0 \<Turnstile> fst (pwd_owner_iv n)"
 by (insert pwd_owner_iv_rel_1, cases "pwd_spy_iii n", simp)
 
 proposition pwd_owner_iv_msg:
  "n \<in> bad_prikey \<inter> bad_id_shakey \<Longrightarrow>
     case pwd_owner_iv n of (s, S, A, B, C, D) \<Rightarrow>
       pwd_owner_iv_state n (S, A, B, C, D) \<subseteq> s \<and>
       {Key (Auth_ShaKey n)} \<in> key_sets (PriKey S) (crypts (Log -` spied s))"
 by (drule pwd_spy_iii_msg, simp add: pwd_owner_iv_def split_def Let_def,
  (erule conjE)+, ((rule conjI | erule key_sets_crypts_subset), blast)+)
 
 
 fun pwd_spy_sep_map_state :: "agent_id \<Rightarrow> seskey_tuple \<Rightarrow> state" where
 "pwd_spy_sep_map_state n (S, A, B, C, D) =
   insert (Spy, PubKey A) (pwd_owner_iv_state n (S, A, B, C, D))"
 
 proposition pwd_spy_sep_map_rel:
  "n \<in> bad_prikey \<inter> bad_id_shakey \<Longrightarrow> s\<^sub>0 \<Turnstile> fst (pwd_spy_sep_map n)"
     (is "_ \<Longrightarrow> _ \<Turnstile> ?t")
 by (rule rtrancl_into_rtrancl, erule pwd_owner_iv_rel, drule pwd_owner_iv_msg,
  subgoal_tac "(fst (pwd_owner_iv n), ?t) \<in> rel_sep", simp_all add: rel_def
  pwd_spy_sep_map_def split_def, blast)
 
 proposition pwd_spy_sep_map_msg:
  "n \<in> bad_prikey \<inter> bad_id_shakey \<Longrightarrow>
     case pwd_spy_sep_map n of (s, S, A, B, C, D) \<Rightarrow>
       pwd_spy_sep_map_state n (S, A, B, C, D) \<subseteq> s \<and>
       {Key (Auth_ShaKey n)} \<in> key_sets (PriKey S) (crypts (Log -` spied s))"
 by (drule pwd_owner_iv_msg, simp add: pwd_spy_sep_map_def split_def,
  (erule conjE)+, ((rule conjI | erule key_sets_crypts_subset), blast)+)
 
 
 fun pwd_spy_sep_agr_state :: "agent_id \<Rightarrow> seskey_tuple \<Rightarrow> state" where
 "pwd_spy_sep_agr_state n (S, A, B, C, D) =
   insert (Spy, PubKey C) (pwd_spy_sep_map_state n (S, A, B, C, D))"
 
 proposition pwd_spy_sep_agr_rel:
  "n \<in> bad_prikey \<inter> bad_id_shakey \<Longrightarrow> s\<^sub>0 \<Turnstile> fst (pwd_spy_sep_agr n)"
     (is "_ \<Longrightarrow> _ \<Turnstile> ?t")
 by (rule rtrancl_into_rtrancl, erule pwd_spy_sep_map_rel, drule pwd_spy_sep_map_msg,
  subgoal_tac "(fst (pwd_spy_sep_map n), ?t) \<in> rel_sep", simp_all add: rel_def
  pwd_spy_sep_agr_def split_def, blast)
 
 proposition pwd_spy_sep_agr_msg:
  "n \<in> bad_prikey \<inter> bad_id_shakey \<Longrightarrow>
     case pwd_spy_sep_agr n of (s, S, A, B, C, D) \<Rightarrow>
       pwd_spy_sep_agr_state n (S, A, B, C, D) \<subseteq> s \<and>
       {Key (Auth_ShaKey n)} \<in> key_sets (PriKey S) (crypts (Log -` spied s))"
 by (drule pwd_spy_sep_map_msg, simp add: pwd_spy_sep_agr_def split_def,
  (erule conjE)+, ((rule conjI | erule key_sets_crypts_subset), blast)+)
 
 
 fun pwd_spy_sesk_state :: "agent_id \<Rightarrow> seskey_tuple \<Rightarrow> state" where
 "pwd_spy_sesk_state n (S, A, B, C, D) = (let SK = (Some S, {A, B}, {C, D}) in
   insert (Spy, SesKey SK) (pwd_spy_sep_agr_state n (S, A, B, C, D)))"
 
 proposition pwd_spy_sesk_rel:
  "n \<in> bad_prikey \<inter> bad_id_shakey \<Longrightarrow> s\<^sub>0 \<Turnstile> fst (pwd_spy_sesk n)"
     (is "_ \<Longrightarrow> _ \<Turnstile> ?t")
 by (rule rtrancl_into_rtrancl, erule pwd_spy_sep_agr_rel, drule pwd_spy_sep_agr_msg,
  subgoal_tac "(fst (pwd_spy_sep_agr n), ?t) \<in> rel_sesk", simp_all add: rel_def
  pwd_spy_sesk_def split_def Let_def, blast)
 
 proposition pwd_spy_sesk_msg:
  "n \<in> bad_prikey \<inter> bad_id_shakey \<Longrightarrow>
     case pwd_spy_sesk n of (s, S, A, B, C, D) \<Rightarrow>
       pwd_spy_sesk_state n (S, A, B, C, D) \<subseteq> s \<and>
       {Key (Auth_ShaKey n)} \<in> key_sets (PriKey S) (crypts (Log -` spied s))"
 by (drule pwd_spy_sep_agr_msg, simp add: pwd_spy_sesk_def split_def Let_def,
  (erule conjE)+, ((rule conjI | erule key_sets_crypts_subset), blast)+)
 
 
 fun pwd_spy_mult_state :: "agent_id \<Rightarrow> seskey_tuple \<Rightarrow> state" where
 "pwd_spy_mult_state n (S, A, B, C, D) =
   insert (Spy, Auth_PriK n \<otimes> B) (pwd_spy_sesk_state n (S, A, B, C, D))"
 
 proposition pwd_spy_mult_rel:
  "n \<in> bad_prikey \<inter> bad_id_shakey \<Longrightarrow> s\<^sub>0 \<Turnstile> fst (pwd_spy_mult n)"
     (is "_ \<Longrightarrow> _ \<Turnstile> ?t")
 by (rule rtrancl_into_rtrancl, erule pwd_spy_sesk_rel, drule pwd_spy_sesk_msg,
  subgoal_tac "(fst (pwd_spy_sesk n), ?t) \<in> rel_mult", simp_all add: rel_def
  pwd_spy_mult_def split_def, blast)
 
 proposition pwd_spy_mult_msg:
  "n \<in> bad_prikey \<inter> bad_id_shakey \<Longrightarrow>
     case pwd_spy_mult n of (s, S, A, B, C, D) \<Rightarrow>
       pwd_spy_mult_state n (S, A, B, C, D) \<subseteq> s \<and>
       {Key (Auth_ShaKey n)} \<in> key_sets (PriKey S) (crypts (Log -` spied s))"
 by (drule pwd_spy_sesk_msg, simp add: pwd_spy_mult_def split_def,
  (erule conjE)+, ((rule conjI | erule key_sets_crypts_subset), blast)+)
 
 
 fun pwd_spy_enc_pubk_state :: "agent_id \<Rightarrow> seskey_tuple \<Rightarrow> state" where
 "pwd_spy_enc_pubk_state n (S, A, B, C, D) =
   (let SK = (Some S, {A, B}, {C, D}) in
   insert (Spy, Crypt (SesK SK) (PubKey C))
     (pwd_spy_mult_state n (S, A, B, C, D)))"
 
 proposition pwd_spy_enc_pubk_rel:
  "n \<in> bad_prikey \<inter> bad_id_shakey \<Longrightarrow> s\<^sub>0 \<Turnstile> fst (pwd_spy_enc_pubk n)"
     (is "_ \<Longrightarrow> _ \<Turnstile> ?t")
 by (rule rtrancl_into_rtrancl, erule pwd_spy_mult_rel, drule pwd_spy_mult_msg,
  subgoal_tac "(fst (pwd_spy_mult n), ?t) \<in> rel_enc", simp_all add: rel_def
  pwd_spy_enc_pubk_def split_def Let_def, blast)
 
 proposition pwd_spy_enc_pubk_msg:
  "n \<in> bad_prikey \<inter> bad_id_shakey \<Longrightarrow>
     case pwd_spy_enc_pubk n of (s, S, A, B, C, D) \<Rightarrow>
       pwd_spy_enc_pubk_state n (S, A, B, C, D) \<subseteq> s \<and>
       {Key (Auth_ShaKey n)} \<in> key_sets (PriKey S) (crypts (Log -` spied s))"
 by (drule pwd_spy_mult_msg, simp add: pwd_spy_enc_pubk_def split_def Let_def,
  (erule conjE)+, ((rule conjI | erule key_sets_crypts_subset), blast)+)
 
 
 fun pwd_spy_enc_mult_state :: "agent_id \<Rightarrow> seskey_tuple \<Rightarrow> state" where
 "pwd_spy_enc_mult_state n (S, A, B, C, D) =
   (let SK = (Some S, {A, B}, {C, D}) in
   insert (Spy, Crypt (SesK SK) (Auth_PriK n \<otimes> B))
     (pwd_spy_enc_pubk_state n (S, A, B, C, D)))"
 
 proposition pwd_spy_enc_mult_rel:
  "n \<in> bad_prikey \<inter> bad_id_shakey \<Longrightarrow> s\<^sub>0 \<Turnstile> fst (pwd_spy_enc_mult n)"
     (is "_ \<Longrightarrow> _ \<Turnstile> ?t")
 by (rule rtrancl_into_rtrancl, erule pwd_spy_enc_pubk_rel, drule pwd_spy_enc_pubk_msg,
  subgoal_tac "(fst (pwd_spy_enc_pubk n), ?t) \<in> rel_enc", simp_all add: rel_def
  pwd_spy_enc_mult_def split_def Let_def, blast)
 
 proposition pwd_spy_enc_mult_msg:
  "n \<in> bad_prikey \<inter> bad_id_shakey \<Longrightarrow>
     case pwd_spy_enc_mult n of (s, S, A, B, C, D) \<Rightarrow>
       pwd_spy_enc_mult_state n (S, A, B, C, D) \<subseteq> s \<and>
       {Key (Auth_ShaKey n)} \<in> key_sets (PriKey S) (crypts (Log -` spied s))"
 by (drule pwd_spy_enc_pubk_msg, simp add: pwd_spy_enc_mult_def split_def Let_def,
  (erule conjE)+, ((rule conjI | erule key_sets_crypts_subset), blast)+)
 
 
 fun pwd_spy_enc_sign_state :: "agent_id \<Rightarrow> seskey_tuple \<Rightarrow> state" where
 "pwd_spy_enc_sign_state n (S, A, B, C, D) =
   (let SK = (Some S, {A, B}, {C, D}) in
   insert (Spy, Crypt (SesK SK) (Sign n (Auth_PriK n)))
     (pwd_spy_enc_mult_state n (S, A, B, C, D)))"
 
 proposition pwd_spy_enc_sign_rel:
  "n \<in> bad_prikey \<inter> bad_id_shakey \<Longrightarrow> s\<^sub>0 \<Turnstile> fst (pwd_spy_enc_sign n)"
     (is "_ \<Longrightarrow> _ \<Turnstile> ?t")
 by (rule rtrancl_into_rtrancl, erule pwd_spy_enc_mult_rel, drule pwd_spy_enc_mult_msg,
  subgoal_tac "(fst (pwd_spy_enc_mult n), ?t) \<in> rel_enc", simp_all add: rel_def
  pwd_spy_enc_sign_def split_def Let_def, blast)
 
 proposition pwd_spy_enc_sign_msg:
  "n \<in> bad_prikey \<inter> bad_id_shakey \<Longrightarrow>
     case pwd_spy_enc_sign n of (s, S, A, B, C, D) \<Rightarrow>
       pwd_spy_enc_sign_state n (S, A, B, C, D) \<subseteq> s \<and>
       {Key (Auth_ShaKey n)} \<in> key_sets (PriKey S) (crypts (Log -` spied s))"
 by (drule pwd_spy_enc_mult_msg, simp add: pwd_spy_enc_sign_def split_def Let_def,
  (erule conjE)+, ((rule conjI | erule key_sets_crypts_subset), blast)+)
 
 
 fun pwd_spy_con_state :: "agent_id \<Rightarrow> seskey_tuple \<Rightarrow> state" where
 "pwd_spy_con_state n (S, A, B, C, D) = (let SK = (Some S, {A, B}, {C, D}) in
   insert (Spy, \<lbrace>Crypt (SesK SK) (Auth_PriK n \<otimes> B),
     Crypt (SesK SK) (Sign n (Auth_PriK n))\<rbrace>)
     (pwd_spy_enc_sign_state n (S, A, B, C, D)))"
 
 proposition pwd_spy_con_rel:
  "n \<in> bad_prikey \<inter> bad_id_shakey \<Longrightarrow> s\<^sub>0 \<Turnstile> fst (pwd_spy_con n)"
     (is "_ \<Longrightarrow> _ \<Turnstile> ?t")
 by (rule rtrancl_into_rtrancl, erule pwd_spy_enc_sign_rel, drule pwd_spy_enc_sign_msg,
  subgoal_tac "(fst (pwd_spy_enc_sign n), ?t) \<in> rel_con", simp_all add: rel_def
  pwd_spy_con_def split_def Let_def, blast)
 
 proposition pwd_spy_con_msg:
  "n \<in> bad_prikey \<inter> bad_id_shakey \<Longrightarrow>
     case pwd_spy_con n of (s, S, A, B, C, D) \<Rightarrow>
       pwd_spy_con_state n (S, A, B, C, D) \<subseteq> s \<and>
       {Key (Auth_ShaKey n)} \<in> key_sets (PriKey S) (crypts (Log -` spied s))"
 by (drule pwd_spy_enc_sign_msg, simp add: pwd_spy_con_def split_def Let_def,
  (erule conjE)+, ((rule conjI | erule key_sets_crypts_subset), blast)+)
 
 
 fun pwd_spy_iv_state :: "agent_id \<Rightarrow> seskey_tuple \<Rightarrow> state" where
 "pwd_spy_iv_state n (S, A, B, C, D) = (let SK = (Some S, {A, B}, {C, D}) in
   insert (Spy, Token n (Auth_PriK n) B C SK)
     (pwd_spy_con_state n (S, A, B, C, D)))"
 
 proposition pwd_spy_iv_rel:
  "n \<in> bad_prikey \<inter> bad_id_shakey \<Longrightarrow> s\<^sub>0 \<Turnstile> fst (pwd_spy_iv n)"
     (is "_ \<Longrightarrow> _ \<Turnstile> ?t")
 by (rule rtrancl_into_rtrancl, erule pwd_spy_con_rel, drule pwd_spy_con_msg,
  subgoal_tac "(fst (pwd_spy_con n), ?t) \<in> rel_con", simp_all add: rel_def
  pwd_spy_iv_def split_def Let_def, blast)
 
 proposition pwd_spy_iv_msg:
  "n \<in> bad_prikey \<inter> bad_id_shakey \<Longrightarrow>
     case pwd_spy_iv n of (s, S, A, B, C, D) \<Rightarrow>
       pwd_spy_iv_state n (S, A, B, C, D) \<subseteq> s \<and>
       {Key (Auth_ShaKey n)} \<in> key_sets (PriKey S) (crypts (Log -` spied s))"
 by (drule pwd_spy_con_msg, simp add: pwd_spy_iv_def split_def Let_def,
  (erule conjE)+, ((rule conjI | erule key_sets_crypts_subset), blast)+)
 
 
 fun pwd_owner_v_state :: "agent_id \<Rightarrow> seskey_tuple \<Rightarrow> state" where
 "pwd_owner_v_state n (S, A, B, C, D) = (let SK = (Some S, {A, B}, {C, D}) in
   insert (Spy, Crypt (SesK SK) (Pwd n)) (pwd_spy_iv_state n (S, A, B, C, D)))"
 
 proposition pwd_owner_v_rel:
  "n \<in> bad_prikey \<inter> bad_id_shakey \<Longrightarrow> s\<^sub>0 \<Turnstile> fst (pwd_owner_v n)"
     (is "_ \<Longrightarrow> _ \<Turnstile> ?t")
 by (rule rtrancl_into_rtrancl, erule pwd_spy_iv_rel, drule pwd_spy_iv_msg,
  subgoal_tac "(fst (pwd_spy_iv n), ?t) \<in> rel_owner_v", simp_all add: rel_def
  pwd_owner_v_def split_def Let_def, (rule exI)+, blast)
 
 proposition pwd_owner_v_msg:
  "n \<in> bad_prikey \<inter> bad_id_shakey \<Longrightarrow>
     let (s, S, A, B, C, D) = pwd_owner_v n; SK = (Some S, {A, B}, {C, D}) in
       pwd_owner_v_state n (S, A, B, C, D) \<subseteq> s \<and>
       {Key (Auth_ShaKey n)} \<in> key_sets (PriKey S) (crypts (Log -` spied s)) \<and>
       {SesKey SK} \<in> key_sets (Pwd n) (crypts (Log -` spied s))"
 by (drule pwd_spy_iv_msg, simp add: pwd_owner_v_def split_def Let_def, (erule conjE)+,
  (rule conjI, (erule key_sets_crypts_subset)?, blast)+, simp add: Image_def, simp
  only: Collect_disj_eq crypts_union key_sets_union, simp add: crypts_insert
  key_sets_insert)
 
 
 abbreviation pwd_spy_dec_state :: "agent_id \<Rightarrow> seskey_tuple \<Rightarrow> state" where
 "pwd_spy_dec_state n x \<equiv> insert (Spy, Pwd n) (pwd_owner_v_state n x)"
 
 proposition pwd_spy_dec_rel:
  "n \<in> bad_prikey \<inter> bad_id_shakey \<Longrightarrow> s\<^sub>0 \<Turnstile> fst (pwd_spy_dec n)"
     (is "_ \<Longrightarrow> _ \<Turnstile> ?t")
 by (rule rtrancl_into_rtrancl, erule pwd_owner_v_rel, drule pwd_owner_v_msg,
  subgoal_tac "(fst (pwd_owner_v n), ?t) \<in> rel_dec", simp_all add: rel_def
  pwd_spy_dec_def split_def Let_def, (rule exI)+, auto)
 
 proposition pwd_spy_dec_msg:
  "n \<in> bad_prikey \<inter> bad_id_shakey \<Longrightarrow>
     let (s, S, A, B, C, D) = pwd_spy_dec n; SK = (Some S, {A, B}, {C, D}) in
       pwd_spy_dec_state n (S, A, B, C, D) \<subseteq> s \<and>
       {Key (Auth_ShaKey n)} \<in> key_sets (PriKey S) (crypts (Log -` spied s)) \<and>
       {SesKey SK} \<in> key_sets (Pwd n) (crypts (Log -` spied s))"
 by (drule pwd_owner_v_msg, simp add: pwd_spy_dec_def split_def Let_def,
  (erule conjE)+, ((rule conjI)?, (erule key_sets_crypts_subset)?, blast)+)
 
 
 fun pwd_spy_id_prik_state :: "agent_id \<Rightarrow> seskey_tuple \<Rightarrow> state" where
 "pwd_spy_id_prik_state n (S, A, B, C, D) =
   insert (Spy, \<langle>n, PriKey S\<rangle>) (pwd_spy_dec_state n (S, A, B, C, D))"
 
 proposition pwd_spy_id_prik_rel:
  "n \<in> bad_prikey \<inter> bad_id_shakey \<Longrightarrow> s\<^sub>0 \<Turnstile> fst (pwd_spy_id_prik n)"
     (is "_ \<Longrightarrow> _ \<Turnstile> ?t")
 by (rule rtrancl_into_rtrancl, erule pwd_spy_dec_rel, drule pwd_spy_dec_msg,
  subgoal_tac "(fst (pwd_spy_dec n), ?t) \<in> rel_id_crypt", simp_all add: rel_def
  pwd_spy_id_prik_def split_def Let_def, (rule exI)+, blast)
 
 proposition pwd_spy_id_prik_msg:
  "n \<in> bad_prikey \<inter> bad_id_shakey \<Longrightarrow>
     let (s, S, A, B, C, D) = pwd_spy_id_prik n;
       SK = (Some S, {A, B}, {C, D}) in
       pwd_spy_id_prik_state n (S, A, B, C, D) \<subseteq> s \<and>
       {SesKey SK} \<in> key_sets (Pwd n) (crypts (Log -` spied s))"
 by (drule pwd_spy_dec_msg, simp add: pwd_spy_id_prik_def split_def Let_def,
  (erule conjE)+, ((rule conjI | erule key_sets_crypts_subset), blast)+)
 
 
 fun pwd_spy_id_pubk_state :: "agent_id \<Rightarrow> seskey_tuple \<Rightarrow> state" where
 "pwd_spy_id_pubk_state n (S, A, B, C, D) =
   insert (Spy, \<langle>n, PubKey S\<rangle>) (pwd_spy_id_prik_state n (S, A, B, C, D))"
 
 proposition pwd_spy_id_pubk_rel:
  "n \<in> bad_prikey \<inter> bad_id_shakey \<Longrightarrow> s\<^sub>0 \<Turnstile> fst (pwd_spy_id_pubk n)"
     (is "_ \<Longrightarrow> _ \<Turnstile> ?t")
 by (rule rtrancl_into_rtrancl, erule pwd_spy_id_prik_rel, drule pwd_spy_id_prik_msg,
  subgoal_tac "(fst (pwd_spy_id_prik n), ?t) \<in> rel_id_invk", simp_all add: rel_def
  pwd_spy_id_pubk_def split_def Let_def, (rule exI)+, auto)
 
 proposition pwd_spy_id_pubk_msg:
  "n \<in> bad_prikey \<inter> bad_id_shakey \<Longrightarrow>
     let (s, S, A, B, C, D) = pwd_spy_id_pubk n;
       SK = (Some S, {A, B}, {C, D}) in
       pwd_spy_id_pubk_state n (S, A, B, C, D) \<subseteq> s \<and>
       {SesKey SK} \<in> key_sets (Pwd n) (crypts (Log -` spied s))"
 by (drule pwd_spy_id_prik_msg, simp add: pwd_spy_id_pubk_def split_def Let_def,
  (erule conjE)+, ((rule conjI | erule key_sets_crypts_subset), blast)+)
 
 
 fun pwd_spy_id_sesk_state :: "agent_id \<Rightarrow> seskey_tuple \<Rightarrow> state" where
 "pwd_spy_id_sesk_state n (S, A, B, C, D) =
   (let SK = (Some S, {A, B}, {C, D}) in
   insert (Spy, \<langle>n, SesKey SK\<rangle>) (pwd_spy_id_pubk_state n (S, A, B, C, D)))"
 
 proposition pwd_spy_id_sesk_rel:
  "n \<in> bad_prikey \<inter> bad_id_shakey \<Longrightarrow> s\<^sub>0 \<Turnstile> fst (pwd_spy_id_sesk n)"
     (is "_ \<Longrightarrow> _ \<Turnstile> ?t")
 by (rule rtrancl_into_rtrancl, erule pwd_spy_id_pubk_rel, drule pwd_spy_id_pubk_msg,
  subgoal_tac "(fst (pwd_spy_id_pubk n), ?t) \<in> rel_id_sesk", simp_all add: rel_def
  pwd_spy_id_sesk_def split_def Let_def, rule exI, rule exI, rule exI
  [of _ "Some (fst (snd (pwd_spy_id_pubk n)))"], auto)
 
 proposition pwd_spy_id_sesk_msg:
  "n \<in> bad_prikey \<inter> bad_id_shakey \<Longrightarrow>
     let (s, S, A, B, C, D) = pwd_spy_id_sesk n;
       SK = (Some S, {A, B}, {C, D}) in
       pwd_spy_id_sesk_state n (S, A, B, C, D) \<subseteq> s \<and>
       {SesKey SK} \<in> key_sets (Pwd n) (crypts (Log -` spied s))"
 by (drule pwd_spy_id_pubk_msg, simp add: pwd_spy_id_sesk_def split_def Let_def,
  (erule conjE)+, ((rule conjI | erule key_sets_crypts_subset), blast)+)
 
 
 abbreviation pwd_spy_id_pwd_state :: "agent_id \<Rightarrow> seskey_tuple \<Rightarrow> state" where
 "pwd_spy_id_pwd_state n x \<equiv> insert (Spy, \<langle>n, Pwd n\<rangle>) (pwd_spy_id_sesk_state n x)"
 
 proposition pwd_spy_id_pwd_rel:
  "n \<in> bad_prikey \<inter> bad_id_shakey \<Longrightarrow> s\<^sub>0 \<Turnstile> fst (pwd_spy_id_pwd n)"
     (is "_ \<Longrightarrow> _ \<Turnstile> ?t")
 by (rule rtrancl_into_rtrancl, erule pwd_spy_id_sesk_rel, drule pwd_spy_id_sesk_msg,
  subgoal_tac "(fst (pwd_spy_id_sesk n), ?t) \<in> rel_id_crypt", simp_all add: rel_def
  pwd_spy_id_pwd_def split_def Let_def, (rule exI)+, blast)
 
 proposition pwd_spy_id_pwd_msg:
  "n \<in> bad_prikey \<inter> bad_id_shakey \<Longrightarrow>
     case pwd_spy_id_pwd n of (s, S, A, B, C, D) \<Rightarrow>
       pwd_spy_id_pwd_state n (S, A, B, C, D) \<subseteq> s"
 by (drule pwd_spy_id_sesk_msg, simp add: pwd_spy_id_pwd_def split_def Let_def,
  blast)
 
 
 theorem pwd_compromised:
  "n \<in> bad_prikey \<inter> bad_id_shakey \<Longrightarrow> \<exists>s. s\<^sub>0 \<Turnstile> s \<and> {Pwd n, \<langle>n, Pwd n\<rangle>} \<subseteq> spied s"
 by (rule exI [of _ "fst (pwd_spy_id_pwd n)"], rule conjI, erule pwd_spy_id_pwd_rel,
  drule pwd_spy_id_pwd_msg, simp add: split_def)
 
 
-end
+end
\ No newline at end of file