Theory Anonymity

(*  Title:       Logging-independent Message Anonymity in the Relational Method
    Author:      Pasquale Noce
                 Software Engineer at HID Global, Italy
                 pasquale dot noce dot lavoro at gmail dot com
                 pasquale dot noce at hidglobal dot com
*)

section "Anonymity of token pseudonymous identifiers"

theory Anonymity
  imports Definitions
begin

text ‹
\null

This section contains a proof of anonymity property @{text id_anonymous}, which states that a token
pseudonymous identifier remains anonymous if its anonymity is not compromised by means other than
attacking the protocol and neither attack option described in section \ref{Protocol} is viable. As
shown here below, this property can be proven by applying rules @{thm [source] rtrancl_induct} and
@{text rtrancl_start} in a suitable combination cite‹"Noce20"›.

\null
›

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. ?P2 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. ?P2 x y u v)" and "¬ P x"
  hence D: "P y ⟶ (∃u v. ?P2 x y u v)" by simp
  show "∃u v. ?P2 x z u v"
  proof (cases "P y")
    case True
    with D obtain u v where "?P2 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 "?P2 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 parts_init:
 "parts (used s0) = used s0"
by (rule equalityI, rule_tac [!] subsetI, erule_tac [2] parts_used,
 erule parts.induct, auto)

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)

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_mono:
 "X ∈ H ⟹ parts_msg X ⊆ parts H"
by (subgoal_tac "{X} ⊆ H", subst parts_msg_def, erule parts_mono, simp)

proposition parts_msg_agrkey [simp]:
 "parts_msg (AgrKey K) = {AgrKey K}"
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_parts:
 "⟦(A, X) ∈ s; Y ∈ parts_msg X⟧ ⟹ Y ∈ parts (used s)"
by (subgoal_tac "X ∈ parts (used s)", drule parts_msg_mono [of X], auto)


proposition prikey_spied:
 "⟦s0 ⊨ s; PriKey K ∈ parts (used s)⟧ ⟹ PriKey K ∈ spied s"
by (induction rule: rtrancl_induct, subst (asm) parts_init,
 auto simp: rel_def parts_insert dest!: parts_msg_parts)

proposition prikey_crypt [simplified]:
 "⟦(Spy, Crypt K (PriKey K')) ∈ s; s0 ⊨ s⟧ ⟹ PriKey K' ∈ spied s"
by (erule prikey_spied, blast)

proposition prikey_mpair_fst [simplified]:
 "⟦(Spy, ⦃PriKey K, Y⦄) ∈ s; s0 ⊨ s⟧ ⟹ PriKey K ∈ spied s"
by (erule prikey_spied, blast)

proposition prikey_mpair_snd [simplified]:
 "⟦(Spy, ⦃Y, PriKey K⦄) ∈ s; s0 ⊨ s⟧ ⟹ PriKey K ∈ spied s"
by (erule prikey_spied, blast)

proposition rev_prikey_secret:
 "s0 ⊨ s ⟹ Rev_PriKey ∉ spied s"
by (induction rule: rtrancl_induct, insert sec_prik_rev tok_prik_rev,
 auto simp: rel_def dest: prikey_crypt prikey_mpair_fst prikey_mpair_snd)

proposition sec_prikey_secret:
 "⟦s0 ⊨ s; n ∉ bad_sec_prik⟧ ⟹ Sec_PriKey n ∉ spied s"
by (induction rule: rtrancl_induct, insert sec_prik_inj sec_prik_tok_prik, auto simp:
 rel_def inj_on_def image_def dest: prikey_crypt prikey_mpair_fst prikey_mpair_snd)

proposition tok_prikey_secret:
 "⟦s0 ⊨ s; n ∉ bad_tok_prik⟧ ⟹ Tok_PriKey n ∉ spied s"
by (induction rule: rtrancl_induct, insert tok_prik_inj sec_prik_tok_prik, auto simp:
 rel_def inj_on_def image_def dest: prikey_crypt prikey_mpair_fst prikey_mpair_snd)


proposition idinfo_spied:
 "⟦s0 ⊨ s; ⟨n, X⟩ ∈ parts (used s)⟧ ⟹ ⟨n, X⟩ ∈ spied s"
by (induction rule: rtrancl_induct, subst (asm) parts_init,
 auto simp: rel_def parts_insert dest!: parts_msg_parts)

proposition idinfo_crypt:
 "⟦(Spy, Crypt K ⟨n, X⟩) ∈ s; s0 ⊨ s⟧ ⟹ ⟨n, X⟩ ∈ spied s"
by (erule idinfo_spied, blast)

proposition idinfo_mpair_fst:
 "⟦(Spy, ⦃⟨n, X⟩, Y⦄) ∈ s; s0 ⊨ s⟧ ⟹ ⟨n, X⟩ ∈ spied s"
by (erule idinfo_spied, blast)

proposition idinfo_mpair_snd:
 "⟦(Spy, ⦃Y, ⟨n, X⟩⦄) ∈ s; s0 ⊨ s⟧ ⟹ ⟨n, X⟩ ∈ spied s"
by (erule idinfo_spied, blast)

proposition idinfo_hash_hash [rotated]:
 "⟦s0 ⊨ s; (Spy, ⟨n, Hash (Hash X)⟩) ∈ s⟧ ⟹ ⟨n, Hash X⟩ ∈ spied s"
by (induction arbitrary: X rule: rtrancl_induct, auto simp: rel_def
 dest: idinfo_crypt idinfo_mpair_fst idinfo_mpair_snd)


proposition sec_prik_eq:
 "{Tok_PriK n, Sec_PriK m, Rev_PriK} =
    {Tok_PriK n, Sec_PriK m', Rev_PriK} ⟹ m' = m"
by (erule equalityE, drule subsetD [where c = "Sec_PriK m"], simp, insert
 sec_prik_inj sec_prik_rev sec_prik_tok_prik, auto simp: inj_on_def image_def)

proposition id_identified:
  assumes
    A: "s0 ⊨ s" and
    B: "(n, m) ∉ bad_id" and
    C: "n ∉ bad_tok_prik" and
    D: "⟨n, Hash (ID n (Sec_PubKey m))⟩ ∈ spied s"
  shows "m ∈ bad_sec_prik ∧
    (∃m'. m' ≠ m ∧ m' ∈ bad_sec_prik ∧ (n, m') ∈ bad_id)"
proof -
  let ?P1 = "λs. ⟨n, Hash (ID n (Sec_PubKey m))⟩ ∈ spied s"
  let ?P2 = "λs. ∃S. ⟨n, PubKey S⟩ ∈ spied s ∧ Sec_PriK m ∈ S"
  let ?P3 = "λS s. ⟨n, Hash (PubKey S)⟩ ∈ spied s"
  let ?P4 = "λS s. ⟨n, PubKey S⟩ ∈ spied s ∧ Rev_PriK ∈ S ∧
    (∀m. Sec_PriK m ∈ S ⟶ (n, m) ∉ bad_id)"
  have E: "∀m. Sec_PriK m ≠ Rev_PriK"
    by (rule allI, rule notI, subgoal_tac "Rev_PriK ∈ range Sec_PriK",
     simp add: sec_prik_rev, rule range_eqI, rule sym)
  have "∃u v. s0 ⊨ u ∧ u ⊢ v ∧ v ⊨ s ∧ ¬ ?P1 u ∧ ?P1 v"
    using A and B and D by (rule_tac rtrancl_start, auto dest: sec_prik_eq)
  then obtain u1 v1 where F: "s0 ⊨ u1 ∧ u1 ⊢ v1 ∧ ¬ ?P1 u1 ∧ ?P1 v1"
    by blast
  moreover from this have G: "⟨n, ID n (Sec_PubKey m)⟩ ∈ spied u1"
    by (auto simp: rel_def dest: idinfo_crypt idinfo_mpair_fst idinfo_mpair_snd
     idinfo_hash_hash)
  ultimately have "∃u v. s0 ⊨ u ∧ u ⊢ v ∧ v ⊨ u1 ∧ ¬ ?P2 u ∧ ?P2 v"
    using B and E by (rule_tac rtrancl_start, insert
     sec_prik_inj sec_prik_tok_prik, auto simp: inj_on_def image_def)
  then obtain u2 v2 where H: "s0 ⊨ u2 ∧ u2 ⊢ v2 ∧ ¬ ?P2 u2 ∧ ?P2 v2"
    by blast
  moreover from this have "Tok_PriKey n ∉ spied u2"
    using C by (rule_tac tok_prikey_secret, simp)
  ultimately have "Sec_PriKey m ∈ spied u2"
  proof (auto simp: rel_def dest: idinfo_crypt idinfo_mpair_fst idinfo_mpair_snd)
    fix S
    assume "(Spy, ⟨n, Hash (AgrKey (PubK S))⟩) ∈ u2"
    moreover assume I: "Sec_PriK m ∈ S"
    hence "⟨n, Hash (PubKey S)⟩ ∉ spied s0"
      using B and E by (insert sec_prik_inj sec_prik_tok_prik,
       auto simp: inj_on_def image_def)
    ultimately have "∃u v. s0 ⊨ u ∧ u ⊢ v ∧ v ⊨ u2 ∧ ¬ ?P3 S u ∧ ?P3 S v"
      using H by (rule_tac rtrancl_start, simp_all)
    then obtain u3 v3 where "s0 ⊨ u3 ∧ u3 ⊢ v3 ∧ v3 ⊨ u2 ∧
      ¬ ?P3 S u3 ∧ ?P3 S v3"
      by blast
    moreover from this have "⟨n, PubKey S⟩ ∈ spied v3"
      by (auto simp: rel_def dest: idinfo_crypt idinfo_mpair_fst idinfo_mpair_snd
       idinfo_hash_hash)
    ultimately have "⟨n, PubKey S⟩ ∈ spied u2"
      by (rule_tac subsetD [of "spied v3"], rule_tac spied_subset, simp)
    hence "Sec_PriK m ∉ S"
      using H by simp
    thus "(Spy, AgrKey (PriK (Sec_PriK m))) ∈ u2"
      using I by contradiction
  qed
  hence I: "m ∈ bad_sec_prik"
    using H by (erule_tac contrapos_pp, rule_tac sec_prikey_secret, simp)
  from B and E and G have "∃S. ?P4 S u1"
    by (rule_tac exI [of _ "{Tok_PriK n, Sec_PriK m, Rev_PriK}"],
     insert sec_prik_inj sec_prik_tok_prik, auto simp: inj_on_def image_def)
  moreover have "¬ (∃S. ?P4 S s0)"
    by (insert tok_prik_rev, auto)
  ultimately have "∃u v. s0 ⊨ u ∧ u ⊢ v ∧ v ⊨ u1 ∧
    ¬ (∃S. ?P4 S u) ∧ (∃S. ?P4 S v)"
    using F by (rule_tac rtrancl_start, simp)
  then obtain u4 v4 S where
    J: "s0 ⊨ u4" and K: "u4 ⊢ v4" and L: "¬ (∃S. ?P4 S u4) ∧ ?P4 S v4"
    by blast
  have M: "⟦(Spy, ⟨n, AgrKey (PubK S)⟩) ∈ u4; Rev_PriK ∈ S;
    ∀m. Sec_PriK m ∈ S ⟶ (n, m) ∉ bad_id;
    ∀S. Rev_PriK ∈ S ⟶ (Spy, ⟨n, AgrKey (PubK S)⟩) ∈ u4 ⟶
      (∃m. Sec_PriK m ∈ S ∧ (n, m) ∈ bad_id)⟧ ⟹ False"
    by blast
  from K and L have "∃m'. m' ≠ m ∧ m' ∈ bad_sec_prik ∧ (n, m') ∈ bad_id"
  proof (simp add: rel_def, (erule_tac disjE, (clarsimp, (erule_tac disjE,
   drule_tac sym, simp, (drule_tac idinfo_crypt [OF _ J] | drule_tac
   idinfo_mpair_fst [OF _ J] | drule_tac idinfo_mpair_snd [OF _ J]), blast)+)?,
   blast)+, (erule_tac disjE, erule_tac [2] disjE, erule_tac [3] disjE; clarsimp))
    fix n' S' A
    assume
      N: "∀S. Rev_PriK ∈ S ⟶ (Spy, ⟨n, AgrKey (PubK S)⟩) ∈ u4 ⟶
        (∃m. Sec_PriK m ∈ S ∧ (n, m) ∈ bad_id)" and
      O: "∀m. Sec_PriK m ∈ S ⟶ (n, m) ∉ bad_id" and
      P: "Rev_PriK ∈ S" and
      Q: "(Spy, ⟨n', AgrKey (PubK S')⟩) ∈ u4" and
      R: "(Spy, AgrKey (PriK A)) ∈ u4"
    assume "n = n' ∧ S = S' - {A} ∨ (Spy, ⟨n, AgrKey (PubK S)⟩) ∈ u4"
    thus ?thesis
    proof (rule disjE, drule_tac [2] M [OF _ P O N]; clarsimp)
      assume S: "n = n'" and "S = S' - {A}"
      moreover from this obtain m' where
       "Sec_PriK m' ∈ S'" and T: "(n, m') ∈ bad_id"
        using N and P and Q by blast
      ultimately have "A = Sec_PriK m'"
        using O by (rule_tac ccontr, simp)
      hence "Sec_PriKey m' ∈ spied u4"
        using R by simp
      hence "m' ∈ bad_sec_prik"
        by (rule contrapos_pp, rule_tac sec_prikey_secret [OF J])
      thus "∃m'. m' ≠ m ∧ m' ∈ bad_sec_prik ∧ (n', m') ∈ bad_id"
        using B and S and T by auto
    qed
  next
    fix n' S' A
    assume
      N: "∀S. Rev_PriK ∈ S ⟶ (Spy, ⟨n, AgrKey (PubK S)⟩) ∈ u4 ⟶
        (∃m. Sec_PriK m ∈ S ∧ (n, m) ∈ bad_id)" and
      O: "∀m. Sec_PriK m ∈ S ⟶ (n, m) ∉ bad_id" and
      P: "Rev_PriK ∈ S" and
      Q: "(Spy, ⟨n', AgrKey (PubK S')⟩) ∈ u4" and
      R: "(Spy, AgrKey (PriK A)) ∈ u4"
    assume "n = n' ∧ S = insert A S' ∨ (Spy, ⟨n, AgrKey (PubK S)⟩) ∈ u4"
    thus ?thesis
    proof (rule disjE, drule_tac [2] M [OF _ P O N]; clarsimp)
      assume "n = n'" and S: "S = insert A S'"
      moreover have "A ≠ Rev_PriK"
        using R by (rule contrapos_pn, insert rev_prikey_secret [OF J], simp)
      ultimately obtain m' where "Sec_PriK m' ∈ S'" and T: "(n, m') ∈ bad_id"
        using N and P and Q by blast
      hence "(n, m') ∉ bad_id"
        using O and S by simp
      thus "∃m'. m' ≠ m ∧ m' ∈ bad_sec_prik ∧ (n', m') ∈ bad_id"
        using T by contradiction
    qed
  next
    fix n' S'
    assume
      N: "∀S. Rev_PriK ∈ S ⟶ (Spy, ⟨n, AgrKey (PubK S)⟩) ∈ u4 ⟶
        (∃m. Sec_PriK m ∈ S ∧ (n, m) ∈ bad_id)" and
      O: "∀m. Sec_PriK m ∈ S ⟶ (n, m) ∉ bad_id" and
      P: "Rev_PriK ∈ S"
    assume "n = n' ∧ S = S' ∨ (Spy, ⟨n, AgrKey (PubK S)⟩) ∈ u4" and
      "(Spy, AgrKey (PriK (Tok_PriK n'))) ∈ u4"
    thus ?thesis
      by (erule_tac disjE, drule_tac [2] M [OF _ P O N],
       insert tok_prikey_secret [OF J C], simp_all)
  next
    fix n' X
    assume
      N: "∀S. Rev_PriK ∈ S ⟶ (Spy, ⟨n, AgrKey (PubK S)⟩) ∈ u4 ⟶
        (∃m. Sec_PriK m ∈ S ∧ (n, m) ∈ bad_id)" and
      O: "∀m. Sec_PriK m ∈ S ⟶ (n, m) ∉ bad_id" and
      P: "Rev_PriK ∈ S" and
      Q: "(Spy, ⟨n', X⟩) ∈ u4 ∨ (Spy, ⟨n', Hash X⟩) ∈ u4"
    assume "n = n' ∧ AgrKey (PubK S) = X ∨
      (Spy, ⟨n, AgrKey (PubK S)⟩) ∈ u4"
    thus ?thesis
    proof (rule disjE, drule_tac [2] M [OF _ P O N]; clarsimp)
      assume R: "n = n'" and S: "X = AgrKey (PubK S)"
      {
        assume "(Spy, ⟨n', X⟩) ∈ u4"
        hence "(Spy, ⟨n, AgrKey (PubK S)⟩) ∈ u4"
          using R and S by simp
      }
      moreover {
        assume "(Spy, ⟨n', Hash X⟩) ∈ u4"
        hence "?P3 S u4"
          using R and S by simp
        moreover have "¬ ?P3 S s0"
          using O by auto
        ultimately have "∃u v. s0 ⊨ u ∧ u ⊢ v ∧ v ⊨ u4 ∧ ¬ ?P3 S u ∧ ?P3 S v"
          using J by (rule_tac rtrancl_start)
        then obtain u3 v3 where "s0 ⊨ u3 ∧ u3 ⊢ v3 ∧ v3 ⊨ u4 ∧
          ¬ ?P3 S u3 ∧ ?P3 S v3"
          by blast
        moreover from this have "⟨n, AgrKey (PubK S)⟩ ∈ spied v3"
          by (auto simp: rel_def dest: idinfo_crypt idinfo_mpair_fst idinfo_mpair_snd
           idinfo_hash_hash)
        ultimately have "⟨n, AgrKey (PubK S)⟩ ∈ spied u4"
          by (rule_tac subsetD [of "spied v3"], rule_tac spied_subset, simp)
      }
      ultimately have "(Spy, ⟨n, AgrKey (PubK S)⟩) ∈ u4"
        using Q by blast
      thus "∃m'. m' ≠ m ∧ m' ∈ bad_sec_prik ∧ (n', m') ∈ bad_id"
        by (drule_tac M [OF _ P O N], simp)
    qed
  qed
  thus ?thesis
    using I by simp
qed


theorem id_anonymous [rotated]:
 "⟦m ∉ bad_sec_prik ∨ ¬ (∃m'. m' ≠ m ∧ m' ∈ bad_sec_prik ∧ (n, m') ∈ bad_id);
    s0 ⊨ s; (n, m) ∉ bad_id; n ∉ bad_tok_prik⟧ ⟹
  ⟨n, Hash (ID n (Sec_PubKey m))⟩ ∉ spied s"
by (erule contrapos_pn, drule id_identified, blast+)

end