Theory Safety_Properties

section ‹Safety properties ›

text ‹Here we prove some safety properties (state invariants) for a CoSMeDis
node that are needed in the proof of BD Security properties.
›

theory Safety_Properties
  imports
    Automation_Setup
begin

declare Let_def[simp]
declare if_splits[split]
declare IDsOK_def[simp]

lemmas eff_defs = s_defs c_defs d_defs u_defs
lemmas obs_defs = r_defs l_defs
lemmas effc_defs = eff_defs com_defs
lemmas all_defs = effc_defs obs_defs

declare sstep_Cons[simp]

lemma Lact_Ract_noStateChange[simp]:
assumes "a ∈ Lact ` UNIV ∪ Ract ` UNIV"
shows "snd (step s a) = s"
using assms by (cases a) auto

lemma Lact_Ract_noStateChange_set:
assumes "set al ⊆ Lact ` UNIV ∪ Ract ` UNIV"
shows "snd (sstep s al) = s"
using assms by (induct al) (auto split: prod.splits)

lemma reach_postIDs_persist:
"pID ∈∈ postIDs s ⟹ step s a = (ou,s') ⟹ pID ∈∈ postIDs s'"
apply (cases a)
  subgoal for x1 apply(cases x1, auto simp: effc_defs) .
  subgoal for x2 apply(cases x2, auto simp: effc_defs) .
  subgoal for x3 apply(cases x3, auto simp: effc_defs) .
  subgoal for x4 apply(cases x4, auto simp: effc_defs) .
  subgoal by auto
  subgoal by auto
  subgoal for x7 apply(cases x7, auto simp: effc_defs) .
done

lemma userOfA_not_userIDs_outErr:
"∃ uid. userOfA a = Some uid ∧ ¬ uid ∈∈ userIDs s ⟹
 ∀ aID uID p name. a ≠ Sact (sSys uID p) ⟹
 ∀ uID name. a ≠ Cact (cNUReq uID name) ⟹
 fst (step s a) = outErr"
apply (cases a)
  subgoal for x1 apply(cases x1, auto simp: all_defs) .
  subgoal for x2 apply(cases x2, auto simp: all_defs) .
  subgoal for x3 apply(cases x3, auto simp: all_defs) .
  subgoal for x4 apply(cases x4, auto simp: all_defs) .
  subgoal for x5 apply(cases x5, auto simp: all_defs) .
  subgoal for x6 apply(cases x6, auto simp: all_defs) .
  subgoal for x7 apply(cases x7, auto simp: all_defs) .
done

lemma reach_vis: "reach s ⟹ vis s pID ∈ {FriendV, PublicV}"
proof (induction rule: reach_step_induct)
  case (Step s a) then show ?case proof (cases a)
     case (Sact sAct) with Step show ?thesis
     apply (cases sAct) by (auto simp add: s_defs)
  next
    case (Cact cAct) with Step show ?thesis
    apply (cases cAct) by (auto simp add: c_defs)
  next
    case (Dact dAct) with Step show ?thesis
    apply (cases dAct) by (auto simp add: d_defs)
  next
    case (Uact uAct) with Step show ?thesis
    apply (cases uAct) by (auto simp add: u_defs)
  next
    case (COMact comAct) with Step show ?thesis apply (cases comAct)
    by (auto simp add: com_defs)
  qed auto
qed (auto simp add: istate_def)

lemma reach_not_postIDs_emptyPost:
"reach s ⟹ PID ∉ set (postIDs s) ⟹ post s PID = emptyPost"
proof (induction rule: reach_step_induct)
  case (Step s a) then show ?case proof (cases a)
     case (Sact sAct) with Step show ?thesis
     apply (cases sAct) by (auto simp add: s_defs)
  next
    case (Cact cAct) with Step show ?thesis
    apply (cases cAct) by (auto simp add: c_defs)
  next
    case (Dact dAct) with Step show ?thesis
    apply (cases dAct) by (auto simp add: d_defs)
  next
    case (Uact uAct) with Step show ?thesis
    apply (cases uAct) by (auto simp add: u_defs)
  next
    case (COMact comAct) with Step show ?thesis apply (cases comAct)
    by (auto simp add: com_defs)
  qed auto
qed (auto simp add: istate_def)

lemma reach_not_postIDs_friendV:
"reach s ⟹ PID ∉ set (postIDs s) ⟹ vis s PID = FriendV"
proof (induction rule: reach_step_induct)
  case (Step s a) then show ?case proof (cases a)
     case (Sact sAct) with Step show ?thesis
     apply (cases sAct) by (auto simp add: s_defs)
  next
    case (Cact cAct) with Step show ?thesis
    apply (cases cAct) by (auto simp add: c_defs)
  next
    case (Dact dAct) with Step show ?thesis
    apply (cases dAct) by (auto simp add: d_defs)
  next
    case (Uact uAct) with Step show ?thesis
    apply (cases uAct) by (auto simp add: u_defs)
  next
    case (COMact comAct) with Step show ?thesis apply (cases comAct)
    by (auto simp add: com_defs)
  qed auto
qed (auto simp add: istate_def)


(* Would only work if we new that the same property holds
for what is being received:
lemma reach_outerVis: "reach s ⟹ outerVis s aID pID ∈ {FriendV, PublicV}"
proof (induction rule: reach_step_induct)
  case (Step s a) then show ?case proof (cases a)
     case (Sact sAct) with Step show ?thesis
     apply (cases sAct) by (auto simp add: s_defs)
  next
    case (Cact cAct) with Step show ?thesis
    apply (cases cAct) by (auto simp add: c_defs)
  next
    case (Dact dAct) with Step show ?thesis
    apply (cases dAct) by (auto simp add: d_defs)
  next
    case (Uact uAct) with Step show ?thesis
    apply (cases uAct) by (auto simp add: u_defs)
  next
    case (COMact comAct) with Step show ?thesis apply (cases comAct)
    apply (auto simp add: com_defs fun_upd2_def)
  qed auto
qed (auto simp add: istate_def)
*)

lemma reach_owner_userIDs: "reach s ⟹ pID ∈∈ postIDs s ⟹ owner s pID ∈∈ userIDs s"
proof (induction rule: reach_step_induct)
  case (Step s a) then show ?case proof (cases a)
     case (Sact sAct) with Step show ?thesis
     apply (cases sAct) by (auto simp add: s_defs)
  next
    case (Cact cAct) with Step show ?thesis
    apply (cases cAct) by (auto simp add: c_defs)
  next
    case (Dact dAct) with Step show ?thesis
    apply (cases dAct) by (auto simp add: d_defs)
  next
    case (Uact uAct) with Step show ?thesis
    apply (cases uAct) by (auto simp add: u_defs)
  next
    case (COMact comAct) with Step show ?thesis apply (cases comAct)
    by (auto simp add: com_defs)
  qed auto
qed (auto simp add: istate_def)

lemma reach_admin_userIDs: "reach s ⟹ uID ∈∈ userIDs s ⟹ admin s ∈∈ userIDs s"
proof (induction rule: reach_step_induct)
  case (Step s a) then show ?case proof (cases a)
     case (Sact sAct) with Step show ?thesis
     apply (cases sAct) by (auto simp add: s_defs)
  next
    case (Cact cAct) with Step show ?thesis
    apply (cases cAct) by (auto simp add: c_defs)
  next
    case (Dact dAct) with Step show ?thesis
    apply (cases dAct) by (auto simp add: d_defs)
  next
    case (Uact uAct) with Step show ?thesis
    apply (cases uAct) by (auto simp add: u_defs)
  next
    case (COMact comAct) with Step show ?thesis apply (cases comAct)
    by (auto simp add: com_defs)
  qed auto
qed (auto simp add: istate_def)

lemma reach_pendingUReqs_distinct: "reach s ⟹ distinct (pendingUReqs s)"
proof (induction rule: reach_step_induct)
  case (Step s a) then show ?case proof (cases a)
    case (Sact sAct) with Step show ?thesis by (cases sAct) (auto simp add: s_defs) next
    case (Cact cAct) with Step show ?thesis by (cases cAct) (auto simp add: c_defs) next
    case (Dact dAct) with Step show ?thesis by (cases dAct) (auto simp add: d_defs) next
    case (Uact uAct) with Step show ?thesis by (cases uAct) (auto simp add: u_defs) next
    case (COMact comAct) with Step show ?thesis by (cases comAct) (auto simp add: com_defs)
  qed auto
qed (auto simp: istate_def)

lemma reach_pendingUReqs:
"reach s ⟹ uid ∈∈ pendingUReqs s ⟹ uid ∉ set (userIDs s) ∧ admin s ∈∈ userIDs s"
proof (induction rule: reach_step_induct)
  case (Step s a) then show ?case proof (cases a)
    case (Sact sAct) with Step show ?thesis by (cases sAct) (auto simp add: s_defs) next
    case (Cact cAct)
      with Step reach_pendingUReqs_distinct show ?thesis
        by (cases cAct) (auto simp add: c_defs) next
    case (Dact dAct) with Step show ?thesis by (cases dAct) (auto simp add: d_defs) next
    case (Uact uAct) with Step show ?thesis by (cases uAct) (auto simp add: u_defs) next
    case (COMact comAct) with Step show ?thesis by (cases comAct) (auto simp add: com_defs)
  qed auto
qed (auto simp: istate_def)

lemma reach_friendIDs_symmetric:
"reach s ⟹ uID1 ∈∈ friendIDs s uID2 ⟷ uID2 ∈∈ friendIDs s uID1"
proof (induction rule: reach_step_induct)
  case (Step s a) then show ?case proof (cases a)
    case (Sact sAct) with Step show ?thesis by (cases sAct) (auto simp add: s_defs) next
    case (Cact cAct) with Step show ?thesis by (cases cAct) (auto simp add: c_defs ) next
    case (Dact dAct) with Step show ?thesis by (cases dAct) (auto simp add: d_defs ) next
    case (Uact uAct) with Step show ?thesis by (cases uAct) (auto simp add: u_defs) next
    case (COMact comAct) with Step show ?thesis by (cases comAct) (auto simp add: com_defs)
  qed auto
qed (auto simp add: istate_def)

(* No longer holds:
lemma friendIDs_mono:
assumes "step s a = (ou, s')"
and "uid ∈∈ friendIDs s uid'"
shows "uid ∈∈ friendIDs s' uid'"
using assms proof (cases a)
  case (Sact sAct) with assms show ?thesis by (cases sAct) (auto simp add: s_defs) next
  case (Cact cAct) with assms show ?thesis by (cases cAct) (auto simp add: c_defs ) next
  case (Dact dAct) with assms show ?thesis by (cases dAct) (auto simp add: d_defs ) next
  case (Uact uAct) with assms show ?thesis by (cases uAct) (auto simp add: u_defs) next
  case (COMact comAct) with assms show ?thesis by (cases comAct) (auto simp add: com_defs)
qed auto
*)

lemma reach_distinct_friends_reqs:
assumes "reach s"
shows "distinct (friendIDs s uid)" and "distinct (pendingFReqs s uid)"
  and "distinct (sentOuterFriendIDs s uid)" and "distinct (recvOuterFriendIDs s uid)"
  and "uid' ∈∈ pendingFReqs s uid ⟹ uid' ∉ set (friendIDs s uid)"
  and "uid' ∈∈ pendingFReqs s uid ⟹ uid ∉ set (friendIDs s uid')"
using assms proof (induction arbitrary: uid uid' rule: reach_step_induct)
  case Istate
    fix uid uid'
    show "distinct (friendIDs istate uid)" and "distinct (pendingFReqs istate uid)"
     and "distinct (sentOuterFriendIDs istate uid)" and "distinct (recvOuterFriendIDs istate uid)"
     and "uid' ∈∈ pendingFReqs istate uid ⟹ uid' ∉ set (friendIDs istate uid)"
     and "uid' ∈∈ pendingFReqs istate uid ⟹ uid ∉ set (friendIDs istate uid')"
      unfolding istate_def by auto
next
  case (Step s a)
    have s': "reach (snd (step s a))" using reach_step[OF Step(1)] .
    { fix uid uid'
      have "distinct (friendIDs (snd (step s a)) uid) ∧ distinct (pendingFReqs (snd (step s a)) uid)
          ∧ distinct (sentOuterFriendIDs (snd (step s a)) uid)
          ∧ distinct (recvOuterFriendIDs (snd (step s a)) uid)
          ∧ (uid' ∈∈ pendingFReqs (snd (step s a)) uid ⟶ uid' ∉ set (friendIDs (snd (step s a)) uid))"
      proof (cases a)
        case (Sact sa) with Step show ?thesis by (cases sa) (auto simp add: s_defs) next
        case (Cact ca) with Step show ?thesis by (cases ca) (auto simp add: c_defs) next
        case (Dact da) with Step show ?thesis by (cases da) (auto simp add: d_defs distinct_removeAll) next
        case (Uact ua) with Step show ?thesis by (cases ua) (auto simp add: u_defs) next
        case (Ract ra) with Step show ?thesis by auto next
        case (Lact ra) with Step show ?thesis by auto next
        case (COMact ca) with Step show ?thesis by (cases ca) (auto simp add: com_defs) next
      qed
    } note goal = this
    fix uid uid'
    from goal show "distinct (friendIDs (snd (step s a)) uid)"
               and "distinct (pendingFReqs (snd (step s a)) uid)"
               and "distinct (sentOuterFriendIDs (snd (step s a)) uid)"
               and "distinct (recvOuterFriendIDs (snd (step s a)) uid)"
 by auto
    assume "uid' ∈∈ pendingFReqs (snd (step s a)) uid"
    with goal show "uid' ∉ set (friendIDs (snd (step s a)) uid)" by auto
    then show "uid ∉ set (friendIDs (snd (step s a)) uid')"
      using reach_friendIDs_symmetric[OF s'] by simp
qed

lemma remove1_in_set: "x ∈∈ remove1 y xs ⟹ x ∈∈ xs"
by (induction xs) auto

lemma reach_IDs_used_IDsOK[rule_format]:
assumes "reach s"
shows "uid ∈∈ pendingFReqs s uid' ⟶ IDsOK s [uid, uid'] [] [] []" (is ?p)
and "uid ∈∈ friendIDs s uid' ⟶ IDsOK s [uid, uid'] [] [] []" (is ?f)
using assms proof -
  from assms have "uid ∈∈ pendingFReqs s uid' ∨ uid ∈∈ friendIDs s uid'
               ⟶ IDsOK s [uid, uid'] [] [] []"
  proof (induction rule: reach_step_induct)
    case Istate then show ?case by (auto simp add: istate_def)
  next
    case (Step s a) then show ?case proof (cases a)
      case (Sact sa) with Step show ?thesis by (cases sa) (auto simp: s_defs) next
      case (Cact ca) with Step show ?thesis by (cases ca) (auto simp: c_defs intro: remove1_in_set) next
      case (Dact da) with Step show ?thesis by (cases da) (auto simp: d_defs) next
      case (Uact ua) with Step show ?thesis by (cases ua) (auto simp: u_defs) next
      case (COMact ca) with Step show ?thesis by (cases ca) (auto simp: com_defs)
    qed auto
  qed
  then show ?p and ?f by auto
qed

lemma reach_AID_used_valid:
assumes "reach s"
and "aid ∈∈ serverApiIDs s ∨ aid ∈∈ clientApiIDs s ∨ aid ∈∈ pendingSApiReqs s ∨ aid ∈∈ pendingCApiReqs s"
shows "admin s ∈∈ userIDs s"
using assms proof (induction rule: reach_step_induct)
  case Istate then show ?case by (auto simp: istate_def)
next
  case (Step s a) then show ?case proof (cases a)
    case (Sact sa) with Step show ?thesis by (cases sa) (auto simp: s_defs) next
    case (Cact ca) with Step show ?thesis by (cases ca) (auto simp: c_defs) next
    case (Dact da) with Step show ?thesis by (cases da) (auto simp: d_defs) next
    case (Uact ua) with Step show ?thesis by (cases ua) (auto simp: u_defs) next
    case (COMact ca) with Step show ?thesis by (cases ca) (auto simp: com_defs intro: remove1_in_set)
  qed auto
qed

lemma IDs_mono[rule_format]:
assumes "step s a = (ou, s')"
shows "uid ∈∈ userIDs s ⟶ uid ∈∈ userIDs s'" (is "?u")
and "nid ∈∈ postIDs s ⟶ nid ∈∈ postIDs s'" (is "?n")
and "aid ∈∈ clientApiIDs s ⟶ aid ∈∈ clientApiIDs s'" (is "?c")
and "sid ∈∈ serverApiIDs s ⟶ sid ∈∈ serverApiIDs s'" (is "?s")
and "nid ∈∈ outerPostIDs s aid ⟶ nid ∈∈ outerPostIDs s' aid" (is "?o")
proof -
  from assms have "?u ∧ ?n ∧ ?c ∧ ?s ∧ ?o" proof (cases a)
    case (Sact sa) with assms show ?thesis by (cases sa) (auto simp add: s_defs) next
    case (Cact ca) with assms show ?thesis by (cases ca) (auto simp add: c_defs) next
    case (Dact da) with assms show ?thesis by (cases da) (auto simp add: d_defs) next
    case (Uact ua) with assms show ?thesis by (cases ua) (auto simp add: u_defs) next
    case (COMact ca) with assms show ?thesis by (cases ca) (auto simp add: com_defs)
  qed (auto)
  then show "?u" "?n" "?c" "?s" "?o" by auto
qed

lemma IDsOK_mono:
assumes "step s a = (ou, s')"
and "IDsOK s uIDs pIDs saID_pIDs_s caIDs"
shows "IDsOK s' uIDs pIDs saID_pIDs_s caIDs"
using IDs_mono[OF assms(1)] assms(2)
by (auto simp add: list_all_iff)


lemma step_outerFriendIDs_idem:
assumes "step s a = (ou, s')"
and "∀uID p aID uID'. a ≠ COMact (comSendCreateOFriend uID p aID uID') ∧
                      a ≠ COMact (comReceiveCreateOFriend aID p uID uID') ∧
                      a ≠ COMact (comSendDeleteOFriend uID p aID uID') ∧
                      a ≠ COMact (comReceiveDeleteOFriend aID p uID uID')"
shows "sentOuterFriendIDs s' = sentOuterFriendIDs s" (is ?sent)
  and "recvOuterFriendIDs s' = recvOuterFriendIDs s" (is ?recv)
proof -
  have "?sent ∧ ?recv" using assms proof (cases a)
    case (Sact sa) with assms show ?thesis by (cases sa) (auto simp add: s_defs) next
    case (Cact ca) with assms show ?thesis by (cases ca) (auto simp add: c_defs) next
    case (Dact da) with assms show ?thesis by (cases da) (auto simp add: d_defs) next
    case (Uact ua) with assms show ?thesis by (cases ua) (auto simp add: u_defs) next
    case (COMact ca) with assms show ?thesis by (cases ca) (auto simp add: com_defs)
  qed auto
  then show "?sent" and "?recv" by auto
qed

lemma istate_sSys:
assumes "step istate a = (ou, s')"
obtains uid p where "a = Sact (sSys uid p)"
      | "s' = istate"
using assms proof (cases a)
  case (Sact sa) with assms show ?thesis by (cases sa) (auto intro: that) next
  case (Cact ca) with assms that(2) show ?thesis by (cases ca) (auto simp add: c_defs istate_def) next
  case (Dact da) with assms that(2) show ?thesis by (cases da) (auto simp add: d_defs istate_def) next
  case (Uact ua) with assms that(2) show ?thesis by (cases ua) (auto simp add: u_defs istate_def) next
  case (COMact ca) with assms that(2) show ?thesis by (cases ca) (auto simp add: com_defs istate_def) next
  case (Ract ra) with assms that(2) show ?thesis by (cases ra) (auto simp add: r_defs istate_def) next
  case (Lact la) with assms that(2) show ?thesis by (cases la) (auto simp add: l_defs istate_def)
qed


end