Theory Possibility
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 s⇩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 _ "λ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:
"s⇩0 ⊨ 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]:
"s⇩0 ⊨ 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:
"s⇩0 ⊨ 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:
"s⇩0 ⊨ 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:
"s⇩0 ⊨ 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:
"s⇩0 ⊨ 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:
"s⇩0 ⊨ 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:
"s⇩0 ⊨ 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:
"s⇩0 ⊨ 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:
"s⇩0 ⊨ 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:
"s⇩0 ⊨ 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:
"s⇩0 ⊨ 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:
"s⇩0 ⊨ 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:
"s⇩0 ⊨ 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: "s⇩0 ⊨ 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:
"s⇩0 ⊨ 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:
"s⇩0 ⊨ 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:
"s⇩0 ⊨ 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:
"s⇩0 ⊨ 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:
"s⇩0 ⊨ 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:
"s⇩0 ⊨ 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:
"s⇩0 ⊨ 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:
"s⇩0 ⊨ 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:
"s⇩0 ⊨ 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:
"s⇩0 ⊨ 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:
"s⇩0 ⊨ 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:
"⟦s⇩0 ⊨ 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:
"s⇩0 ⊨ 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:
"s⇩0 ⊨ 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:
"s⇩0 ⊨ 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:
"s⇩0 ⊨ 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:
"s⇩0 ⊨ 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:
"s⇩0 ⊨ 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:
"s⇩0 ⊨ 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:
"s⇩0 ⊨ 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:
"s⇩0 ⊨ 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:
"s⇩0 ⊨ 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:
"s⇩0 ⊨ 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:
"s⇩0 ⊨ 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:
"⟦s⇩0 ⊨ 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:
"s⇩0 ⊨ 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)) s⇩0,
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 ⟹ s⇩0 ⊨ fst (pwd_spy_i n)"
(is "_ ⟹ _ ⊨ ?t")
by (rule r_into_rtrancl, subgoal_tac "(s⇩0, ?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 ⟹ s⇩0 ⊨ 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 ⟹ s⇩0 ⊨ 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 ⟹ s⇩0 ⊨ 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 ⟹ s⇩0 ⊨ 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)⟧ ⟹
s⇩0 ⊨ 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 ⟹ s⇩0 ⊨ 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 ⟹ s⇩0 ⊨ 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 ⟹ s⇩0 ⊨ 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 ⟹ s⇩0 ⊨ 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 ⟹ s⇩0 ⊨ 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 ⟹ s⇩0 ⊨ 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 ⟹ s⇩0 ⊨ 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 ⟹ s⇩0 ⊨ 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 ⟹ s⇩0 ⊨ 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 ⟹ s⇩0 ⊨ 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 ⟹ s⇩0 ⊨ 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 ⟹ s⇩0 ⊨ 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 ⟹ s⇩0 ⊨ 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 ⟹ s⇩0 ⊨ 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 ⟹ s⇩0 ⊨ 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 ⟹ s⇩0 ⊨ 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. s⇩0 ⊨ 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