Theory Possibility

(*  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 ‹
\label{Possibility}
›


type_synonym seskey_tuple = "key_id × key_id × key_id × key_id × key_id"

type_synonym stage = "state × seskey_tuple"


abbreviation pred_asset_i :: "agent_id  state  stage  bool" where
"pred_asset_i n s x 
  S. PriKey S  used s  x = (insert (Asset n, PriKey S) s 
    {Asset n, Spy} × {Crypt (Auth_ShaKey n) (PriKey S)} 
    {(Spy, Log (Crypt (Auth_ShaKey n) (PriKey S)))},
    S, 0, 0, 0, 0)"

definition run_asset_i :: "agent_id  state  stage" where
"run_asset_i n s  SOME x. pred_asset_i n s x"


abbreviation pred_owner_ii :: "agent_id  stage  stage  bool" where
"pred_owner_ii n x y  case x of (s, S, _) 
  A. PriKey A  used s  y = (insert (Owner n, PriKey A) s 
    {Owner n, Spy} × {Num 1, PubKey A} 
    {Spy} × Log ` {Crypt (Auth_ShaKey n) (PriKey S), Num 1, PubKey A},
    S, A, 0, 0, 0)"

definition run_owner_ii :: "agent_id  state  stage" where
"run_owner_ii n s  SOME x. pred_owner_ii n (run_asset_i n s) x"


abbreviation pred_asset_ii :: "agent_id  stage  stage  bool" where
"pred_asset_ii n x y  case x of (s, S, A, _) 
  B. PriKey B  used s  y = (insert (Asset n, PriKey B) s 
    {Asset n, Spy} × {Num 2, PubKey B} 
    {Spy} × Log ` {Num 1, PubKey A, Num 2, PubKey B},
    S, A, B, 0, 0)"

definition run_asset_ii :: "agent_id  state  stage" where
"run_asset_ii n s  SOME x. pred_asset_ii n (run_owner_ii n s) x"


abbreviation pred_owner_iii :: "agent_id  stage  stage  bool" where
"pred_owner_iii n x y  case x of (s, S, A, B, _) 
  C. PriKey C  used s  y = (insert (Owner n, PriKey C) s 
    {Owner n, Spy} × {Num 3, PubKey C} 
    {Spy} × Log ` {Num 2, PubKey B, Num 3, PubKey C},
    S, A, B, C, 0)"

definition run_owner_iii :: "agent_id  state  stage" where
"run_owner_iii n s  SOME x. pred_owner_iii n (run_asset_ii n s) x"


abbreviation pred_asset_iii :: "agent_id  stage  stage  bool" where
"pred_asset_iii n x y  case x of (s, S, A, B, C, _) 
  D. PriKey D  used s  y = (insert (Asset n, PriKey D) s 
    {Asset n, Spy} × {Num 4, PubKey D} 
    {Spy} × Log ` {Num 3, PubKey C, Num 4, PubKey D},
    S, A, B, C, D)"

definition run_asset_iii :: "agent_id  state  stage" where
"run_asset_iii n s  SOME x. pred_asset_iii n (run_owner_iii n s) x"


abbreviation stage_owner_iv :: "agent_id  stage  stage" where
"stage_owner_iv n x  let (s, S, A, B, C, D) = x;
  SK = (Some S, {A, B}, {C, D}) in
  (insert (Owner n, SesKey SK) s 
    {Owner n, Spy} × {Crypt (SesK SK) (PubKey D)} 
    {Spy} × Log ` {Num 4, PubKey D, Crypt (SesK SK) (PubKey D)},
    S, A, B, C, D)"

definition run_owner_iv :: "agent_id  state  stage" where
"run_owner_iv n s  stage_owner_iv n (run_asset_iii n s)"


abbreviation stage_asset_iv :: "agent_id  stage  stage" where
"stage_asset_iv n x  let (s, S, A, B, C, D) = x;
  SK = (Some S, {A, B}, {C, D}) in
  (s  {Asset n} × {SesKey SK, PubKey B} 
    {Asset n, Spy} × {Token n (Auth_PriK n) B C SK} 
    {Spy} × 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  state  stage" where
"run_asset_iv n s  stage_asset_iv n (run_owner_iv n s)"


abbreviation stage_owner_v :: "agent_id  stage  stage" where
"stage_owner_v n x  let (s, S, A, B, C, D) = x;
  SK = (Some S, {A, B}, {C, D}) in
  (s  {Owner n, Spy} × {Crypt (SesK SK) (Pwd n)} 
    {Spy} × 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  state  stage" where
"run_owner_v n s  stage_owner_v n (run_asset_iv n s)"


abbreviation stage_asset_v :: "agent_id  stage  stage" where
"stage_asset_v n x  let (s, S, A, B, C, D) = x;
  SK = (Some S, {A, B}, {C, D}) in
  (s  {Asset n, Spy} × {Crypt (SesK SK) (Num 0)} 
    {Spy} × Log ` {Crypt (SesK SK) (Pwd n), Crypt (SesK SK) (Num 0)},
    S, A, B, C, D)"

definition run_asset_v :: "agent_id  state  stage" where
"run_asset_v n s  stage_asset_v n (run_owner_v n s)"


lemma prikey_unused_1:
 "infinite {A. PriKey A  used s0}"
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 _ "λn. 0"], simp)

lemma prikey_unused_2:
 "s  s'; infinite {A. PriKey A  used s} 
    infinite {A. PriKey A  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:
 "s0  s  A. PriKey A  used s"
by (subgoal_tac "infinite {A. PriKey A  used s}", drule infinite_imp_nonempty,
 simp, erule rtrancl_induct, rule prikey_unused_1, rule prikey_unused_2)


lemma pubkey_unused_1:
 "s  s'; PubKey A  parts (used s)  PriKey A  used s;
    PubKey A  parts (used s') 
  PriKey A  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]:
 "s0  s 
    PriKey A  used s 
  PubKey A  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:
 "s0  s  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:
 "s0  s  s  fst (run_asset_i n s)"
    (is "_  _  ?t")
by (drule run_asset_i_ex [of _ n], rule r_into_rtrancl,
 subgoal_tac "(s, ?t)  rel_asset_i", simp_all add: rel_def, erule exE, auto)

proposition run_asset_i_msg:
 "s0  s 
    case run_asset_i n s of (s', S, _) 
      (Asset n, Crypt (Auth_ShaKey n) (PriKey S))  s'"
by (drule run_asset_i_ex [of _ n], auto)

proposition run_asset_i_nonce:
 "s0  s  PriKey (fst (snd (run_asset_i n s)))  used s"
by (drule run_asset_i_ex [of _ n], auto)

proposition run_asset_i_unused:
 "s0  s  A. PriKey A  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:
 "s0  s  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:
 "s0  s  s  fst (run_owner_ii n s)"
    (is "_  _  ?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)  rel_owner_ii",
 simp_all add: rel_def split_def, erule exE, (rule exI)+, auto)

proposition run_owner_ii_msg:
 "s0  s 
    case run_owner_ii n s of (s', S, A, _) 
      {(Asset n, Crypt (Auth_ShaKey n) (PriKey S)),
        (Owner n, Num 1, PubKey A)}  s'"
by (frule run_asset_i_msg [of _ n], drule run_owner_ii_ex [of _ n], auto)

proposition run_owner_ii_nonce:
 "s0  s  PriKey (fst (snd (run_owner_ii n s)))  used s"
by (frule run_asset_i_nonce [of _ n], drule run_owner_ii_ex [of _ n], auto)

proposition run_owner_ii_unused:
 "s0  s  B. PriKey B  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:
 "s0  s  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:
 "s0  s  s  fst (run_asset_ii n s)"
    (is "_  _  ?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)  rel_asset_ii",
 simp_all add: rel_def split_def, erule exE, (rule exI)+, auto)

proposition run_asset_ii_msg:
  assumes A: "s0  s"
  shows "case run_asset_ii n s of (s', S, A, B, _) 
    insert (Owner n, Num 1, PubKey A)
      ({Asset n} × {Crypt (Auth_ShaKey n) (PriKey S),
       Num 2, PubKey B})  s' 
    (Asset n, PubKey B)  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:
 "s0  s  PriKey (fst (snd (run_asset_ii n s)))  used s"
by (frule run_owner_ii_nonce [of _ n], drule run_asset_ii_ex [of _ n], auto)

proposition run_asset_ii_unused:
 "s0  s  C. PriKey C  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:
 "s0  s  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:
 "s0  s  s  fst (run_owner_iii n s)"
    (is "_  _  ?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)  rel_owner_iii",
 simp_all add: rel_def split_def, erule exE, (rule exI)+, auto)

proposition run_owner_iii_msg:
 "s0  s 
    case run_owner_iii n s of (s', S, A, B, C, _) 
      {Asset n} × {Crypt (Auth_ShaKey n) (PriKey S), Num 2, PubKey B} 
      {Owner n} × {Num 1, PubKey A, Num 3, PubKey C}  s' 
      (Asset n, PubKey B)  s'"
by (frule run_asset_ii_msg [of _ n], drule run_owner_iii_ex [of _ n], auto)

proposition run_owner_iii_nonce:
 "s0  s  PriKey (fst (snd (run_owner_iii n s)))  used s"
by (frule run_asset_ii_nonce [of _ n], drule run_owner_iii_ex [of _ n], auto)

proposition run_owner_iii_unused:
 "s0  s  D. PriKey D  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:
 "s0  s  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:
 "s0  s  s  fst (run_asset_iii n s)"
    (is "_  _  ?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)  rel_asset_iii",
 simp_all add: rel_def split_def, erule exE, (rule exI)+, auto)

proposition run_asset_iii_msg:
 "s0  s 
    case run_asset_iii n s of (s', S, A, B, C, D) 
      {Asset n} × {Crypt (Auth_ShaKey n) (PriKey S), Num 2, PubKey B,
        Num 4, PubKey D} 
      {Owner n} × {Num 1, PubKey A, Num 3, PubKey C}  s' 
      (Asset n, PubKey B)  s'"
by (frule run_owner_iii_msg [of _ n], drule run_asset_iii_ex [of _ n], auto)

proposition run_asset_iii_nonce:
 "s0  s  PriKey (fst (snd (run_asset_iii n s)))  used s"
by (frule run_owner_iii_nonce [of _ n], drule run_asset_iii_ex [of _ n], auto)


lemma run_owner_iv_rel_1:
 "s0  s; run_asset_iii n s = (s', S, A, B, C, D) 
    s  fst (run_owner_iv n s)"
      (is "_; _  _  ?t")
by (rule rtrancl_into_rtrancl, erule run_asset_iii_rel [of _ n], drule run_asset_iii_msg
 [of _ n], subgoal_tac "(s', ?t)  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:
 "s0  s  s  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:
 "s0  s 
    let (s', S, A, B, C, D) = run_owner_iv n s;
      SK = (Some S, {A, B}, {C, D}) in
      {Asset n} × {Crypt (Auth_ShaKey n) (PriKey S), Num 2, PubKey B,
        Num 4, PubKey D} 
      {Owner n} × {Num 1, PubKey A, Num 3, PubKey C, SesKey SK,
        Crypt (SesK SK) (PubKey D)}  s' 
      (Asset n, PubKey B)  s'"
by (drule run_asset_iii_msg [of _ n], simp add: run_owner_iv_def split_def Let_def)

proposition run_owner_iv_nonce:
 "s0  s  PriKey (fst (snd (run_owner_iv n s)))  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:
 "s0  s  s  fst (run_asset_iv n s)"
    (is "_  _  ?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)  rel_asset_iv", simp_all add:
 rel_def run_asset_iv_def split_def Let_def, blast)

proposition run_asset_iv_msg:
 "s0  s 
    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} × {SesKey SK, Token n (Auth_PriK n) B C SK})  s'"
by (drule run_owner_iv_msg [of _ n], simp add: run_asset_iv_def split_def Let_def)

proposition run_asset_iv_nonce:
 "s0  s  PriKey (fst (snd (run_asset_iv n s)))  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:
 "s0  s  s  fst (run_owner_v n s)"
    (is "_  _  ?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)  rel_owner_v", simp_all add:
 rel_def run_owner_v_def split_def Let_def, blast)

proposition run_owner_v_msg:
 "s0  s 
    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))}  s'"
by (drule run_asset_iv_msg [of _ n], simp add: run_owner_v_def split_def Let_def)

proposition run_owner_v_nonce:
 "s0  s  PriKey (fst (snd (run_owner_v n s)))  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:
 "s0  s  s  fst (run_asset_v n s)"
    (is "_  _  ?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)  rel_asset_v", simp_all add:
 rel_def run_asset_v_def split_def Let_def, blast)

proposition run_asset_v_msg:
 "s0  s 
    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))}  s'"
by (drule run_owner_v_msg [of _ n], simp add: run_asset_v_def split_def Let_def)

proposition run_asset_v_nonce:
 "s0  s  PriKey (fst (snd (run_asset_v n s)))  used s"
by (drule run_owner_v_nonce [of _ n], simp add: run_asset_v_def split_def Let_def)


lemma runs_unbounded_1:
 "s0  s; run_asset_v n s = (s', S, A, B, C, D) 
    s' S SK. (Asset n, Crypt (Auth_ShaKey n) (PriKey S))  s 
      {(Owner n, Crypt (SesK SK) (Pwd n)),
       (Asset n, Crypt (SesK SK) (Num 0))}  s' 
      s  s'  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:
 "s0  s  s' S SK. s  s'  fst SK = Some S 
    (Asset n, Crypt (Auth_ShaKey n) (PriKey S))  s 
    {(Owner n, Crypt (SesK SK) (Pwd n)),
     (Asset n, Crypt (SesK SK) (Num 0))}  s'"
by (insert runs_unbounded_1, cases "run_asset_v n s", blast)


definition pwd_spy_i :: "agent_id  stage" where
"pwd_spy_i n 
  (insert (Spy, Crypt (Auth_ShaKey n) (Auth_PriKey n)) s0,
    Auth_PriK n, 0, 0, 0, 0)"

definition pwd_owner_ii :: "agent_id  stage" where
"pwd_owner_ii n  SOME x. pred_owner_ii n (pwd_spy_i n) x"

definition pwd_spy_ii :: "agent_id  stage" where
"pwd_spy_ii n 
  case pwd_owner_ii n of (s, S, A, _) 
    (insert (Spy, Num 2, PubKey S) s, S, A, S, 0, 0)"

definition pwd_owner_iii :: "agent_id  stage" where
"pwd_owner_iii n  SOME x. pred_owner_iii n (pwd_spy_ii n) x"

definition pwd_spy_iii :: "agent_id  stage" where
"pwd_spy_iii n 
  case pwd_owner_iii n of (s, S, A, B, C, _) 
    (insert (Spy, Num 4, PubKey S) s, S, A, B, C, S)"

definition pwd_owner_iv :: "agent_id  stage" where
"pwd_owner_iv n  stage_owner_iv n (pwd_spy_iii n)"


definition pwd_spy_sep_map :: "agent_id  stage" where
"pwd_spy_sep_map n 
  case pwd_owner_iv n of (s, S, A, B, C, D) 
    (insert (Spy, PubKey A) s, S, A, B, C, D)"

definition pwd_spy_sep_agr :: "agent_id  stage" where
"pwd_spy_sep_agr n 
  case pwd_spy_sep_map n of (s, S, A, B, C, D) 
    (insert (Spy, PubKey C) s, S, A, B, C, D)"

definition pwd_spy_sesk :: "agent_id  stage" where
"pwd_spy_sesk n 
  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  stage" where
"pwd_spy_mult n 
  case pwd_spy_sesk n of (s, S, A, B, C, D) 
    (insert (Spy, Auth_PriK n  B) s, S, A, B, C, D)"

definition pwd_spy_enc_pubk :: "agent_id  stage" where
"pwd_spy_enc_pubk n 
  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  stage" where
"pwd_spy_enc_mult n 
  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  B)) s, S, A, B, C, D)"

definition pwd_spy_enc_sign :: "agent_id  stage" where
"pwd_spy_enc_sign n 
  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  stage" where
"pwd_spy_con n 
  let (s, S, A, B, C, D) = pwd_spy_enc_sign n;
    SK = (Some S, {A, B}, {C, D}) in
    (insert (Spy, Crypt (SesK SK) (Auth_PriK n  B),
      Crypt (SesK SK) (Sign n (Auth_PriK n))) s, S, A, B, C, D)"

definition pwd_spy_iv :: "agent_id  stage" where
"pwd_spy_iv n 
  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  stage" where
"pwd_owner_v n  stage_owner_v n (pwd_spy_iv n)"

definition pwd_spy_dec :: "agent_id  stage" where
"pwd_spy_dec n 
  case pwd_owner_v n of (s, S, A, B, C, D) 
    (insert (Spy, Pwd n) s, S, A, B, C, D)"

definition pwd_spy_id_prik :: "agent_id  stage" where
"pwd_spy_id_prik n 
  case pwd_spy_dec n of (s, S, A, B, C, D) 
    (insert (Spy, n, PriKey S) s, S, A, B, C, D)"

definition pwd_spy_id_pubk :: "agent_id  stage" where
"pwd_spy_id_pubk n 
  case pwd_spy_id_prik n of (s, S, A, B, C, D) 
    (insert (Spy, n, PubKey S) s, S, A, B, C, D)"

definition pwd_spy_id_sesk :: "agent_id  stage" where
"pwd_spy_id_sesk n 
  let (s, S, A, B, C, D) = pwd_spy_id_pubk n;
    SK = (Some S, {A, B}, {C, D}) in
    (insert (Spy, n, SesKey SK) s, S, A, B, C, D)"

definition pwd_spy_id_pwd :: "agent_id  stage" where
"pwd_spy_id_pwd n 
  case pwd_spy_id_sesk n of (s, S, A, B, C, D) 
    (insert (Spy, n, Pwd n) s, S, A, B, C, D)"


proposition key_sets_crypts_subset:
 "U  key_sets X (crypts (Log -` spied H)); H  H' 
    U  key_sets X (crypts (Log -` spied H'))"
      (is "_  ?A; _  _")
by (rule subsetD [of ?A], rule key_sets_mono, rule crypts_mono, blast)


fun pwd_spy_i_state :: "agent_id  seskey_tuple  state" where
"pwd_spy_i_state n (S, _) = {Spy} × ({PriKey S, PubKey S, Key (Auth_ShaKey n),
  Auth_PriKey n, Sign n (Auth_PriK n), Crypt (Auth_ShaKey n) (PriKey S),
  n, Key (Auth_ShaKey n)}  range Num)"

proposition pwd_spy_i_rel:
 "n  bad_prikey  bad_id_shakey  s0  fst (pwd_spy_i n)"
    (is "_  _  ?t")
by (rule r_into_rtrancl, subgoal_tac "(s0, ?t)  rel_enc", simp_all add: rel_def
 pwd_spy_i_def, blast)

proposition pwd_spy_i_msg:
 "n  bad_prikey  bad_id_shakey 
    case pwd_spy_i n of (s, S, A, B, C, D) 
      pwd_spy_i_state n (S, A, B, C, D)  s"
by (simp add: pwd_spy_i_def, blast)

proposition pwd_spy_i_unused:
 "n  bad_prikey  bad_id_shakey  A. PriKey A  used (fst (pwd_spy_i n))"
by (drule pwd_spy_i_rel, rule prikey_unused)


fun pwd_owner_ii_state :: "agent_id  seskey_tuple  state" where
"pwd_owner_ii_state n (S, A, B, C, D) =
  pwd_spy_i_state n (S, A, B, C, D)  {Owner n, Spy} × {Num 1, PubKey A}"

proposition pwd_owner_ii_ex:
 "n  bad_prikey  bad_id_shakey 
    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  bad_prikey  bad_id_shakey  s0  fst (pwd_owner_ii n)"
    (is "_  _  ?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)  rel_owner_ii",
 simp_all add: rel_def split_def, erule exE, rule exI, auto)

proposition pwd_owner_ii_msg:
 "n  bad_prikey  bad_id_shakey 
    case pwd_owner_ii n of (s, S, A, B, C, D) 
      pwd_owner_ii_state n (S, A, B, C, D)  s 
      {Key (Auth_ShaKey n)}  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  seskey_tuple  state" where
"pwd_spy_ii_state n (S, A, B, C, D) =
  pwd_owner_ii_state n (S, A, B, C, D)  {Spy} × {PriKey B,
    Num 2, PubKey B}"

proposition pwd_spy_ii_rel:
 "n  bad_prikey  bad_id_shakey  s0  fst (pwd_spy_ii n)"
    (is "_  _  ?t")
by (rule rtrancl_into_rtrancl, erule pwd_owner_ii_rel, drule pwd_owner_ii_msg,
 subgoal_tac "(fst (pwd_owner_ii n), ?t)  rel_con", simp_all add: rel_def
 pwd_spy_ii_def split_def, blast)

proposition pwd_spy_ii_msg:
 "n  bad_prikey  bad_id_shakey 
    case pwd_spy_ii n of (s, S, A, B, C, D) 
      pwd_spy_ii_state n (S, A, B, C, D)  s 
      {Key (Auth_ShaKey n)}  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  bad_prikey  bad_id_shakey  C. PriKey C  used (fst (pwd_spy_ii n))"
by (drule pwd_spy_ii_rel, rule prikey_unused)


fun pwd_owner_iii_state :: "agent_id  seskey_tuple  state" where
"pwd_owner_iii_state n (S, A, B, C, D) =
  pwd_spy_ii_state n (S, A, B, C, D)  {Owner n, Spy} × {Num 3, PubKey C}"

proposition pwd_owner_iii_ex:
 "n  bad_prikey  bad_id_shakey 
    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  bad_prikey  bad_id_shakey  s0  fst (pwd_owner_iii n)"
    (is "_  _  ?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)  rel_owner_iii",
 simp_all add: rel_def split_def, rule exI, rule exI, auto)

proposition pwd_owner_iii_msg:
 "n  bad_prikey  bad_id_shakey 
    case pwd_owner_iii n of (s, S, A, B, C, D) 
      pwd_owner_iii_state n (S, A, B, C, D)  s 
      {Key (Auth_ShaKey n)}  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  seskey_tuple  state" where
"pwd_spy_iii_state n (S, A, B, C, D) =
  pwd_owner_iii_state n (S, A, B, C, D)  {Spy} × {PriKey D,
    Num 4, PubKey D}"

proposition pwd_spy_iii_rel:
 "n  bad_prikey  bad_id_shakey  s0  fst (pwd_spy_iii n)"
    (is "_  _  ?t")
by (rule rtrancl_into_rtrancl, erule pwd_owner_iii_rel, drule pwd_owner_iii_msg,
 subgoal_tac "(fst (pwd_owner_iii n), ?t)  rel_con", simp_all add: rel_def
 pwd_spy_iii_def split_def, blast)

proposition pwd_spy_iii_msg:
 "n  bad_prikey  bad_id_shakey 
    case pwd_spy_iii n of (s, S, A, B, C, D) 
      pwd_spy_iii_state n (S, A, B, C, D)  s 
      {Key (Auth_ShaKey n)}  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  seskey_tuple  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:
 "n  bad_prikey  bad_id_shakey; pwd_spy_iii n = (s, S, A, B, C, D) 
    s0  fst (pwd_owner_iv n)"
      (is "_; _  _  ?t")
by (rule rtrancl_into_rtrancl, erule pwd_spy_iii_rel, drule pwd_spy_iii_msg,
 subgoal_tac "(s, ?t)  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  bad_prikey  bad_id_shakey  s0  fst (pwd_owner_iv n)"
by (insert pwd_owner_iv_rel_1, cases "pwd_spy_iii n", simp)

proposition pwd_owner_iv_msg:
 "n  bad_prikey  bad_id_shakey 
    case pwd_owner_iv n of (s, S, A, B, C, D) 
      pwd_owner_iv_state n (S, A, B, C, D)  s 
      {Key (Auth_ShaKey n)}  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  seskey_tuple  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  bad_prikey  bad_id_shakey  s0  fst (pwd_spy_sep_map n)"
    (is "_  _  ?t")
by (rule rtrancl_into_rtrancl, erule pwd_owner_iv_rel, drule pwd_owner_iv_msg,
 subgoal_tac "(fst (pwd_owner_iv n), ?t)  rel_sep", simp_all add: rel_def
 pwd_spy_sep_map_def split_def, blast)

proposition pwd_spy_sep_map_msg:
 "n  bad_prikey  bad_id_shakey 
    case pwd_spy_sep_map n of (s, S, A, B, C, D) 
      pwd_spy_sep_map_state n (S, A, B, C, D)  s 
      {Key (Auth_ShaKey n)}  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  seskey_tuple  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  bad_prikey  bad_id_shakey  s0  fst (pwd_spy_sep_agr n)"
    (is "_  _  ?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)  rel_sep", simp_all add: rel_def
 pwd_spy_sep_agr_def split_def, blast)

proposition pwd_spy_sep_agr_msg:
 "n  bad_prikey  bad_id_shakey 
    case pwd_spy_sep_agr n of (s, S, A, B, C, D) 
      pwd_spy_sep_agr_state n (S, A, B, C, D)  s 
      {Key (Auth_ShaKey n)}  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  seskey_tuple  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  bad_prikey  bad_id_shakey  s0  fst (pwd_spy_sesk n)"
    (is "_  _  ?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)  rel_sesk", simp_all add: rel_def
 pwd_spy_sesk_def split_def Let_def, blast)

proposition pwd_spy_sesk_msg:
 "n  bad_prikey  bad_id_shakey 
    case pwd_spy_sesk n of (s, S, A, B, C, D) 
      pwd_spy_sesk_state n (S, A, B, C, D)  s 
      {Key (Auth_ShaKey n)}  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  seskey_tuple  state" where
"pwd_spy_mult_state n (S, A, B, C, D) =
  insert (Spy, Auth_PriK n  B) (pwd_spy_sesk_state n (S, A, B, C, D))"

proposition pwd_spy_mult_rel:
 "n  bad_prikey  bad_id_shakey  s0  fst (pwd_spy_mult n)"
    (is "_  _  ?t")
by (rule rtrancl_into_rtrancl, erule pwd_spy_sesk_rel, drule pwd_spy_sesk_msg,
 subgoal_tac "(fst (pwd_spy_sesk n), ?t)  rel_mult", simp_all add: rel_def
 pwd_spy_mult_def split_def, blast)

proposition pwd_spy_mult_msg:
 "n  bad_prikey  bad_id_shakey 
    case pwd_spy_mult n of (s, S, A, B, C, D) 
      pwd_spy_mult_state n (S, A, B, C, D)  s 
      {Key (Auth_ShaKey n)}  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  seskey_tuple  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  bad_prikey  bad_id_shakey  s0  fst (pwd_spy_enc_pubk n)"
    (is "_  _  ?t")
by (rule rtrancl_into_rtrancl, erule pwd_spy_mult_rel, drule pwd_spy_mult_msg,
 subgoal_tac "(fst (pwd_spy_mult n), ?t)  rel_enc", simp_all add: rel_def
 pwd_spy_enc_pubk_def split_def Let_def, blast)

proposition pwd_spy_enc_pubk_msg:
 "n  bad_prikey  bad_id_shakey 
    case pwd_spy_enc_pubk n of (s, S, A, B, C, D) 
      pwd_spy_enc_pubk_state n (S, A, B, C, D)  s 
      {Key (Auth_ShaKey n)}  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  seskey_tuple  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  B))
    (pwd_spy_enc_pubk_state n (S, A, B, C, D)))"

proposition pwd_spy_enc_mult_rel:
 "n  bad_prikey  bad_id_shakey  s0  fst (pwd_spy_enc_mult n)"
    (is "_  _  ?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)  rel_enc", simp_all add: rel_def
 pwd_spy_enc_mult_def split_def Let_def, blast)

proposition pwd_spy_enc_mult_msg:
 "n  bad_prikey  bad_id_shakey 
    case pwd_spy_enc_mult n of (s, S, A, B, C, D) 
      pwd_spy_enc_mult_state n (S, A, B, C, D)  s 
      {Key (Auth_ShaKey n)}  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  seskey_tuple  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  bad_prikey  bad_id_shakey  s0  fst (pwd_spy_enc_sign n)"
    (is "_  _  ?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)  rel_enc", simp_all add: rel_def
 pwd_spy_enc_sign_def split_def Let_def, blast)

proposition pwd_spy_enc_sign_msg:
 "n  bad_prikey  bad_id_shakey 
    case pwd_spy_enc_sign n of (s, S, A, B, C, D) 
      pwd_spy_enc_sign_state n (S, A, B, C, D)  s 
      {Key (Auth_ShaKey n)}  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  seskey_tuple  state" where
"pwd_spy_con_state n (S, A, B, C, D) = (let SK = (Some S, {A, B}, {C, D}) in
  insert (Spy, Crypt (SesK SK) (Auth_PriK n  B),
    Crypt (SesK SK) (Sign n (Auth_PriK n)))
    (pwd_spy_enc_sign_state n (S, A, B, C, D)))"

proposition pwd_spy_con_rel:
 "n  bad_prikey  bad_id_shakey  s0  fst (pwd_spy_con n)"
    (is "_  _  ?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)  rel_con", simp_all add: rel_def
 pwd_spy_con_def split_def Let_def, blast)

proposition pwd_spy_con_msg:
 "n  bad_prikey  bad_id_shakey 
    case pwd_spy_con n of (s, S, A, B, C, D) 
      pwd_spy_con_state n (S, A, B, C, D)  s 
      {Key (Auth_ShaKey n)}  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  seskey_tuple  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  bad_prikey  bad_id_shakey  s0  fst (pwd_spy_iv n)"
    (is "_  _  ?t")
by (rule rtrancl_into_rtrancl, erule pwd_spy_con_rel, drule pwd_spy_con_msg,
 subgoal_tac "(fst (pwd_spy_con n), ?t)  rel_con", simp_all add: rel_def
 pwd_spy_iv_def split_def Let_def, blast)

proposition pwd_spy_iv_msg:
 "n  bad_prikey  bad_id_shakey 
    case pwd_spy_iv n of (s, S, A, B, C, D) 
      pwd_spy_iv_state n (S, A, B, C, D)  s 
      {Key (Auth_ShaKey n)}  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  seskey_tuple  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  bad_prikey  bad_id_shakey  s0  fst (pwd_owner_v n)"
    (is "_  _  ?t")
by (rule rtrancl_into_rtrancl, erule pwd_spy_iv_rel, drule pwd_spy_iv_msg,
 subgoal_tac "(fst (pwd_spy_iv n), ?t)  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  bad_prikey  bad_id_shakey 
    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)  s 
      {Key (Auth_ShaKey n)}  key_sets (PriKey S) (crypts (Log -` spied s)) 
      {SesKey SK}  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  seskey_tuple  state" where
"pwd_spy_dec_state n x  insert (Spy, Pwd n) (pwd_owner_v_state n x)"

proposition pwd_spy_dec_rel:
 "n  bad_prikey  bad_id_shakey  s0  fst (pwd_spy_dec n)"
    (is "_  _  ?t")
by (rule rtrancl_into_rtrancl, erule pwd_owner_v_rel, drule pwd_owner_v_msg,
 subgoal_tac "(fst (pwd_owner_v n), ?t)  rel_dec", simp_all add: rel_def
 pwd_spy_dec_def split_def Let_def, (rule exI)+, auto)

proposition pwd_spy_dec_msg:
 "n  bad_prikey  bad_id_shakey 
    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)  s 
      {Key (Auth_ShaKey n)}  key_sets (PriKey S) (crypts (Log -` spied s)) 
      {SesKey SK}  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  seskey_tuple  state" where
"pwd_spy_id_prik_state n (S, A, B, C, D) =
  insert (Spy, n, PriKey S) (pwd_spy_dec_state n (S, A, B, C, D))"

proposition pwd_spy_id_prik_rel:
 "n  bad_prikey  bad_id_shakey  s0  fst (pwd_spy_id_prik n)"
    (is "_  _  ?t")
by (rule rtrancl_into_rtrancl, erule pwd_spy_dec_rel, drule pwd_spy_dec_msg,
 subgoal_tac "(fst (pwd_spy_dec n), ?t)  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  bad_prikey  bad_id_shakey 
    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)  s 
      {SesKey SK}  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  seskey_tuple  state" where
"pwd_spy_id_pubk_state n (S, A, B, C, D) =
  insert (Spy, n, PubKey S) (pwd_spy_id_prik_state n (S, A, B, C, D))"

proposition pwd_spy_id_pubk_rel:
 "n  bad_prikey  bad_id_shakey  s0  fst (pwd_spy_id_pubk n)"
    (is "_  _  ?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)  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  bad_prikey  bad_id_shakey 
    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)  s 
      {SesKey SK}  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  seskey_tuple  state" where
"pwd_spy_id_sesk_state n (S, A, B, C, D) =
  (let SK = (Some S, {A, B}, {C, D}) in
  insert (Spy, n, SesKey SK) (pwd_spy_id_pubk_state n (S, A, B, C, D)))"

proposition pwd_spy_id_sesk_rel:
 "n  bad_prikey  bad_id_shakey  s0  fst (pwd_spy_id_sesk n)"
    (is "_  _  ?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)  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  bad_prikey  bad_id_shakey 
    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)  s 
      {SesKey SK}  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  seskey_tuple  state" where
"pwd_spy_id_pwd_state n x  insert (Spy, n, Pwd n) (pwd_spy_id_sesk_state n x)"

proposition pwd_spy_id_pwd_rel:
 "n  bad_prikey  bad_id_shakey  s0  fst (pwd_spy_id_pwd n)"
    (is "_  _  ?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)  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  bad_prikey  bad_id_shakey 
    case pwd_spy_id_pwd n of (s, S, A, B, C, D) 
      pwd_spy_id_pwd_state n (S, A, B, C, D)  s"
by (drule pwd_spy_id_sesk_msg, simp add: pwd_spy_id_pwd_def split_def Let_def,
 blast)


theorem pwd_compromised:
 "n  bad_prikey  bad_id_shakey  s. s0  s  {Pwd n, n, Pwd n}  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