Theory Outer_Friend_Issuer

theory Outer_Friend_Issuer
  imports
    "Outer_Friend_Issuer_Value_Setup"
    "Bounded_Deducibility_Security.Compositional_Reasoning"
begin

subsubsection ‹Declassification bound›

(* We verify the following:
   Given an arbitrary but fixed user UID at node AID (who is not an observer) and a set of
   observers at each network node, the observers may learn about the *occurrence* of remote
   friendship actions of UID (because network traffic is assumed to be observable), but they
   learn nothing about the *content* of those actions (who was added or deleted as a friend)
   beyond public knowledge (friendship addition and deletion occur alternatingly),
   except if the action adds or deletes one of the observers themselves as friend.
*)

context OuterFriendIssuer
begin

fun T :: "(state,act,out) trans ⇒ bool"
where "T trn = False"

text ‹For each user ‹uid› at a node ‹aid›, the remote friendship updates with
the fixed user ‹UID› at node ‹AID› form an alternating sequence of friending and unfriending.

Note that actions involving remote users who are observers do not produce secret values;
instead, those actions are observable, and the property we verify does not protect their
confidentiality.›

fun validValSeq :: "value list ⇒ (apiID × userID) list ⇒ bool" where
  "validValSeq [] _ = True"
| "validValSeq (FrVal aid uid True # vl) auidl ⟷ (aid, uid) ∉ set auidl ∧ uid ∉ UIDs aid ∧ validValSeq vl (auidl ## (aid, uid))"
| "validValSeq (FrVal aid uid False # vl) auidl ⟷ (aid, uid) ∈∈ auidl ∧ uid ∉ UIDs aid ∧ validValSeq vl (removeAll (aid, uid) auidl)"
| "validValSeq (OVal _ # vl) auidl = validValSeq vl auidl"

abbreviation validValSeqFrom :: "value list ⇒ state ⇒ bool" where
  "validValSeqFrom vl s ≡ validValSeq vl (removeUIDs (sentOuterFriendIDs s UID))"

text ‹When the access window is closed, observers may learn about the occurrence of
remote friendship actions (by observing network traffic), but not their content;
the actions can be replaced by different actions involving different users (who are not observers)
without affecting the observations.›

inductive BC :: "value list ⇒ value list ⇒ bool"
where
  BC_Nil[simp,intro]: "BC [] []"
| BC_FrVal[intro]:
    "BC vl vl1 ⟹ uid' ∉ UIDs aid ⟹ BC (FrVal aid uid st # vl) (FrVal aid uid' st' # vl1)"

text ‹When the access window is open, i.e.~the user ‹UID› is a local friend of an observer,
all information about the remote friends of ‹UID› is declassified;
when the access window closes again, the contents of future updates are kept confidential.›

definition "BO vl vl1 ≡
 (vl1 = vl) ∨
 (∃vl0 vl' vl1'. vl = vl0 @ OVal False # vl' ∧ vl1 = vl0 @ OVal False # vl1' ∧ BC vl' vl1')"

definition "B vl vl1 ≡ (BC vl vl1 ∨ BO vl vl1) ∧ validValSeqFrom vl1 istate"


lemma B_Nil_Nil: "B vl vl1 ⟹ vl1 = [] ⟷ vl = []"
unfolding B_def BO_def by (auto elim: BC.cases)

sublocale BD_Security_IO where
istate = istate and step = step and
φ = φ and f = f and γ = γ and g = g and T = T and B = B
done


subsubsection ‹Unwinding proof›

definition Δ0 :: "state ⇒ value list ⇒ state ⇒ value list ⇒ bool" where
"Δ0 s vl s1 vl1 ≡
 s1 = istate ∧ s = istate ∧ B vl vl1"


definition Δ1 :: "state ⇒ value list ⇒ state ⇒ value list ⇒ bool" where
"Δ1 s vl s1 vl1 ≡
 BO vl vl1 ∧
 s1 = s ∧
 validValSeqFrom vl1 s1"


definition Δ2 :: "state ⇒ value list ⇒ state ⇒ value list ⇒ bool" where
"Δ2 s vl s1 vl1 ≡
 BC vl vl1 ∧
 eqButUID s s1 ∧ ¬open s1 ∧
 validValSeqFrom vl1 s1"


lemma validValSeq_prefix: "validValSeq (vl @ vl') auidl ⟹ validValSeq vl auidl"
by (induction vl arbitrary: auidl) (auto elim: validValSeq.elims)

lemma filter_removeAll: "filter P (removeAll x xs) = removeAll x (filter P xs)"
unfolding removeAll_filter_not_eq by (auto intro: filter_cong)

lemma step_validValSeqFrom:
assumes step: "step s a = (ou, s')"
and rs: "reach s"
and c: "consume (Trans s a ou s') vl vl'" (is "consume ?trn vl vl'")
and vVS: "validValSeqFrom vl s"
shows "validValSeqFrom vl' s'"
proof cases
  assume "φ ?trn"
  moreover then obtain v where "vl = v # vl'" using c by (cases vl, auto simp: consume_def)
  moreover have "distinct (sentOuterFriendIDs s UID)" using rs by (intro reach_distinct_friends_reqs)
  ultimately show ?thesis using assms
    by (elim φE)
       (auto simp: com_defs c_defs d_defs consume_def distinct_remove1_removeAll filter_removeAll)
next
  assume nφ: "¬φ ?trn"
  then have vl': "vl' = vl" using c by (auto simp: consume_def)
  then show ?thesis using vVS step proof (cases a)
    case (Sact sa) then show ?thesis using assms vl' by (cases sa) (auto simp: s_defs) next
    case (Cact ca) then show ?thesis using assms vl' by (cases ca) (auto simp: c_defs) next
    case (Dact da) then show ?thesis using assms vl' by (cases da) (auto simp: d_defs) next
    case (Uact ua) then show ?thesis using assms vl' by (cases ua) (auto simp: u_defs) next
    case (COMact ca) then show ?thesis using assms vl' nφ by (cases ca) (auto simp: com_defs filter_remove1)
  qed auto
qed

lemma istate_Δ0:
assumes B: "B vl vl1"
shows "Δ0 istate vl istate vl1"
using assms unfolding Δ0_def
by auto

lemma unwind_cont_Δ0: "unwind_cont Δ0 {Δ1,Δ2}"
proof(rule, simp)
  let ?Δ = "λs vl s1 vl1. Δ1 s vl s1 vl1 ∨
                           Δ2 s vl s1 vl1"
  fix s s1 :: state and vl vl1 :: "value list"
  assume rsT: "reachNT s" and rs1: "reach s1" and Δ0: "Δ0 s vl s1 vl1"
  then have rs: "reach s" and s: "s = istate" and s1: "s1 = istate" and B: "B vl vl1"
    using reachNT_reach unfolding Δ0_def by auto
  show "iaction ?Δ s vl s1 vl1 ∨
        ((vl = [] ⟶ vl1 = []) ∧ reaction ?Δ s vl s1 vl1)" (is "?iact ∨ (_ ∧ ?react)")
  proof-
    have ?react proof
      fix a :: act and ou :: out and s' :: state and vl'
      let ?trn = "Trans s a ou s'"
      assume step: "step s a = (ou, s')" and T: "¬ T ?trn" and c: "consume ?trn vl vl'"
      show "match ?Δ s s1 vl1 a ou s' vl' ∨ ignore ?Δ s s1 vl1 a ou s' vl'" (is "?match ∨ ?ignore")
      proof (intro disjI1)
        obtain uid p where a: "a = Sact (sSys uid p) ∨ s' = s"
          using step unfolding s by (elim istate_sSys) auto
        have "¬open s'" using step a s by (auto simp: istate_def s_defs open_def)
        moreover then have "¬φ ?trn" using step rs a by (auto elim!: φE simp: s istate_def com_defs)
        moreover have "sentOuterFriendIDs s' UID = sentOuterFriendIDs s UID"
          using s a step by (auto simp: s_defs)
        ultimately show "?match" using s s1 step B c unfolding Δ1_def Δ2_def B_def
          by (intro matchI[of s1 a ou s' vl1 vl1]) (auto simp: consume_def)
      qed
    qed
    with B_Nil_Nil[OF B] show ?thesis by auto
  qed
qed


lemma unwind_cont_Δ1: "unwind_cont Δ1 {Δ1,Δ2}"
proof(rule, simp)
  let ?Δ = "λs vl s1 vl1. Δ1 s vl s1 vl1 ∨
                           Δ2 s vl s1 vl1"
  fix s s1 :: state and vl vl1 :: "value list"
  assume rsT: "reachNT s" and rs1: "reach s1" and Δ0: "Δ1 s vl s1 vl1"
  then have rs: "reach s" and s: "s1 = s" and BO: "BO vl vl1"
        and vVS1: "validValSeqFrom vl1 s1"
    using reachNT_reach unfolding Δ1_def by auto
  show "iaction ?Δ s vl s1 vl1 ∨
        ((vl = [] ⟶ vl1 = []) ∧ reaction ?Δ s vl s1 vl1)" (is "?iact ∨ (_ ∧ ?react)")
  proof-
    have ?react proof
      fix a :: act and ou :: out and s' :: state and vl'
      let ?trn = "Trans s a ou s'"
      assume step: "step s a = (ou, s')" and T: "¬ T ?trn" and c: "consume ?trn vl vl'"
      show "match ?Δ s s1 vl1 a ou s' vl' ∨ ignore ?Δ s s1 vl1 a ou s' vl'" (is "?match ∨ ?ignore")
      proof cases
        assume φ: "φ ?trn"
        consider (Eq) "vl1 = vl"
          | (BC) vl0 vl'' vl1'' where "vl = vl0 @ OVal False # vl''"
                                and "vl1 = vl0 @ OVal False # vl1''"
                                and "BC vl'' vl1''"
          using BO
          by (auto simp: BO_def)
        then have "?match"
        proof cases
          case Eq
          then show ?thesis
            using step s c vVS1 step_validValSeqFrom[OF step rs c]
            by (intro matchI[of s1 a ou s' vl1 vl']) (auto simp: Δ1_def BO_def)
        next
          case BC
          show "?match" proof (cases vl0)
            case Nil
              then have "consume ?trn vl1 vl1''" and "vl' = vl''" and f: "f ?trn = OVal False"
                using φ c BC by (auto simp: consume_def)
              moreover then have "validValSeqFrom vl1'' s'"
                using s rs vVS1 by (intro step_validValSeqFrom[OF step]) auto
              moreover have "¬open s'" using φ step rs f by (auto elim: φE)
              ultimately show ?thesis
                using step s BC by (intro matchI[of s1 a ou s' vl1 vl1'']) (auto simp: Δ2_def)
          next
            case (Cons v vl0')
              then have "consume ?trn vl1 (vl0' @ OVal False # vl1'')" and "vl' = vl0' @ OVal False # vl''"
                using φ c BC by (auto simp: consume_def)
              moreover then have "validValSeqFrom (vl0' @ OVal False # vl1'') s'"
                using s rs vVS1 by (intro step_validValSeqFrom[OF step]) auto
              ultimately show ?thesis
                using step s BC
                by (intro matchI[of s1 a ou s' vl1 "(vl0' @ OVal False # vl1'')"]) (auto simp: Δ1_def BO_def)
          qed
        qed
        then show "?match ∨ ?ignore" ..
      next
        assume nφ: "¬φ ?trn"
        then have "consume ?trn vl1 vl1" and "vl' = vl" using c by (auto simp: consume_def)
        moreover then have "validValSeqFrom vl1 s'"
          using s rs vVS1 by (intro step_validValSeqFrom[OF step]) auto
        ultimately have "?match"
          using step s BO by (intro matchI[of s1 a ou s' vl1 vl1]) (auto simp: Δ1_def)
        then show "?match ∨ ?ignore" ..
      qed
    qed
    with BO show ?thesis by (auto simp: BO_def)
  qed
qed

lemma unwind_cont_Δ2: "unwind_cont Δ2 {Δ2}"
proof(rule, simp)
  fix s s1 :: state and vl vl1 :: "value list"
  assume rsT: "reachNT s" and rs1: "reach s1" and Δ2: "Δ2 s vl s1 vl1"
  then have rs: "reach s" and ss1: "eqButUID s s1" and BC: "BC vl vl1"
        and os: "¬open s1" and vVS1: "validValSeqFrom vl1 s1"
    using reachNT_reach unfolding Δ2_def by auto
  show "iaction Δ2 s vl s1 vl1 ∨
        ((vl = [] ⟶ vl1 = []) ∧ reaction Δ2 s vl s1 vl1)" (is "?iact ∨ (_ ∧ ?react)")
  proof-
    have ?react proof
      fix a :: act and ou :: out and s' :: state and vl'
      let ?trn = "Trans s a ou s'"
      assume step: "step s a = (ou, s')" and T: "¬ T ?trn" and c: "consume ?trn vl vl'"
      show "match Δ2 s s1 vl1 a ou s' vl' ∨ ignore Δ2 s s1 vl1 a ou s' vl'" (is "?match ∨ ?ignore")
      proof cases
        assume φ: "φ ?trn"
        with BC c have "?match" proof (cases rule: BC.cases)
          case (BC_FrVal vl'' vl1'' uid' aid uid st st')
            then show ?thesis proof (cases st')
              case True
                let ?a1 = "COMact (comSendCreateOFriend UID (pass s1 UID) aid uid')"
                let ?ou1 = "O_sendCreateOFriend (aid, clientPass s aid, UID, uid')"
                let ?s1' = "snd (sendCreateOFriend s1 UID (pass s1 UID) aid uid')"
                let ?trn1 = "Trans s1 ?a1 ?ou1 ?s1'"
                have c1: "consume ?trn1 vl1 vl1''" and "vl' = vl''" and "f ?trn = FrVal aid uid st"
                  using φ c BC_FrVal True by (auto simp: consume_def)
                moreover then have a: "(a = COMact (comSendCreateOFriend UID (pass s UID) aid uid)
                                        ∧ ou = O_sendCreateOFriend (aid, clientPass s aid, UID, uid))
                                     ∨ (a = COMact (comSendDeleteOFriend UID (pass s UID) aid uid)
                                        ∧ ou = O_sendDeleteOFriend (aid, clientPass s aid, UID, uid))"
                               and IDs: "IDsOK s [UID] [] [] [aid]"
                               and uid: "uid ∉ UIDs aid"
                  using φ step rs by (auto elim!: φE split: prod.splits simp: com_defs)
                moreover have step1: "step s1 ?a1 = (?ou1, ?s1')"
                  using IDs vVS1 BC_FrVal True ss1 by (auto simp: com_defs eqButUID_def)
                moreover then have "validValSeqFrom vl1'' ?s1'"
                  using vVS1 rs1 c1 by (intro step_validValSeqFrom[OF step1]) auto
                moreover have "¬open ?s1'" using os by (auto simp: open_def com_defs)
                moreover have "eqButUID s' ?s1'"
                  using ss1 step a uid BC_FrVal(4) eqButUID_eqButUIDf[OF ss1] eqButUID_eqButUIDs[OF ss1]
                  by (auto split: prod.splits simp: com_defs filter_remove1 intro!: eqButUID_cong eqButUIDf_cong)
                moreover have "γ ?trn = γ ?trn1" and "g ?trn = g ?trn1"
                  using BC_FrVal a uid by (auto simp: com_defs)
                ultimately show "?match"
                  using BC_FrVal by (intro matchI[of s1 ?a1 ?ou1 ?s1' vl1 vl1'']) (auto simp: Δ2_def)
            next
              case False
                let ?a1 = "COMact (comSendDeleteOFriend UID (pass s1 UID) aid uid')"
                let ?ou1 = "O_sendDeleteOFriend (aid, clientPass s aid, UID, uid')"
                let ?s1' = "snd (sendDeleteOFriend s1 UID (pass s1 UID) aid uid')"
                let ?trn1 = "Trans s1 ?a1 ?ou1 ?s1'"
                have c1: "consume ?trn1 vl1 vl1''" and "vl' = vl''" and "f ?trn = FrVal aid uid st"
                  using φ c BC_FrVal False by (auto simp: consume_def)
                moreover then have a: "(a = COMact (comSendCreateOFriend UID (pass s UID) aid uid)
                                        ∧ ou = O_sendCreateOFriend (aid, clientPass s aid, UID, uid))
                                     ∨ (a = COMact (comSendDeleteOFriend UID (pass s UID) aid uid)
                                        ∧ ou = O_sendDeleteOFriend (aid, clientPass s aid, UID, uid))"
                               and IDs: "IDsOK s [UID] [] [] [aid]"
                               and uid: "uid ∉ UIDs aid"
                  using φ step rs by (auto elim!: φE split: prod.splits simp: com_defs)
                moreover have step1: "step s1 ?a1 = (?ou1, ?s1')"
                  using IDs vVS1 BC_FrVal False ss1 by (auto simp: com_defs eqButUID_def)
                moreover then have "validValSeqFrom vl1'' ?s1'"
                  using vVS1 rs1 c1 by (intro step_validValSeqFrom[OF step1]) auto
                moreover have "¬open ?s1'" using os by (auto simp: open_def com_defs)
                moreover have "eqButUID s' ?s1'"
                  using ss1 step a uid BC_FrVal(4) eqButUID_eqButUIDf[OF ss1] eqButUID_eqButUIDs[OF ss1]
                  by (auto split: prod.splits simp: com_defs filter_remove1 intro!: eqButUID_cong eqButUIDf_cong)
                moreover have "γ ?trn = γ ?trn1" and "g ?trn = g ?trn1"
                  using BC_FrVal a uid by (auto simp: com_defs)
                ultimately show "?match"
                  using BC_FrVal by (intro matchI[of s1 ?a1 ?ou1 ?s1' vl1 vl1'']) (auto simp: Δ2_def)
            qed
        qed (auto simp: consume_def)
        then show "?match ∨ ?ignore" ..
      next
        assume nφ: "¬φ ?trn"
        then have vl': "vl' = vl" using c by (auto simp: consume_def)
        obtain ou1 s1' where step1: "step s1 a = (ou1, s1')" by (cases "step s1 a")
        let ?trn1 = "Trans s1 a ou1 s1'"
        show "?match ∨ ?ignore"
        proof (cases "∀aID uID'. uID' ∉ UIDs aID ⟶
                                 a ≠ COMact (comSendCreateOFriend UID (pass s UID) aID uID') ∧
                                 a ≠ COMact (comSendDeleteOFriend UID (pass s UID) aID uID')")
          case True
            then have nφ1: "¬φ ?trn1"
              using nφ ss1 rs rs1 step step1 by (auto simp: eqButUID_step_φ)
            have "?match" using step1 unfolding vl' proof (intro matchI[of s1 a ou1 s1' vl1 vl1])
              show c1: "consume ?trn1 vl1 vl1" using nφ1 by (auto simp: consume_def)
              show "Δ2 s' vl s1' vl1" using BC unfolding Δ2_def proof (intro conjI)
                show "eqButUID s' s1'" using eqButUID_step[OF ss1 step step1 rs rs1] .
                show "¬open s1'" proof
                  assume "open s1'"
                  with os have "open s1 ≠ open s1'" by auto
                  then show "False" using step1 nφ1 by (elim open_step_cases[of s1 s1']) auto
                qed
                show "validValSeqFrom vl1 s1'"
                  using c1 rs1 vVS1 by (intro step_validValSeqFrom[OF step1]) auto
              qed auto
              show "γ ?trn = γ ?trn1" using ss1 rs rs1 step step1 True by (intro eqButUID_step_γ) auto
            next
              assume "γ ?trn"
              then have "ou = ou1" using os nφ nφ1 by (intro eqButUID_step_γ_out[OF ss1 step step1]) auto
              then show "g ?trn = g ?trn1" by (cases a) auto
            qed auto
            then show "?match ∨ ?ignore" ..
        next
          case False
            with nφ have "?ignore"
              using UID_UIDs BC step ss1 os vVS1 unfolding vl'
              by (intro ignoreI) (auto simp: Δ2_def split: prod.splits)
            then show "?match ∨ ?ignore" ..
        qed
      qed
    qed
    with BC show ?thesis by (cases rule: BC.cases) auto
  qed
qed

definition Gr where
"Gr =
 {
 (Δ0, {Δ1,Δ2}),
 (Δ1, {Δ1,Δ2}),
 (Δ2, {Δ2})
 }"


theorem secure: secure
apply (rule unwind_decomp_secure_graph[of Gr Δ0])
unfolding Gr_def
apply (simp, smt insert_subset order_refl)
using
istate_Δ0 unwind_cont_Δ0 unwind_cont_Δ1 unwind_cont_Δ2
unfolding Gr_def by (auto intro: unwind_cont_mono)

end

end