Theory Authentication
section "Confidentiality and authenticity properties"
theory Authentication
imports Definitions
begin
text ‹
\label{Authentication}
›
proposition rtrancl_start [rule_format]:
"(x, y) ∈ r⇧* ⟹ P y ⟶ ¬ P x ⟶
(∃u v. (x, u) ∈ r⇧* ∧ (u, v) ∈ r ∧ (v, y) ∈ r⇧* ∧ ¬ P u ∧ P v)"
(is "_ ⟹ _ ⟶ _ ⟶ (∃u v. ?Q x y u v)")
proof (erule rtrancl_induct, simp, (rule impI)+)
fix y z
assume
A: "(x, y) ∈ r⇧*" and
B: "(y, z) ∈ r" and
C: "P z"
assume "P y ⟶ ¬ P x ⟶(∃u v. ?Q x y u v)" and "¬ P x"
hence D: "P y ⟶ (∃u v. ?Q x y u v)" by simp
show "∃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) ∈ r⇧*" 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 ⊨ s' ⟹ s ⊆ s'"
by (erule rtrancl_induct, auto simp add: rel_def image_def)
proposition spied_subset:
"s ⊨ s' ⟹ spied s ⊆ spied s'"
by (rule Image_mono, erule state_subset, simp)
proposition used_subset:
"s ⊨ s' ⟹ used s ⊆ used s'"
by (rule Range_mono, rule state_subset)
proposition asset_ii_init:
"⟦s⇩0 ⊨ s; (Asset n, ⦃Num 2, PubKey A⦄) ∈ s⟧ ⟹
PriKey A ∉ spied s⇩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⇩0 ⊨ s ⟹ Auth_PriKey n ∈ used s"
by (drule used_subset, erule subsetD, simp add: Range_iff image_def, blast)
proposition asset_i_used:
"s⇩0 ⊨ s ⟹
(Asset n, Crypt (Auth_ShaKey n) (PriKey A)) ∈ s ⟶
PriKey A ∈ used s"
by (erule rtrancl_induct, auto simp add: rel_def image_def)
proposition owner_ii_used:
"s⇩0 ⊨ s ⟹
(Owner n, ⦃Num 1, PubKey A⦄) ∈ s ⟶
PriKey A ∈ used s"
by (erule rtrancl_induct, auto simp add: rel_def image_def)
proposition asset_ii_used:
"s⇩0 ⊨ s ⟹
(Asset n, ⦃Num 2, PubKey A⦄) ∈ s ⟶
PriKey A ∈ used s"
by (erule rtrancl_induct, auto simp add: rel_def image_def)
proposition owner_iii_used:
"s⇩0 ⊨ s ⟹
(Owner n, ⦃Num 3, PubKey A⦄) ∈ s ⟶
PriKey A ∈ used s"
by (erule rtrancl_induct, auto simp add: rel_def image_def)
proposition asset_iii_used:
"s⇩0 ⊨ s ⟹
(Asset n, ⦃Num 4, PubKey A⦄) ∈ s ⟶
PriKey A ∈ used s"
by (erule rtrancl_induct, auto simp add: rel_def image_def)
proposition asset_i_unique [rule_format]:
"s⇩0 ⊨ s ⟹
(Asset m, Crypt (Auth_ShaKey m) (PriKey A)) ∈ s ⟶
(Asset n, Crypt (Auth_ShaKey n) (PriKey A)) ∈ s ⟶
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⇩0 ⊨ s ⟹
(Owner m, ⦃Num 1, PubKey A⦄) ∈ s ⟶
(Owner n, ⦃Num 1, PubKey A⦄) ∈ s ⟶
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⇩0 ⊨ s ⟹
(Asset m, ⦃Num 2, PubKey A⦄) ∈ s ⟶
(Asset n, ⦃Num 2, PubKey A⦄) ∈ s ⟶
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⇩0 ⊨ s ⟹
(Asset m, Crypt (Auth_ShaKey m) (Auth_PriKey n)) ∈ s ⟶
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⇩0 ⊨ s ⟹
(Owner m, ⦃Num 1, Auth_PubKey n⦄) ∈ s ⟶
False"
by (erule rtrancl_induct, simp add: image_def, drule auth_prikey_used [of _ n],
auto simp add: rel_def)
proposition auth_pubkey_owner_iii [rule_format]:
"s⇩0 ⊨ s ⟹
(Owner m, ⦃Num 3, Auth_PubKey n⦄) ∈ s ⟶
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⇩0 ⊨ s ⟹
(Asset m, ⦃Num 2, Auth_PubKey n⦄) ∈ s ⟶
False"
by (erule rtrancl_induct, simp add: image_def, drule auth_prikey_used [of _ n],
auto simp add: rel_def)
proposition auth_pubkey_asset_iii [rule_format]:
"s⇩0 ⊨ s ⟹
(Asset m, ⦃Num 4, Auth_PubKey n⦄) ∈ s ⟶
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⇩0 ⊨ s ⟹
(Asset m, Crypt (Auth_ShaKey m) (PriKey A)) ∈ s ⟶
(Owner n, ⦃Num 1, PubKey A⦄) ∈ s ⟶
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_owner_iii [rule_format]:
"s⇩0 ⊨ s ⟹
(Asset m, Crypt (Auth_ShaKey m) (PriKey A)) ∈ s ⟶
(Owner n, ⦃Num 3, PubKey A⦄) ∈ s ⟶
False"
by (erule rtrancl_induct, simp add: image_def, frule asset_i_used [of _ m A],
drule owner_iii_used [of _ n A], auto simp add: rel_def)
proposition asset_i_asset_ii [rule_format]:
"s⇩0 ⊨ s ⟹
(Asset m, Crypt (Auth_ShaKey m) (PriKey A)) ∈ s ⟶
(Asset n, ⦃Num 2, PubKey A⦄) ∈ s ⟶
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_i_asset_iii [rule_format]:
"s⇩0 ⊨ s ⟹
(Asset m, Crypt (Auth_ShaKey m) (PriKey A)) ∈ s ⟶
(Asset n, ⦃Num 4, PubKey A⦄) ∈ s ⟶
False"
by (erule rtrancl_induct, simp add: image_def, frule asset_i_used [of _ m A],
drule asset_iii_used [of _ n A], auto simp add: rel_def)
proposition asset_ii_owner_ii [rule_format]:
"s⇩0 ⊨ s ⟹
(Asset m, ⦃Num 2, PubKey A⦄) ∈ s ⟶
(Owner n, ⦃Num 1, PubKey A⦄) ∈ s ⟶
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_ii_owner_iii [rule_format]:
"s⇩0 ⊨ s ⟹
(Asset m, ⦃Num 2, PubKey A⦄) ∈ s ⟶
(Owner n, ⦃Num 3, PubKey A⦄) ∈ s ⟶
False"
by (erule rtrancl_induct, simp add: image_def, frule asset_ii_used [of _ m A],
drule owner_iii_used [of _ n A], auto simp add: rel_def)
proposition asset_ii_asset_iii [rule_format]:
"s⇩0 ⊨ s ⟹
(Asset m, ⦃Num 2, PubKey A⦄) ∈ s ⟶
(Asset n, ⦃Num 4, PubKey A⦄) ∈ s ⟶
False"
by (erule rtrancl_induct, simp add: image_def, frule asset_ii_used [of _ m A],
drule asset_iii_used [of _ n A], auto simp add: rel_def)
proposition asset_iii_owner_iii [rule_format]:
"s⇩0 ⊨ s ⟹
(Asset m, ⦃Num 4, PubKey A⦄) ∈ s ⟶
(Owner n, ⦃Num 3, PubKey A⦄) ∈ s ⟶
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⇩0 ⊨ s ⟹
(Asset n, Token n (Auth_PriK n) B C SK) ∈ s ⟶
(∃A D. fst (snd SK) = {A, B} ∧ snd (snd SK) = {C, D} ∧
(Asset n, ⦃Num 2, PubKey B⦄) ∈ s ∧ (Asset n, ⦃Num 4, PubKey D⦄) ∈ s ∧
Crypt (SesK SK) (PubKey D) ∈ used s ∧ (Asset n, PubKey B) ∈ s)"
by (erule rtrancl_induct, auto simp add: rel_def)
proposition owner_v_state [rule_format]:
"s⇩0 ⊨ s ⟹
(Owner n, Crypt (SesK SK) (Pwd n)) ∈ s ⟶
(Owner n, SesKey SK) ∈ s ∧
(∃A B C. Token n A B C SK ∈ used s ∧ B ∈ fst (snd SK))"
by (erule rtrancl_induct, auto simp add: rel_def, blast)
proposition asset_v_state [rule_format]:
"s⇩0 ⊨ s ⟹
(Asset n, Crypt (SesK SK) (Num 0)) ∈ s ⟶
(Asset n, SesKey SK) ∈ s ∧ Crypt (SesK SK) (Pwd n) ∈ 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:
"⟦s ⊢ s';
(Owner n, SesKey SK) ∈ s ⟶
(∃S. fst SK = Some S ∧ Crypt (Auth_ShaKey n) (PriKey S) ∈ used s) ∨
fst SK = None;
(Owner n, SesKey SK) ∈ s'⟧ ⟹
(∃S. fst SK = Some S ∧ Crypt (Auth_ShaKey n) (PriKey S) ∈ used s') ∨
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⇩0 ⊨ s ⟹
(Owner n, SesKey SK) ∈ s ⟶
(∃S. fst SK = Some S ∧ Crypt (Auth_ShaKey n) (PriKey S) ∈ used s) ∨
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⇩0 ⊨ s ⟹
(Owner n, SesKey SK) ∈ s ⟶
(∃A B C D. fst (snd SK) = {A, B} ∧ snd (snd SK) = {C, D} ∧
(Owner n, ⦃Num 1, PubKey A⦄) ∈ s ∧
(Owner n, ⦃Num 3, PubKey C⦄) ∈ s ∧
(Owner n, Crypt (SesK SK) (PubKey D)) ∈ s)"
by (erule rtrancl_induct, auto simp add: rel_def, blast+)
proposition asset_seskey_nonce [rule_format]:
"s⇩0 ⊨ s ⟹
(Asset n, SesKey SK) ∈ s ⟶
(∃S. fst SK = Some S ∧ (Asset n, Crypt (Auth_ShaKey n) (PriKey S)) ∈ s)"
by (erule rtrancl_induct, auto simp add: rel_def)
proposition asset_seskey_other [rule_format]:
"s⇩0 ⊨ s ⟹
(Asset n, SesKey SK) ∈ s ⟶
(∃A B C D. fst (snd SK) = {A, B} ∧ snd (snd SK) = {C, D} ∧
(Asset n, ⦃Num 2, PubKey B⦄) ∈ s ∧ (Asset n, ⦃Num 4, PubKey D⦄) ∈ s ∧
(Asset n, Token n (Auth_PriK n) B C SK) ∈ s)"
by (erule rtrancl_induct, auto simp add: rel_def, blast)
declare Range_Un_eq [simp]
proposition used_prod [simp]:
"A ≠ {} ⟹ used (A × 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 ⊆ H' ⟹ parts H ⊆ parts H'"
by (rule subsetI, erule parts.induct, auto)
proposition parts_msg_mono:
"X ∈ H ⟹ parts_msg X ⊆ parts H"
by (subgoal_tac "{X} ⊆ H", subst parts_msg_def, erule parts_mono, simp)
lemma parts_union_1:
"parts (H ∪ H') ⊆ parts H ∪ parts H'"
by (rule subsetI, erule parts.induct, auto)
lemma parts_union_2:
"parts H ∪ parts H' ⊆ parts (H ∪ H')"
by (rule subsetI, erule UnE, erule_tac [!] parts.induct, auto)
proposition parts_union [simp]:
"parts (H ∪ H') = parts H ∪ parts H'"
by (rule equalityI, rule parts_union_1, rule parts_union_2)
proposition parts_insert:
"parts (insert X H) = parts_msg X ∪ 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 ⊗ B) = {A ⊗ 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} ⊆ insert (Crypt K X) (parts {X})"
by (rule subsetI, erule parts.induct, auto)
lemma parts_crypt_2:
"insert (Crypt K X) (parts {X}) ⊆ 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 {⦃X, Y⦄} ⊆ insert ⦃X, Y⦄ (parts {X} ∪ parts {Y})"
by (rule subsetI, erule parts.induct, auto)
lemma parts_mpair_2:
"insert ⦃X, Y⦄ (parts {X} ∪ parts {Y}) ⊆ parts {⦃X, Y⦄}"
by (rule subsetI, simp, erule disjE, blast, erule disjE, erule_tac [!] parts.induct,
auto)
proposition parts_msg_mpair [simp]:
"parts_msg ⦃X, Y⦄ = insert ⦃X, Y⦄ (parts_msg X ∪ 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 ⟨n, X⟩ = {⟨n, X⟩}"
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:
"⟦s' = insert (Spy, X) s ∧ (Spy, Crypt K X) ∈ s ∧ (Spy, Key (InvK K)) ∈ s;
Y ∈ parts_msg X⟧ ⟹
Y ∈ parts (used s)"
by (subgoal_tac "X ∈ parts (used s)", drule parts_msg_mono [of X], auto)
proposition parts_enc:
"⟦s' = insert (Spy, Crypt K X) s ∧ (Spy, X) ∈ s ∧ (Spy, Key K) ∈ s;
Y ∈ parts_msg X⟧ ⟹
Y ∈ parts (used s)"
by (subgoal_tac "X ∈ parts (used s)", drule parts_msg_mono [of X], auto)
proposition parts_sep:
"⟦s' = insert (Spy, X) (insert (Spy, Y) s) ∧ (Spy, ⦃X, Y⦄) ∈ s;
Z ∈ parts_msg X ∨ Z ∈ parts_msg Y⟧ ⟹
Z ∈ parts (used s)"
by (erule disjE, subgoal_tac "X ∈ parts (used s)", drule parts_msg_mono [of X],
subgoal_tac [3] "Y ∈ parts (used s)", drule_tac [3] parts_msg_mono [of Y], auto)
proposition parts_con:
"⟦s' = insert (Spy, ⦃X, Y⦄) s ∧ (Spy, X) ∈ s ∧ (Spy, Y) ∈ s;
Z ∈ parts_msg X ∨ Z ∈ parts_msg Y⟧ ⟹
Z ∈ parts (used s)"
by (erule disjE, subgoal_tac "X ∈ parts (used s)", drule parts_msg_mono [of X],
subgoal_tac [3] "Y ∈ parts (used s)", drule_tac [3] parts_msg_mono [of Y], auto)
lemma parts_init_1:
"parts (used s⇩0) ⊆ used s⇩0 ∪ range (Hash ∘ Agent) ∪
range (Hash ∘ Auth_PubKey) ∪
range (λn. ⦃Hash (Agent n), Hash (Auth_PubKey n)⦄)"
by (rule subsetI, erule parts.induct, (clarify | simp add: Range_iff image_def)+)
lemma parts_init_2:
"used s⇩0 ∪ range (Hash ∘ Agent) ∪ range (Hash ∘ Auth_PubKey) ∪
range (λn. ⦃Hash (Agent n), Hash (Auth_PubKey n)⦄) ⊆ parts (used s⇩0)"
by (rule subsetI, auto simp add: parts_insert)
proposition parts_init:
"parts (used s⇩0) = used s⇩0 ∪ range (Hash ∘ Agent) ∪
range (Hash ∘ Auth_PubKey) ∪
range (λn. ⦃Hash (Agent n), Hash (Auth_PubKey n)⦄)"
by (rule equalityI, rule parts_init_1, rule parts_init_2)
proposition parts_crypt_prikey_start:
"⟦s ⊢ s'; Crypt K (PriKey A) ∈ parts (used s');
Crypt K (PriKey A) ∉ parts (used s)⟧ ⟹
(∃n. K = Auth_ShaKey n ∧
(Asset n, Crypt (Auth_ShaKey n) (PriKey A)) ∈ s') ∨
{PriKey A, Key K} ⊆ 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:
"⟦s⇩0 ⊨ s; Crypt K (PriKey A) ∈ parts (used s)⟧ ⟹
(∃n. K = Auth_ShaKey n ∧
(Asset n, Crypt (Auth_ShaKey n) (PriKey A)) ∈ s) ∨
{PriKey A, Key K} ⊆ 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:
"⟦s ⊢ s'; Crypt (SesK SK) (PubKey C) ∈ parts (used s');
Crypt (SesK SK) (PubKey C) ∉ parts (used s)⟧ ⟹
C ∈ snd (snd SK) ∧ ((∃n. (Owner n, SesKey SK) ∈ s') ∨
(∃n B. (Asset n, Token n (Auth_PriK n) B C SK) ∈ s')) ∨
SesKey SK ∈ 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:
"⟦s⇩0 ⊨ s; Crypt (SesK SK) (PubKey C) ∈ parts (used s)⟧ ⟹
C ∈ snd (snd SK) ∧ ((∃n. (Owner n, SesKey SK) ∈ s) ∨
(∃n B. (Asset n, Token n (Auth_PriK n) B C SK) ∈ s)) ∨
SesKey SK ∈ 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:
"⟦s ⊢ s'; Crypt K (Key K') ∈ parts (used s');
Crypt K (Key K') ∉ parts (used s); K' ∉ range PriK ∪ range PubK⟧ ⟹
{Key K', Key K} ⊆ 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:
"⟦s⇩0 ⊨ s; Crypt K (Key K') ∈ parts (used s);
K' ∉ range PriK ∪ range PubK⟧ ⟹
{Key K', Key K} ⊆ 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:
"⟦s ⊢ s'; Crypt (SesK SK) (Sign n A) ∈ parts (used s');
Crypt (SesK SK) (Sign n A) ∉ parts (used s)⟧ ⟹
(Asset n, SesKey SK) ∈ s' ∨ SesKey SK ∈ 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:
"⟦s⇩0 ⊨ s; Crypt (SesK SK) (Sign n A) ∈ parts (used s)⟧ ⟹
(Asset n, SesKey SK) ∈ s ∨ SesKey SK ∈ 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:
"⟦s ⊢ s'; Crypt K (Pwd n) ∈ parts (used s');
Crypt K (Pwd n) ∉ parts (used s)⟧ ⟹
(∃SK. K = SesK SK ∧ (Owner n, Crypt (SesK SK) (Pwd n)) ∈ s') ∨
{Pwd n, Key K} ⊆ 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:
"⟦s⇩0 ⊨ s; Crypt K (Pwd n) ∈ parts (used s)⟧ ⟹
(∃SK. K = SesK SK ∧ (Owner n, Crypt (SesK SK) (Pwd n)) ∈ s) ∨
{Pwd n, Key K} ⊆ 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:
"⟦s ⊢ s'; Crypt (SesK SK) (Num 0) ∈ parts (used s');
Crypt (SesK SK) (Num 0) ∉ parts (used s)⟧ ⟹
(∃n. (Asset n, Crypt (SesK SK) (Num 0)) ∈ s') ∨ SesKey SK ∈ 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:
"⟦s⇩0 ⊨ s; Crypt (SesK SK) (Num 0) ∈ parts (used s)⟧ ⟹
(∃n. (Asset n, Crypt (SesK SK) (Num 0)) ∈ s) ∨ SesKey SK ∈ 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:
"⟦s ⊢ s'; Crypt (SesK SK) (A ⊗ B) ∈ parts (used s');
Crypt (SesK SK) (A ⊗ B) ∉ parts (used s)⟧ ⟹
B ∈ fst (snd SK) ∧ (∃n C. (Asset n, Token n (Auth_PriK n) B C SK) ∈ s') ∨
{A ⊗ B, SesKey SK} ⊆ 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:
"⟦s⇩0 ⊨ s; Crypt (SesK SK) (A ⊗ B) ∈ parts (used s)⟧ ⟹
B ∈ fst (snd SK) ∧ (∃n C. (Asset n, Token n (Auth_PriK n) B C SK) ∈ s) ∨
{A ⊗ B, SesKey SK} ⊆ 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:
"⟦s ⊢ s'; A ⊗ B ∈ parts (used s'); A ⊗ B ∉ parts (used s)⟧ ⟹
(∃n SK. A = Auth_PriK n ∧ (Asset n, ⦃Num 2, PubKey B⦄) ∈ s' ∧
Crypt (SesK SK) (A ⊗ B) ∈ parts (used s')) ∨
{PriKey A, PriKey B} ⊆ 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:
"⟦s⇩0 ⊨ s; A ⊗ B ∈ parts (used s)⟧ ⟹
(∃n. A = Auth_PriK n ∧ (Asset n, ⦃Num 2, PubKey B⦄) ∈ s) ∨
{PriKey A, PriKey B} ⊆ 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:
"⟦s ⊢ s'; ⦃X, Y⦄ ∈ parts (used s'); ⦃X, Y⦄ ∉ parts (used s);
X = Key K ∨ Y = Key K ∧ K ∉ range PubK⟧ ⟹
{X, Y} ⊆ 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:
"⟦s⇩0 ⊨ s; ⦃X, Y⦄ ∈ parts (used s);
X = Key K ∨ Y = Key K ∧ K ∉ range PubK⟧ ⟹
{X, Y} ⊆ 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:
"⟦s ⊢ s'; ⦃X, Y⦄ ∈ parts (used s'); ⦃X, Y⦄ ∉ parts (used s);
X = Pwd n ∨ Y = Pwd n⟧ ⟹
{X, Y} ⊆ 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:
"⟦s⇩0 ⊨ s; ⦃X, Y⦄ ∈ parts (used s); X = Pwd n ∨ Y = Pwd n⟧ ⟹
{X, Y} ⊆ 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⇩0 ⊨ s" and
B: "s ⊢ s'" and
C: "Crypt (SesK SK) (PubKey C) ∈ parts (used s')" and
D: "Crypt (SesK SK) (PubKey C) ∉ parts (used s)" and
E: "∀n. (Owner n, SesKey SK) ∉ s'" and
F: "SesKey SK ∉ spied s'"
shows False
proof -
have "C ∈ snd (snd SK) ∧ ((∃n. (Owner n, SesKey SK) ∈ s') ∨
(∃n B. (Asset n, Token n (Auth_PriK n) B C SK) ∈ s')) ∨
SesKey SK ∈ spied s'"
(is "?P C ∧ ((∃n. ?Q n s') ∨ (∃n B. ?R n B C s')) ∨ ?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 "¬ ?R n B C s"
using D by blast
ultimately have "∃D. Crypt (SesK SK) (PubKey D) ∈ used s"
(is "∃D. ?U D")
using B by (auto simp add: rel_def)
then obtain D where "?U D" ..
hence "?P D ∧ ((∃n. ?Q n s) ∨ (∃n B. ?R n B D s)) ∨ ?S s"
by (rule_tac parts_crypt_pubkey [OF A], blast)
moreover have G: "s ⊆ s'"
by (rule state_subset, insert B, simp)
have "∀n. (Owner n, SesKey SK) ∉ s"
by (rule allI, rule notI, drule subsetD [OF G], insert E, simp)
moreover have H: "spied s ⊆ spied s'"
by (rule Image_mono [OF G], simp)
have "SesKey SK ∉ 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 "∃A' D'. fst (snd SK) = {A', B'} ∧ snd (snd SK) = {D, D'} ∧
(Asset n', ⦃Num 2, PubKey B'⦄) ∈ s ∧
(Asset n', ⦃Num 4, PubKey D'⦄) ∈ s ∧
?U D' ∧ (Asset n', PubKey B') ∈ 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) ∈ parts (used s)"
using ‹?P C› and ‹?U D› by auto
thus False
using D by contradiction
qed
proposition parts_pubkey_false:
"⟦s⇩0 ⊨ s; Crypt (SesK SK) (PubKey C) ∈ parts (used s);
∀n. (Owner n, SesKey SK) ∉ s; SesKey SK ∉ spied s⟧ ⟹
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) ∈ v" and "v ⊨ s"
hence "(Owner n, SesKey SK) ∈ s"
by (erule_tac rev_subsetD, rule_tac state_subset)
moreover assume "∀n. (Owner n, SesKey SK) ∉ s"
ultimately show False by simp
next
fix v
assume "SesKey SK ∈ spied v" and "v ⊨ s"
hence "SesKey SK ∈ spied s"
by (erule_tac rev_subsetD, rule_tac spied_subset)
moreover assume "SesKey SK ∉ spied s"
ultimately show False by contradiction
qed
proposition asset_ii_spied_start:
assumes
A: "s⇩0 ⊨ s" and
B: "s ⊢ s'" and
C: "PriKey B ∈ spied s'" and
D: "PriKey B ∉ spied s" and
E: "(Asset n, ⦃Num 2, PubKey B⦄) ∈ s"
shows "Auth_PriKey n ∈ spied s ∧
(∃C SK. (Asset n, Token n (Auth_PriK n) B C SK) ∈ s)"
(is "_ ∧ (∃C SK. ?P n C SK s)")
proof -
have "∃A. (A ⊗ B ∈ spied s ∨ B ⊗ A ∈ spied s) ∧ PriKey A ∈ spied s"
proof (insert B C D, auto simp add: rel_def, rule_tac [!] FalseE)
assume "Key (PriK B) ∉ used s"
moreover have "PriKey B ∈ 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))) ∈ s"
hence "Crypt K (PriKey B) ∈ parts (used s)" by auto
hence "(∃m. K = Auth_ShaKey m ∧
(Asset m, Crypt (Auth_ShaKey m) (PriKey B)) ∈ s) ∨
{PriKey B, Key K} ⊆ spied s"
(is "(∃m. _ ∧ ?P m) ∨ _")
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, ⦃Key (PriK B), Y⦄) ∈ s"
hence "⦃PriKey B, Y⦄ ∈ parts (used s)" by auto
hence "{PriKey B, Y} ⊆ 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, ⦃X, Key (PriK B)⦄) ∈ s"
hence "⦃X, PriKey B⦄ ∈ parts (used s)" by auto
hence "{X, PriKey B} ⊆ 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 ∈ spied s" and
"A ⊗ B ∈ spied s ∨ B ⊗ A ∈ spied s"
by blast
hence "A ⊗ B ∈ parts (used s) ∨ B ⊗ A ∈ parts (used s)" by blast
moreover have "B ⊗ A ∉ parts (used s)"
proof
assume "B ⊗ A ∈ parts (used s)"
hence "(∃m. B = Auth_PriK m ∧ (Asset m, ⦃Num 2, PubKey A⦄) ∈ s) ∨
{PriKey B, PriKey A} ⊆ spied s"
by (rule parts_mult [OF A])
then obtain m where "B = Auth_PriK m"
using D by blast
hence "(Asset n, ⦃Num 2, Auth_PubKey m⦄) ∈ s"
using E by simp
thus False
by (rule auth_pubkey_asset_ii [OF A])
qed
ultimately have "A ⊗ B ∈ parts (used s)" by simp
with A have "∃u v. s⇩0 ⊨ u ∧ u ⊢ v ∧ v ⊨ s ∧
A ⊗ B ∉ parts (used u) ∧ A ⊗ B ∈ parts (used v)"
by (rule rtrancl_start, subst parts_init, simp add: Range_iff image_def)
then obtain u v where G: "u ⊢ v" and H: "v ⊨ s" and
I: "A ⊗ B ∉ parts (used u)" and "A ⊗ B ∈ parts (used v)"
by blast
hence "(∃m SK. A = Auth_PriK m ∧ (Asset m, ⦃Num 2, PubKey B⦄) ∈ v ∧
Crypt (SesK SK) (A ⊗ B) ∈ parts (used v)) ∨
{PriKey A, PriKey B} ⊆ spied v"
by (rule_tac parts_mult_start, simp_all)
moreover have "PriKey B ∉ spied v"
proof
assume "PriKey B ∈ spied v"
hence "PriKey B ∈ 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 ⊗ B) ∈ parts (used v)" and
"A = Auth_PriK m" and "(Asset m, ⦃Num 2, PubKey B⦄) ∈ v"
by blast
moreover from this have "(Asset m, ⦃Num 2, PubKey B⦄) ∈ 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 ∈ spied s"
using F by simp
have "Crypt (SesK SK) (A ⊗ B) ∉ parts (used u)"
using I by blast
hence "B ∈ fst (snd SK) ∧ (∃m C. ?P m C SK v) ∨
{A ⊗ B, SesKey SK} ⊆ spied u"
by (rule parts_crypt_mult_start [OF G J])
moreover have "A ⊗ B ∉ 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 "∃A' D. fst (snd SK) = {A', B} ∧
snd (snd SK) = {C, D} ∧ (Asset m', ⦃Num 2, PubKey B⦄) ∈ s ∧
(Asset m', ⦃Num 4, PubKey D⦄) ∈ s ∧
Crypt (SesK SK) (PubKey D) ∈ used s ∧ (Asset m', PubKey B) ∈ s"
by (rule asset_iv_state [OF A])
hence "(Asset m', ⦃Num 2, PubKey B⦄) ∈ 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⇩0 ⊨ s" and
B: "PriKey B ∈ spied s" and
C: "(Asset n, ⦃Num 2, PubKey B⦄) ∈ s"
shows "Auth_PriKey n ∈ spied s ∧
(∃C SK. (Asset n, Token n (Auth_PriK n) B C SK) ∈ s)"
(is "?P s")
proof -
have "∃u v. s⇩0 ⊨ u ∧ u ⊢ v ∧ v ⊨ s ∧
(Asset n, ⦃Num 2, PubKey B⦄) ∉ u ∧ (Asset n, ⦃Num 2, PubKey B⦄) ∈ v"
using A and C by (rule rtrancl_start, auto)
then obtain u v where "v ⊨ s" and "(Asset n, ⦃Num 2, PubKey B⦄) ∉ u" and
D: "s⇩0 ⊨ u" and E: "u ⊢ v" and F: "(Asset n, ⦃Num 2, PubKey B⦄) ∈ v"
by blast
moreover from this have "PriKey B ∉ spied v"
by (auto simp add: rel_def)
ultimately have "∃w x. v ⊨ w ∧ w ⊢ x ∧ x ⊨ s ∧
PriKey B ∉ spied w ∧ PriKey B ∈ spied x"
using B by (rule_tac rtrancl_start, simp_all)
then obtain w x where "PriKey B ∉ spied w" and "PriKey B ∈ spied x" and
G: "v ⊨ w" and H: "w ⊢ x" and I: "x ⊨ s"
by blast
moreover from this have "s⇩0 ⊨ w"
using D and E by simp
moreover have "(Asset n, ⦃Num 2, PubKey B⦄) ∈ 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 ⊆ s"
using H and I by (rule_tac state_subset, simp)
ultimately show ?thesis by blast
qed
proposition asset_iv_unique:
assumes
A: "s⇩0 ⊨ s" and
B: "(Asset m, Token m (Auth_PriK m) B C' SK') ∈ s" and
C: "(Asset n, Token n (Auth_PriK n) B C SK) ∈ s"
(is "?P n C SK s")
shows "m = n ∧ C' = C ∧ SK' = SK"
proof (subst (2) cases_simp [of "m = n", symmetric], simp, rule conjI, rule impI,
rule ccontr)
assume D: "¬ (C' = C ∧ SK' = SK)" and "m = n"
moreover have "∃u v. s⇩0 ⊨ u ∧ u ⊢ v ∧ v ⊨ s ∧
¬ (?P m C' SK' u ∧ ?P n C SK u) ∧ ?P m C' SK' v ∧ ?P n C SK v"
using B and C by (rule_tac rtrancl_start [OF A], auto)
ultimately obtain u v where E: "s⇩0 ⊨ u" and F: "u ⊢ v" and
G: "?P n C' SK' v" and H: "?P n C SK v" and
"¬ ?P n C' SK' u ∨ ¬ ?P n C SK u"
by blast
moreover {
assume I: "¬ ?P n C' SK' u"
hence "?P n C SK u"
by (insert D F G H, auto simp add: rel_def)
hence "∃A D. fst (snd SK) = {A, B} ∧ snd (snd SK) = {C, D} ∧
(Asset n, ⦃Num 2, PubKey B⦄) ∈ u ∧ (Asset n, ⦃Num 4, PubKey D⦄) ∈ u ∧
Crypt (SesK SK) (PubKey D) ∈ used u ∧ (Asset n, PubKey B) ∈ u"
by (rule asset_iv_state [OF E])
moreover have "(Asset n, PubKey B) ∉ u"
by (insert F G I, auto simp add: rel_def)
ultimately have False by simp
}
moreover {
assume I: "¬ ?P n C SK u"
hence "?P n C' SK' u"
by (insert D F G H, auto simp add: rel_def)
hence "∃A D. fst (snd SK') = {A, B} ∧ snd (snd SK') = {C', D} ∧
(Asset n, ⦃Num 2, PubKey B⦄) ∈ u ∧ (Asset n, ⦃Num 4, PubKey D⦄) ∈ u ∧
Crypt (SesK SK') (PubKey D) ∈ used u ∧ (Asset n, PubKey B) ∈ u"
by (rule asset_iv_state [OF E])
moreover have "(Asset n, PubKey B) ∉ u"
by (insert F H I, auto simp add: rel_def)
ultimately have False by simp
}
ultimately show False by blast
next
have "∃A D. fst (snd SK') = {A, B} ∧ snd (snd SK') = {C', D} ∧
(Asset m, ⦃Num 2, PubKey B⦄) ∈ s ∧ (Asset m, ⦃Num 4, PubKey D⦄) ∈ s ∧
Crypt (SesK SK') (PubKey D) ∈ used s ∧ (Asset m, PubKey B) ∈ s"
(is "?Q m C' SK'")
by (rule asset_iv_state [OF A B])
hence "(Asset m, ⦃Num 2, PubKey B⦄) ∈ s" by blast
moreover have "?Q n C SK"
by (rule asset_iv_state [OF A C])
hence "(Asset n, ⦃Num 2, PubKey B⦄) ∈ s" by blast
ultimately show "m = n"
by (rule asset_ii_unique [OF A])
qed
theorem sigkey_secret:
"s⇩0 ⊨ s ⟹ SigKey ∉ spied s"
proof (erule rtrancl_induct, simp add: image_def)
fix s s'
assume
A: "s⇩0 ⊨ s" and
B: "s ⊢ s'" and
C: "SigKey ∉ spied s"
show "SigKey ∉ spied s'"
proof (insert B C, auto simp add: rel_def)
fix K
assume "(Spy, Crypt K SigKey) ∈ s"
hence "Crypt K SigKey ∈ parts (used s)" by blast
hence "{SigKey, Key K} ⊆ spied s"
by (rule parts_crypt_key [OF A], simp add: image_def)
with C show False by simp
next
fix Y
assume "(Spy, ⦃SigKey, Y⦄) ∈ s"
hence "⦃SigKey, Y⦄ ∈ parts (used s)" by blast
hence "{SigKey, Y} ⊆ spied s"
by (rule parts_mpair_key [OF A, where K = "SigK"], simp)
with C show False by simp
next
fix X
assume "(Spy, ⦃X, SigKey⦄) ∈ s"
hence "⦃X, SigKey⦄ ∈ parts (used s)" by blast
hence "{X, SigKey} ⊆ 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⇩0 ⊨ s"
shows "⟦s ⊢ s'; Sign n A ∈ parts (used s'); Sign n A ∉ parts (used s)⟧ ⟹
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:
"⟦s⇩0 ⊨ s; Sign n A ∈ parts (used s)⟧ ⟹
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:
"⟦s⇩0 ⊨ s; n ∉ bad_shakey⟧ ⟹
Key (Auth_ShaKey n) ∉ spied s"
proof (erule rtrancl_induct, simp add: image_def)
fix s s'
assume
A: "s⇩0 ⊨ s" and
B: "s ⊢ s'" and
C: "Key (Auth_ShaKey n) ∉ spied s"
show "Key (Auth_ShaKey n) ∉ spied s'"
proof (insert B C, auto simp add: rel_def)
fix K
assume "(Spy, Crypt K (Key (ShaK (Auth_ShaK n)))) ∈ s"
hence "Crypt K (Key (Auth_ShaKey n)) ∈ parts (used s)" by auto
hence "{Key (Auth_ShaKey n), Key K} ⊆ spied s"
by (rule parts_crypt_key [OF A], simp add: image_def)
with C show False by simp
next
fix Y
assume "(Spy, ⦃Key (ShaK (Auth_ShaK n)), Y⦄) ∈ s"
hence "⦃Key (Auth_ShaKey n), Y⦄ ∈ parts (used s)" by auto
hence "{Key (Auth_ShaKey n), Y} ⊆ 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, ⦃X, Key (ShaK (Auth_ShaK n))⦄) ∈ s"
hence "⦃X, Key (Auth_ShaKey n)⦄ ∈ parts (used s)" by auto
hence "{X, Key (Auth_ShaKey n)} ⊆ 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⇩0 ⊨ s" and
B: "n ∉ bad_prikey"
shows "Auth_PriKey n ∉ spied s"
proof
assume "Auth_PriKey n ∈ spied s"
moreover have "Auth_PriKey n ∉ spied s⇩0"
using B by auto
ultimately have "∃u v. s⇩0 ⊨ u ∧ u ⊢ v ∧ v ⊨ s ∧
Auth_PriKey n ∉ spied u ∧ Auth_PriKey n ∈ spied v"
by (rule rtrancl_start [OF A])
then obtain u v where C: "s⇩0 ⊨ u" and D: "u ⊢ v" and
E: "Auth_PriKey n ∉ spied u" and F: "Auth_PriKey n ∈ spied v"
by blast
have "∃B. (Auth_PriK n ⊗ B ∈ spied u ∨ B ⊗ Auth_PriK n ∈ spied u) ∧
PriKey B ∈ spied u"
proof (insert D E F, auto simp add: rel_def, rule_tac [!] FalseE)
assume "Key (PriK (Auth_PriK n)) ∉ used u"
moreover have "Auth_PriKey n ∈ 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)))) ∈ u"
hence "Crypt K (PriKey (Auth_PriK n)) ∈ parts (used u)" by auto
hence "(∃m. K = Auth_ShaKey m ∧
(Asset m, Crypt (Auth_ShaKey m) (PriKey (Auth_PriK n))) ∈ u) ∨
{PriKey (Auth_PriK n), Key K} ⊆ spied u"
by (rule parts_crypt_prikey [OF C])
then obtain m where
"(Asset m, Crypt (Auth_ShaKey m) (Auth_PriKey n)) ∈ u"
using E by auto
thus False
by (rule auth_prikey_asset_i [OF C])
next
fix Y
assume "(Spy, ⦃Key (PriK (Auth_PriK n)), Y⦄) ∈ u"
hence "⦃Auth_PriKey n, Y⦄ ∈ parts (used u)" by auto
hence "{Auth_PriKey n, Y} ⊆ 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, ⦃X, Key (PriK (Auth_PriK n))⦄) ∈ u"
hence "⦃X, Auth_PriKey n⦄ ∈ parts (used u)" by auto
hence "{X, Auth_PriKey n} ⊆ 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 ∈ spied u" and
"Auth_PriK n ⊗ B ∈ spied u ∨ B ⊗ Auth_PriK n ∈ spied u"
by blast
hence "Auth_PriK n ⊗ B ∈ parts (used u) ∨ B ⊗ Auth_PriK n ∈ parts (used u)"
by blast
moreover have "B ⊗ Auth_PriK n ∉ parts (used u)"
proof
assume "B ⊗ Auth_PriK n ∈ parts (used u)"
hence "(∃m. B = Auth_PriK m ∧
(Asset m, ⦃Num 2, PubKey (Auth_PriK n)⦄) ∈ u) ∨
{PriKey B, PriKey (Auth_PriK n)} ⊆ spied u"
by (rule parts_mult [OF C])
then obtain m where "(Asset m, ⦃Num 2, Auth_PubKey n⦄) ∈ u"
using E by auto
thus False
by (rule auth_pubkey_asset_ii [OF C])
qed
ultimately have "Auth_PriK n ⊗ B ∈ parts (used u)" by simp
hence "(∃m. Auth_PriK n = Auth_PriK m ∧
(Asset m, ⦃Num 2, PubKey B⦄) ∈ u) ∨
{PriKey (Auth_PriK n), PriKey B} ⊆ spied u"
by (rule parts_mult [OF C])
then obtain m where "Auth_PriK n = Auth_PriK m" and
"(Asset m, ⦃Num 2, PubKey B⦄) ∈ u"
using E by auto
moreover from this have "Auth_PriKey m ∈ spied u ∧
(∃C SK. (Asset m, Token m (Auth_PriK m) B C SK) ∈ u)"
by (rule_tac asset_ii_spied [OF C G])
ultimately show False
using E by simp
qed
proposition asset_ii_secret:
"⟦s⇩0 ⊨ s; n ∉ bad_prikey; (Asset n, ⦃Num 2, PubKey B⦄) ∈ s⟧ ⟹
PriKey B ∉ spied s"
by (rule notI, frule asset_ii_spied, assumption+, drule auth_prikey_secret, simp+)
proposition asset_i_secret [rule_format]:
assumes
A: "s⇩0 ⊨ s" and
B: "n ∉ bad_shakey"
shows "(Asset n, Crypt (Auth_ShaKey n) (PriKey S)) ∈ s ⟶
PriKey S ∉ spied s"
proof (rule rtrancl_induct [OF A], simp add: image_def, rule impI)
fix s s'
assume
C: "s⇩0 ⊨ s" and
D: "s ⊢ s'" and
E: "(Asset n, Crypt (Auth_ShaKey n) (PriKey S)) ∈ s ⟶
PriKey S ∉ spied s" and
F: "(Asset n, Crypt (Auth_ShaKey n) (PriKey S)) ∈ s'"
show "PriKey S ∉ spied s'"
proof (insert D E F, auto simp add: rel_def)
assume "(Asset n, Crypt (ShaK (Auth_ShaK n)) (Key (PriK S))) ∈ s"
hence "(Asset n, Crypt (Auth_ShaKey n) (PriKey S)) ∈ s" by simp
hence "PriKey S ∈ used s"
by (rule asset_i_used [OF C, THEN mp])
moreover assume "Key (PriK S) ∉ used s"
ultimately show False by simp
next
fix K
assume "(Spy, Crypt K (Key (PriK S))) ∈ s"
hence "Crypt K (PriKey S) ∈ parts (used s)" by auto
hence "(∃m. K = Auth_ShaKey m ∧
(Asset m, Crypt (Auth_ShaKey m) (PriKey S)) ∈ s) ∨
{PriKey S, Key K} ⊆ spied s"
(is "(∃m. ?P m ∧ ?Q m) ∨ _")
by (rule parts_crypt_prikey [OF C])
moreover assume "(Spy, Key (PriK S)) ∉ s"
ultimately obtain m where G: "?P m ∧ ?Q m" by auto
hence "?Q m" ..
moreover assume
"(Asset n, Crypt (ShaK (Auth_ShaK n)) (Key (PriK S))) ∈ s"
hence "(Asset n, Crypt (Auth_ShaKey n) (PriKey S)) ∈ s" by simp
ultimately have "m = n"
by (rule asset_i_unique [OF C])
moreover assume "(Spy, Key (InvK K)) ∈ s"
ultimately have "Key (Auth_ShaKey n) ∈ spied s"
using G by simp
moreover have "Key (Auth_ShaKey n) ∉ spied s"
by (rule auth_shakey_secret [OF C B])
ultimately show False by contradiction
next
fix B
assume "(Spy, S ⊗ B) ∈ s"
hence "S ⊗ B ∈ parts (used s)" by blast
hence "(∃m. S = Auth_PriK m ∧ (Asset m, ⦃Num 2, PubKey B⦄) ∈ s) ∨
{PriKey S, PriKey B} ⊆ spied s"
(is "(∃m. ?P m ∧ _) ∨ _")
by (rule parts_mult [OF C])
moreover assume "(Spy, Key (PriK S)) ∉ s"
ultimately obtain m where "?P m" by auto
moreover assume
"(Asset n, Crypt (ShaK (Auth_ShaK n)) (Key (PriK S))) ∈ s"
ultimately have "(Asset n, Crypt (Auth_ShaKey n) (Auth_PriKey m)) ∈ s"
by simp
thus False
by (rule auth_prikey_asset_i [OF C])
next
fix A
assume "(Spy, A ⊗ S) ∈ s"
hence "A ⊗ S ∈ parts (used s)" by blast
hence "(∃m. A = Auth_PriK m ∧ (Asset m, ⦃Num 2, PubKey S⦄) ∈ s) ∨
{PriKey A, PriKey S} ⊆ spied s"
(is "(∃m. _ ∧ ?P m) ∨ _")
by (rule parts_mult [OF C])
moreover assume "(Spy, Key (PriK S)) ∉ s"
ultimately obtain m where "?P m" by auto
assume "(Asset n, Crypt (ShaK (Auth_ShaK n)) (Key (PriK S))) ∈ s"
hence "(Asset n, Crypt (Auth_ShaKey n) (PriKey S)) ∈ s" by simp
thus False
by (rule asset_i_asset_ii [OF C _ ‹?P m›])
next
fix Y
assume "(Spy, ⦃Key (PriK S), Y⦄) ∈ s"
hence "⦃PriKey S, Y⦄ ∈ parts (used s)" by auto
hence "{PriKey S, Y} ⊆ spied s"
by (rule parts_mpair_key [OF C, where K = "PriK S"], simp)
moreover assume "(Spy, Key (PriK S)) ∉ s"
ultimately show False by simp
next
fix X
assume "(Spy, ⦃X, Key (PriK S)⦄) ∈ s"
hence "⦃X, PriKey S⦄ ∈ parts (used s)" by auto
hence "{X, PriKey S} ⊆ spied s"
by (rule parts_mpair_key [OF C, where K = "PriK S"], simp add: image_def)
moreover assume "(Spy, Key (PriK S)) ∉ s"
ultimately show False by simp
qed
qed
proposition owner_ii_secret [rule_format]:
"s⇩0 ⊨ s ⟹
(Owner n, ⦃Num 1, PubKey A⦄) ∈ s ⟶
PriKey A ∉ spied s"
proof (erule rtrancl_induct, simp add: image_def, rule impI)
fix s s'
assume
A: "s⇩0 ⊨ s" and
B: "s ⊢ s'" and
C: "(Owner n, ⦃Num 1, PubKey A⦄) ∈ s ⟶ PriKey A ∉ spied s" and
D: "(Owner n, ⦃Num 1, PubKey A⦄) ∈ s'"
show "PriKey A ∉ spied s'"
proof (insert B C D, auto simp add: rel_def)
assume "(Owner n, ⦃Num (Suc 0), Key (PubK A)⦄) ∈ s"
hence "(Owner n, ⦃Num 1, PubKey A⦄) ∈ s" by simp
hence "PriKey A ∈ used s"
by (rule owner_ii_used [OF A, THEN mp])
moreover assume "Key (PriK A) ∉ used s"
ultimately show False by simp
next
fix K
assume "(Spy, Crypt K (Key (PriK A))) ∈ s"
hence "Crypt K (PriKey A) ∈ parts (used s)" by auto
hence "(∃m. K = Auth_ShaKey m ∧
(Asset m, Crypt (Auth_ShaKey m) (PriKey A)) ∈ s) ∨
{PriKey A, Key K} ⊆ spied s"
(is "(∃m. _ ∧ ?P m) ∨ _")
by (rule parts_crypt_prikey [OF A])
moreover assume "(Spy, Key (PriK A)) ∉ s"
ultimately obtain m where "?P m" by auto
moreover assume "(Owner n, ⦃Num (Suc 0), Key (PubK A)⦄) ∈ s"
hence "(Owner n, ⦃Num 1, PubKey A⦄) ∈ s" by simp
ultimately show False
by (rule asset_i_owner_ii [OF A])
next
fix B
assume "(Spy, A ⊗ B) ∈ s"
hence "A ⊗ B ∈ parts (used s)" by blast
hence "(∃m. A = Auth_PriK m ∧ (Asset m, ⦃Num 2, PubKey B⦄) ∈ s) ∨
{PriKey A, PriKey B} ⊆ spied s"
(is "(∃m. ?P m ∧ _) ∨ _")
by (rule parts_mult [OF A])
moreover assume "(Spy, Key (PriK A)) ∉ s"
ultimately obtain m where "?P m" by auto
moreover assume "(Owner n, ⦃Num (Suc 0), Key (PubK A)⦄) ∈ s"
ultimately have "(Owner n, ⦃Num 1, Auth_PubKey m⦄) ∈ s" by simp
thus False
by (rule auth_pubkey_owner_ii [OF A])
next
fix B
assume "(Spy, B ⊗ A) ∈ s"
hence "B ⊗ A ∈ parts (used s)" by blast
hence "(∃m. B = Auth_PriK m ∧ (Asset m, ⦃Num 2, PubKey A⦄) ∈ s) ∨
{PriKey B, PriKey A} ⊆ spied s"
(is "(∃m. _ ∧ ?P m) ∨ _")
by (rule parts_mult [OF A])
moreover assume "(Spy, Key (PriK A)) ∉ s"
ultimately obtain m where "?P m" by auto
moreover assume "(Owner n, ⦃Num (Suc 0), Key (PubK A)⦄) ∈ s"
hence "(Owner n, ⦃Num 1, PubKey A⦄) ∈ s" by simp
ultimately show False
by (rule asset_ii_owner_ii [OF A])
next
fix Y
assume "(Spy, ⦃Key (PriK A), Y⦄) ∈ s"
hence "⦃PriKey A, Y⦄ ∈ parts (used s)" by auto
hence "{PriKey A, Y} ⊆ spied s"
by (rule parts_mpair_key [OF A, where K = "PriK A"], simp)
moreover assume "(Spy, Key (PriK A)) ∉ s"
ultimately show False by simp
next
fix X
assume "(Spy, ⦃X, Key (PriK A)⦄) ∈ s"
hence "⦃X, PriKey A⦄ ∈ parts (used s)" by auto
hence "{X, PriKey A} ⊆ spied s"
by (rule parts_mpair_key [OF A, where K = "PriK A"], simp add: image_def)
moreover assume "(Spy, Key (PriK A)) ∉ s"
ultimately show False by simp
qed
qed
proposition seskey_spied [rule_format]:
"s⇩0 ⊨ s ⟹
SesKey SK ∈ spied s ⟶
(∃S A C. fst SK = Some S ∧ A ∈ fst (snd SK) ∧ C ∈ snd (snd SK) ∧
{PriKey S, PriKey A, PriKey C} ⊆ spied s)"
(is "_ ⟹ _ ⟶ (∃S A C. ?P S A C s)")
proof (erule rtrancl_induct, simp add: image_def, rule impI)
fix s s'
assume
A: "s⇩0 ⊨ s" and
B: "s ⊢ s'" and
C: "SesKey SK ∈ spied s ⟶ (∃S A C. ?P S A C s)" and
D: "SesKey SK ∈ spied s'"
show "∃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))) ∈ s"
hence "Crypt K (Key (SesK SK)) ∈ parts (used s)" by blast
hence "{Key (SesK SK), Key K} ⊆ spied s"
by (rule parts_crypt_key [OF A], simp add: image_def)
moreover assume "(Spy, Key (SesK SK)) ∉ s"
ultimately show False by simp
next
fix Y
assume "(Spy, ⦃Key (SesK SK), Y⦄) ∈ s"
hence "⦃SesKey SK, Y⦄ ∈ parts (used s)" by auto
hence "{SesKey SK, Y} ⊆ spied s"
by (rule parts_mpair_key [OF A, where K = "SesK SK"], simp)
moreover assume "(Spy, Key (SesK SK)) ∉ s"
ultimately show False by simp
next
fix X
assume "(Spy, ⦃X, Key (SesK SK)⦄) ∈ s"
hence "⦃X, SesKey SK⦄ ∈ parts (used s)" by auto
hence "{X, SesKey SK} ⊆ spied s"
by (rule parts_mpair_key [OF A, where K = "SesK SK"], simp add: image_def)
moreover assume "(Spy, Key (SesK SK)) ∉ s"
ultimately show False by simp
qed
qed
proposition owner_seskey_shakey:
assumes
A: "s⇩0 ⊨ s" and
B: "n ∉ bad_shakey" and
C: "(Owner n, SesKey SK) ∈ s"
shows "SesKey SK ∉ spied s"
proof
have "(∃S. fst SK = Some S ∧ Crypt (Auth_ShaKey n) (PriKey S) ∈ used s) ∨
fst SK = None"
(is "(∃S. ?P S) ∨ _")
by (rule owner_seskey_nonce [OF A C])
moreover assume "SesKey SK ∈ spied s"
hence D: "∃S A C. fst SK = Some S ∧ A ∈ fst (snd SK) ∧
C ∈ snd (snd SK) ∧ {PriKey S, PriKey A, PriKey C} ⊆ spied s"
by (rule seskey_spied [OF A])
ultimately obtain S where "?P S" by auto
hence "Crypt (Auth_ShaKey n) (PriKey S) ∈ parts (used s)" by blast
hence "(∃m. Auth_ShaKey n = Auth_ShaKey m ∧
(Asset m, Crypt (Auth_ShaKey m) (PriKey S)) ∈ s) ∨
{PriKey S, Key (Auth_ShaKey n)} ⊆ spied s"
(is "(∃m. ?Q m ∧ ?R m) ∨ _")
by (rule parts_crypt_prikey [OF A])
moreover have "Key (Auth_ShaKey n) ∉ spied s"
by (rule auth_shakey_secret [OF A B])
ultimately obtain m where "?Q m" and "?R m" by blast
hence "m ∉ bad_shakey"
using B by simp
hence "PriKey S ∉ spied s"
by (rule asset_i_secret [OF A _ ‹?R m›])
moreover have "PriKey S ∈ spied s"
using D and ‹?P S› by auto
ultimately show False by contradiction
qed
proposition owner_seskey_prikey:
assumes
A: "s⇩0 ⊨ s" and
B: "n ∉ bad_prikey" and
C: "(Owner m, SesKey SK) ∈ s" and
D: "(Asset n, ⦃Num 2, PubKey B⦄) ∈ s" and
E: "B ∈ fst (snd SK)"
shows "SesKey SK ∉ spied s"
proof
have "∃A B C D. fst (snd SK) = {A, B} ∧ snd (snd SK) = {C, D} ∧
(Owner m, ⦃Num 1, PubKey A⦄) ∈ s ∧
(Owner m, ⦃Num 3, PubKey C⦄) ∈ s ∧
(Owner m, Crypt (SesK SK) (PubKey D)) ∈ s"
(is "∃A B C D. ?P A B ∧ _ ∧ ?Q A ∧ _")
by (rule owner_seskey_other [OF A C])
then obtain A B' where "?P A B'" and "?Q A" by blast
assume "SesKey SK ∈ spied s"
hence "∃S A' C. fst SK = Some S ∧ A' ∈ fst (snd SK) ∧ C ∈ snd (snd SK) ∧
{PriKey S, PriKey A', PriKey C} ⊆ spied s"
(is "∃S A' C. _ ∧ ?R A' ∧ _")
by (rule seskey_spied [OF A])
then obtain A' where "A' ∈ fst (snd SK)" and "PriKey A' ∈ spied s" (is "?R A'")
by blast
hence "{A', A, B} ⊆ {A, B'}"
using E and ‹?P A B'› by simp
hence "card {A', A, B} ≤ card {A, B'}"
by (rule_tac card_mono, simp)
also have "… ≤ Suc (Suc 0)"
by (rule card_insert_le_m1, simp_all)
finally have "card {A', A, B} ≤ 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 "¬ ?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 "¬ ?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, ⦃Num 2, PubKey A⦄) ∈ 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⇩0 ⊨ s" and
B: "n ∉ bad_shakey" and
C: "(Asset n, SesKey SK) ∈ s"
shows "SesKey SK ∉ spied s"
proof
have "∃S. fst SK = Some S ∧
(Asset n, Crypt (Auth_ShaKey n) (PriKey S)) ∈ s"
(is "∃S. ?P S ∧ ?Q S")
by (rule asset_seskey_nonce [OF A C])
then obtain S where "?P S" and "?Q S" by blast
have "PriKey S ∉ spied s"
by (rule asset_i_secret [OF A B ‹?Q S›])
moreover assume "SesKey SK ∈ spied s"
hence "∃S A C. fst SK = Some S ∧ A ∈ fst (snd SK) ∧ C ∈ snd (snd SK) ∧
{PriKey S, PriKey A, PriKey C} ⊆ spied s"
by (rule seskey_spied [OF A])
hence "PriKey S ∈ spied s"
using ‹?P S› by auto
ultimately show False by contradiction
qed
theorem owner_seskey_unique:
assumes
A: "s⇩0 ⊨ s" and
B: "(Owner m, Crypt (SesK SK) (Pwd m)) ∈ s" and
C: "(Owner n, Crypt (SesK SK) (Pwd n)) ∈ s"
shows "m = n"
proof (rule ccontr)
have D: "(Owner m, SesKey SK) ∈ s ∧
(∃A B C. Token m A B C SK ∈ used s ∧ B ∈ fst (snd SK))"
(is "?P m ∧ (∃A B C. ?Q m A B C)")
by (rule owner_v_state [OF A B])
hence "?P m" by blast
hence "∃A B C D. fst (snd SK) = {A, B} ∧ snd (snd SK) = {C, D} ∧
(Owner m, ⦃Num 1, PubKey A⦄) ∈ s ∧
(Owner m, ⦃Num 3, PubKey C⦄) ∈ s ∧
(Owner m, Crypt (SesK SK) (PubKey D)) ∈ s"
(is "∃A B C D. ?R A B ∧ ?S C D ∧ ?T m A ∧ ?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 ∧ (∃A B C. ?Q n A B C)"
by (rule owner_v_state [OF A C])
hence "?P n" by blast
hence "∃A B C D. ?R A B ∧ ?S C D ∧ ?T n A ∧ ?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 ∈ parts (used s)" by blast
hence "Crypt (SesK SK) (A'' ⊗ B'') ∈ parts (used s)" by blast
hence "B'' ∈ fst (snd SK) ∧
(∃i C'. (Asset i, Token i (Auth_PriK i) B'' C' SK) ∈ s) ∨
{A'' ⊗ B'', SesKey SK} ⊆ spied s"
(is "?V B'' ∧ (∃i C'. ?W i B'' C') ∨ _")
by (rule parts_crypt_mult [OF A])
hence "∃D. ?V D ∧ D ∉ {A, A'}"
proof (rule disjE, (erule_tac conjE, ((erule_tac exE)+)?)+)
fix i C'
assume "?V B''" and "?W i B'' C'"
have "∃A D. ?R A B'' ∧ ?S C' D ∧
(Asset i, ⦃Num 2, PubKey B''⦄) ∈ s ∧ (Asset i, ⦃Num 4, PubKey D⦄) ∈ s ∧
Crypt (SesK SK) (PubKey D) ∈ used s ∧ (Asset i, PubKey B'') ∈ s"
(is "∃A D. _ ∧ _ ∧ ?X i B'' ∧ _")
by (rule asset_iv_state [OF A ‹?W i B'' C'›])
hence "?X i B''" by blast
have "B'' ≠ 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'' ≠ 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'' ⊗ B'', SesKey SK} ⊆ spied s"
hence "SesKey SK ∈ spied s" by simp
hence "∃S D E. fst SK = Some S ∧ ?V D ∧ E ∈ snd (snd SK) ∧
{PriKey S, PriKey D, PriKey E} ⊆ spied s"
by (rule seskey_spied [OF A])
then obtain D where "?V D" and "PriKey D ∈ spied s" (is "?X D")
by blast
moreover have "D ≠ A"
proof
assume "D = A"
hence "?X A"
using ‹?X D› by simp
moreover have "¬ ?X A"
by (rule owner_ii_secret [OF A ‹?T m A›])
ultimately show False by contradiction
qed
moreover have "D ≠ A'"
proof
assume "D = A'"
hence "?X A'"
using ‹?X D› by simp
moreover have "¬ ?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 ∉ {A, A'}" by blast
hence "{D, A, A'} ⊆ {A, B}"
using ‹?R A B› and ‹?R A' B'› by blast
hence "card {D, A, A'} ≤ card {A, B}"
by (rule_tac card_mono, simp)
also have "… ≤ Suc (Suc 0)"
by (rule card_insert_le_m1, simp_all)
finally have "card {D, A, A'} ≤ Suc (Suc 0)" .
moreover have "card {D, A, A'} = Suc (card {A, A'})"
by (rule card_insert_disjoint [OF _ E], simp)
moreover assume "m ≠ 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⇩0 ⊨ s" and
B: "n ∉ bad_shakey ∩ bad_prikey" and
C: "(Owner n, Crypt (SesK SK) (Pwd n)) ∈ s"
shows "SesKey SK ∉ spied s"
proof -
have "(Owner n, SesKey SK) ∈ s ∧
(∃A B C. Token n A B C SK ∈ used s ∧ B ∈ fst (snd SK))"
(is "?P ∧ (∃A B C. ?Q A B C ∧ ?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 ∈ bad_shakey ∨ n ∉ bad_shakey" by simp
moreover {
assume "n ∈ bad_shakey"
hence D: "n ∉ bad_prikey"
using B by simp
hence "Auth_PriKey n ∉ spied s"
by (rule auth_prikey_secret [OF A])
moreover have "Sign n A ∈ 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 ⊗ B ∈ parts (used s)" by blast
hence "(∃m. Auth_PriK n = Auth_PriK m ∧
(Asset m, ⦃Num 2, PubKey B⦄) ∈ s) ∨
{PriKey (Auth_PriK n), PriKey B} ⊆ spied s"
(is "(∃m. ?S m ∧ ?T m) ∨ _")
by (rule parts_mult [OF A])
ultimately obtain m where "?S m" and "?T m" by auto
hence "m ∉ bad_prikey"
using D by simp
hence ?thesis
by (rule owner_seskey_prikey [OF A _ ‹?P› ‹?T m› ‹?R B›])
}
moreover {
assume "n ∉ bad_shakey"
hence ?thesis
by (rule owner_seskey_shakey [OF A _ ‹?P›])
}
ultimately show ?thesis ..
qed
theorem owner_num_genuine:
assumes
A: "s⇩0 ⊨ s" and
B: "n ∉ bad_shakey ∩ bad_prikey" and
C: "(Owner n, Crypt (SesK SK) (Pwd n)) ∈ s" and
D: "Crypt (SesK SK) (Num 0) ∈ used s"
shows "(Asset n, Crypt (SesK SK) (Num 0)) ∈ s"
proof -
have "Crypt (SesK SK) (Num 0) ∈ parts (used s)"
using D ..
hence "(∃m. (Asset m, Crypt (SesK SK) (Num 0)) ∈ s) ∨
SesKey SK ∈ spied s"
by (rule parts_crypt_num [OF A])
moreover have E: "SesKey SK ∉ spied s"
by (rule owner_seskey_secret [OF A B C])
ultimately obtain m where "(Asset m, Crypt (SesK SK) (Num 0)) ∈ s"
by blast
moreover from this have "(Asset m, SesKey SK) ∈ s ∧
Crypt (SesK SK) (Pwd m) ∈ used s"
by (rule asset_v_state [OF A])
hence "Crypt (SesK SK) (Pwd m) ∈ parts (used s)" by blast
hence "(∃SK'. SesK SK = SesK SK' ∧
(Owner m, Crypt (SesK SK') (Pwd m)) ∈ s) ∨
{Pwd m, Key (SesK SK)} ⊆ spied s"
by (rule parts_crypt_pwd [OF A])
hence "(Owner m, Crypt (SesK SK) (Pwd m)) ∈ 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⇩0 ⊨ s" and
B: "n ∉ bad_shakey ∩ bad_prikey" and
C: "(Owner n, ⦃Num 3, PubKey C⦄) ∈ s" and
D: "(Owner n, Crypt (SesK SK) (Pwd n)) ∈ s" and
E: "Token n A B C SK ∈ used s"
shows "A = Auth_PriK n ∧ B ∈ fst (snd SK) ∧ C ∈ snd (snd SK) ∧
(Asset n, ⦃Num 2, PubKey B⦄) ∈ s ∧ (Asset n, Token n A B C SK) ∈ s"
(is "?P n A ∧ ?Q B ∧ ?R C ∧ ?S n B ∧ _")
proof -
have "Crypt (SesK SK) (Sign n A) ∈ parts (used s)"
using E by blast
hence "(Asset n, SesKey SK) ∈ s ∨ SesKey SK ∈ spied s"
by (rule parts_crypt_sign [OF A])
moreover have "SesKey SK ∉ spied s"
by (rule owner_seskey_secret [OF A B D])
ultimately have "(Asset n, SesKey SK) ∈ s" by simp
hence "∃A B C D. fst (snd SK) = {A, B} ∧ snd (snd SK) = {C, D} ∧
?S n B ∧ (Asset n, ⦃Num 4, PubKey D⦄) ∈ s ∧
(Asset n, Token n (Auth_PriK n) B C SK) ∈ s"
(is "∃A B C D. ?T A B ∧ ?U C D ∧ _ ∧ ?V n D ∧ ?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 ∈ parts (used s)"
using E by blast
hence "?P n A"
by (rule parts_sign [OF A])
have "Crypt (SesK SK) (A ⊗ B) ∈ parts (used s)"
using E by blast
hence "?Q B ∧ (∃m C''. ?W m B C'') ∨ {A ⊗ B, SesKey SK} ⊆ spied s"
by (rule parts_crypt_mult [OF A])
moreover have F: "SesKey SK ∉ 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 "∃A D. ?T A B ∧ ?U C'' D ∧ ?S m B ∧ ?V m D ∧
Crypt (SesK SK) (PubKey D) ∈ used s ∧ (Asset m, PubKey B) ∈ s"
by (rule asset_iv_state [OF A ‹?W m B C''›])
hence "?S m B" by blast
have "(Owner n, SesKey SK) ∈ s ∧
(∃A B C. Token n A B C SK ∈ used s ∧ B ∈ fst (snd SK))"
by (rule owner_v_state [OF A D])
hence "(Owner n, SesKey SK) ∈ s" by blast
hence "∃A B C D. ?T A B ∧ ?U C D ∧
(Owner n, ⦃Num 1, PubKey A⦄) ∈ s ∧
(Owner n, ⦃Num 3, PubKey C⦄) ∈ s ∧
(Owner n, Crypt (SesK SK) (PubKey D)) ∈ s"
(is "∃A B C D. _ ∧ _ ∧ ?X A ∧ _")
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} ⊆ {A', B'}"
using ‹?T A' B'› and ‹?Q B› and ‹?Q A''› by simp
hence "card {A'', B', B} ≤ card {A', B'}"
by (rule_tac card_mono, simp)
also have "… ≤ Suc (Suc 0)"
by (rule card_insert_le_m1, simp_all)
finally have "card {A'', B', B} ≤ Suc (Suc 0)" .
moreover have "A'' ∉ {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' ≠ 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) ∈ parts (used s)"
using E by blast
hence "?R C ∧ ((∃n. (Owner n, SesKey SK) ∈ s) ∨ (∃n B. ?W n B C)) ∨
SesKey SK ∈ spied s"
by (rule parts_crypt_pubkey [OF A])
hence "?R C"
using F by simp
hence "C ∈ {C', D}"
using ‹?U C' D› by simp
moreover have "C ≠ 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) ∈ 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⇩0 ⊨ s" and
B: "n ∉ bad_pwd ∪ bad_shakey ∩ bad_prikey"
shows "Pwd n ∉ spied s"
proof (rule rtrancl_induct [OF A], insert B, simp add: image_def)
fix s s'
assume
C: "s⇩0 ⊨ s" and
D: "s ⊢ s'" and
E: "Pwd n ∉ spied s"
show "Pwd n ∉ spied s'"
proof (insert D E, auto simp add: rel_def)
fix K
assume "(Spy, Crypt K (Pwd n)) ∈ s"
hence "Crypt K (Pwd n) ∈ parts (used s)" by blast
hence "(∃SK. K = SesK SK ∧ (Owner n, Crypt (SesK SK) (Pwd n)) ∈ s) ∨
{Pwd n, Key K} ⊆ spied s"
(is "(∃SK. ?P SK ∧ ?Q SK) ∨ _")
by (rule parts_crypt_pwd [OF C])
then obtain SK where "?P SK" and "?Q SK"
using E by blast
have "n ∉ bad_shakey ∩ bad_prikey"
using B by simp
hence "SesKey SK ∉ spied s"
by (rule owner_seskey_secret [OF C _ ‹?Q SK›])
moreover assume "(Spy, Key (InvK K)) ∈ s"
ultimately show False
using ‹?P SK› by simp
next
fix Y
assume "(Spy, ⦃Pwd n, Y⦄) ∈ s"
hence "⦃Pwd n, Y⦄ ∈ parts (used s)" by blast
hence "{Pwd n, Y} ⊆ spied s"
by (rule parts_mpair_pwd [OF C, where n = n], simp)
with E show False by simp
next
fix X
assume "(Spy, ⦃X, Pwd n⦄) ∈ s"
hence "⦃X, Pwd n⦄ ∈ parts (used s)" by blast
hence "{X, Pwd n} ⊆ 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⇩0 ⊨ s" and
B: "(Asset m, Token m (Auth_PriK m) B' C' SK) ∈ s" and
C: "(Asset n, Token n (Auth_PriK n) B C SK) ∈ s"
(is "?P n B C SK s")
shows "m = n ∧ B' = B ∧ 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' ≠ B"
moreover have "∃A D. fst (snd SK) = {A, B'} ∧ snd (snd SK) = {C', D} ∧
(Asset m, ⦃Num 2, PubKey B'⦄) ∈ s ∧ (Asset m, ⦃Num 4, PubKey D⦄) ∈ s ∧
Crypt (SesK SK) (PubKey D) ∈ used s ∧ (Asset m, PubKey B') ∈ 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, ⦃Num 2, PubKey B'⦄) ∈ s"
by blast
moreover have "?Q n B C"
by (rule asset_iv_state [OF A C])
hence "B ∈ fst (snd SK)" and "(Asset n, ⦃Num 2, PubKey B⦄) ∈ s"
by auto
ultimately have D: "∀A ∈ fst (snd SK).
∃i C. (Asset i, ⦃Num 2, PubKey A⦄) ∈ s ∧ ?P i A C SK s"
using B and C by auto
have "Crypt (SesK SK) (PubKey C) ∈ 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) ∈ s"
hence "∃A B C D. fst (snd SK) = {A, B} ∧ snd (snd SK) = {C, D} ∧
(Owner i, ⦃Num 1, PubKey A⦄) ∈ s ∧
(Owner i, ⦃Num 3, PubKey C⦄) ∈ s ∧
(Owner i, Crypt (SesK SK) (PubKey D)) ∈ s"
by (rule owner_seskey_other [OF A])
then obtain A where "A ∈ fst (snd SK)" and
E: "(Owner i, ⦃Num 1, PubKey A⦄) ∈ s"
by blast
then obtain j where "(Asset j, ⦃Num 2, PubKey A⦄) ∈ s"
using D by blast
thus False
by (rule asset_ii_owner_ii [OF A _ E])
next
assume "SesKey SK ∈ spied s"
hence "∃S A C. fst SK = Some S ∧ A ∈ fst (snd SK) ∧ C ∈ snd (snd SK) ∧
{PriKey S, PriKey A, PriKey C} ⊆ spied s"
(is "?R s")
by (rule seskey_spied [OF A])
moreover have "¬ (∃A ∈ fst (snd SK). PriKey A ∈ spied s)"
(is "¬ ?S s")
proof
assume "?S s"
moreover have "¬ ?S s⇩0"
by (subst bex_simps, rule ballI, drule bspec [OF D], (erule exE)+,
erule conjE, rule asset_ii_init [OF A])
ultimately have "∃u v. s⇩0 ⊨ u ∧ u ⊢ v ∧ v ⊨ s ∧ ¬ ?S u ∧ ?S v"
by (rule rtrancl_start [OF A])
then obtain u v A where E: "s⇩0 ⊨ u" and F: "u ⊢ v" and G: "v ⊨ s" and
H: "¬ ?S u" and I: "A ∈ fst (snd SK)" and J: "PriKey A ∉ spied u" and
K: "PriKey A ∈ spied v"
by blast
then obtain i where "(Asset i, ⦃Num 2, PubKey A⦄) ∈ s"
using D by blast
hence "(Asset i, ⦃Num 2, PubKey A⦄) ∈ v"
proof (rule_tac ccontr, drule_tac rtrancl_start [OF G], simp,
(erule_tac exE)+, (erule_tac conjE)+)
fix w x
assume "w ⊢ x" and "(Asset i, ⦃Num 2, PubKey A⦄) ∉ w" and
"(Asset i, ⦃Num 2, PubKey A⦄) ∈ x"
hence "PriKey A ∉ spied w"
by (auto simp add: rel_def)
moreover assume "v ⊨ w"
hence "PriKey A ∈ spied w"
by (rule_tac rev_subsetD [OF K], rule spied_subset)
ultimately show False by contradiction
qed
hence "(Asset i, ⦃Num 2, PubKey A⦄) ∈ u"
using F and K by (auto simp add: rel_def)
hence "Auth_PriKey i ∈ spied u ∧ (∃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 ⊨ 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 ∧ C' = C ∧ SK' = SK"
by (rule asset_iv_unique [OF A])
hence "Crypt (SesK SK) (PubKey C) ∈ 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) ∈ u"
hence "∃A B C D. fst (snd SK) = {A, B} ∧ snd (snd SK) = {C, D} ∧
(Owner i, ⦃Num 1, PubKey A⦄) ∈ u ∧
(Owner i, ⦃Num 3, PubKey C⦄) ∈ u ∧
(Owner i, Crypt (SesK SK) (PubKey D)) ∈ u"
by (rule owner_seskey_other [OF E])
then obtain A where "A ∈ fst (snd SK)" and
N: "(Owner i, ⦃Num 1, PubKey A⦄) ∈ u"
by blast
then obtain j where "(Asset j, ⦃Num 2, PubKey A⦄) ∈ s"
using D by blast
moreover have "(Owner i, ⦃Num 1, PubKey A⦄) ∈ 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 ∈ 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⇩0 ⊨ s" and
B: "n ∉ bad_shakey ∩ (bad_pwd ∪ bad_prikey)" and
C: "(Asset n, Crypt (SesK SK) (Num 0)) ∈ s"
shows "SesKey SK ∉ spied s"
proof -
have D: "(Asset n, SesKey SK) ∈ s ∧ Crypt (SesK SK) (Pwd n) ∈ used s"
by (rule asset_v_state [OF A C])
have "n ∈ bad_shakey ∨ n ∉ bad_shakey" by simp
moreover {
assume "n ∈ bad_shakey"
hence "Pwd n ∉ spied s"
using B by (rule_tac pwd_secret [OF A], simp)
moreover have "Crypt (SesK SK) (Pwd n) ∈ parts (used s)"
using D by blast
hence "(∃SK'. SesK SK = SesK SK' ∧
(Owner n, Crypt (SesK SK') (Pwd n)) ∈ s) ∨
{Pwd n, Key (SesK SK)} ⊆ spied s"
by (rule parts_crypt_pwd [OF A])
ultimately have "(Owner n, Crypt (SesK SK) (Pwd n)) ∈ s" by simp
hence ?thesis
using B by (rule_tac owner_seskey_secret [OF A], simp_all)
}
moreover {
assume "n ∉ 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⇩0 ⊨ s" and
B: "n ∉ bad_shakey ∩ (bad_pwd ∪ bad_prikey)" and
C: "(Asset n, Crypt (SesK SK) (Num 0)) ∈ s"
shows "(Owner n, Crypt (SesK SK) (Pwd n)) ∈ s"
proof -
have "(Asset n, SesKey SK) ∈ s ∧ Crypt (SesK SK) (Pwd n) ∈ used s"
by (rule asset_v_state [OF A C])
hence "Crypt (SesK SK) (Pwd n) ∈ parts (used s)" by blast
hence "(∃SK'. SesK SK = SesK SK' ∧
(Owner n, Crypt (SesK SK') (Pwd n)) ∈ s) ∨
{Pwd n, Key (SesK SK)} ⊆ spied s"
by (rule parts_crypt_pwd [OF A])
moreover have "SesKey SK ∉ spied s"
by (rule asset_seskey_secret [OF A B C])
ultimately show ?thesis by simp
qed
theorem asset_token_genuine:
assumes
A: "s⇩0 ⊨ s" and
B: "n ∉ bad_shakey ∩ (bad_pwd ∪ bad_prikey)" and
C: "(Asset n, ⦃Num 4, PubKey D⦄) ∈ s" and
D: "(Asset n, Crypt (SesK SK) (Num 0)) ∈ s" and
E: "D ∈ snd (snd SK)"
shows "(Owner n, Crypt (SesK SK) (PubKey D)) ∈ s"
proof -
have "(Owner n, Crypt (SesK SK) (Pwd n)) ∈ s"
by (rule asset_pwd_genuine [OF A B D])
hence "(Owner n, SesKey SK) ∈ s ∧
(∃A B C. Token n A B C SK ∈ used s ∧ B ∈ fst (snd SK))"
by (rule owner_v_state [OF A])
hence "(Owner n, SesKey SK) ∈ s" ..
hence "∃A B C D. fst (snd SK) = {A, B} ∧ snd (snd SK) = {C, D} ∧
(Owner n, ⦃Num 1, PubKey A⦄) ∈ s ∧
(Owner n, ⦃Num 3, PubKey C⦄) ∈ s ∧
(Owner n, Crypt (SesK SK) (PubKey D)) ∈ s"
(is "∃A B C D. _ ∧ ?P C D ∧ _ ∧ ?Q C ∧ ?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 ≠ 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
proposition owner_iii_secret [rule_format]:
"s⇩0 ⊨ s ⟹
(Owner n, ⦃Num 3, PubKey C⦄) ∈ s ⟶
PriKey C ∉ spied s"
proof (erule rtrancl_induct, simp add: image_def, rule impI)
fix s s'
assume
A: "s⇩0 ⊨ s" and
B: "s ⊢ s'" and
C: "(Owner n, ⦃Num 3, PubKey C⦄) ∈ s ⟶ PriKey C ∉ spied s" and
D: "(Owner n, ⦃Num 3, PubKey C⦄) ∈ s'"
show "PriKey C ∉ spied s'"
proof (insert B C D, auto simp add: rel_def)
assume "(Owner n, ⦃Num 3, Key (PubK C)⦄) ∈ s"
hence "(Owner n, ⦃Num 3, PubKey C⦄) ∈ s" by simp
hence "PriKey C ∈ used s"
by (rule owner_iii_used [OF A, THEN mp])
moreover assume "Key (PriK C) ∉ used s"
ultimately show False by simp
next
fix K
assume "(Spy, Crypt K (Key (PriK C))) ∈ s"
hence "Crypt K (PriKey C) ∈ parts (used s)" by auto
hence "(∃m. K = Auth_ShaKey m ∧
(Asset m, Crypt (Auth_ShaKey m) (PriKey C)) ∈ s) ∨
{PriKey C, Key K} ⊆ spied s"
(is "(∃m. _ ∧ ?P m) ∨ _")
by (rule parts_crypt_prikey [OF A])
moreover assume "(Spy, Key (PriK C)) ∉ s"
ultimately obtain m where "?P m" by auto
moreover assume "(Owner n, ⦃Num 3, Key (PubK C)⦄) ∈ s"
hence "(Owner n, ⦃Num 3, PubKey C⦄) ∈ s" by simp
ultimately show False
by (rule asset_i_owner_iii [OF A])
next
fix A
assume "(Spy, C ⊗ A) ∈ s"
hence "C ⊗ A ∈ parts (used s)" by blast
hence "(∃m. C = Auth_PriK m ∧ (Asset m, ⦃Num 2, PubKey A⦄) ∈ s) ∨
{PriKey C, PriKey A} ⊆ spied s"
(is "(∃m. ?P m ∧ _) ∨ _")
by (rule parts_mult [OF A])
moreover assume "(Spy, Key (PriK C)) ∉ s"
ultimately obtain m where "?P m" by auto
moreover assume "(Owner n, ⦃Num 3, Key (PubK C)⦄) ∈ s"
ultimately have "(Owner n, ⦃Num 3, Auth_PubKey m⦄) ∈ s" by simp
thus False
by (rule auth_pubkey_owner_iii [OF A])
next
fix A
assume "(Spy, A ⊗ C) ∈ s"
hence "A ⊗ C ∈ parts (used s)" by blast
hence "(∃m. A = Auth_PriK m ∧ (Asset m, ⦃Num 2, PubKey C⦄) ∈ s) ∨
{PriKey A, PriKey C} ⊆ spied s"
(is "(∃m. _ ∧ ?P m) ∨ _")
by (rule parts_mult [OF A])
moreover assume "(Spy, Key (PriK C)) ∉ s"
ultimately obtain m where "?P m" by auto
moreover assume "(Owner n, ⦃Num 3, Key (PubK C)⦄) ∈ s"
hence "(Owner n, ⦃Num 3, PubKey C⦄) ∈ s" by simp
ultimately show False
by (rule asset_ii_owner_iii [OF A])
next
fix Y
assume "(Spy, ⦃Key (PriK C), Y⦄) ∈ s"
hence "⦃PriKey C, Y⦄ ∈ parts (used s)" by auto
hence "{PriKey C, Y} ⊆ spied s"
by (rule parts_mpair_key [OF A, where K = "PriK C"], simp)
moreover assume "(Spy, Key (PriK C)) ∉ s"
ultimately show False by simp
next
fix X
assume "(Spy, ⦃X, Key (PriK C)⦄) ∈ s"
hence "⦃X, PriKey C⦄ ∈ parts (used s)" by auto
hence "{X, PriKey C} ⊆ spied s"
by (rule parts_mpair_key [OF A, where K = "PriK C"], simp add: image_def)
moreover assume "(Spy, Key (PriK C)) ∉ s"
ultimately show False by simp
qed
qed
proposition asset_iii_secret [rule_format]:
"s⇩0 ⊨ s ⟹
(Asset n, ⦃Num 4, PubKey D⦄) ∈ s ⟶
PriKey D ∉ spied s"
proof (erule rtrancl_induct, simp add: image_def, rule impI)
fix s s'
assume
A: "s⇩0 ⊨ s" and
B: "s ⊢ s'" and
C: "(Asset n, ⦃Num 4, PubKey D⦄) ∈ s ⟶ PriKey D ∉ spied s" and
D: "(Asset n, ⦃Num 4, PubKey D⦄) ∈ s'"
show "PriKey D ∉ spied s'"
proof (insert B C D, auto simp add: rel_def)
assume "(Asset n, ⦃Num 4, Key (PubK D)⦄) ∈ s"
hence "(Asset n, ⦃Num 4, PubKey D⦄) ∈ s" by simp
hence "PriKey D ∈ used s"
by (rule asset_iii_used [OF A, THEN mp])
moreover assume "Key (PriK D) ∉ used s"
ultimately show False by simp
next
fix K
assume "(Spy, Crypt K (Key (PriK D))) ∈ s"
hence "Crypt K (PriKey D) ∈ parts (used s)" by auto
hence "(∃m. K = Auth_ShaKey m ∧
(Asset m, Crypt (Auth_ShaKey m) (PriKey D)) ∈ s) ∨
{PriKey D, Key K} ⊆ spied s"
(is "(∃m. _ ∧ ?P m) ∨ _")
by (rule parts_crypt_prikey [OF A])
moreover assume "(Spy, Key (PriK D)) ∉ s"
ultimately obtain m where "?P m" by auto
moreover assume "(Asset n, ⦃Num 4, Key (PubK D)⦄) ∈ s"
hence "(Asset n, ⦃Num 4, PubKey D⦄) ∈ s" by simp
ultimately show False
by (rule asset_i_asset_iii [OF A])
next
fix A
assume "(Spy, D ⊗ A) ∈ s"
hence "D ⊗ A ∈ parts (used s)" by blast
hence "(∃m. D = Auth_PriK m ∧ (Asset m, ⦃Num 2, PubKey A⦄) ∈ s) ∨
{PriKey D, PriKey A} ⊆ spied s"
(is "(∃m. ?P m ∧ _) ∨ _")
by (rule parts_mult [OF A])
moreover assume "(Spy, Key (PriK D)) ∉ s"
ultimately obtain m where "?P m" by auto
moreover assume "(Asset n, ⦃Num 4, Key (PubK D)⦄) ∈ s"
ultimately have "(Asset n, ⦃Num 4, Auth_PubKey m⦄) ∈ s" by simp
thus False
by (rule auth_pubkey_asset_iii [OF A])
next
fix A
assume "(Spy, A ⊗ D) ∈ s"
hence "A ⊗ D ∈ parts (used s)" by blast
hence "(∃m. A = Auth_PriK m ∧ (Asset m, ⦃Num 2, PubKey D⦄) ∈ s) ∨
{PriKey A, PriKey D} ⊆ spied s"
(is "(∃m. _ ∧ ?P m) ∨ _")
by (rule parts_mult [OF A])
moreover assume "(Spy, Key (PriK D)) ∉ s"
ultimately obtain m where "?P m" by auto
moreover assume "(Asset n, ⦃Num 4, Key (PubK D)⦄) ∈ s"
hence "(Asset n, ⦃Num 4, PubKey D⦄) ∈ s" by simp
ultimately show False
by (rule asset_ii_asset_iii [OF A])
next
fix Y
assume "(Spy, ⦃Key (PriK D), Y⦄) ∈ s"
hence "⦃PriKey D, Y⦄ ∈ parts (used s)" by auto
hence "{PriKey D, Y} ⊆ spied s"
by (rule parts_mpair_key [OF A, where K = "PriK D"], simp)
moreover assume "(Spy, Key (PriK D)) ∉ s"
ultimately show False by simp
next
fix X
assume "(Spy, ⦃X, Key (PriK D)⦄) ∈ s"
hence "⦃X, PriKey D⦄ ∈ parts (used s)" by auto
hence "{X, PriKey D} ⊆ spied s"
by (rule parts_mpair_key [OF A, where K = "PriK D"], simp add: image_def)
moreover assume "(Spy, Key (PriK D)) ∉ s"
ultimately show False by simp
qed
qed
theorem seskey_forward_secret:
assumes
A: "s⇩0 ⊨ s" and
B: "(Owner m, Crypt (SesK SK) (Pwd m)) ∈ s" and
C: "(Asset n, Crypt (SesK SK) (Num 0)) ∈ s"
shows "m = n ∧ SesKey SK ∉ spied s"
proof -
have "(Owner m, SesKey SK) ∈ s"
using A and B by (drule_tac owner_v_state, auto)
with A have "∃C D. snd (snd SK) = {C, D} ∧
(Owner m, ⦃Num 3, PubKey C⦄) ∈ s"
by (drule_tac owner_seskey_other, auto)
then obtain C D where
D: "snd (snd SK) = {C, D} ∧ (Owner m, ⦃Num 3, PubKey C⦄) ∈ s"
by blast
with A have "PriKey C ∉ spied s"
by (erule_tac owner_iii_secret, simp)
moreover have "(Asset n, SesKey SK) ∈ s"
using A and C by (drule_tac asset_v_state, auto)
with A have "∃D. D ∈ snd (snd SK) ∧ (Asset n, ⦃Num 4, PubKey D⦄) ∈ s"
by (drule_tac asset_seskey_other, auto)
then obtain D' where
E: "D' ∈ snd (snd SK) ∧ (Asset n, ⦃Num 4, PubKey D'⦄) ∈ s"
by blast
with A have "PriKey D' ∉ spied s"
by (erule_tac asset_iii_secret, simp)
moreover have "C ≠ D'"
using A and D and E by (rule_tac notI, erule_tac asset_iii_owner_iii, auto)
ultimately have "¬ (∃A. A ∈ snd (snd SK) ∧ PriKey A ∈ spied s)"
using D and E by auto
hence F: "SesKey SK ∉ spied s"
using A by (rule_tac notI, drule_tac seskey_spied, auto)
moreover have "Crypt (SesK SK) (Pwd n) ∈ used s"
using A and C by (drule_tac asset_v_state, auto)
hence "(∃SK'. SesK SK = SesK SK' ∧
(Owner n, Crypt (SesK SK') (Pwd n)) ∈ s) ∨
{Pwd n, Key (SesK SK)} ⊆ spied s"
using A by (rule_tac parts_crypt_pwd, auto)
ultimately have "(Owner n, Crypt (SesK SK) (Pwd n)) ∈ s"
by simp
with A and B have "m = n"
by (rule owner_seskey_unique)
thus ?thesis
using F ..
qed
end