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
unbundle no relcomp_syntax
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›
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
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