Theory Friend

theory Friend
  imports
    "Friend_Value_Setup"
    "Bounded_Deducibility_Security.Compositional_Reasoning"
begin

subsection ‹Declassification bound›


context Friend
begin

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

text ‹The bound has the same ``while-or-last-before'' shape as the dynamic version of
the issuer bound for post confidentiality (Section~\ref{sec:dynamic-post-issuer}),
alternating between phases with open (‹BO›) or closed (‹BC›) access to the
confidential information.

The access window is initially open, because the two users are known not to exist when the system
is initialized, so there cannot be friendship between them.

The bound also incorporates the static knowledge that the friendship status alternates between
‹False› and ‹True›.›

fun alternatingFriends :: "value list ⇒ bool ⇒ bool" where
  "alternatingFriends [] _ = True"
| "alternatingFriends (FrVal st # vl) st' ⟷ st' = (¬st) ∧ alternatingFriends vl st"
| "alternatingFriends (OVal _ # vl) st = alternatingFriends vl st"

inductive BO :: "value list ⇒ value list ⇒ bool"
and BC :: "value list ⇒ value list ⇒ bool"
where
 BO_FrVal[simp,intro!]:
  "BO (map FrVal fs) (map FrVal fs)"
|BO_BC[intro]:
  "BC vl vl1 ⟹
   BO (map FrVal fs @ OVal False # vl) (map FrVal fs @ OVal False # vl1)"
(*  *)
|BC_FrVal[simp,intro!]:
  "BC (map FrVal fs) (map FrVal fs1)"
|BC_BO[intro]:
  "BO vl vl1 ⟹ (fs = [] ⟷ fs1 = []) ⟹ (fs ≠ [] ⟹ last fs = last fs1) ⟹
   BC (map FrVal fs  @ OVal True # vl)
      (map FrVal fs1 @ OVal True # vl1)"

definition "B vl vl1 ≡ BO vl vl1 ∧ alternatingFriends vl1 False"


lemma BO_Nil_Nil: "BO vl vl1 ⟹ vl = [] ⟹ vl1 = []"
by (cases rule: BO.cases) auto

no_notation relcomp (infixr "O" 75)

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


subsection ‹Unwinding proof›

(* helper *) lemma toggle_friends12_True:
assumes rs: "reach s"
    and IDs: "IDsOK s [UID1, UID2] [] [] []"
    and nf12: "¬friends12 s"
obtains al oul
where "sstep s al = (oul, createFriend s UID1 (pass s UID1) UID2)"
  and "al ≠ []" and "eqButUID s (createFriend s UID1 (pass s UID1) UID2)"
  and "friends12 (createFriend s UID1 (pass s UID1) UID2)"
  and "O (traceOf s al) = []" and "V (traceOf s al) = [FrVal True]"
proof cases
  assume "UID1 ∈∈ pendingFReqs s UID2 ∨ UID2 ∈∈ pendingFReqs s UID1"
  then show thesis proof
    assume pFR: "UID1 ∈∈ pendingFReqs s UID2"
    let ?a = "Cact (cFriend UID2 (pass s UID2) UID1)"
    let ?s' = "createFriend s UID1 (pass s UID1) UID2"
    let ?trn = "Trans s ?a outOK ?s'"
    have step: "step s ?a = (outOK, ?s')" using IDs pFR UID1_UID2
      unfolding createFriend_sym[of "s" "UID1" "pass s UID1" "UID2" "pass s UID2"]
      by (auto simp add: c_defs)
    moreover then have "φ ?trn" and "f ?trn = FrVal True" and "friends12 ?s'"
      by (auto simp: c_defs friends12_def)
    moreover have "¬γ ?trn" using UID1_UID2_UIDs by auto
    ultimately show thesis using nf12 rs
      by (intro that[of "[?a]" "[outOK]"]) (auto intro: Cact_cFriend_step_eqButUID)
  next
    assume pFR: "UID2 ∈∈ pendingFReqs s UID1"
    let ?a = "Cact (cFriend UID1 (pass s UID1) UID2)"
    let ?s' = "createFriend s UID1 (pass s UID1) UID2"
    let ?trn = "Trans s ?a outOK ?s'"
    have step: "step s ?a = (outOK, ?s')" using IDs pFR UID1_UID2 by (auto simp add: c_defs)
    moreover then have "φ ?trn" and "f ?trn = FrVal True" and "friends12 ?s'"
      by (auto simp: c_defs friends12_def)
    moreover have "¬γ ?trn" using UID1_UID2_UIDs by auto
    ultimately show thesis using nf12 rs
      by (intro that[of "[?a]" "[outOK]"]) (auto intro: Cact_cFriend_step_eqButUID)
  qed
next
  assume pFR: "¬(UID1 ∈∈ pendingFReqs s UID2 ∨ UID2 ∈∈ pendingFReqs s UID1)"
  let ?a1 = "Cact (cFriendReq UID2 (pass s UID2) UID1 emptyRequestInfo)"
  let ?s1 = "createFriendReq s UID2 (pass s UID2) UID1 emptyRequestInfo"
  let ?trn1 = "Trans s ?a1 outOK ?s1"
  let ?a2 = "Cact (cFriend UID1 (pass ?s1 UID1) UID2)"
  let ?s2 = "createFriend ?s1 UID1 (pass ?s1 UID1) UID2"
  let ?trn2 = "Trans ?s1 ?a2 outOK ?s2"
  have eFR: "e_createFriendReq s UID2 (pass s UID2) UID1 emptyRequestInfo" using IDs pFR nf12
    using reach_friendIDs_symmetric[OF rs]
    by (auto simp add: c_defs friends12_def)
  then have step1: "step s ?a1 = (outOK, ?s1)" by auto
  moreover then have "¬φ ?trn1" and "¬γ ?trn1" using UID1_UID2_UIDs by auto
  moreover have "eqButUID s ?s1" by (intro Cact_cFriendReq_step_eqButUID[OF step1]) auto
  moreover have rs1: "reach ?s1" using step1 by (intro reach_PairI[OF rs])
  moreover have step2: "step ?s1 ?a2 = (outOK, ?s2)" using IDs by (auto simp: c_defs)
  moreover then have "φ ?trn2" and "f ?trn2 = FrVal True" and "friends12 ?s2"
    by (auto simp: c_defs friends12_def)
  moreover have "¬γ ?trn2" using UID1_UID2_UIDs by auto
  moreover have "eqButUID ?s1 ?s2" by (intro Cact_cFriend_step_eqButUID[OF step2 rs1]) auto
  moreover have "?s2 = createFriend s UID1 (pass s UID1) UID2"
    using eFR by (intro createFriendReq_createFriend_absorb)
  ultimately show thesis using nf12 rs
    by (intro that[of "[?a1, ?a2]" "[outOK, outOK]"]) (auto intro: eqButUID_trans)
qed

(* helper *) lemma toggle_friends12_False:
assumes rs: "reach s"
    and IDs: "IDsOK s [UID1, UID2] [] [] []"
    and f12: "friends12 s"
obtains al oul
where "sstep s al = (oul, deleteFriend s UID1 (pass s UID1) UID2)"
  and "al ≠ []" and "eqButUID s (deleteFriend s UID1 (pass s UID1) UID2)"
  and "¬friends12 (deleteFriend s UID1 (pass s UID1) UID2)"
  and "O (traceOf s al) = []" and "V (traceOf s al) = [FrVal False]"
proof -
  let ?a = "Dact (dFriend UID1 (pass s UID1) UID2)"
  let ?s' = "deleteFriend s UID1 (pass s UID1) UID2"
  let ?trn = "Trans s ?a outOK ?s'"
  have step: "step s ?a = (outOK, ?s')" using IDs f12 UID1_UID2
    by (auto simp add: d_defs friends12_def)
  moreover then have "φ ?trn" and "f ?trn = FrVal False" and "¬friends12 ?s'"
    using reach_friendIDs_symmetric[OF rs] by (auto simp: d_defs friends12_def)
  moreover have "¬γ ?trn" using UID1_UID2_UIDs by auto
  ultimately show thesis using f12 rs
    by (intro that[of "[?a]" "[outOK]"]) (auto intro: Dact_dFriend_step_eqButUID)
qed


definition Δ0 :: "state ⇒ value list ⇒ state ⇒ value list ⇒ bool" where
"Δ0 s vl s1 vl1 ≡
 eqButUID s s1 ∧ friendIDs s = friendIDs s1 ∧ open s ∧
 BO vl vl1 ∧ alternatingFriends vl1 (friends12 s1)"

definition Δ1 :: "state ⇒ value list ⇒ state ⇒ value list ⇒ bool" where
"Δ1 s vl s1 vl1 ≡ (∃fs fs1.
 eqButUID s s1 ∧ ¬open s ∧
 alternatingFriends vl1 (friends12 s1) ∧
 vl = map FrVal fs ∧ vl1 = map FrVal fs1)"

definition Δ2 :: "state ⇒ value list ⇒ state ⇒ value list ⇒ bool" where
"Δ2 s vl s1 vl1 ≡ (∃fs fs1 vlr vlr1.
 eqButUID s s1 ∧ ¬open s ∧ BO vlr vlr1 ∧
 alternatingFriends vl1 (friends12 s1) ∧
 (fs = [] ⟷ fs1 = []) ∧
 (fs ≠ [] ⟶ last fs = last fs1) ∧
 (fs = [] ⟶ friendIDs s = friendIDs s1) ∧
 vl =  map FrVal fs  @ OVal True # vlr ∧
 vl1 = map FrVal fs1 @ OVal True # vlr1)"

lemma Δ2_I:
assumes "eqButUID s s1" "¬open s" "BO vlr vlr1" "alternatingFriends vl1 (friends12 s1)"
        "fs = [] ⟷ fs1 = []" "fs ≠ [] ⟶ last fs = last fs1"
        "fs = [] ⟶ friendIDs s = friendIDs s1"
        "vl =  map FrVal fs  @ OVal True # vlr"
        "vl1 = map FrVal fs1 @ OVal True # vlr1"
shows "Δ2 s vl s1 vl1"
using assms unfolding Δ2_def by blast


lemma istate_Δ0:
assumes B: "B vl vl1"
shows "Δ0 istate vl istate vl1"
using assms unfolding Δ0_def istate_def B_def open_def openByA_def openByF_def friends12_def
by auto

lemma unwind_cont_Δ0: "unwind_cont Δ0 {Δ0,Δ1,Δ2}"
proof(rule, simp)
  let ?Δ = "λs vl s1 vl1. Δ0 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 ss1: "eqButUID s s1" and fIDs: "friendIDs s = friendIDs s1"
        and os: "open s" and BO: "BO vl vl1" and aF1: "alternatingFriends vl1 (friends12 s1)"
    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 cases
        assume φ: "φ ?trn"
        then have vl: "vl = f ?trn # vl'" using c by (auto simp: consume_def)
        from BO have ?match proof (cases "f ?trn")
          case (FrVal fv)
            with BO vl obtain vl1' where vl1': "vl1 = f ?trn # vl1'" and BO': "BO vl' vl1'"
            proof (cases rule: BO.cases)
              case (BO_BC vl'' vl1'' fs)
                moreover with vl FrVal obtain fs' where "fs = fv # fs'" by (cases fs) auto
                ultimately show ?thesis using FrVal BO_BC vl
                  by (intro that[of "map FrVal fs' @ OVal False # vl1''"]) auto
            qed auto
            from fIDs have f12: "friends12 s = friends12 s1" unfolding friends12_def by auto
            show ?match using φ step rs FrVal proof (cases rule: φE)
              case (Friend uid p uid')
                then have IDs1: "IDsOK s1 [UID1, UID2] [] [] []"
                  using ss1 unfolding eqButUID_def by auto
                let ?s1' = "createFriend s1 UID1 (pass s1 UID1) UID2"
                have s': "s' = createFriend s UID1 p UID2"
                  using Friend step by (auto simp: createFriend_sym)
                have ss': "eqButUID s s'" using rs step Friend
                  by (auto intro: Cact_cFriend_step_eqButUID)
                moreover then have os': "open s'" using os eqButUID_open_eq by auto
                moreover obtain al oul where al: "sstep s1 al = (oul, ?s1')" "al ≠ []"
                                         and tr1: "O (traceOf s1 al) = []"
                                                  "V (traceOf s1 al) = [FrVal True]"
                                         and f12s1': "friends12 ?s1'"
                                         and s1s1': "eqButUID s1 ?s1'"
                  using rs1 IDs1 Friend unfolding f12 by (auto elim: toggle_friends12_True)
                moreover have "friendIDs s' = friendIDs ?s1'"
                  using Friend(6) f12 unfolding s'
                  by (intro eqButUID_createFriend12_friendIDs_eq[OF ss1 rs rs1]) auto
                ultimately have "Δ0 s' vl' ?s1' vl1'"
                  using ss1 BO' aF1 unfolding Δ0_def vl1' Friend(3)
                  by (auto intro: eqButUID_trans eqButUID_sym)
                then show ?match using tr1 vl1' Friend UID1_UID2_UIDs
                  by (intro matchI_ms[OF al]) (auto simp: consumeList_def)
            next
              case (Unfriend uid p uid')
                then have IDs1: "IDsOK s1 [UID1, UID2] [] [] []"
                  using ss1 unfolding eqButUID_def by auto
                let ?s1' = "deleteFriend s1 UID1 (pass s1 UID1) UID2"
                have s': "s' = deleteFriend s UID1 p UID2"
                  using Unfriend step by (auto simp: deleteFriend_sym)
                have ss': "eqButUID s s'" using rs step Unfriend
                  by (auto intro: Dact_dFriend_step_eqButUID)
                moreover then have os': "open s'" using os eqButUID_open_eq by auto
                moreover obtain al oul where al: "sstep s1 al = (oul, ?s1')" "al ≠ []"
                                         and tr1: "O (traceOf s1 al) = []"
                                                  "V (traceOf s1 al) = [FrVal False]"
                                         and f12s1': "¬friends12 ?s1'"
                                         and s1s1': "eqButUID s1 ?s1'"
                  using rs1 IDs1 Unfriend unfolding f12 by (auto elim: toggle_friends12_False)
                moreover have "friendIDs s' = friendIDs ?s1'"
                  using fIDs unfolding s' by (auto simp: d_defs)
                ultimately have "Δ0 s' vl' ?s1' vl1'"
                  using ss1 BO' aF1 unfolding Δ0_def vl1' Unfriend(3)
                  by (auto intro: eqButUID_trans eqButUID_sym)
                then show ?match using tr1 vl1' Unfriend UID1_UID2_UIDs
                  by (intro matchI_ms[OF al]) (auto simp: consumeList_def)
            qed auto
        next
          case (OVal ov)
            with BO vl obtain vl1' where vl1': "vl1 = OVal False # vl1'"
                                      and vl': "vl = OVal False # vl'"
                                      and BC: "BC vl' vl1'"
            proof (cases rule: BO.cases)
              case (BO_BC vl'' vl1'' fs)
                moreover then have "fs = []" using vl unfolding OVal by (cases fs) auto
                ultimately show thesis using vl by (intro that[of vl1'']) auto
            qed auto
            then have "f ?trn = OVal False" using vl by auto
            with φ step rs show ?match proof (cases rule: φE)
              case (CloseF uid p uid')
                let ?s1' = "deleteFriend s1 uid p uid'"
                let ?trn1 = "Trans s1 a outOK ?s1'"
                have s': "s' = deleteFriend s uid p uid'" using CloseF step by auto
                have step1: "step s1 a = (outOK, ?s1')"
                  using CloseF step ss1 fIDs unfolding eqButUID_def by (auto simp: d_defs)
                have s's1': "eqButUID s' ?s1'" using eqButUID_step[OF ss1 step step1 rs rs1] .
                moreover have os': "¬open s'" using CloseF os unfolding open_def by auto
                moreover have fIDs': "friendIDs s' = friendIDs ?s1'"
                  using fIDs unfolding s' by (auto simp: d_defs)
                moreover have f12s1: "friends12 s1 = friends12 ?s1'"
                  using CloseF(2) UID1_UID2_UIDs unfolding friends12_def d_defs by auto
                from BC have "Δ1 s' vl' ?s1' vl1' ∨ Δ2 s' vl' ?s1' vl1'"
                proof (cases rule: BC.cases)
                  case (BC_FrVal fs fs1)
                    then show ?thesis using aF1 os' fIDs' f12s1 s's1' unfolding Δ1_def vl1' by auto
                next
                  case (BC_BO vlr vlr1 fs fs1)
                    then have "Δ2 s' vl' ?s1' vl1'" using s's1' os' aF1 f12s1 fIDs' unfolding vl1'
                      by (intro Δ2_I[of _ _ _ _ _ fs fs1]) auto
                    then show ?thesis ..
                qed
                moreover have "open s1" "¬open ?s1'"
                  using ss1 os s's1' os' by (auto simp: eqButUID_open_eq)
                moreover then have "φ ?trn1" unfolding CloseF by auto
                ultimately show ?match using step1 vl1' CloseF UID1_UID2 UID1_UID2_UIDs
                  by (intro matchI[of s1 a outOK ?s1' vl1 vl1']) (auto simp: consume_def)
            next
              case (CloseA uid p uid' p')
                let ?s1' = "createUser s1 uid p uid' p'"
                let ?trn1 = "Trans s1 a outOK ?s1'"
                have s': "s' = createUser s uid p uid' p'" using CloseA step by auto
                have step1: "step s1 a = (outOK, ?s1')"
                  using CloseA step ss1 unfolding eqButUID_def by (auto simp: c_defs)
                have s's1': "eqButUID s' ?s1'" using eqButUID_step[OF ss1 step step1 rs rs1] .
                moreover have os': "¬open s'" using CloseA os unfolding open_def by auto
                moreover have fIDs': "friendIDs s' = friendIDs ?s1'"
                  using fIDs unfolding s' by (auto simp: c_defs)
                moreover have f12s1: "friends12 s1 = friends12 ?s1'"
                  unfolding friends12_def by (auto simp: c_defs)
                from BC have "Δ1 s' vl' ?s1' vl1' ∨ Δ2 s' vl' ?s1' vl1'"
                proof (cases rule: BC.cases)
                  case (BC_FrVal fs fs1)
                    then show ?thesis using aF1 os' fIDs' f12s1 s's1' unfolding Δ1_def vl1' by auto
                next
                  case (BC_BO vlr vlr1 fs fs1)
                    then have "Δ2 s' vl' ?s1' vl1'" using s's1' os' aF1 f12s1 fIDs' unfolding vl1'
                      by (intro Δ2_I[of _ _ _ _ _ fs fs1]) auto
                    then show ?thesis ..
                qed
                moreover have "open s1" "¬open ?s1'"
                  using ss1 os s's1' os' by (auto simp: eqButUID_open_eq)
                moreover then have "φ ?trn1" unfolding CloseA by auto
                ultimately show ?match using step1 vl1' CloseA UID1_UID2 UID1_UID2_UIDs
                  by (intro matchI[of s1 a outOK ?s1' vl1 vl1']) (auto simp: consume_def)
            qed auto
        qed
        then show "?match ∨ ?ignore" ..
      next
        assume nφ: "¬φ ?trn"
        then have os': "open s = open s'" and f12s': "friends12 s = friends12 s'"
          using step_open_φ[OF step] step_friends12_φ[OF step] by auto
        have vl': "vl' = vl" using nφ c by (auto simp: consume_def)
        show ?thesis proof (cases "a ≠ Cact (cFriend UID1 (pass s UID1) UID2) ∧
                                   a ≠ Cact (cFriend UID2 (pass s UID2) UID1) ∧
                                   a ≠ Dact (dFriend UID1 (pass s UID1) UID2) ∧
                                   a ≠ Dact (dFriend UID2 (pass s UID2) UID1)")
          case True
            obtain ou1 s1' where step1: "step s1 a = (ou1, s1')" by (cases "step s1 a") auto
            let ?trn1 = "Trans s1 a ou1 s1'"
            have fIDs': "friendIDs s' = friendIDs s1'"
              using eqButUID_step_friendIDs_eq[OF ss1 rs rs1 step step1 True fIDs] .
            from True nφ have nφ': "¬φ ?trn1" using eqButUID_step_φ[OF ss1 rs rs1 step step1] by auto
            then have f12s1': "friends12 s1 = friends12 s1'"
              using step_friends12_φ[OF step1] by auto
            have "eqButUID s' s1'" using eqButUID_step[OF ss1 step step1 rs rs1] .
            then have "Δ0 s' vl' s1' vl1" using os fIDs' aF1 BO
              unfolding Δ0_def os' f12s1' vl' by auto
            then have ?match
              using step1 nφ' fIDs eqButUID_step_γ_out[OF ss1 step step1]
              by (intro matchI[of s1 a ou1 s1' vl1 vl1]) (auto simp: consume_def)
            then show "?match ∨ ?ignore" ..
        next
          case False
            with nφ have "ou ≠ outOK" by auto
            then have "s' = s" using step False by auto
            then have ?ignore using Δ0 False UID1_UID2_UIDs unfolding vl' by (intro ignoreI) auto
            then show "?match ∨ ?ignore" ..
        qed
      qed
    qed
    then show ?thesis using BO BO_Nil_Nil by auto
  qed
qed

lemma unwind_cont_Δ1: "unwind_cont Δ1 {Δ1, Δ0}"
proof(rule, simp)
  let ?Δ = "λs vl s1 vl1. Δ1 s vl s1 vl1 ∨ Δ0 s vl s1 vl1"
  fix s s1 :: state and vl vl1 :: "value list"
  assume rsT: "reachNT s" and rs1: "reach s1" and 1: "Δ1 s vl s1 vl1"
  from rsT have rs: "reach s" by (intro reachNT_reach)
  from 1 obtain fs fs1
  where ss1: "eqButUID s s1" and os: "¬open s"
    and aF1: "alternatingFriends vl1 (friends12 s1)"
    and vl: "vl = map FrVal fs" and vl1: "vl1 = map FrVal fs1"
    unfolding Δ1_def by auto
  from os have IDs: "IDsOK s [UID1, UID2] [] [] []" unfolding open_defs by auto
  then have IDs1: "IDsOK s1 [UID1, UID2] [] [] []" using ss1 unfolding eqButUID_def by auto
  show "iaction ?Δ s vl s1 vl1 ∨
        ((vl = [] ⟶ vl1 = []) ∧ reaction ?Δ s vl s1 vl1)" (is "?iact ∨ (_ ∧ ?react)")
  proof cases
    assume fs1: "fs1 = []"
    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"
        with vl c obtain fv fs' where vl': "vl' = map FrVal fs'" and fv: "f ?trn = FrVal fv"
          by (cases fs) (auto simp: consume_def)
        from φ step rs fv have ss': "eqButUID s s'"
          by (elim φE) (auto intro: Cact_cFriend_step_eqButUID Dact_dFriend_step_eqButUID)
        then have "¬open s'" using os by (auto simp: eqButUID_open_eq)
        moreover have "eqButUID s' s1" using ss1 ss' by (auto intro: eqButUID_sym eqButUID_trans)
        ultimately have "Δ1 s' vl' s1 vl1" using aF1 unfolding Δ1_def vl' vl1 by auto
        moreover have "¬γ ?trn" using φ step rs fv UID1_UID2_UIDs by (elim φE) auto
        ultimately have ?ignore by (intro ignoreI) auto
        then show "?match ∨ ?ignore" ..
      next
        assume nφ: "¬φ ?trn"
        then have os': "open s = open s'" and f12s': "friends12 s = friends12 s'"
          using step_open_φ[OF step] step_friends12_φ[OF step] by auto
        have vl': "vl' = vl" using nφ c by (auto simp: consume_def)
        show ?thesis proof (cases "a ≠ Cact (cFriend UID1 (pass s UID1) UID2) ∧
                                   a ≠ Cact (cFriend UID2 (pass s UID2) UID1) ∧
                                   a ≠ Dact (dFriend UID1 (pass s UID1) UID2) ∧
                                   a ≠ Dact (dFriend UID2 (pass s UID2) UID1)")
          case True
            obtain ou1 s1' where step1: "step s1 a = (ou1, s1')" by (cases "step s1 a") auto
            let ?trn1 = "Trans s1 a ou1 s1'"
            from True nφ have nφ': "¬φ ?trn1" using eqButUID_step_φ[OF ss1 rs rs1 step step1] by auto
            then have f12s1': "friends12 s1 = friends12 s1'"
              using step_friends12_φ[OF step1] by auto
            have "eqButUID s' s1'" using eqButUID_step[OF ss1 step step1 rs rs1] .
            then have "Δ1 s' vl' s1' vl1" using os aF1 vl vl1
              unfolding Δ1_def os' vl' f12s1' by auto
            then have ?match
              using step1 nφ' os eqButUID_step_γ_out[OF ss1 step step1]
              by (intro matchI[of s1 a ou1 s1' vl1 vl1]) (auto simp: consume_def)
            then show "?match ∨ ?ignore" ..
        next
          case False
            with nφ have "ou ≠ outOK" by auto
            then have "s' = s" using step False by auto
            then have ?ignore using 1 False UID1_UID2_UIDs unfolding vl' by (intro ignoreI) auto
            then show "?match ∨ ?ignore" ..
        qed
      qed
    qed
    then show ?thesis using fs1 unfolding vl1 by auto
  next
    assume "fs1 ≠ []"
    then obtain fs1' where fs1: "fs1 = (¬friends12 s1) # fs1'"
                       and aF1': "alternatingFriends (map FrVal fs1') (¬friends12 s1)"
      using aF1 unfolding vl1 by (cases fs1) auto
    obtain al oul s1' where "sstep s1 al = (oul, s1')" "al ≠ []" "eqButUID s1 s1'"
                            "friends12 s1' = (¬friends12 s1)"
                            "O (traceOf s1 al) = []" "V (traceOf s1 al) = [FrVal (¬friends12 s1)]"
      using rs1 IDs1
      by (cases "friends12 s1") (auto intro: toggle_friends12_True toggle_friends12_False)
    moreover then have "Δ1 s vl s1' (map FrVal fs1')"
      using os aF1' vl ss1 unfolding Δ1_def by (auto intro: eqButUID_sym eqButUID_trans)
    ultimately have ?iact using vl1 unfolding fs1
      by (intro iactionI_ms[of s1 al oul s1'])
         (auto simp: consumeList_def O_Nil_never list_ex_iff_length_V)
    then show ?thesis ..
  qed
qed

lemma unwind_cont_Δ2: "unwind_cont Δ2 {Δ2,Δ0}"
proof(rule, simp)
  let ?Δ = "λs vl s1 vl1. Δ2 s vl s1 vl1 ∨ Δ0 s vl s1 vl1"
  fix s s1 :: state and vl vl1 :: "value list"
  assume rsT: "reachNT s" and rs1: "reach s1" and 2: "Δ2 s vl s1 vl1"
  from rsT have rs: "reach s" by (intro reachNT_reach)
  obtain fs fs1 vlr vlr1
  where ss1: "eqButUID s s1" and os: "¬open s" and BO: "BO vlr vlr1"
    and aF1: "alternatingFriends vl1 (friends12 s1)"
    and vl:  "vl =  map FrVal fs  @ OVal True # vlr"
    and vl1: "vl1 = map FrVal fs1 @ OVal True # vlr1"
    and fs_fs1: "fs = [] ⟷ fs1 = []"
    and last_fs: "fs ≠ [] ⟶ last fs = last fs1"
    and fs_fIDs: "fs = [] ⟶ friendIDs s = friendIDs s1"
    using 2 unfolding Δ2_def by auto
  from os have IDs: "IDsOK s [UID1, UID2] [] [] []" unfolding open_defs by auto
  then have IDs1: "IDsOK s1 [UID1, UID2] [] [] []" using ss1 unfolding eqButUID_def by auto
  show "iaction ?Δ s vl s1 vl1 ∨
        ((vl = [] ⟶ vl1 = []) ∧ reaction ?Δ s vl s1 vl1)" (is "?iact ∨ (_ ∧ ?react)")
  proof cases
    assume "length fs1 > 1"
    then obtain fs1'
    where fs1: "fs1 = (¬friends12 s1) # fs1'" and fs1': "fs1' ≠ []"
      and last_fs': "last fs1 = last fs1'"
      and aF1': "alternatingFriends (map FrVal fs1' @ OVal True # vlr1) (¬friends12 s1)"
      using vl1 aF1 by (cases fs1) auto
    obtain al oul s1' where "sstep s1 al = (oul, s1')" "al ≠ []" "eqButUID s1 s1'"
                            "friends12 s1' = (¬friends12 s1)"
                            "O (traceOf s1 al) = []" "V (traceOf s1 al) = [FrVal (¬friends12 s1)]"
      using rs1 IDs1
      by (cases "friends12 s1") (auto intro: toggle_friends12_True toggle_friends12_False)
    moreover then have "Δ2 s vl s1' (map FrVal fs1' @ OVal True # vlr1)"
      using os aF1' vl ss1 fs1' last_fs' fs_fs1 last_fs BO unfolding fs1
      by (intro Δ2_I[of _ _ vlr vlr1 _ fs fs1'])
         (auto intro: eqButUID_sym eqButUID_trans)
    ultimately have ?iact using vl1 unfolding fs1
      by (intro iactionI_ms[of s1 al oul s1'])
         (auto simp: consumeList_def O_Nil_never list_ex_iff_length_V)
    then show ?thesis ..
  next
    assume len1_leq_1: "¬ length fs1 > 1"
    have ?react proof
      fix a :: act and ou :: out and s' :: state and vl'
      let ?trn = "Trans s a ou s'"  let ?trn1 = "Trans s1 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"
        show ?thesis proof cases
          assume "length fs > 1"
          then obtain fv fs'
          where fs1: "fs = fv # fs'" and fs1': "fs' ≠ []"
            and last_fs': "last fs = last fs'"
            using vl by (cases fs) auto
          with φ c have fv: "f ?trn = FrVal fv" and vl': "vl' = map FrVal fs' @ OVal True # vlr"
            unfolding vl consume_def by auto
          from φ step rs fv have ss': "eqButUID s s'"
            by (elim φE) (auto intro: Cact_cFriend_step_eqButUID Dact_dFriend_step_eqButUID)
          then have "¬open s'" using os by (auto simp: eqButUID_open_eq)
          moreover have "eqButUID s' s1" using ss1 ss' by (auto intro: eqButUID_sym eqButUID_trans)
          ultimately have "Δ2 s' vl' s1 vl1"
            using aF1 vl' fs1' fs_fs1 last_fs BO unfolding fs1 vl1
            by (intro Δ2_I[of _ _ vlr vlr1 _ fs' fs1])
               (auto intro: eqButUID_sym eqButUID_trans)
          moreover have "¬γ ?trn" using φ step rs fv UID1_UID2_UIDs by (elim φE) auto
          ultimately have ?ignore by (intro ignoreI) auto
          then show "?match ∨ ?ignore" ..
        next
          assume len_leq_1: "¬ length fs > 1"
          show ?thesis proof cases
            assume fs: "fs = []"
            then have fs1: "fs1 = []" and fIDs: "friendIDs s = friendIDs s1"
              using fs_fs1 fs_fIDs by auto
            from fs φ c have ov: "f ?trn = OVal True" and vl': "vl' = vlr"
              unfolding vl consume_def by auto
            with φ step rs have ?match proof (cases rule: φE)
              case (OpenF uid p uid')
                let ?s1' = "createFriend s1 uid p uid'"
                let ?trn1 = "Trans s1 a outOK ?s1'"
                have s': "s' = createFriend s uid p uid'" using OpenF step by auto
                have "eqButUIDf (pendingFReqs s) (pendingFReqs s1)"
                  using ss1 unfolding eqButUID_def by auto
                then have "uid' ∈∈ pendingFReqs s uid ⟷ uid' ∈∈ pendingFReqs s1 uid"
                  using OpenF by (intro eqButUIDf_not_UID') auto
                then have step1: "step s1 a = (outOK, ?s1')"
                  using OpenF step ss1 fIDs unfolding eqButUID_def by (auto simp: c_defs)
                have s's1': "eqButUID s' ?s1'" using eqButUID_step[OF ss1 step step1 rs rs1] .
                moreover have os': "open s'" using OpenF unfolding open_def by auto
                moreover have fIDs': "friendIDs s' = friendIDs ?s1'"
                  using fIDs unfolding s' by (auto simp: c_defs)
                moreover have f12s1: "friends12 s1 = friends12 ?s1'"
                  using OpenF(2) UID1_UID2_UIDs unfolding friends12_def c_defs by auto
                ultimately have "Δ0 s' vl' ?s1' vlr1"
                  using BO aF1 unfolding Δ0_def vl' vl1 fs1 by auto
                moreover have "¬open s1" "open ?s1'"
                  using ss1 os s's1' os' by (auto simp: eqButUID_open_eq)
                moreover then have "φ ?trn1" unfolding OpenF by auto
                ultimately show ?match using step1 vl1 fs1 OpenF UID1_UID2 UID1_UID2_UIDs
                  by (intro matchI[of s1 a outOK ?s1' vl1 vlr1]) (auto simp: consume_def)
            qed auto
            then show ?thesis ..
          next
            assume "fs ≠ []"
            then obtain fv where fs: "fs = [fv]" using len_leq_1 by (cases fs) auto
            then have fs1: "fs1 = [fv]" using len1_leq_1 fs_fs1 last_fs by (cases fs1) auto
            with aF1 have f12s1: "friends12 s1 = (¬fv)" unfolding vl1 by auto
            have fv: "f ?trn = FrVal fv" and vl': "vl' = OVal True # vlr"
              using c φ unfolding vl fs by (auto simp: consume_def)
            with φ step rs have ?match proof (cases rule: φE)
              case (Friend uid p uid')
                then have IDs1: "IDsOK s1 [UID1, UID2] [] [] []"
                  using ss1 unfolding eqButUID_def by auto
                have fv: "fv = True" using fv Friend by auto
                let ?s1' = "createFriend s1 UID1 (pass s1 UID1) UID2"
                have s': "s' = createFriend s UID1 p UID2"
                  using Friend step by (auto simp: createFriend_sym)
                have ss': "eqButUID s s'" using rs step Friend
                  by (auto intro: Cact_cFriend_step_eqButUID)
                moreover then have os': "¬open s'" using os eqButUID_open_eq by auto
                moreover obtain al oul where al: "sstep s1 al = (oul, ?s1')" "al ≠ []"
                                         and tr1: "O (traceOf s1 al) = []"
                                                  "V (traceOf s1 al) = [FrVal True]"
                                         and f12s1': "friends12 ?s1'"
                                         and s1s1': "eqButUID s1 ?s1'"
                  using rs1 IDs1 Friend f12s1 unfolding fv by (auto elim: toggle_friends12_True)
                moreover have "friendIDs s' = friendIDs ?s1'"
                  using Friend(6) f12s1 unfolding s' fv
                  by (intro eqButUID_createFriend12_friendIDs_eq[OF ss1 rs rs1]) auto
                ultimately have "Δ2 s' vl' ?s1' (OVal True # vlr1)"
                  using BO ss1 aF1 unfolding vl' vl1 fs1 f12s1 fv
                  by (intro Δ2_I[of _ _ _ _ _ "[]" "[]"])
                     (auto intro: eqButUID_trans eqButUID_sym)
                then show ?match using tr1 vl1 Friend UID1_UID2_UIDs unfolding fs1 fv
                  by (intro matchI_ms[OF al]) (auto simp: consumeList_def)
            next
              case (Unfriend uid p uid')
                then have IDs1: "IDsOK s1 [UID1, UID2] [] [] []"
                  using ss1 unfolding eqButUID_def by auto
                have fv: "fv = False" using fv Unfriend by auto
                let ?s1' = "deleteFriend s1 UID1 (pass s1 UID1) UID2"
                have s': "s' = deleteFriend s UID1 p UID2"
                  using Unfriend step by (auto simp: deleteFriend_sym)
                have ss': "eqButUID s s'" using rs step Unfriend
                  by (auto intro: Dact_dFriend_step_eqButUID)
                moreover then have os': "¬open s'" using os eqButUID_open_eq by auto
                moreover obtain al oul where al: "sstep s1 al = (oul, ?s1')" "al ≠ []"
                                         and tr1: "O (traceOf s1 al) = []"
                                                  "V (traceOf s1 al) = [FrVal False]"
                                         and f12s1': "¬friends12 ?s1'"
                                         and s1s1': "eqButUID s1 ?s1'"
                  using rs1 IDs1 Unfriend f12s1 unfolding fv by (auto elim: toggle_friends12_False)
                moreover have "friendIDs s' = friendIDs ?s1'"
                  using Unfriend(6) f12s1 unfolding s' fv
                  by (intro eqButUID_deleteFriend12_friendIDs_eq[OF ss1 rs rs1])
                ultimately have "Δ2 s' vl' ?s1' (OVal True # vlr1)"
                  using BO ss1 aF1 unfolding vl' vl1 fs1 f12s1 fv
                  by (intro Δ2_I[of _ _ _ _ _ "[]" "[]"])
                     (auto intro: eqButUID_trans eqButUID_sym)
                then show ?match using tr1 vl1 Unfriend UID1_UID2_UIDs unfolding fs1 fv
                  by (intro matchI_ms[OF al]) (auto simp: consumeList_def)
            qed auto
            then show ?thesis ..
          qed
        qed
      next
        assume nφ: "¬φ ?trn"
        then have os': "open s = open s'" and f12s': "friends12 s = friends12 s'"
          using step_open_φ[OF step] step_friends12_φ[OF step] by auto
        have vl': "vl' = vl" using nφ c by (auto simp: consume_def)
        show ?thesis proof (cases "a ≠ Cact (cFriend UID1 (pass s UID1) UID2) ∧
                                   a ≠ Cact (cFriend UID2 (pass s UID2) UID1) ∧
                                   a ≠ Dact (dFriend UID1 (pass s UID1) UID2) ∧
                                   a ≠ Dact (dFriend UID2 (pass s UID2) UID1)")
          case True
            obtain ou1 s1' where step1: "step s1 a = (ou1, s1')" by (cases "step s1 a") auto
            let ?trn1 = "Trans s1 a ou1 s1'"
            from True nφ have nφ': "¬φ ?trn1" using eqButUID_step_φ[OF ss1 rs rs1 step step1] by auto
            then have f12s1': "friends12 s1 = friends12 s1'"
              using step_friends12_φ[OF step1] by auto
            have "eqButUID s' s1'" using eqButUID_step[OF ss1 step step1 rs rs1] .
            moreover have "friendIDs s = friendIDs s1 ⟶ friendIDs s' = friendIDs s1'"
              using eqButUID_step_friendIDs_eq[OF ss1 rs rs1 step step1 True] ..
            ultimately have "Δ2 s' vl' s1' vl1"
              using os' os aF1 BO fs_fs1 last_fs fs_fIDs unfolding f12s1' vl' vl vl1
              by (intro Δ2_I) auto
            then have ?match
              using step1 nφ' os eqButUID_step_γ_out[OF ss1 step step1]
              by (intro matchI[of s1 a ou1 s1' vl1 vl1]) (auto simp: consume_def)
            then show "?match ∨ ?ignore" ..
        next
          case False
            with nφ have "ou ≠ outOK" by auto
            then have "s' = s" using step False by auto
            then have ?ignore using 2 False UID1_UID2_UIDs unfolding vl' by (intro ignoreI) auto
            then show "?match ∨ ?ignore" ..
        qed
      qed
    qed
    then show ?thesis unfolding vl by auto
  qed
qed


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


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